--- a/Nominal/ExLeroy.thy	Tue Mar 23 08:51:43 2010 +0100
+++ b/Nominal/ExLeroy.thy	Tue Mar 23 09:05:23 2010 +0100
@@ -1,4 +1,4 @@
-theory Test
+theory ExLeroy
 imports "Parser"
 begin
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/ExLet.thy	Tue Mar 23 09:05:23 2010 +0100
@@ -0,0 +1,35 @@
+theory ExLet
+imports "Parser"
+begin
+
+text {* example 3 or example 5 from Terms.thy *}
+
+atom_decl name
+
+ML {* val _ = recursive := false  *}
+nominal_datatype trm =
+  Vr "name"
+| Ap "trm" "trm"
+| Lm x::"name" t::"trm"  bind x in t
+| Lt a::"lts" t::"trm"   bind "bv a" in t
+and lts =
+  Nil
+| Cons "name" "trm" "lts"
+binder
+  bn
+where
+  "bn Nil = {}"
+| "bn (Cons x t l) = {atom x} \<union> (bn l)"
+
+thm trm_lts.fv
+thm trm_lts.eq_iff
+thm trm_lts.bn
+thm trm_lts.perm
+thm trm_lts.induct
+thm trm_lts.distinct
+thm trm_lts.fv[simplified trm_lts.supp]
+
+end
+
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/ExNotRsp.thy	Tue Mar 23 09:05:23 2010 +0100
@@ -0,0 +1,48 @@
+theory ExNotRsp
+imports "Parser"
+begin
+
+atom_decl name
+
+(* example 6 from Terms.thy *)
+
+nominal_datatype trm6 =
+  Vr6 "name"
+| Lm6 x::"name" t::"trm6"         bind x in t
+| Lt6 left::"trm6" right::"trm6"  bind "bv6 left" in right
+binder
+  bv6
+where
+  "bv6 (Vr6 n) = {}"
+| "bv6 (Lm6 n t) = {atom n} \<union> bv6 t"
+| "bv6 (Lt6 l r) = bv6 l \<union> bv6 r"
+
+(* example 7 from Terms.thy *)
+nominal_datatype trm7 =
+  Vr7 "name"
+| Lm7 l::"name" r::"trm7"   bind l in r
+| Lt7 l::"trm7" r::"trm7"   bind "bv7 l" in r
+binder
+  bv7
+where
+  "bv7 (Vr7 n) = {atom n}"
+| "bv7 (Lm7 n t) = bv7 t - {atom n}"
+| "bv7 (Lt7 l r) = bv7 l \<union> bv7 r"
+*)
+
+(* example 9 from Terms.thy *)
+nominal_datatype lam9 =
+  Var9 "name"
+| Lam9 n::"name" l::"lam9" bind n in l
+and bla9 =
+  Bla9 f::"lam9" s::"lam9" bind "bv9 f" in s
+binder
+  bv9
+where
+  "bv9 (Var9 x) = {}"
+| "bv9 (Lam9 x b) = {atom x}"
+
+end
+
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/ExPS3.thy	Tue Mar 23 09:05:23 2010 +0100
@@ -0,0 +1,37 @@
+theory ExPS3
+imports "Parser"
+begin
+
+(* example 3 from Peter Sewell's bestiary *)
+
+atom_decl name
+
+ML {* val _ = recursive := false  *}
+nominal_datatype exp =
+  VarP "name"
+| AppP "exp" "exp"
+| LamP x::"name" e::"exp" bind x in e
+| LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp'' p" in e1
+and pat3 =
+  PVar "name"
+| PUnit
+| PPair "pat3" "pat3"
+binder
+  bp'' :: "pat3 \<Rightarrow> atom set"
+where
+  "bp'' (PVar x) = {atom x}"
+| "bp'' (PUnit) = {}"
+| "bp'' (PPair p1 p2) = bp'' p1 \<union> bp'' p2"
+
+thm exp_pat3.fv
+thm exp_pat3.eq_iff
+thm exp_pat3.bn
+thm exp_pat3.perm
+thm exp_pat3.induct
+thm exp_pat3.distinct
+thm exp_pat3.fv[simplified exp_pat3.supp]
+
+end
+
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/ExPS6.thy	Tue Mar 23 09:05:23 2010 +0100
@@ -0,0 +1,35 @@
+theory ExPS6
+imports "Parser"
+begin
+
+(* example 6 from Peter Sewell's bestiary *)
+
+atom_decl name
+
+ML {* val _ = recursive := false  *}
+nominal_datatype exp6 =
+  EVar name
+| EPair exp6 exp6
+| ELetRec x::name p::pat6 e1::exp6 e2::exp6 bind x in e1, bind x in e2, bind "bp6 p" in e1
+and pat6 =
+  PVar' name
+| PUnit'
+| PPair' pat6 pat6
+binder
+  bp6 :: "pat6 \<Rightarrow> atom set"
+where
+  "bp6 (PVar' x) = {atom x}"
+| "bp6 (PUnit') = {}"
+| "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2"
+
+thm exp6_pat6.fv
+thm exp6_pat6.eq_iff
+thm exp6_pat6.bn
+thm exp6_pat6.perm
+thm exp6_pat6.induct
+thm exp6_pat6.distinct
+
+end
+
+
+

--- a/Nominal/NotRsp.thy	Tue Mar 23 08:51:43 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,48 +0,0 @@
-theory NotRsp
-imports "Parser" "../Attic/Prove"
-begin
-
-atom_decl name
-
-(* example 6 from Terms.thy *)
-
-nominal_datatype trm6 =
-  Vr6 "name"
-| Lm6 x::"name" t::"trm6"         bind x in t
-| Lt6 left::"trm6" right::"trm6"  bind "bv6 left" in right
-binder
-  bv6
-where
-  "bv6 (Vr6 n) = {}"
-| "bv6 (Lm6 n t) = {atom n} \<union> bv6 t"
-| "bv6 (Lt6 l r) = bv6 l \<union> bv6 r"
-
-(* example 7 from Terms.thy *)
-nominal_datatype trm7 =
-  Vr7 "name"
-| Lm7 l::"name" r::"trm7"   bind l in r
-| Lt7 l::"trm7" r::"trm7"   bind "bv7 l" in r
-binder
-  bv7
-where
-  "bv7 (Vr7 n) = {atom n}"
-| "bv7 (Lm7 n t) = bv7 t - {atom n}"
-| "bv7 (Lt7 l r) = bv7 l \<union> bv7 r"
-*)
-
-(* example 9 from Terms.thy *)
-nominal_datatype lam9 =
-  Var9 "name"
-| Lam9 n::"name" l::"lam9" bind n in l
-and bla9 =
-  Bla9 f::"lam9" s::"lam9" bind "bv9 f" in s
-binder
-  bv9
-where
-  "bv9 (Var9 x) = {}"
-| "bv9 (Lam9 x b) = {atom x}"
-
-end
-
-
-

--- a/Nominal/Test.thy	Tue Mar 23 08:51:43 2010 +0100
+++ b/Nominal/Test.thy	Tue Mar 23 09:05:23 2010 +0100
@@ -2,109 +2,13 @@
 imports "Parser"
 begin
 
+(* This file contains only the examples that are not supposed to work yet. *)
+
+
 atom_decl name
 
 ML {* val _ = recursive := false  *}
 
-text {* example 3 from Terms.thy *}
-
-nominal_datatype trm3 =
-  Vr3 "name"
-| Ap3 "trm3" "trm3"
-| Lm3 x::"name" t::"trm3"        bind x in t
-| Lt3 r::"rassigns3" t::"trm3"   bind "bv3 r" in t
-and rassigns3 =
-  ANil
-| ACons "name" "trm3" "rassigns3"
-binder
-  bv3
-where
-  "bv3 ANil = {}"
-| "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)"
-
-thm trm3_rassigns3.fv
-thm trm3_rassigns3.eq_iff
-thm trm3_rassigns3.bn
-thm trm3_rassigns3.perm
-thm trm3_rassigns3.induct
-thm trm3_rassigns3.distinct
-thm trm3_rassigns3.fv[simplified trm3_rassigns3.supp]
-
-(* example 5 from Terms.thy *)
-
-nominal_datatype trm5 =
-  Vr5 "name"
-| Ap5 "trm5" "trm5"
-| Lt5 l::"lts" t::"trm5"  bind "bv5 l" in t
-and lts =
-  Lnil
-| Lcons "name" "trm5" "lts"
-binder
-  bv5
-where
-  "bv5 Lnil = {}"
-| "bv5 (Lcons n t ltl) = {atom n} \<union> (bv5 ltl)"
-
-thm trm5_lts.fv
-thm trm5_lts.eq_iff
-thm trm5_lts.bn
-thm trm5_lts.perm
-thm trm5_lts.induct
-thm trm5_lts.distinct
-thm trm5_lts.fv[simplified trm5_lts.supp]
-
-(* example 3 from Peter Sewell's bestiary *)
-
-nominal_datatype exp =
-  VarP "name"
-| AppP "exp" "exp"
-| LamP x::"name" e::"exp" bind x in e
-| LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp'' p" in e1
-and pat3 =
-  PVar "name"
-| PUnit
-| PPair "pat3" "pat3"
-binder
-  bp'' :: "pat3 \<Rightarrow> atom set"
-where
-  "bp'' (PVar x) = {atom x}"
-| "bp'' (PUnit) = {}"
-| "bp'' (PPair p1 p2) = bp'' p1 \<union> bp'' p2"
-
-thm exp_pat3.fv
-thm exp_pat3.eq_iff
-thm exp_pat3.bn
-thm exp_pat3.perm
-thm exp_pat3.induct
-thm exp_pat3.distinct
-thm exp_pat3.fv[simplified exp_pat3.supp]
-
-(* example 6 from Peter Sewell's bestiary *)
-nominal_datatype exp6 =
-  EVar name
-| EPair exp6 exp6
-| ELetRec x::name p::pat6 e1::exp6 e2::exp6 bind x in e1, bind x in e2, bind "bp6 p" in e1
-and pat6 =
-  PVar' name
-| PUnit'
-| PPair' pat6 pat6
-binder
-  bp6 :: "pat6 \<Rightarrow> atom set"
-where
-  "bp6 (PVar' x) = {atom x}"
-| "bp6 (PUnit') = {}"
-| "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2"
-
-thm exp6_pat6.fv
-thm exp6_pat6.eq_iff
-thm exp6_pat6.bn
-thm exp6_pat6.perm
-thm exp6_pat6.induct
-thm exp6_pat6.distinct
-
-
-(* THE REST ARE NOT SUPPOSED TO WORK YET *)
-
 (* example 7 from Peter Sewell's bestiary *)
 (* dest_Const raised
 nominal_datatype exp7 =
@@ -180,61 +84,6 @@
 thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars]
 thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]
 *)
-(* core haskell *)
-atom_decl var
-atom_decl tvar
-
-(* there are types, coercion types and regular types *)
-(* list-data-structure
-nominal_datatype tkind =
-  KStar
-| KFun "tkind" "tkind"
-and ckind =
-  CKEq "ty" "ty"
-and ty =
-  TVar "tvar"
-| TC "string"
-| TApp "ty" "ty"
-| TFun "string" "ty list"
-| TAll tv::"tvar" "tkind" T::"ty"  bind tv in T
-| TEq "ty" "ty" "ty"
-and co =
-  CC "string"
-| CApp "co" "co"
-| CFun "string" "co list"
-| CAll tv::"tvar" "ckind" C::"co"  bind tv in C
-| CEq "co" "co" "co"
-| CSym "co"
-| CCir "co" "co"
-| CLeft "co"
-| CRight "co"
-| CSim "co"
-| CRightc "co"
-| CLeftc "co"
-| CCoe "co" "co"
-
-abbreviation
-  "atoms A \<equiv> atom ` A"
-
-nominal_datatype trm =
-  Var "var"
-| C "string"
-| LAM tv::"tvar" "kind" t::"trm"   bind tv in t
-| APP "trm" "ty"
-| Lam v::"var" "ty" t::"trm"       bind v in t
-| App "trm" "trm"
-| Let x::"var" "ty" "trm" t::"trm" bind x in t
-| Case "trm" "assoc list"
-| Cast "trm" "ty"                   --"ty is supposed to be a coercion type only"
-and assoc =
-  A p::"pat" t::"trm" bind "bv p" in t
-and pat =
-  K "string" "(tvar \<times> kind) list" "(var \<times> ty) list"
-binder
- bv :: "pat \<Rightarrow> atom set"
-where
- "bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))"
-*)
 
 (* example 8 from Terms.thy *)