diff -r cdbef6152dcc -r 6704045112a8 src/HOL/Nominal/Examples/Contexts.thy
--- 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