src/HOL/Nominal/Examples/Contexts.thy

--- a/src/HOL/Nominal/Examples/Contexts.thy	Mon Dec 31 19:36:29 2007 +0100
+++ b/src/HOL/Nominal/Examples/Contexts.thy	Tue Jan 01 07:28:20 2008 +0100
@@ -7,12 +7,12 @@
 text {* 
   
   We show here that the Plotkin-style of defining
-  reductions relation based on congruence rules is
+  reduction relations (based on congruence rules) is
   equivalent to the Felleisen-Hieb-style representation 
-  based on contexts. 
+  (based on contexts). 
   
-  The interesting point is that contexts do not bind 
-  anything. On the other hand the operation of replacing 
+  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. 
 
 *}
@@ -25,14 +25,17 @@
   | App "lam" "lam"
   | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
 
-text {* Contexts - the lambda case in contexts does not bind a name *}
+text {* 
+  Contexts - the lambda case in contexts does not bind a name 
+  even if we introduce the nomtation [_]._ fro CLam.
+*}
 nominal_datatype ctx = 
     Hole
   | CAppL "ctx" "lam"
   | CAppR "lam" "ctx" 
   | CLam "name" "ctx"  ("CLam [_]._" [100,100] 100) 
 
-text {* Capture-avoiding substitution and three lemmas *}
+text {* Capture-avoiding substitution and two lemmas *}
 
 consts subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]" [100,100,100] 100)
 
@@ -60,13 +63,13 @@
    (auto simp add: abs_fresh fresh_prod fresh_atm)
 
 text {* 
-  Replace is the operation that fills a term into a hole. While
+  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. 
 *}
 
 consts 
-  replace :: "ctx \<Rightarrow> lam \<Rightarrow> lam" ("_<_>" [100,100] 100)
+  filling :: "ctx \<Rightarrow> lam \<Rightarrow> lam" ("_<_>" [100,100] 100)
 
 nominal_primrec
   "Hole<t> = t"
@@ -75,12 +78,10 @@
   "(CLam [x].E)<t> = Lam [x].(E<t>)" 
 by (rule TrueI)+
 
-
 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)>"
@@ -95,7 +96,7 @@
    (auto simp add: fresh_prod abs_fresh)
 
 
-text {* Composition of two contexts *}
+text {* The composition of two contexts *}
 
 consts 
  ctx_replace :: "ctx \<Rightarrow> ctx \<Rightarrow> ctx" ("_ \<circ> _" [100,100] 100)
@@ -118,7 +119,7 @@
 by (induct E1 rule: ctx.weak_induct)
    (auto simp add: fresh_prod)
 
-text {* Beta-reduction via contexts *}
+text {* Beta-reduction via contexts in the Felleisen-Hieb style. *}
 
 inductive
   ctx_red :: "lam\<Rightarrow>lam\<Rightarrow>bool" ("_ \<longrightarrow>x _" [80,80] 80) 
@@ -130,7 +131,7 @@
 nominal_inductive ctx_red
   by (simp_all add: replace_fresh subst_fresh abs_fresh)
 
-text {* Beta-reduction via congruence rules *}
+text {* Beta-reduction via congruence rules in the Plotkin style. *}
 
 inductive
   cong_red :: "lam\<Rightarrow>lam\<Rightarrow>bool" ("_ \<longrightarrow>o _" [80,80] 80) 
@@ -145,7 +146,7 @@
 nominal_inductive cong_red
   by (simp_all add: subst_fresh abs_fresh)
 
-text {* The proof that shows both relations are equal *}
+text {* The proof that shows both relations are equal. *}
 
 lemma cong_red_ctx:
   assumes a: "t \<longrightarrow>o t'"
@@ -179,7 +180,7 @@
 apply(rule ctx_red_hole)
 apply(rule xbeta)
 apply(simp)
-apply(metis ctx_red_ctx replace.simps)+ (* found by SledgeHammer *)
+apply(metis ctx_red_ctx filling.simps)+ (* found by SledgeHammer *)
 done
 
 end