--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Tutorial/Tutorial4.thy Thu Jan 20 23:19:30 2011 +0100
@@ -0,0 +1,354 @@
+
+theory Tutorial4
+imports Tutorial1
+begin
+
+section {* The CBV Reduction Relation (Small-Step Semantics) *}
+
+text {*
+ In order to help establishing the property that the CK Machine
+ calculates a nomrmalform that corresponds to the evaluation
+ relation, we introduce the call-by-value small-step semantics.
+*}
+
+inductive
+ cbv :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<longrightarrow>cbv _" [60, 60] 60)
+where
+ cbv1: "\<lbrakk>val v; atom x \<sharp> v\<rbrakk> \<Longrightarrow> App (Lam [x].t) v \<longrightarrow>cbv t[x ::= v]"
+| cbv2[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> App t t2 \<longrightarrow>cbv App t' t2"
+| cbv3[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> App t2 t \<longrightarrow>cbv App t2 t'"
+
+equivariance val
+equivariance cbv
+nominal_inductive cbv
+ avoids cbv1: "x"
+ unfolding fresh_star_def
+ by (simp_all add: lam.fresh Abs_fresh_iff fresh_Pair fresh_fact)
+
+text {*
+ In order to satisfy the vc-condition we have to formulate
+ this relation with the additional freshness constraint
+ atom x \<sharp> v. Although this makes the definition vc-ompatible, it
+ makes the definition less useful. We can with a little bit of
+ pain show that the more restricted rule is equivalent to the
+ usual rule.
+*}
+
+lemma subst_rename:
+ assumes a: "atom y \<sharp> t"
+ shows "t[x ::= s] = ((y \<leftrightarrow> x) \<bullet> t)[y ::= s]"
+using a
+by (nominal_induct t avoiding: x y s rule: lam.strong_induct)
+ (auto simp add: lam.fresh fresh_at_base)
+
+
+lemma better_cbv1 [intro]:
+ assumes a: "val v"
+ shows "App (Lam [x].t) v \<longrightarrow>cbv t[x::=v]"
+proof -
+ obtain y::"name" where fs: "atom y \<sharp> (x, t, v)" by (rule obtain_fresh)
+ have "App (Lam [x].t) v = App (Lam [y].((y \<leftrightarrow> x) \<bullet> t)) v" using fs
+ by (auto simp add: lam.eq_iff Abs1_eq_iff' flip_def fresh_Pair fresh_at_base)
+ also have "\<dots> \<longrightarrow>cbv ((y \<leftrightarrow> x) \<bullet> t)[y ::= v]" using fs a cbv1 by auto
+ also have "\<dots> = t[x ::= v]" using fs subst_rename[symmetric] by simp
+ finally show "App (Lam [x].t) v \<longrightarrow>cbv t[x ::= v]" by simp
+qed
+
+text {*
+ The transitive closure of the cbv-reduction relation:
+*}
+
+inductive
+ "cbvs" :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>cbv* _" [60, 60] 60)
+where
+ cbvs1[intro]: "e \<longrightarrow>cbv* e"
+| cbvs2[intro]: "\<lbrakk>e1\<longrightarrow>cbv e2; e2 \<longrightarrow>cbv* e3\<rbrakk> \<Longrightarrow> e1 \<longrightarrow>cbv* e3"
+
+lemma cbvs3 [intro]:
+ assumes a: "e1 \<longrightarrow>cbv* e2" "e2 \<longrightarrow>cbv* e3"
+ shows "e1 \<longrightarrow>cbv* e3"
+using a by (induct) (auto)
+
+
+subsection {* EXERCISE 8 *}
+
+text {*
+ If more simple exercises are needed, then complete the following proof.
+*}
+
+lemma cbv_in_ctx:
+ assumes a: "t \<longrightarrow>cbv t'"
+ shows "E\<lbrakk>t\<rbrakk> \<longrightarrow>cbv E\<lbrakk>t'\<rbrakk>"
+using a
+proof (induct E)
+ case Hole
+ have "t \<longrightarrow>cbv t'" by fact
+ then show "\<box>\<lbrakk>t\<rbrakk> \<longrightarrow>cbv \<box>\<lbrakk>t'\<rbrakk>" by simp
+next
+ case (CAppL E s)
+ have ih: "t \<longrightarrow>cbv t' \<Longrightarrow> E\<lbrakk>t\<rbrakk> \<longrightarrow>cbv E\<lbrakk>t'\<rbrakk>" by fact
+ moreover
+ have "t \<longrightarrow>cbv t'" by fact
+ ultimately
+ have "E\<lbrakk>t\<rbrakk> \<longrightarrow>cbv E\<lbrakk>t'\<rbrakk>" by simp
+ then show "(CAppL E s)\<lbrakk>t\<rbrakk> \<longrightarrow>cbv (CAppL E s)\<lbrakk>t'\<rbrakk>" by auto
+next
+ case (CAppR s E)
+ have ih: "t \<longrightarrow>cbv t' \<Longrightarrow> E\<lbrakk>t\<rbrakk> \<longrightarrow>cbv E\<lbrakk>t'\<rbrakk>" by fact
+ moreover
+ have a: "t \<longrightarrow>cbv t'" by fact
+ ultimately
+ have "E\<lbrakk>t\<rbrakk> \<longrightarrow>cbv E\<lbrakk>t'\<rbrakk>" by simp
+ then show "(CAppR s E)\<lbrakk>t\<rbrakk> \<longrightarrow>cbv (CAppR s E)\<lbrakk>t'\<rbrakk>" by auto
+qed
+
+section {* EXERCISE 9 *}
+
+text {*
+ The point of the cbv-reduction was that we can easily relatively
+ establish the follwoing property:
+*}
+
+lemma machine_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
+proof (induct)
+ case (m1 t1 t2 Es)
+
+ show "Es\<down>\<lbrakk>App t1 t2\<rbrakk> \<longrightarrow>cbv* ((CAppL \<box> t2) # Es)\<down>\<lbrakk>t1\<rbrakk>" sorry
+next
+ case (m2 v t2 Es)
+ have "val v" by fact
+
+ show "((CAppL \<box> t2) # Es)\<down>\<lbrakk>v\<rbrakk> \<longrightarrow>cbv* (CAppR v \<box> # Es)\<down>\<lbrakk>t2\<rbrakk>" sorry
+next
+ case (m3 v x t Es)
+ have "val v" by fact
+
+ show "(((CAppR (Lam [x].t) \<box>) # Es)\<down>)\<lbrakk>v\<rbrakk> \<longrightarrow>cbv* (Es\<down>)\<lbrakk>(t[x ::= v])\<rbrakk>" sorry
+qed
+
+text {*
+ It is not difficult to extend the lemma above to
+ arbitrary reductions sequences of the CK machine. *}
+
+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)
+
+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. *}
+
+corollary machines_implies_cbvs:
+ assumes a: "<e, []> \<mapsto>* <e', []>"
+ shows "e \<longrightarrow>cbv* e'"
+using a by (auto dest: machines_implies_cbvs_ctx)
+
+text {*
+ We now want to relate the cbv-reduction to the evaluation
+ relation. For this we need two auxiliary lemmas. *}
+
+lemma eval_val:
+ assumes a: "val t"
+ shows "t \<Down> t"
+using a by (induct) (auto)
+
+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"
+using a by (cases) (auto simp add: lam.eq_iff lam.distinct)
+
+text {******************************************************************
+
+ 10.) Exercise
+ -------------
+
+ Complete the first case in the proof below.
+
+*}
+
+lemma cbv_eval:
+ assumes a: "t1 \<longrightarrow>cbv t2" "t2 \<Down> t3"
+ shows "t1 \<Down> t3"
+using a
+proof(induct arbitrary: t3)
+ 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
+next
+ case (cbv2 t t' t2 t3)
+ have ih: "\<And>t3. t' \<Down> t3 \<Longrightarrow> t \<Down> t3" by fact
+ have "App t' t2 \<Down> t3" by fact
+ 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
+ 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)
+
+
+text {*
+ Next we extend the lemma above to arbitray initial
+ sequences of cbv-reductions. *}
+
+lemma cbvs_eval:
+ assumes a: "t1 \<longrightarrow>cbv* t2" "t2 \<Down> t3"
+ shows "t1 \<Down> t3"
+using a by (induct) (auto intro: cbv_eval)
+
+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. *}
+
+lemma cbvs_implies_eval:
+ assumes a: "t \<longrightarrow>cbv* v" "val v"
+ shows "t \<Down> v"
+using a
+by (induct) (auto intro: eval_val cbvs_eval)
+
+text {*
+ All facts tied together give us the desired property about
+ K 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)
+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"
+ shows "\<exists>T'. \<Gamma> \<turnstile> t1 : T' \<rightarrow> T \<and> \<Gamma> \<turnstile> t2 : T'"
+using a
+by (cases) (auto simp add: lam.eq_iff lam.distinct)
+
+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"
+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(perm_simp)
+apply(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 dest!: 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 -
+ 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)
+qed
+
+theorem eval_type_preservation:
+ assumes a: "t \<Down> t'"
+ 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)
+qed
+
+text {* The Progress Property *}
+
+lemma canonical_tArr:
+ assumes a: "[] \<turnstile> t : T1 \<rightarrow> T2"
+ and b: "val t"
+ shows "\<exists>x t'. 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 intro: cbv.intros dest!: canonical_tArr)
+
+