theory Tutorial5

imports Tutorial4

begin

section {* Type Preservation (fixme separate file) *}

lemma valid_elim:

  assumes a: "valid ((x, T) # \<Gamma>)"

  shows "atom x \<sharp> \<Gamma> \<and> valid \<Gamma>"

using a by (cases) (auto)

lemma valid_insert:

  assumes a: "valid (\<Delta> @ [(x, T)] @ \<Gamma>)"

  shows "valid (\<Delta> @ \<Gamma>)" 

using a

by (induct \<Delta>)

   (auto simp add: fresh_append fresh_Cons dest!: valid_elim)

lemma fresh_list: 

  shows "atom y \<sharp> xs = (\<forall>x \<in> set xs. atom y \<sharp> x)"

by (induct xs) (simp_all add: fresh_Nil fresh_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_list fresh_Pair fresh_at_base)

lemma type_substitution_aux:

  assumes a: "\<Delta> @ [(x, T')] @ \<Gamma> \<turnstile> e : T"

  and     b: "\<Gamma> \<turnstile> e' : T'"

  shows "\<Delta> @ \<Gamma> \<turnstile> e[x ::= e'] : T" 

using a b 

proof (nominal_induct \<Gamma>'\<equiv>"\<Delta> @ [(x, T')] @ \<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct)

  case (t_Var y T x e' \<Delta>)

  have a1: "valid (\<Delta> @ [(x, T')] @ \<Gamma>)" by fact

  have a2: "(y,T) \<in> set (\<Delta> @ [(x, T')] @ \<Gamma>)" by fact 

  have a3: "\<Gamma> \<turnstile> e' : T'" by fact

  from a1 have a4: "valid (\<Delta> @ \<Gamma>)" by (rule valid_insert)

  { assume eq: "x = y"

    from a1 a2 have "T = T'" using eq by (auto intro: context_unique)

    with a3 have "\<Delta> @ \<Gamma> \<turnstile> Var y[x ::= e'] : T" using eq a4 by (auto intro: weakening)

  }

  moreover

  { assume ineq: "x \<noteq> y"

    from a2 have "(y, T) \<in> set (\<Delta> @ \<Gamma>)" using ineq by simp

    then have "\<Delta> @ \<Gamma> \<turnstile> Var y[x ::= e'] : T" using ineq a4 by auto

  }

  ultimately show "\<Delta> @ \<Gamma> \<turnstile> Var y[x::=e'] : T" by blast

qed (force simp add: fresh_append fresh_Cons)+

corollary type_substitution:

  assumes a: "(x, T') # \<Gamma> \<turnstile> e : T"

  and     b: "\<Gamma> \<turnstile> e' : T'"

  shows "\<Gamma> \<turnstile> e[x ::= e'] : T"

using a b type_substitution_aux[where \<Delta>="[]"]

by auto

lemma t_App_elim:

  assumes a: "\<Gamma> \<turnstile> App t1 t2 : T"

  obtains T' where "\<Gamma> \<turnstile> t1 : T' \<rightarrow> T" "\<Gamma> \<turnstile> t2 : T'"

using a

by (cases) (auto simp add: lam.eq_iff lam.distinct)

text {* we have not yet generated strong elimination rules *}

lemma t_Lam_elim:

  assumes ty: "\<Gamma> \<turnstile> Lam [x].t : T" 

  and     fc: "atom x \<sharp> \<Gamma>" 

  obtains T1 T2 where "T = T1 \<rightarrow> T2" "(x, T1) # \<Gamma> \<turnstile> t : T2"

using ty fc

apply(cases)

apply(auto simp add: lam.eq_iff lam.distinct ty.eq_iff)

apply(auto simp add: Abs1_eq_iff)

apply(rotate_tac 3)

apply(drule_tac p="(x \<leftrightarrow> xa)" in permute_boolI)

apply(perm_simp)

apply(auto simp add: flip_def swap_fresh_fresh ty_fresh)

done

theorem cbv_type_preservation:

  assumes a: "t \<longrightarrow>cbv t'"

  and     b: "\<Gamma> \<turnstile> t : T" 

  shows "\<Gamma> \<turnstile> t' : T"

using a b

by (nominal_induct avoiding: \<Gamma> T rule: cbv.strong_induct)

   (auto elim!: t_Lam_elim t_App_elim simp add: type_substitution ty.eq_iff)

corollary cbvs_type_preservation:

  assumes a: "t \<longrightarrow>cbv* t'"

  and     b: "\<Gamma> \<turnstile> t : T" 

  shows "\<Gamma> \<turnstile> t' : T"

using a b

by (induct) (auto intro: cbv_type_preservation)

text {* 

  The type-preservation property for the machine and 

  evaluation relation. 

*}

theorem machine_type_preservation:

  assumes a: "<t, []> \<mapsto>* <t', []>"

  and     b: "\<Gamma> \<turnstile> t : T" 

  shows "\<Gamma> \<turnstile> t' : T"

proof -

  have "t \<longrightarrow>cbv* t'" using a machines_implies_cbvs by simp

  then show "\<Gamma> \<turnstile> t' : T" using b cbvs_type_preservation by simp

qed

theorem eval_type_preservation:

  assumes a: "t \<Down> t'"

  and     b: "\<Gamma> \<turnstile> t : T" 

  shows "\<Gamma> \<turnstile> t' : T"

proof -

  have "<t, []> \<mapsto>* <t', []>" using a eval_implies_machines by simp

  then show "\<Gamma> \<turnstile> t' : T" using b machine_type_preservation by simp

qed

text {* The Progress Property *}

lemma canonical_tArr:

  assumes a: "[] \<turnstile> t : T1 \<rightarrow> T2"

  and     b: "val t"

  obtains x t' where "t = Lam [x].t'"

using b a by (induct) (auto) 

theorem progress:

  assumes a: "[] \<turnstile> t : T"

  shows "(\<exists>t'. t \<longrightarrow>cbv t') \<or> (val t)"

using a

by (induct \<Gamma>\<equiv>"[]::ty_ctx" t T)

text {*

  Done! Congratulations!

*}

end