diff -r 87b735f86060 -r ddc05a611005 Tutorial/Tutorial4.thy
--- a/Tutorial/Tutorial4.thy	Fri Jan 21 00:55:28 2011 +0100
+++ b/Tutorial/Tutorial4.thy	Fri Jan 21 21:58:51 2011 +0100
@@ -1,6 +1,5 @@
-
 theory Tutorial4
-imports Tutorial1
+imports Tutorial1 Tutorial2
 begin
 
 section {* The CBV Reduction Relation (Small-Step Semantics) *}
@@ -136,22 +135,28 @@
 lemma machines_implies_cbvs_ctx:
   assumes a: "<e, Es> \<mapsto>* <e', Es'>"
   shows "(Es\<down>)\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* (Es'\<down>)\<lbrakk>e'\<rbrakk>"
-using a 
-by (induct) (auto dest: machine_implies_cbvs_ctx)
+using a machine_implies_cbvs_ctx 
+by (induct) (blast)+
 
 text {* 
   So whenever we let the CL machine start in an initial
   state and it arrives at a final state, then there exists
-  a corresponding cbv-reduction sequence. *}
+  a corresponding cbv-reduction sequence. 
+*}
 
 corollary machines_implies_cbvs:
   assumes a: "<e, []> \<mapsto>* <e', []>"
   shows "e \<longrightarrow>cbv* e'"
-using a by (auto dest: machines_implies_cbvs_ctx)
+proof - 
+  have "[]\<down>\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* []\<down>\<lbrakk>e'\<rbrakk>" 
+     using a machines_implies_cbvs_ctx by blast
+  then show "e \<longrightarrow>cbv* e'" by simp  
+qed
 
 text {*
   We now want to relate the cbv-reduction to the evaluation
-  relation. For this we need two auxiliary lemmas. *}
+  relation. For this we need two auxiliary lemmas. 
+*}
 
 lemma eval_val:
   assumes a: "val t"
@@ -160,16 +165,15 @@
 
 lemma e_App_elim:
   assumes a: "App t1 t2 \<Down> v"
-  shows "\<exists>x t v'. t1 \<Down> Lam [x].t \<and> t2 \<Down> v' \<and> t[x::=v'] \<Down> v"
+  obtains x t v' where "t1 \<Down> Lam [x].t" "t2 \<Down> v'" "t[x::=v'] \<Down> v"
 using a by (cases) (auto simp add: lam.eq_iff lam.distinct) 
 
-text {******************************************************************
-  
-  10.) Exercise
-  -------------
+
+subsection {* EXERCISE *}
 
-  Complete the first case in the proof below. 
-
+text {*
+  Complete the first and second case in the 
+  proof below. 
 *}
 
 lemma cbv_eval:
@@ -180,8 +184,9 @@
   case (cbv1 v x t t3)
   have a1: "val v" by fact
   have a2: "t[x ::= v] \<Down> t3" by fact
-
-  show "App (Lam [x].t) v \<Down> t3" sorry
+  have a3: "Lam [x].t \<Down> Lam [x].t" by auto
+  have a4: "v \<Down> v" using a1 eval_val by auto
+  show "App (Lam [x].t) v \<Down> t3" using a3 a4 a2 by auto 
 next
   case (cbv2 t t' t2 t3)
   have ih: "\<And>t3. t' \<Down> t3 \<Longrightarrow> t \<Down> t3" by fact
@@ -189,10 +194,10 @@
   then obtain x t'' v' 
     where a1: "t' \<Down> Lam [x].t''" 
       and a2: "t2 \<Down> v'" 
-      and a3: "t''[x ::= v'] \<Down> t3" using e_App_elim by blast
+      and a3: "t''[x ::= v'] \<Down> t3" by (rule e_App_elim) 
   have "t \<Down>  Lam [x].t''" using ih a1 by auto 
   then show "App t t2 \<Down> t3" using a2 a3 by auto
-qed (auto dest!: e_App_elim)
+qed (auto elim!: e_App_elim)
 
 
 text {* 
@@ -206,7 +211,8 @@
 
 text {* 
   Finally, we can show that if from a term t we reach a value 
-  by a cbv-reduction sequence, then t evaluates to this value. *}
+  by a cbv-reduction sequence, then t evaluates to this value. 
+*}
 
 lemma cbvs_implies_eval:
   assumes a: "t \<longrightarrow>cbv* v" "val v"
@@ -216,15 +222,16 @@
 
 text {* 
   All facts tied together give us the desired property about
-  K machines. *}
+  machines. 
+*}
 
 theorem machines_implies_eval:
   assumes a: "<t1, []> \<mapsto>* <t2, []>" 
   and     b: "val t2" 
   shows "t1 \<Down> t2"
 proof -
-  have "t1 \<longrightarrow>cbv* t2" using a by (simp add: machines_implies_cbvs)
-  then show "t1 \<Down> t2" using b by (simp add: cbvs_implies_eval)
+  have "t1 \<longrightarrow>cbv* t2" using a machines_implies_cbvs by simp
+  then show "t1 \<Down> t2" using b cbvs_implies_eval by simp
 qed
 
 lemma valid_elim:
@@ -252,9 +259,9 @@
 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"
+  assumes a: "\<Delta> @ [(x, T')] @ \<Gamma> \<turnstile> e : T"
   and     b: "\<Gamma> \<turnstile> e' : T'"
-  shows "(\<Delta> @ \<Gamma>) \<turnstile> e[x ::= 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>)
@@ -264,40 +271,42 @@
   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)
+    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
+    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"
+  assumes a: "(x, T') # \<Gamma> \<turnstile> e : T"
   and     b: "\<Gamma> \<turnstile> e' : T'"
-  shows "\<Gamma> \<turnstile> e[x::=e'] : T"
+  shows "\<Gamma> \<turnstile> e[x ::= e'] : T"
 using a b type_substitution_aux[where \<Delta>="[]"]
-by (auto)
+by auto
 
 lemma t_App_elim:
   assumes a: "\<Gamma> \<turnstile> App t1 t2 : T"
-  shows "\<exists>T'. \<Gamma> \<turnstile> t1 : T' \<rightarrow> T \<and> \<Gamma> \<turnstile> 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>" 
-  shows "\<exists>T1 T2. T = T1 \<rightarrow> T2 \<and> (x, T1) # \<Gamma> \<turnstile> t : T2"
+  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(rule_tac p="(x \<leftrightarrow> xa)" in permute_boolE)
+apply(rotate_tac 3)
+apply(drule_tac p="(x \<leftrightarrow> xa)" in permute_boolI)
 apply(perm_simp)
-apply(simp add: flip_def swap_fresh_fresh ty_fresh)
+apply(auto simp add: flip_def swap_fresh_fresh ty_fresh)
 done
 
 theorem cbv_type_preservation:
@@ -306,7 +315,7 @@
   shows "\<Gamma> \<turnstile> t' : T"
 using a b
 by (nominal_induct avoiding: \<Gamma> T rule: cbv.strong_induct)
-   (auto dest!: t_Lam_elim t_App_elim simp add: type_substitution ty.eq_iff)
+   (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'"
@@ -316,15 +325,17 @@
 by (induct) (auto intro: cbv_type_preservation)
 
 text {* 
-  The Type-Preservation Property for the Machine and Evaluation Relation. *}
+  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 -
-  from a have "t \<longrightarrow>cbv* t'" by (simp add: machines_implies_cbvs)
-  then show "\<Gamma> \<turnstile> t' : T" using b by (simp add: cbvs_type_preservation)
+  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:
@@ -332,8 +343,8 @@
   and     b: "\<Gamma> \<turnstile> t : T" 
   shows "\<Gamma> \<turnstile> t' : T"
 proof -
-  from a have "<t, []> \<mapsto>* <t', []>" by (simp add: eval_implies_machines)
-  then show "\<Gamma> \<turnstile> t' : T" using b by (simp add: machine_type_preservation)
+  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 *}
@@ -341,7 +352,7 @@
 lemma canonical_tArr:
   assumes a: "[] \<turnstile> t : T1 \<rightarrow> T2"
   and     b: "val t"
-  shows "\<exists>x t'. t = Lam [x].t'"
+  obtains x t' where "t = Lam [x].t'"
 using b a by (induct) (auto) 
 
 theorem progress:
@@ -349,6 +360,11 @@
   shows "(\<exists>t'. t \<longrightarrow>cbv t') \<or> (val t)"
 using a
 by (induct \<Gamma>\<equiv>"[]::ty_ctx" t T)
-   (auto intro: cbv.intros dest!: canonical_tArr)
+   (auto elim: canonical_tArr)
 
+text {*
+  Done!
+*}
 
+end
+