--- a/Nominal/ExPS6.thy	Fri Mar 26 10:35:26 2010 +0100
+++ b/Nominal/ExPS6.thy	Fri Mar 26 10:55:13 2010 +0100
@@ -6,7 +6,8 @@
 
 atom_decl name
 
-(* The binding structure is too complicated, so we cannot show equivalence *)
+(* The binding structure is too complicated, so equivalence the
+   way we define it is not true *)
 ML {* val _ = cheat_equivp := true *}
 
 ML {* val _ = recursive := false  *}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/ExPS7.thy	Fri Mar 26 10:55:13 2010 +0100
@@ -0,0 +1,33 @@
+theory ExPS7
+imports "Parser"
+begin
+
+(* example 7 from Peter Sewell's bestiary *)
+
+atom_decl name
+
+ML {* val _ = recursive := true  *}
+nominal_datatype exp7 =
+  EVar name
+| EUnit
+| EPair exp7 exp7
+| ELetRec l::"lrbs" e::"exp7" bind "b7s l" in e
+and lrb =
+  Assign name exp7
+and lrbs =
+  Single lrb
+| More lrb lrbs
+binder
+  b7 :: "lrb \<Rightarrow> atom set" and
+  b7s :: "lrbs \<Rightarrow> atom set"
+where
+  "b7 (Assign x e) = {atom x}"
+| "b7s (Single a) = b7 a"
+| "b7s (More a as) = (b7 a) \<union> (b7s as)"
+thm exp7_lrb_lrbs.eq_iff
+thm exp7_lrb_lrbs.supp
+
+end
+
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/ExPS8.thy	Fri Mar 26 10:55:13 2010 +0100
@@ -0,0 +1,56 @@
+theory ExPS8
+imports "Parser"
+begin
+
+(* example 8 from Peter Sewell's bestiary *)
+
+atom_decl name
+
+(* One function is recursive and the other one is not,
+   and as the parser cannot handle this we cannot set
+   the reference.  *)
+ML {* val _ = recursive := false  *}
+
+nominal_datatype exp8 =
+  EVar name
+| EUnit
+| EPair exp8 exp8
+| ELetRec l::lrbs8 e::exp8 bind "b_lrbs8 l" in e (* rec *)
+and fnclause =
+  K x::name p::pat8 f::exp8 bind "b_pat p" in f (* non-rec *)
+and fnclauses =
+  S fnclause
+| ORs fnclause fnclauses
+and lrb8 =
+  Clause fnclauses
+and lrbs8 =
+  Single lrb8
+| More lrb8 lrbs8
+and pat8 =
+  PVar name
+| PUnit
+| PPair pat8 pat8
+binder
+  b_lrbs8 :: "lrbs8 \<Rightarrow> atom set" and
+  b_pat :: "pat8 \<Rightarrow> atom set" and
+  b_fnclauses :: "fnclauses \<Rightarrow> atom set" and
+  b_fnclause :: "fnclause \<Rightarrow> atom set" and
+  b_lrb8 :: "lrb8 \<Rightarrow> atom set"
+where
+  "b_lrbs8 (Single l) = b_lrb8 l"
+| "b_lrbs8 (More l ls) = b_lrb8 l \<union> b_lrbs8 ls"
+| "b_pat (PVar x) = {atom x}"
+| "b_pat (PUnit) = {}"
+| "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2"
+| "b_fnclauses (S fc) = (b_fnclause fc)"
+| "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)"
+| "b_lrb8 (Clause fcs) = (b_fnclauses fcs)"
+| "b_fnclause (K x pat exp8) = {atom x}"
+
+thm exp7_lrb_lrbs.eq_iff
+thm exp7_lrb_lrbs.supp
+
+end
+
+
+

--- a/Nominal/Test.thy	Fri Mar 26 10:35:26 2010 +0100
+++ b/Nominal/Test.thy	Fri Mar 26 10:55:13 2010 +0100
@@ -8,71 +8,6 @@
 
 atom_decl name
 
-ML {* val _ = recursive := false  *}
-
-(* example 7 from Peter Sewell's bestiary *)
-(* dest_Const raised
-nominal_datatype exp7 =
-  EVar' name
-| EUnit'
-| EPair' exp7 exp7
-| ELetRec' l::lrbs e::exp7 bind "b7s l" in e, bind "b7s l" in l
-and lrb =
-  Assign' name exp7
-and lrbs =
-  Single' lrb
-| More' lrb lrbs
-binder
-  b7 :: "lrb \<Rightarrow> atom set" and
-  b7s :: "lrbs \<Rightarrow> atom set"
-where
-  "b7 (Assign x e) = {atom x}"
-| "b7s (Single a) = b7 a"
-| "b7s (More a as) = (b7 a) \<union> (b7s as)"
-thm alpha_exp7_raw_alpha_lrb_raw_alpha_lrbs_raw.intros
-*)
-
-(* example 8 from Peter Sewell's bestiary *)
-(*
-*** fv_bn: recursive argument, but wrong datatype.
-*** At command "nominal_datatype".
-nominal_datatype exp8 =
-  EVar' name
-| EUnit'
-| EPair' exp8 exp8
-| ELetRec' l::lrbs8 e::exp8 bind "b_lrbs8 l" in e, bind "b_lrbs8 l" in l
-and fnclause =
-  K' x::name p::pat8 e::exp8 bind "b_pat p" in e
-and fnclauses =
-  S' fnclause
-| ORs' fnclause fnclauses
-and lrb8 =
-  Clause' fnclauses
-and lrbs8 =
-  Single' lrb8
-| More' lrb8 lrbs8
-and pat8 =
-  PVar'' name
-| PUnit''
-| PPair'' pat8 pat8
-binder
-  b_lrbs8 :: "lrbs8 \<Rightarrow> atom set" and
-  b_pat :: "pat8 \<Rightarrow> atom set" and
-  b_fnclauses :: "fnclauses \<Rightarrow> atom set" and
-  b_fnclause :: "fnclause \<Rightarrow> atom set" and
-  b_lrb8 :: "lrb8 \<Rightarrow> atom set"
-where
-  "b_lrbs8 (Single' l) = b_lrb8 l"
-| "b_lrbs8 (More' l ls) = b_lrb8 l \<union> b_lrbs8 ls"
-| "b_pat (PVar'' x) = {atom x}"
-| "b_pat (PUnit'') = {}"
-| "b_pat (PPair'' p1 p2) = b_pat p1 \<union> b_pat p2"
-| "b_fnclauses (S' fc) = (b_fnclause fc)"
-| "b_fnclauses (ORs' fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)"
-| "b_lrb8 (Clause' fcs) = (b_fnclauses fcs)"
-| "b_fnclause (K' x pat exp8) = {atom x}"
-thm alpha_exp8_raw_alpha_fnclause_raw_alpha_fnclauses_raw_alpha_lrb8_raw_alpha_lrbs8_raw_alpha_pat8_raw.intros
-*)
 (* example 4 from Terms.thy *)
 (* fv_eqvt does not work, we need to repaire defined permute functions
    defined fv and defined alpha... *)