--- a/Tutorial/Tutorial4.thy	Fri Jan 21 22:02:34 2011 +0100
+++ b/Tutorial/Tutorial4.thy	Fri Jan 21 22:23:44 2011 +0100
@@ -1,5 +1,6 @@
+
 theory Tutorial4
-imports Tutorial1 Tutorial2
+imports Tutorial1 Tutorial2 Tutorial3
 begin
 
 section {* The CBV Reduction Relation (Small-Step Semantics) *}
@@ -163,6 +164,7 @@
   shows "t \<Down> t"
 using a by (induct) (auto)
 
+
 lemma e_App_elim:
   assumes a: "App t1 t2 \<Down> v"
   obtains x t v' where "t1 \<Down> Lam [x].t" "t2 \<Down> v'" "t[x::=v'] \<Down> v"
@@ -234,137 +236,8 @@
   then show "t1 \<Down> t2" using b cbvs_implies_eval by simp
 qed
 
-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)
-   (auto elim: canonical_tArr)
-
-text {*
-  Done!
-*}
 
 end