--- 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
+