header {*

  Hand-in on 10 June at noon. Please rename the file 
  and send your solution to me as

        Hw13_\<guillemotleft>your name\<guillemotright>

  The purpose of this homework is to prove the
  type-preservation property for beta-reduction.

*}

theory Hw13
  imports Nominal
begin

text {* Lambda-terms and substitution *}

atom_decl name

nominal_datatype lam =
  Var "name"
| App "lam" "lam" 
| Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._")

consts 
  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]" [100,100,100] 100)

nominal_primrec
  "(Var x)[y::=s] = (if x=y then s else (Var x))"
  "(App t\<^isub>1 t\<^isub>2)[y::=s] = App (t\<^isub>1[y::=s]) (t\<^isub>2[y::=s])"
  "x\<sharp>(y,s) \<Longrightarrow> (Lam [x].t)[y::=s] = Lam [x].(t[y::=s])"
apply(finite_guess)+
apply(rule TrueI)+
apply(simp add: abs_fresh)
apply(fresh_guess)+
done

lemma  subst_eqvt[eqvt]:
  fixes pi::"name prm"
  shows "pi\<bullet>(t1[x::=t2]) = (pi\<bullet>t1)[(pi\<bullet>x)::=(pi\<bullet>t2)]"
by (nominal_induct t1 avoiding: x t2 rule: lam.strong_induct)
   (auto simp add: perm_bij fresh_atm fresh_bij)

text {* 

  Task 1 (easy)

  Later on we need the following fact about how freshness behaves 
  in substitutions. Prove this lemma by structural induction on t 
  where you have to avoid z, y and s. To set up the induction
  you have to use nominal_induct and the rule lam.induct.

*}

lemma fresh_fact:
  fixes z::"name"
  shows "\<lbrakk>z\<sharp>s; (z=y \<or> z\<sharp>t)\<rbrakk> \<Longrightarrow> z\<sharp>t[y::=s]"
by (nominal_induct t avoiding: z y s rule: lam.strong_induct)
   (auto simp add: abs_fresh fresh_prod fresh_atm)


text {* Types *}

nominal_datatype ty =
    TVar "string"
  | TArr "ty" "ty" ("_ \<rightarrow> _")

lemma ty_fresh:
  fixes x::"name"
  and   T::"ty"
  shows "x\<sharp>T"
by (induct T rule: ty.induct)
   (auto simp add: fresh_string)

text {* Sublists and context difference *}

abbreviation
  "sub_list" :: "(name\<times>ty) list\<Rightarrow>(name\<times>ty) list\<Rightarrow>bool" ("_ \<subseteq> _") 
where
  "\<Gamma>\<^isub>1 \<subseteq> \<Gamma>\<^isub>2 \<equiv> \<forall>x T. (x,T) \<in> set \<Gamma>\<^isub>1 \<longrightarrow> (x,T) \<in> set \<Gamma>\<^isub>2"

abbreviation
  "diff_list" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" ("_ - _") 
where
   "xs - ys \<equiv> [x \<leftarrow> xs. x\<notin>set ys]"

lemma diff_cons[simp]:
  assumes a: "x\<notin>set ys"
  shows "(x#xs)-ys = x#(xs-ys)"
using a by auto

text {*

  Task 2 (easy)

  We also need the fact how freshness behaves when we
  remove some members of a list. Prove the following 
  lemma by induction on \<Gamma>. The lemmas

      thm fresh_list_nil fresh_list_cons

  might be helpful.

*}

lemma fresh_diff:
  fixes x::"name"
  and \<Gamma> \<Delta>::"(name\<times>ty) list"
  assumes a: "x\<sharp>\<Gamma>"
  shows "x\<sharp>(\<Gamma>-\<Delta>)"
using a
by (induct \<Gamma>) (auto simp add: fresh_list_cons)

text {* Validity of typing contexts *}

inductive
  valid :: "(name\<times>ty) list \<Rightarrow> bool"
where
    v1[intro]: "valid []"
  | v2[intro]: "\<lbrakk>valid \<Gamma>; x\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((x,T)#\<Gamma>)"

equivariance valid

lemma valid_elim:
  assumes a: "valid ((x,T)#\<Gamma>)"
  shows "x\<sharp>\<Gamma> \<and> valid \<Gamma>"
using a by (cases) (auto)

lemma valid_diff:
  assumes a: "valid \<Gamma>"
  shows "valid (\<Gamma>-\<Delta>)"
using a
by (induct) (auto simp add: fresh_diff)

lemma fresh_set: 
  shows "y\<sharp>xs = (\<forall>x\<in>set xs. y\<sharp>x)"
by (induct xs) (simp_all add: fresh_list_nil fresh_list_cons)

lemma context_unique:
  assumes a1: "valid \<Gamma>"
  and     a2: "(x,T) \<in> set \<Gamma>"
  and     a3: "(x,U) \<in> set \<Gamma>"
  shows "T = U" 
using a1 a2 a3
by (induct) (auto simp add: fresh_set fresh_prod fresh_atm)

text {* The typing relation *}

inductive
  typing :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ : _") 
where
  t1[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
| t2[intro]: "\<lbrakk>\<Gamma> \<turnstile> t\<^isub>1 : T\<^isub>1\<rightarrow>T\<^isub>2; \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t\<^isub>1 t\<^isub>2 : T\<^isub>2"
| t3[intro]: "\<lbrakk>x\<sharp>\<Gamma>; (x,T\<^isub>1)#\<Gamma> \<turnstile> t : T\<^isub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : T\<^isub>1\<rightarrow>T\<^isub>2"

equivariance typing
nominal_inductive typing
  by (simp_all add: abs_fresh ty_fresh)

lemma typing_implies_valid:
  assumes a: "\<Gamma> \<turnstile> t : T"
  shows "valid \<Gamma>"
using a
by (induct) (auto dest: valid_elim)

text {* 

  Task 3 (hard)

  Prove the weakening property for the typing relation.
  You have to use typing.induct and avoid \<Gamma>2.

*}


lemma weakening: 
  fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list"
  assumes a: "\<Gamma>1 \<turnstile> t : T" 
  and     b: "valid \<Gamma>2" 
  and     c: "\<Gamma>1 \<subseteq> \<Gamma>2"
  shows "\<Gamma>2 \<turnstile> t : T"
using a b c
by (nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct)
   (auto | atomize)+

text {*

  Task 4 (very hard)

  In order to prove the type-preservation property, we need to prove a
  type-substitution property. Prove it by induction on \<Gamma> \<turnstile> e : T and avoid e'
  and x. In the variable case you need, amongst other lemmas, the context_unique
  lemma. The lambda-case needs, amongst others, the weakening lemma.

*}

lemma type_substitution: 
  fixes \<Gamma>::"(name\<times>ty) list"
  assumes a: "\<Gamma> \<turnstile> e : T" 
  and     b: "(x,T')\<in>set \<Gamma>"
  and     c: "\<Gamma> - [(x,T')] \<turnstile> e': T'" 
  shows "\<Gamma> - [(x,T')] \<turnstile> e[x::=e'] : T"
  using a b c
proof (nominal_induct \<Gamma> e T avoiding: e' x rule: typing.strong_induct)
  case (t1 \<Gamma> y T e' x)
  have a1: "valid \<Gamma>" by fact
  have a2: "(y,T) \<in> set \<Gamma>" by fact
  have a3: "(x,T') \<in> set \<Gamma>" by fact
  have a4: "\<Gamma> - [(x,T')] \<turnstile> e' : T'" by fact
  { assume eq: "x=y"
    from a1 a2 a3 have "T=T'" using eq by (simp add: context_unique)
    with a4 have "\<Gamma> - [(x,T')] \<turnstile> Var y[x::=e'] : T" using eq by simp
  }
  moreover
  { assume ineq: "x\<noteq>y"
    from a1 have "valid (\<Gamma> - [(x,T')])" by (simp only: valid_diff)
    moreover 
    from a3 have "(y,T) \<in> set (\<Gamma> - [(x,T')])" using ineq by simp
    ultimately
    have "\<Gamma> - [(x,T')] \<turnstile> Var y[x::=e'] : T" using ineq by auto
  }
  ultimately show "\<Gamma> - [(x,T')] \<turnstile> Var y[x::=e'] : T" by blast
next
  case (t3 y \<Gamma> T\<^isub>1 t T\<^isub>2 e' x)
  have vc: "y\<sharp>x" "y\<sharp>e'" "y\<sharp>\<Gamma>" by fact
  have a1: "(x, T') \<in> set \<Gamma>" by fact
  have a2: "\<Gamma> - [(x,T')] \<turnstile> e' : T'" by fact
  have a3: "(y,T\<^isub>1)#\<Gamma> \<turnstile> t : T\<^isub>2" by fact
  have ih: "\<lbrakk>(x,T') \<in> set ((y,T\<^isub>1)#\<Gamma>); ((y,T\<^isub>1)#\<Gamma>) - [(x,T')] \<turnstile> e' : T'\<rbrakk> 
                               \<Longrightarrow> ((y,T\<^isub>1)#\<Gamma>) - [(x,T')] \<turnstile> (t[x::=e']) : T\<^isub>2" by fact 
  have "(x,T') \<in> set ((y,T\<^isub>1)#\<Gamma>)" using a1 vc by (simp add: fresh_atm) 
  moreover
  have "valid ((y,T\<^isub>1)#\<Gamma>)" using a3 by (simp add: typing_implies_valid)
  then have a5: "valid ((y,T\<^isub>1)#\<Gamma>) - [(x,T')]" by (simp only: valid_diff) 
  then have "((y,T\<^isub>1)#\<Gamma>) - [(x,T')] \<turnstile> e' : T'" using a2 by (auto intro: weakening) 
  ultimately have "((y,T\<^isub>1)#\<Gamma>) - [(x,T')] \<turnstile> (t[x::=e']) : T\<^isub>2" using ih by blast
  then have "(y,T\<^isub>1)#(\<Gamma> - [(x,T')]) \<turnstile> (t[x::=e']) : T\<^isub>2" using vc by (simp add: fresh_atm)
  moreover
  have "y\<sharp>(\<Gamma> - [(x,T')])" using vc by (simp only: fresh_diff)
  ultimately have "(\<Gamma> - [(x,T')]) \<turnstile> Lam [y].(t[x::=e']) : T\<^isub>1 \<rightarrow> T\<^isub>2" by blast
  then show "(\<Gamma> - [(x,T')]) \<turnstile> (Lam [y].t)[x::=e'] : T\<^isub>1 \<rightarrow> T\<^isub>2" using vc by simp
qed (force)

corollary type_substitution2:
  assumes a: "(x,T')#\<Gamma> \<turnstile> e : T"
  and     b: "\<Gamma> \<turnstile> e' : T'"
  shows "\<Gamma> \<turnstile> e[x::=e'] : T"
proof -
  from a have c: "valid ((x,T')#\<Gamma>)" by (simp add: typing_implies_valid)
  then have "x\<sharp>\<Gamma>" by (auto dest: valid_elim)
  then have eq: "((x,T')#\<Gamma>) - [(x,T')] = \<Gamma>" 
    by (induct \<Gamma>) (auto simp add: fresh_list_cons fresh_prod fresh_atm)
  with a b show "\<Gamma> \<turnstile> e[x::=e'] : T" by (auto dest: type_substitution)
qed

text {* Type inversion lemmas *}
  
lemma t_Lam_inversion[dest]:
  assumes ty: "\<Gamma> \<turnstile> Lam [x].t : T" 
  and     fc: "x\<sharp>\<Gamma>" 
  shows "\<exists>T\<^isub>1 T\<^isub>2. T = T\<^isub>1 \<rightarrow> T\<^isub>2 \<and> (x,T\<^isub>1)#\<Gamma> \<turnstile> t : T\<^isub>2"
using ty fc 
by (cases rule: typing.strong_cases) 
   (auto simp add: alpha lam.inject abs_fresh ty_fresh)

lemma t_App_inversion[dest]:
  assumes ty: "\<Gamma> \<turnstile> App t1 t2 : T" 
  shows "\<exists>T'. \<Gamma> \<turnstile> t1 : T' \<rightarrow> T \<and> \<Gamma> \<turnstile> t2 : T'"
using ty 
by (cases) (auto simp add: lam.inject)

text {* Beta-reduction *}

inductive 
  "beta" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta> _")
where
  b1[intro]: "t1 \<longrightarrow>\<^isub>\<beta> t2 \<Longrightarrow> App t1 s \<longrightarrow>\<^isub>\<beta> App t2 s"
| b2[intro]: "s1 \<longrightarrow>\<^isub>\<beta> s2 \<Longrightarrow> App t s1 \<longrightarrow>\<^isub>\<beta> App t s2"
| b3[intro]: "t1 \<longrightarrow>\<^isub>\<beta> t2 \<Longrightarrow> Lam [x].t1 \<longrightarrow>\<^isub>\<beta> Lam [x].t2"
| b4[intro]: "x\<sharp>s \<Longrightarrow> App (Lam [x].t) s \<longrightarrow>\<^isub>\<beta> t[x::=s]"

equivariance beta
nominal_inductive beta
  by (auto simp add: abs_fresh fresh_fact)

text {*
  Task 4 (easy)

  Now we can prove the type-preservation theorem.
  Prove it by induction over t \<longrightarrow>\<^isub>\<beta> t' and avoid
  \<Gamma> and T.

*}
  
theorem type_preservation:
  assumes a: "t \<longrightarrow>\<^isub>\<beta> t'"
  and     b: "\<Gamma> \<turnstile> t : T" 
  shows "\<Gamma> \<turnstile> t' : T" 
using a b
proof (nominal_induct avoiding: \<Gamma> T rule: beta.strong_induct)
  case (b1 t1 t2 s \<Gamma> T)
  have "\<Gamma> \<turnstile> App t1 s : T" by fact
  then obtain T' where a1: "\<Gamma> \<turnstile> t1 : T' \<rightarrow> T" and a2: "\<Gamma> \<turnstile> s : T'" by auto
  have ih: "\<Gamma> \<turnstile> t1 : T' \<rightarrow> T \<Longrightarrow> \<Gamma> \<turnstile> t2 : T' \<rightarrow> T" by fact
  with a1 a2 show "\<Gamma> \<turnstile> App t2 s : T" by auto
next 
  case (b2 s1 s2 t \<Gamma> T)
  have "\<Gamma> \<turnstile> App t s1 : T" by fact
  then obtain T' where a1: "\<Gamma> \<turnstile> t : T' \<rightarrow> T" and a2: "\<Gamma> \<turnstile> s1 : T'" by auto
  have ih: "\<Gamma> \<turnstile> s1 : T' \<Longrightarrow> \<Gamma> \<turnstile> s2 : T'" by fact
  with a1 a2 show "\<Gamma> \<turnstile> App t s2 : T" by auto
next 
  case (b3 t1 t2 x \<Gamma> T)
  have vc: "x\<sharp>\<Gamma>" by fact
  have "\<Gamma> \<turnstile> Lam [x].t1 : T" by fact
  then obtain T1 T2 where a1: "(x,T1)#\<Gamma> \<turnstile> t1 : T2" and a2: "T = T1 \<rightarrow> T2" using vc by auto
  have ih: "(x,T1)#\<Gamma> \<turnstile> t1 : T2 \<Longrightarrow> (x,T1)#\<Gamma> \<turnstile> t2 : T2" by fact
  with a1 a2 show "\<Gamma> \<turnstile> Lam [x].t2 : T" using vc by auto
next
  case (b4 x s t \<Gamma> T)
  have vc: "x\<sharp>\<Gamma>" by fact
  have "\<Gamma> \<turnstile> App (Lam [x].t) s : T" by fact
  then obtain T' where a1: "\<Gamma> \<turnstile> Lam [x].t : T' \<rightarrow> T" and a2: "\<Gamma> \<turnstile> s : T'" by auto
  from a1 obtain T1 T2 where a3: "(x,T')#\<Gamma> \<turnstile> t : T" using vc by (auto simp add: ty.inject)
  from a3 a2 show "\<Gamma> \<turnstile> t[x::=s] : T" by (simp add: type_substitution2)
qed


end