2 imports Tutorial1 Tutorial2

     3 imports Tutorial1 Tutorial2 Tutorial3

   237 lemma valid_elim:

   239 

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

   240 

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

   240 using a by (cases) (auto)

   241 

   242 lemma valid_insert:

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

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

   245 using a

   246 by (induct \<Delta>)

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

   248 

   249 lemma fresh_list: 

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

   251 by (induct xs) (simp_all add: fresh_Nil fresh_Cons)

   252 

   253 lemma context_unique:

   254   assumes a1: "valid \<Gamma>"

   255   and     a2: "(x, T) \<in> set \<Gamma>"

   256   and     a3: "(x, U) \<in> set \<Gamma>"

   257   shows "T = U" 

   258 using a1 a2 a3

   259 by (induct) (auto simp add: fresh_list fresh_Pair fresh_at_base)

   260 

   261 lemma type_substitution_aux:

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

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

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

   265 using a b 

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

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

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

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

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

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

   272   { assume eq: "x = y"

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

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

   275   }

   276   moreover

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

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

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

   280   }

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

   282 qed (force simp add: fresh_append fresh_Cons)+

   283 

   284 corollary type_substitution:

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

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

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

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

   289 by auto

   290 

   291 lemma t_App_elim:

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

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

   294 using a

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

   296 

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

   298 lemma t_Lam_elim:

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

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

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

   302 using ty fc

   303 apply(cases)

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

   305 apply(auto simp add: Abs1_eq_iff)

   306 apply(rotate_tac 3)

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

   308 apply(perm_simp)

   309 apply(auto simp add: flip_def swap_fresh_fresh ty_fresh)

   310 done

   311 

   312 theorem cbv_type_preservation:

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

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

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

   316 using a b

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

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

   319 

   320 corollary cbvs_type_preservation:

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

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

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

   324 using a b

   325 by (induct) (auto intro: cbv_type_preservation)

   326 

   327 text {* 

   328   The type-preservation property for the machine and 

   329   evaluation relation. 

   330 *}

   331 

   332 theorem machine_type_preservation:

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

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

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

   336 proof -

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

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

   339 qed

   340 

   341 theorem eval_type_preservation:

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

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

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

   345 proof -

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

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

   348 qed

   349 

   350 text {* The Progress Property *}

   351 

   352 lemma canonical_tArr:

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

   354   and     b: "val t"

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

   356 using b a by (induct) (auto) 

   357 

   358 theorem progress:

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

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

   361 using a

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

   363    (auto elim: canonical_tArr)

   364 

   365 text {*

   366   Done!

   367 *}