nominal2: comparison Tutorial/Tutorial4.thy

equal deleted inserted replaced

-:87b735f86060
+:ddc05a611005
 theory Tutorial4
-imports Tutorial1
+imports Tutorial1 Tutorial2
 begin
 section {* The CBV Reduction Relation (Small-Step Semantics) *}
 text {*
 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
+using a machine_implies_cbvs_ctx
-by (induct) (auto dest: 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"
 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"
+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 {******************************************************************
+subsection {* EXERCISE *}
-10.) Exercise
--------------
+text {*
+Complete the first and second case in the
-Complete the first case in the proof below.
+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
+have a3: "Lam [x].t \<Down> Lam [x].t" by auto
-show "App (Lam [x].t) v \<Down> t3" sorry
+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
 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
+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 {*
 Next we extend the lemma above to arbitray initial
 sequences of cbv-reductions. *}
 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. *}
+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. *}
+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)
+have "t1 \<longrightarrow>cbv* t2" using a machines_implies_cbvs by simp
-then show "t1 \<Down> t2" using b by (simp add: cbvs_implies_eval)
+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>"
 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"
+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>)
 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)
+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:
 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)
+(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. *}
+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)
+have "t \<longrightarrow>cbv* t'" using a machines_implies_cbvs by simp
-then show "\<Gamma> \<turnstile> t' : T" using b by (simp add: cbvs_type_preservation)
+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 -
-from a have "<t, []> \<mapsto>* <t', []>" by (simp add: eval_implies_machines)
+have "<t, []> \<mapsto>* <t', []>" using a eval_implies_machines by simp
-then show "\<Gamma> \<turnstile> t' : T" using b by (simp add: machine_type_preservation)
+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"
-shows "\<exists>x t'. t = Lam [x].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 intro: cbv.intros dest!: canonical_tArr)
+(auto elim: canonical_tArr)
+text {*
+Done!
+*}
+end

changeset 2689	ddc05a611005
parent 2687	d0fb94035969
child 2691	abb6c3ac2df2