--- a/src/HOL/Nominal/Examples/Contexts.thy Sun Jan 06 19:18:01 2008 +0100
+++ b/src/HOL/Nominal/Examples/Contexts.thy Mon Jan 07 02:24:24 2008 +0100
@@ -9,7 +9,8 @@
We show here that the Plotkin-style of defining
reduction relations (based on congruence rules) is
equivalent to the Felleisen-Hieb-style representation
- (based on contexts).
+ (based on contexts), and show cbv-evaluation via a
+ list-machine described by Roshan James.
The interesting point is that contexts do not contain
any binders. On the other hand the operation of filling
@@ -27,10 +28,10 @@
text {*
Contexts - the lambda case in contexts does not bind a name
- even if we introduce the nomtation [_]._ fro CLam.
+ even if we introduce the nomtation [_]._ for CLam.
*}
nominal_datatype ctx =
- Hole
+ Hole ("\<box>" 1000)
| CAppL "ctx" "lam"
| CAppR "lam" "ctx"
| CLam "name" "ctx" ("CLam [_]._" [100,100] 100)
@@ -49,52 +50,26 @@
apply(fresh_guess)+
done
-lemma subst_eqvt[eqvt]:
- fixes pi::"name prm"
- shows "pi\<bullet>t1[x::=t2] = (pi\<bullet>t1)[(pi\<bullet>x)::=(pi\<bullet>t2)]"
-by (nominal_induct t1 avoiding: x t2 rule: lam.induct)
- (auto simp add: perm_bij fresh_atm fresh_bij)
-
-lemma subst_fresh:
- fixes x y::"name"
- and t t'::"lam"
- shows "y\<sharp>([x].t,t') \<Longrightarrow> y\<sharp>t[x::=t']"
-by (nominal_induct t avoiding: x y t' rule: lam.inducts)
- (auto simp add: abs_fresh fresh_prod fresh_atm)
-
-text {*
- Filling is the operation that fills a term into a hole. While
- contexts themselves are not alpha-equivalence classes, the
- filling operation produces an alpha-equivalent lambda-term.
-*}
+text {* Filling is the operation that fills a term into a hole. *}
consts
filling :: "ctx \<Rightarrow> lam \<Rightarrow> lam" ("_<_>" [100,100] 100)
nominal_primrec
- "Hole<t> = t"
+ "\<box><t> = t"
"(CAppL E t')<t> = App (E<t>) t'"
"(CAppR t' E)<t> = App t' (E<t>)"
"(CLam [x].E)<t> = Lam [x].(E<t>)"
by (rule TrueI)+
+text {*
+ While contexts themselves are not alpha-equivalence classes, the
+ filling operation produces an alpha-equivalent lambda-term.
+*}
lemma alpha_test:
- shows "(CLam [x].Hole)<Var x> = (CLam [y].Hole)<Var y>"
-by (auto simp add: alpha lam.inject calc_atm fresh_atm)
-
-lemma replace_eqvt[eqvt]:
- fixes pi:: "name prm"
- shows "pi\<bullet>(E<e>) = (pi\<bullet>E)<(pi\<bullet>e)>"
-by (nominal_induct E rule: ctx.inducts) (auto)
-
-lemma replace_fresh:
- fixes x::"name"
- and E::"ctx"
- and t::"lam"
- shows "x\<sharp>(E,t) \<Longrightarrow> x\<sharp>E<t>"
-by (induct E rule: ctx.weak_induct)
- (auto simp add: fresh_prod abs_fresh)
-
+ shows "x\<noteq>y \<Longrightarrow> (CLam [x].\<box>) \<noteq> (CLam [y].\<box>)"
+ and "(CLam [x].\<box>)<Var x> = (CLam [y].\<box>)<Var y>"
+by (auto simp add: alpha ctx.inject lam.inject calc_atm fresh_atm)
text {* The composition of two contexts *}
@@ -102,7 +77,7 @@
ctx_replace :: "ctx \<Rightarrow> ctx \<Rightarrow> ctx" ("_ \<circ> _" [100,100] 100)
nominal_primrec
- "Hole \<circ> E' = E'"
+ "\<box> \<circ> E' = E'"
"(CAppL E t') \<circ> E' = CAppL (E \<circ> E') t'"
"(CAppR t' E) \<circ> E' = CAppR t' (E \<circ> E')"
"(CLam [x].E) \<circ> E' = CLam [x].(E \<circ> E')"
@@ -112,75 +87,110 @@
shows "E1<E2<t>> = (E1 \<circ> E2)<t>"
by (induct E1 rule: ctx.weak_induct) (auto)
-lemma ctx_compose_fresh:
- fixes x::"name"
- and E1 E2::"ctx"
- shows "x\<sharp>(E1,E2) \<Longrightarrow> x\<sharp>(E1\<circ>E2)"
-by (induct E1 rule: ctx.weak_induct)
- (auto simp add: fresh_prod)
-
text {* Beta-reduction via contexts in the Felleisen-Hieb style. *}
inductive
ctx_red :: "lam\<Rightarrow>lam\<Rightarrow>bool" ("_ \<longrightarrow>x _" [80,80] 80)
where
- xbeta[intro]: "x\<sharp>(E,t') \<Longrightarrow> E<App (Lam [x].t) t'> \<longrightarrow>x E<t[x::=t']>"
-
-equivariance ctx_red
-
-nominal_inductive ctx_red
- by (simp_all add: replace_fresh subst_fresh abs_fresh)
+ xbeta[intro]: "E<App (Lam [x].t) t'> \<longrightarrow>x E<t[x::=t']>"
text {* Beta-reduction via congruence rules in the Plotkin style. *}
inductive
cong_red :: "lam\<Rightarrow>lam\<Rightarrow>bool" ("_ \<longrightarrow>o _" [80,80] 80)
where
- obeta[intro]: "x\<sharp>t' \<Longrightarrow> App (Lam [x].t) t' \<longrightarrow>o t[x::=t']"
+ obeta[intro]: "App (Lam [x].t) t' \<longrightarrow>o t[x::=t']"
| oapp1[intro]: "t \<longrightarrow>o t' \<Longrightarrow> App t t2 \<longrightarrow>o App t' t2"
| oapp2[intro]: "t \<longrightarrow>o t' \<Longrightarrow> App t2 t \<longrightarrow>o App t2 t'"
| olam[intro]: "t \<longrightarrow>o t' \<Longrightarrow> Lam [x].t \<longrightarrow>o Lam [x].t'"
-equivariance cong_red
-
-nominal_inductive cong_red
- by (simp_all add: subst_fresh abs_fresh)
-
text {* The proof that shows both relations are equal. *}
-lemma cong_red_ctx:
+lemma cong_red_in_ctx:
assumes a: "t \<longrightarrow>o t'"
shows "E<t> \<longrightarrow>o E<t'>"
using a
by (induct E rule: ctx.weak_induct) (auto)
-lemma ctx_red_ctx:
+lemma ctx_red_in_ctx:
assumes a: "t \<longrightarrow>x t'"
shows "E<t> \<longrightarrow>x E<t'>"
using a
-by (nominal_induct t t' avoiding: E rule: ctx_red.strong_induct)
- (auto simp add: ctx_compose ctx_compose_fresh)
+by (induct) (auto simp add: ctx_compose)
-lemma ctx_red_hole:
- assumes a: "Hole<t> \<longrightarrow>x Hole<t'>"
- shows "t \<longrightarrow>x t'"
-using a by simp
-
-theorem ctx_red_cong_red:
+theorem ctx_red_implies_cong_red:
assumes a: "t \<longrightarrow>x t'"
shows "t \<longrightarrow>o t'"
using a
-by (induct) (auto intro!: cong_red_ctx)
+by (induct) (auto intro!: cong_red_in_ctx)
-theorem cong_red_ctx_red:
+theorem cong_red_implies_ctx_red:
assumes a: "t \<longrightarrow>o t'"
shows "t \<longrightarrow>x t'"
-using a
-apply(induct)
-apply(rule ctx_red_hole)
-apply(rule xbeta)
-apply(simp)
-apply(metis ctx_red_ctx filling.simps)+ (* found by SledgeHammer *)
-done
+using a
+proof (induct)
+ case (obeta x t' t)
+ have "\<box><App (Lam [x].t) t'> \<longrightarrow>x \<box><t[x::=t']>" by (rule xbeta)
+ then show "App (Lam [x].t) t' \<longrightarrow>x t[x::=t']" by simp
+qed (metis ctx_red_in_ctx filling.simps)+ (* found by SledgeHammer *)
+
+section {* We now use context in a cbv list machine *}
+
+text {* First the function that composes a list of contexts *}
+consts
+ ctx_composes :: "ctx list \<Rightarrow> ctx" ("_\<down>" [80] 80)
+
+primrec
+ "[]\<down> = \<box>"
+ "(E#Es)\<down> = (Es\<down>) \<circ> E"
+
+text {* Values *}
+inductive
+ val :: "lam\<Rightarrow>bool"
+where
+ v_Lam[intro]: "val (Lam [x].e)"
+ | v_Var[intro]: "val (Var x)"
+
+
+text {* CBV reduction using contexts *}
+inductive
+ cbv :: "lam\<Rightarrow>lam\<Rightarrow>bool" ("_ \<longrightarrow>cbv _" [80,80] 80)
+where
+ cbv_beta[intro]: "val v \<Longrightarrow> E<App (Lam [x].e) v> \<longrightarrow>cbv E<e[x::=v]>"
+
+text {* reflexive, transitive closure of CBV reduction *}
+inductive
+ "cbv_star" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>cbv* _" [80,80] 80)
+where
+ cbvs1[intro]: "e \<longrightarrow>cbv* e"
+| cbvs2[intro]: "e \<longrightarrow>cbv e' \<Longrightarrow> e \<longrightarrow>cbv* e'"
+| cbvs3[intro,trans]: "\<lbrakk>e1\<longrightarrow>cbv* e2; e2 \<longrightarrow>cbv* e3\<rbrakk> \<Longrightarrow> e1 \<longrightarrow>cbv* e3"
+
+text {* A list machine which builds up a list of contexts *}
+inductive
+ machine :: "lam\<Rightarrow>ctx list\<Rightarrow>lam\<Rightarrow>ctx list\<Rightarrow>bool" ("<_,_> \<mapsto> <_,_>" [60,60,60,60] 60)
+where
+ m1[intro]: "<App e1 e2, Es> \<mapsto> <e1,(CAppL \<box> e2)#Es>"
+| m2[intro]: "val v \<Longrightarrow> <v,(CAppL \<box> e2)#Es> \<mapsto> <e2,(CAppR v \<box>)#Es>"
+| m3[intro]: "val v \<Longrightarrow> <v,(CAppR (Lam [x].e) \<box>)#Es> \<mapsto> <e[x::=v],Es>"
+
+inductive
+ "machine_star" :: "lam\<Rightarrow>ctx list\<Rightarrow>lam\<Rightarrow>ctx list\<Rightarrow>bool" ("<_,_> \<mapsto>* <_,_>" [60,60,60,60] 60)
+where
+ ms1[intro]: "<e,Es> \<mapsto>* <e,Es>"
+| ms2[intro]: "<e,Es> \<mapsto> <e',Es'> \<Longrightarrow> <e,Es> \<mapsto>* <e',Es'>"
+| ms3[intro,trans]: "\<lbrakk><e1,Es1> \<mapsto>* <e2,Es2>; <e2,Es2> \<mapsto>* <e3,Es3>\<rbrakk> \<Longrightarrow> <e1,Es1> \<mapsto>* <e3,Es3>"
+
+lemma machine_red_implies_cbv_reds_aux:
+ assumes a: "<e,Es> \<mapsto> <e',Es'>"
+ shows "(Es\<down>)<e> \<longrightarrow>cbv* (Es'\<down>)<e'>"
+using a
+by (induct) (auto simp add: ctx_compose[symmetric])
+
+lemma machine_execution_implies_cbv_reds:
+ assumes a: "<e,[]> \<mapsto> <e',[]>"
+ shows "e \<longrightarrow>cbv* e'"
+using a
+by (auto dest: machine_red_implies_cbv_reds_aux)
end