theory s1
imports Main
begin

section "Q1: \<lambda>-Calculus"

(* TODO: provide your answers here or in an separate PDF file *)


text \<open> Q1 (a) \<close>

term "(x y)(\<lambda>x.(\<lambda>y.(\<lambda>z.(z(x y)))))"
term "x y (\<lambda>x.(\<lambda>y.(\<lambda>z.(z(x y)))))" (* application binds to the left *)
term "x y (\<lambda>x.\<lambda>y.\<lambda>z. z(x y))" (* abstraction binds to the right *)
term "x y (\<lambda>x y z. z(x y))"  (* list variables for \<lambda> *)


text \<open> Q1 (b) \<close>

(* term given in the question *)
(*term "x (\<lambda>x y. x (y z) (x y)) (\<lambda>y. y z)"*)

(* with parentheses restored *)
(*term "(x (\<lambda>x. (\<lambda>y. ((x (y z)) (x y))))) (\<lambda>y. (y z))"*)


text \<open> Q1 (c) \<close>

text \<open>

(\<lambda>f.\<lambda>x.f(f(fx)))(\<lambda>g.\<lambda>y.g(gy))
-----------------------------
\<mapsto> \<lambda>x.(\<lambda>g.\<lambda>y.g(gy))((\<lambda>g.\<lambda>y.g(gy))((\<lambda>g.\<lambda>y.g(gy))x))
                                  --------------
\<mapsto> \<lambda>x.(\<lambda>g.\<lambda>y.g(gy))((\<lambda>g.\<lambda>y.g(gy))(\<lambda>y.x(xy)))
                             alpha (not necessary)
\<mapsto> \<lambda>x.(\<lambda>g.\<lambda>y.g(gy))((\<lambda>g.\<lambda>z.g(gz))(\<lambda>y.x(xy)))
                    -----------------------
\<mapsto> \<lambda>x.(\<lambda>g.\<lambda>y.g(gy))(\<lambda>z.(\<lambda>y.x(xy))((\<lambda>y.x(xy))z))
                                  -----------
\<mapsto> \<lambda>x.(\<lambda>g.\<lambda>y.g(gy))(\<lambda>z.(\<lambda>y.x(xy))(x(xz)))
                       -----------------
\<mapsto> \<lambda>x.(\<lambda>g.\<lambda>y.g(gy))(\<lambda>z.x(x(x(xz))))
      -----------------------------
\<mapsto> \<lambda>x.(\<lambda>y.(\<lambda>z.x(x(x(xz))))((\<lambda>z.x(x(x(xz))))y))
                           -----------------
\<mapsto> \<lambda>x.(\<lambda>y.(\<lambda>z.x(x(x(xz))))(x(x(x(xy)))))
          ----------------------------- 
\<mapsto> \<lambda>x.(\<lambda>y.x(x(x(x(x(x(x(xy))))))))
\<close>

text \<open> Q1 (d) \<close>

text \<open>
exp = \<lambda>m n. n m

For the justification, show that
exp (\<lambda>f.\<lambda>x.f^n x) (\<lambda>f.\<lambda>x.f^m x)
beta-reduces to \<lambda>f.\<lambda>x.f^(m^n) x
using the previous question and reasonable omissions.

Here, f^n x abbreviates f(f(...(f x))) (n-fold application of f to n).

(\<lambda>f.\<lambda>x.f^n x) (\<lambda>f.\<lambda>x.f^m x)
\<mapsto> \<lambda>y.(\<lambda>f.\<lambda>x.f^m x)^n y (beta+alpha)
\<equiv> \<lambda>y.(\<lambda>f.\<lambda>x.f^m x)((\<lambda>f.\<lambda>x.f^m x)...((\<lambda>f.\<lambda>x.f^m x)((\<lambda>f.\<lambda>x.f^m x) y))) (n-times repeat)
\<mapsto> \<lambda>y.(\<lambda>f.\<lambda>x.f^m x)((\<lambda>f.\<lambda>x.f^m x)...(\<lambda>x.(\<lambda>x. y^m x)^m x)) (beta, n-1)
\<equiv> \<lambda>y.(\<lambda>f.\<lambda>x.f^m x)((\<lambda>f.\<lambda>x.f^m x)...(\<lambda>x.(\<lambda>x. y^m x)...((\<lambda>x. y^m x)((\<lambda>x. y^m x) x))))) (n-1, m)
\<mapsto> \<lambda>y.(\<lambda>f.\<lambda>x.f^m x)((\<lambda>f.\<lambda>x.f^m x)...(\<lambda>x.(\<lambda>x. y^m x)...((\<lambda>x. y^m x)(y^m x))))) (beta, n-1, m-1)
\<mapsto> \<lambda>y.(\<lambda>f.\<lambda>x.f^m x)((\<lambda>f.\<lambda>x.f^m x)...(\<lambda>x.(\<lambda>x. y^m x)...(y^m (y^m x)))))) (beta, n-1, m-2)
\<equiv> \<lambda>y.(\<lambda>f.\<lambda>x.f^m x)((\<lambda>f.\<lambda>x.f^m x)...(\<lambda>x.(\<lambda>x. y^m x)...(y^(m+m) x)))) (n-1, m-2)
\<mapsto> \<lambda>y.(\<lambda>f.\<lambda>x.f^m x)((\<lambda>f.\<lambda>x.f^m x)...(\<lambda>x.y^(m^2) x)) (beta*,n-2)
\<mapsto> \<lambda>y.(\<lambda>f.\<lambda>x.f^m x)(\<lambda>x.y^(m^(n-1)) x) (beta*)
\<mapsto> \<lambda>y.(\<lambda>x.(\<lambda>x.y^(m^(n-1)) x)^m x) (beta)
\<mapsto> \<lambda>y.(\<lambda>x.y^(m^n) x) (beta*)

\<close>


section "Q2: Types"

(* TODO: provide your answers here or in an separate PDF file *)


text \<open> Q2 (a) \<close>

context
notes [[show_types]]
begin
term "\<lambda> a b. a (c b) b"
end

text \<open>

\lambda a b. a (c b) b has type ('a => 'b => 'c) => 'b => 'c

in the context that gives c: 'b => 'a
\<close>

text \<open> Type derivation:

Let \<Gamma> \<equiv> [a::'a => 'b => 'c, b::'b, c::'b => 'a]
and \<Gamma>' \<equiv> [a::'a => 'b => 'c, c::'b => 'a].


                           ------------ Var    ----------- Var
                           \<Gamma> \<turnstile> c::'b=>'a       \<Gamma> \<turnstile> b :: 'b
 ----------------- Var    --------------------------------- App
 \<Gamma> \<turnstile> a::'a=>'b=>'c              \<Gamma> \<turnstile> cb::'a
 -------------------------------------------- App              ---------- Var
            \<Gamma> \<turnstile> a(cb)::'b=>'c                                  \<Gamma> \<turnstile> b::'b
           -------------------------------------------------------------- App
                    \<Gamma> \<turnstile> a(cb)b::'c
               ------------------------ Abs
                \<Gamma>' \<turnstile> \<lambda>b.a(cb)b::'b=>'c
       --------------------------------------------- Abs
       c::'b=>'a \<turnstile> \<lambda>ab.a(cb)b::('a=>'b=>'c)=>'b=>'c

\<close>

text \<open> Q2 (b) \<close>

context
notes [[show_types]]
begin
term "\<lambda> x y z. z y (x y)"
end

typ "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'c"


text \<open> 2 (c) \<close>

text \<open>Argue that, if the term is typable, the type should be derived by
applying the typing rules given in the lecture. However, there is no
rule that can be applied to xx because x cannot have the type of the function
and the argument at the same type in the Application rule.\<close>

text \<open> 2 (d) \<close>

text \<open>
(\<lambda>xy.y)(\<lambda>z.zz)
\<mapsto> \<lambda>y.y :: 'a => 'a
\<close>


text \<open> 2 (e) \<close>

text \<open>The term is not typable, which follows from Q2(c).
The subject reduction says that the type of a term does not change after
applying beta-reductions. The situation here is that a term that is not
typable may become typable after some beta-reduction, indicating that 
the typable property is preserved only in the direction of the reduction but
not backwards.\<close>

text \<open> Question 3 \<close>

lemma prop_a: "A \<longrightarrow> \<not>\<not>A"
  apply (rule impI)
  apply (rule notI)
  apply (erule notE)
  apply assumption
  done

lemma prop_b: "\<not>\<not>\<not> A \<longrightarrow> \<not>A"
  apply (rule impI)
  apply (rule notI)
  apply (erule notE)
  apply (rule notI)
  apply (erule notE)
  apply assumption
  done

lemma prop_c: "\<not>\<not> A \<longrightarrow> A"
  apply (rule impI)
  apply (case_tac A)
  apply assumption
  apply (erule notE)
  apply assumption
  done
(*
lemma prop_d: "(\<not>A \<longrightarrow> False) \<longrightarrow> A"
  apply (rule impI)
  apply (case_tac A)
   apply assumption
  apply (drule mp)
   apply assumption
  apply (erule notE)
  apply (erule FalseE)
  done
*)
lemma prop_d:  "\<not>(A \<and> B) \<longrightarrow> \<not> A \<or> \<not> B"
  apply (rule impI)
  apply (case_tac A)
  apply (rule disjI2)
  apply (rule notI)
   apply (erule notE)
   apply (rule conjI)
   apply assumption+
  apply (rule disjI1)
  apply assumption
  done

lemma prop_e:  "(A \<longrightarrow> B) \<longrightarrow> (\<not> A \<or> B)"
  apply (rule impI)
  apply (case_tac A)
   apply (drule mp)
    apply assumption
   apply (rule disjI2)
   apply assumption
  apply (rule disjI1)
  apply assumption
  done
 
lemma prop_f:  "\<not>A\<and>\<not>B \<longleftrightarrow> \<not>(A\<or>B)"
  apply (rule iffI)
   apply (rule notI)
   apply (erule disjE)
    apply (erule conjE)
    apply (erule notE)
    apply assumption
    apply (erule conjE)
  apply (erule_tac P=B in notE)
   apply assumption
  apply (rule conjI)
   apply (rule notI)
   apply (erule notE)
   apply (rule disjI1)
   apply assumption
   apply (rule notI)
   apply (erule notE)
   apply (rule disjI2)
   apply assumption
  done

lemma prop_g: "(A \<longrightarrow> B) \<longrightarrow> (((B \<longrightarrow> C) \<longrightarrow> A) \<longrightarrow> B)"
  apply (rule impI)
  apply (rule impI)
  apply (case_tac B)
  apply assumption
   apply (erule impE)
   apply (erule impE)
  apply (rule impI)
  apply (erule notE)
    apply assumption+
  done


text \<open> Question 4 \<close>


lemma hol_a: "(\<exists>x. P x \<longrightarrow> Q) \<longrightarrow> (\<forall>x. P x) \<longrightarrow> Q"
  apply (rule impI)
  apply (rule impI)
  apply (erule exE)
  apply (erule mp)
  apply (erule_tac x=x in allE)
  apply assumption
  done

lemma hol_b: "((\<exists>x. P x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P x \<longrightarrow> Q)"
  apply (rule iffI)
  apply (rule allI)
  apply (rule impI)
  apply (erule mp)
  apply (rule_tac x=x in exI)
  apply assumption
  apply (rule impI)
  apply (erule exE)
  apply (drule_tac x=x in spec)
  apply (erule mp)
  apply assumption
  done

lemma hol_c: "(\<forall>x. P x) \<longleftrightarrow> \<not> (\<exists>x. \<not> P x)"
  apply (rule iffI)
  apply (rule notI)
  apply (erule exE)
   apply (drule_tac x=x in spec)
   apply (erule notE)
  apply assumption
  apply (rule allI)
  apply (rule classical)
  apply (erule notE)
  apply (rule_tac x=x in exI)
  apply assumption
  done

lemma hol_d: "(\<forall>x. P x \<and> Q x) \<longrightarrow> (\<forall>x. P x) \<and> (\<forall>x. Q x)"
  apply (rule impI)
   apply (rule conjI)
  apply (rule allI)
  apply (drule_tac x=x in spec)
    apply (erule conjE)
  apply assumption
  apply (rule allI)
  apply (drule_tac x=x in spec)
    apply (erule conjE)
   apply assumption
  done

lemma hol_e: "(\<exists>x. P x \<or> Q x) \<longrightarrow> (\<exists>x. P x) \<or> (\<exists>x. Q x)"
  apply (rule impI)
  apply (erule exE)
   apply (erule disjE)
    apply (rule disjI1)
  apply (rule_tac x=x in exI)
    apply assumption
    apply (rule disjI2)
  apply (rule_tac x=x in exI)
   apply assumption
  done

lemma hol_f:
  "(\<forall>x y. A y \<or> B x) \<longrightarrow> (\<forall>x. B x) \<or> (\<forall>y. A y)" 
  apply (rule impI)
   apply (case_tac "(\<forall>x. A x)") 
    apply (rule disjI2)
    apply assumption
   apply (rule disjI1)
   apply (rule allI)
  apply (rule ccontr)
  apply (drule_tac x=x in spec)
   apply (erule notE)
  apply (rule allI)
   apply (drule_tac x=xa in spec)
  apply (erule disjE)
    apply assumption
   apply (erule notE)
   apply assumption
  done
  
end