diff -r 78ed28528ca6 -r fba4995cb0f9 src/HOL/Nominal/Examples/Contexts.thy
--- a/src/HOL/Nominal/Examples/Contexts.thy	Tue Apr 29 19:55:02 2008 +0200
+++ b/src/HOL/Nominal/Examples/Contexts.thy	Fri May 02 02:16:10 2008 +0200
@@ -7,14 +7,15 @@
 text {* 
   
   We show here that the Plotkin-style of defining
-  reduction relations (based on congruence rules) is
+  beta-reduction (based on congruence rules) is
   equivalent to the Felleisen-Hieb-style representation 
-  (based on contexts), and show cbv-evaluation via a 
-  CK-machine described by Roshan James.
+  (based on contexts). We also define cbv-evaluation 
+  via a CK-machine described by Roshan James.
   
-  The interesting point is that contexts do not contain 
-  any binders. On the other hand the operation of filling 
-  a term into a context produces an alpha-equivalent term. 
+  The interesting point in this theory is that contexts 
+  do not contain any binders. On the other hand the operation 
+  of filling a term into a context produces an alpha-equivalent 
+  term. 
 
 *}
 
@@ -29,9 +30,10 @@
   | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
 
 text {* 
-  Contexts - the lambda case in contexts does not bind a name, 
-  even if we introduce the notation [_]._ for CLam.
+  Contexts - the lambda case in contexts does not bind 
+  a name, even if we introduce the notation [_]._ for CLam.
 *}
+
 nominal_datatype ctx = 
     Hole ("\<box>" 1000)  
   | CAppL "ctx" "lam"
@@ -58,22 +60,23 @@
 *}
 
 consts 
-  filling :: "ctx \<Rightarrow> lam \<Rightarrow> lam" ("_<_>" [100,100] 100)
+  filling :: "ctx \<Rightarrow> lam \<Rightarrow> lam" ("_\<lbrakk>_\<rbrakk>" [100,100] 100)
 
 nominal_primrec
-  "\<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>)" 
+  "\<box>\<lbrakk>t\<rbrakk> = t"
+  "(CAppL E t')\<lbrakk>t\<rbrakk> = App (E\<lbrakk>t\<rbrakk>) t'"
+  "(CAppR t' E)\<lbrakk>t\<rbrakk> = App t' (E\<lbrakk>t\<rbrakk>)"
+  "(CLam [x].E)\<lbrakk>t\<rbrakk> = Lam [x].(E\<lbrakk>t\<rbrakk>)" 
 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 "x\<noteq>y \<Longrightarrow> (CLam [x].\<box>) \<noteq> (CLam [y].\<box>)"
-  and   "(CLam [x].\<box>)<Var x> = (CLam [y].\<box>)<Var y>"
+  and   "(CLam [x].\<box>)\<lbrakk>Var x\<rbrakk> = (CLam [y].\<box>)\<lbrakk>Var y\<rbrakk>"
 by (auto simp add: alpha ctx.inject lam.inject calc_atm fresh_atm) 
 
 text {* The composition of two contexts. *}
@@ -89,7 +92,7 @@
 by (rule TrueI)+
   
 lemma ctx_compose:
-  shows "E1<E2<t>> = (E1 \<circ> E2)<t>"
+  shows "(E1 \<circ> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>"
 by (induct E1 rule: ctx.weak_induct) (auto)
 
 text {* Beta-reduction via contexts in the Felleisen-Hieb style. *}
@@ -97,7 +100,7 @@
 inductive
   ctx_red :: "lam\<Rightarrow>lam\<Rightarrow>bool" ("_ \<longrightarrow>x _" [80,80] 80) 
 where
-  xbeta[intro]: "E<App (Lam [x].t) t'> \<longrightarrow>x E<t[x::=t']>" 
+  xbeta[intro]: "E\<lbrakk>App (Lam [x].t) t'\<rbrakk> \<longrightarrow>x E\<lbrakk>t[x::=t']\<rbrakk>" 
 
 text {* Beta-reduction via congruence rules in the Plotkin style. *}
 
@@ -113,21 +116,20 @@
 
 lemma cong_red_in_ctx:
   assumes a: "t \<longrightarrow>o t'"
-  shows "E<t> \<longrightarrow>o E<t'>"
+  shows "E\<lbrakk>t\<rbrakk> \<longrightarrow>o E\<lbrakk>t'\<rbrakk>"
 using a
 by (induct E rule: ctx.weak_induct) (auto)
 
 lemma ctx_red_in_ctx:
   assumes a: "t \<longrightarrow>x t'"
-  shows "E<t> \<longrightarrow>x E<t'>"
-using a 
-by (induct) (auto simp add: ctx_compose)
+  shows "E\<lbrakk>t\<rbrakk> \<longrightarrow>x E\<lbrakk>t'\<rbrakk>"
+using a
+by (induct) (auto simp add: ctx_compose[symmetric])
 
 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_in_ctx)
+using a by (induct) (auto intro: cong_red_in_ctx)
 
 theorem cong_red_implies_ctx_red:
   assumes a: "t \<longrightarrow>o t'"
@@ -135,13 +137,14 @@
 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) 
+  have "\<box>\<lbrakk>App (Lam [x].t) t'\<rbrakk> \<longrightarrow>x \<box>\<lbrakk>t[x::=t']\<rbrakk>" 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 *}
+section {* We now use context in a CBV list machine. *}
+
+text {* First, a function that composes a list of contexts. *}
 
 primrec
   ctx_composes :: "ctx list \<Rightarrow> ctx" ("_\<down>" [80] 80)
@@ -150,6 +153,7 @@
   | "(E#Es)\<down> = (Es\<down>) \<circ> E"    
 
 text {* Values *}
+
 inductive
   val :: "lam\<Rightarrow>bool" 
 where
@@ -157,10 +161,11 @@
  | 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]>"
+  cbv_beta[intro]: "val v \<Longrightarrow> E\<lbrakk>App (Lam [x].e) v\<rbrakk> \<longrightarrow>cbv E\<lbrakk>e[x::=v]\<rbrakk>"
 
 text {* reflexive, transitive closure of CBV reduction *}
 inductive 
@@ -171,6 +176,7 @@
 | cbvs3[intro,trans]: "\<lbrakk>e1\<longrightarrow>cbv* e2; e2 \<longrightarrow>cbv* e3\<rbrakk> \<Longrightarrow> e1 \<longrightarrow>cbv* e3"
 
 text {* A little CK-machine, which builds up a list of evaluation contexts. *}
+
 inductive
   machine :: "lam\<Rightarrow>ctx list\<Rightarrow>lam\<Rightarrow>ctx list\<Rightarrow>bool" ("<_,_> \<mapsto> <_,_>" [60,60,60,60] 60)
 where
@@ -180,15 +186,13 @@
 
 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])
+  shows "(Es\<down>)\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* (Es'\<down>)\<lbrakk>e'\<rbrakk>"
+using a by (induct) (auto simp add: ctx_compose)
 
 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)
+using a by (auto dest: machine_red_implies_cbv_reds_aux)
 
 text {*
   One would now like to show something about the opposite