113 shows "(Es\<down>)\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* (Es'\<down>)\<lbrakk>e'\<rbrakk>" |
113 shows "(Es\<down>)\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* (Es'\<down>)\<lbrakk>e'\<rbrakk>" |
114 using a |
114 using a |
115 proof (induct) |
115 proof (induct) |
116 case (m1 t1 t2 Es) |
116 case (m1 t1 t2 Es) |
117 thm machine.intros thm cbv2 |
117 thm machine.intros thm cbv2 |
118 have "Es\<down>\<lbrakk>App t1 t2\<rbrakk> = (Es\<down> \<odot> CAppL \<box> t2)\<lbrakk>t1\<rbrakk>" using ctx_compose ctx_composes.simps filling.simps by simp |
118 have "Es\<down>\<lbrakk>App t1 t2\<rbrakk> = (Es\<down> \<odot> CAppL \<box> t2)\<lbrakk>t1\<rbrakk>" |
|
119 using ctx_compose ctx_composes.simps filling.simps by simp |
119 then show "Es\<down>\<lbrakk>App t1 t2\<rbrakk> \<longrightarrow>cbv* ((CAppL \<box> t2) # Es)\<down>\<lbrakk>t1\<rbrakk>" using cbvs.intros by simp |
120 then show "Es\<down>\<lbrakk>App t1 t2\<rbrakk> \<longrightarrow>cbv* ((CAppL \<box> t2) # Es)\<down>\<lbrakk>t1\<rbrakk>" using cbvs.intros by simp |
120 next |
121 next |
121 case (m2 v t2 Es) |
122 case (m2 v t2 Es) |
122 have "val v" by fact |
123 have "val v" by fact |
123 have "((CAppL \<box> t2) # Es)\<down>\<lbrakk>v\<rbrakk> = (CAppR v \<box> # Es)\<down>\<lbrakk>t2\<rbrakk>" using ctx_compose ctx_composes.simps filling.simps by simp |
124 have "((CAppL \<box> t2) # Es)\<down>\<lbrakk>v\<rbrakk> = (CAppR v \<box> # Es)\<down>\<lbrakk>t2\<rbrakk>" |
|
125 using ctx_compose ctx_composes.simps filling.simps by simp |
124 then show "((CAppL \<box> t2) # Es)\<down>\<lbrakk>v\<rbrakk> \<longrightarrow>cbv* (CAppR v \<box> # Es)\<down>\<lbrakk>t2\<rbrakk>" using cbvs.intros by simp |
126 then show "((CAppL \<box> t2) # Es)\<down>\<lbrakk>v\<rbrakk> \<longrightarrow>cbv* (CAppR v \<box> # Es)\<down>\<lbrakk>t2\<rbrakk>" using cbvs.intros by simp |
125 next |
127 next |
126 case (m3 v x t Es) |
128 case (m3 v x t Es) |
127 have aa: "val v" by fact |
129 have aa: "val v" by fact |
128 have "(((CAppR (Lam [x].t) \<box>) # Es)\<down>)\<lbrakk>v\<rbrakk> = Es\<down>\<lbrakk>App (Lam [x]. t) v\<rbrakk>" using ctx_compose ctx_composes.simps filling.simps by simp |
130 have "(((CAppR (Lam [x].t) \<box>) # Es)\<down>)\<lbrakk>v\<rbrakk> = Es\<down>\<lbrakk>App (Lam [x]. t) v\<rbrakk>" |
129 then have "(((CAppR (Lam [x].t) \<box>) # Es)\<down>)\<lbrakk>v\<rbrakk> \<longrightarrow>cbv (Es\<down>)\<lbrakk>(t[x ::= v])\<rbrakk>" using better_cbv1[OF aa] cbv_in_ctx by simp |
131 using ctx_compose ctx_composes.simps filling.simps by simp |
|
132 then have "(((CAppR (Lam [x].t) \<box>) # Es)\<down>)\<lbrakk>v\<rbrakk> \<longrightarrow>cbv (Es\<down>)\<lbrakk>(t[x ::= v])\<rbrakk>" |
|
133 using better_cbv1[OF aa] cbv_in_ctx by simp |
130 then show "(((CAppR (Lam [x].t) \<box>) # Es)\<down>)\<lbrakk>v\<rbrakk> \<longrightarrow>cbv* (Es\<down>)\<lbrakk>(t[x ::= v])\<rbrakk>" using cbvs.intros by blast |
134 then show "(((CAppR (Lam [x].t) \<box>) # Es)\<down>)\<lbrakk>v\<rbrakk> \<longrightarrow>cbv* (Es\<down>)\<lbrakk>(t[x ::= v])\<rbrakk>" using cbvs.intros by blast |
131 qed |
135 qed |
132 |
136 |
133 text {* |
137 text {* |
134 It is not difficult to extend the lemma above to |
138 It is not difficult to extend the lemma above to |