--- a/Nominal/Test.thy	Wed Mar 17 06:49:33 2010 +0100
+++ b/Nominal/Test.thy	Wed Mar 17 08:07:25 2010 +0100
@@ -74,19 +74,6 @@
 apply(simp only: eqvts)
 apply(simp only: supp_Abs)
 (* LET case *)
-defer
-(* BP case *)
-apply(simp only: supp_def)
-apply(simp only: lam_bp_perm)
-apply(simp only: lam_bp_inject)
-apply(simp only: de_Morgan_conj)
-apply(simp only: Collect_disj_eq)
-apply(simp only: infinite_Un)
-apply(simp only: Collect_disj_eq)
-apply(simp only: supp_def[symmetric])
-apply(simp only: supp_at_base)
-apply(simp)
-(* LET case *)
 apply(rule_tac t="supp (LET bp_raw lam_raw)" and s="supp (Abs (bi bp_raw) lam_raw) \<union> fv_bi bp_raw" in subst)
 apply(simp (no_asm) only: supp_def)
 apply(simp only: lam_bp_perm)
@@ -105,6 +92,17 @@
 apply(blast)
 apply(simp add: supp_Abs)
 apply(blast)
+(* BP case *)
+apply(simp only: supp_def)
+apply(simp only: lam_bp_perm)
+apply(simp only: lam_bp_inject)
+apply(simp only: de_Morgan_conj)
+apply(simp only: Collect_disj_eq)
+apply(simp only: infinite_Un)
+apply(simp only: Collect_disj_eq)
+apply(simp only: supp_def[symmetric])
+apply(simp only: supp_at_base)
+apply(simp)
 done
 
 thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]]
@@ -498,17 +496,17 @@
   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
+| 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"
+  bp'' :: "pat3 \<Rightarrow> atom set"
 where
-  "bp' (PVar x) = {atom x}"
-| "bp' (PUnit) = {}"
-| "bp' (PPair p1 p2) = bp' p1 \<union> bp' p2"
+  "bp'' (PVar x) = {atom x}"
+| "bp'' (PUnit) = {}"
+| "bp'' (PPair p1 p2) = bp'' p1 \<union> bp'' p2"
 
 thm exp_pat3_fv
 thm exp_pat3_inject
@@ -543,16 +541,17 @@
 (* THE REST ARE NOT SUPPOSED TO WORK YET *)
 
 (* 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
+  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
+  Assign' name exp7
 and lrbs =
-  Single lrb
-| More lrb lrbs
+  Single' lrb
+| More' lrb lrbs
 binder
   b7 :: "lrb \<Rightarrow> atom set" and
   b7s :: "lrbs \<Rightarrow> atom set"
@@ -561,27 +560,31 @@
 | "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
+  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
+  K' x::name p::pat8 e::exp8 bind "b_pat p" in e
 and fnclauses =
-  S fnclause
-| ORs fnclause fnclauses
+  S' fnclause
+| ORs' fnclause fnclauses
 and lrb8 =
-  Clause fnclauses
+  Clause' fnclauses
 and lrbs8 =
-  Single lrb8
-| More lrb8 lrbs8
+  Single' lrb8
+| More' lrb8 lrbs8
 and pat8 =
-  PVar name
-| PUnit
-| PPair pat8 pat8
+  PVar'' name
+| PUnit''
+| PPair'' pat8 pat8
 binder
   b_lrbs8 :: "lrbs8 \<Rightarrow> atom set" and
   b_pat :: "pat8 \<Rightarrow> atom set" and
@@ -589,20 +592,21 @@
   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}"
+  "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... *)
+(* lists-datastructure does not work yet
 nominal_datatype trm4 =
   Vr4 "name"
 | Ap4 "trm4" "trm4 list"
@@ -610,12 +614,13 @@
 
 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"
@@ -643,13 +648,6 @@
 | CLeftc "co"
 | CCoe "co" "co"
 
-
-typedecl ty --"hack since ty is not yet defined"
-typedecl kind
-
-instance ty and kind:: pt
-sorry
-
 abbreviation
   "atoms A \<equiv> atom ` A"
 
@@ -671,15 +669,8 @@
  bv :: "pat \<Rightarrow> atom set"
 where
  "bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))"
-
-(*
-compat (K s ts vs) pi (K s' ts' vs') ==
-  s = s' &
-
 *)
 
-
-
 text {* weirdo example from Peter Sewell's bestiary *}
 
 nominal_datatype weird =
@@ -695,6 +686,7 @@
 (* example 6 from Terms.thy *)
 
 (* BV is not respectful, needs to fail*)
+(*
 nominal_datatype trm6 =
   Vr6 "name"
 | Lm6 x::"name" t::"trm6"         bind x in t
@@ -705,9 +697,11 @@
   "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 *)
+*)
 
+(* example 7 from Terms.thy *)
 (* BV is not respectful, needs to fail*)
+(*
 nominal_datatype trm7 =
   Vr7 "name"
 | Lm7 l::"name" r::"trm7"   bind l in r
@@ -718,10 +712,12 @@
   "bv7 (Vr7 n) = {atom n}"
 | "bv7 (Lm7 n t) = bv7 t - {atom n}"
 | "bv7 (Lt7 l r) = bv7 l \<union> bv7 r"
+*)
 
 (* example 8 from Terms.thy *)
 
 (* Binding in a term under a bn, needs to fail *)
+(*
 nominal_datatype foo8 =
   Foo0 "name"
 | Foo1 b::"bar8" f::"foo8" bind "bv8 b" in f --"check fo error if this is called foo"
@@ -733,10 +729,11 @@
 where
   "bv8 (Bar0 x) = {}"
 | "bv8 (Bar1 v x b) = {atom v}"
-
+*)
 (* example 9 from Terms.thy *)
 
 (* BV is not respectful, needs to fail*)
+(*
 nominal_datatype lam9 =
   Var9 "name"
 | Lam9 n::"name" l::"lam9" bind n in l
@@ -747,18 +744,20 @@
 where
   "bv9 (Var9 x) = {}"
 | "bv9 (Lam9 x b) = {atom x}"
-
+*)
 
 (* Type schemes with separate datatypes *)
-nominal_datatype t =
-  Var "name"
-| Fun "t" "t"
+nominal_datatype T =
+  TVar "name"
+| TFun "T" "T"
 
-nominal_datatype tyS =
-  All xs::"name list" ty::"t_raw" bind xs in ty
-
-
-
+(* PROBLEM: 
+*** exception Datatype raised 
+*** (line 218 of "/usr/local/src/Isabelle_16-Mar-2010/src/HOL/Tools/Datatype/datatype_aux.ML")
+*** At command "nominal_datatype".
+nominal_datatype TyS =
+  TAll xs::"name list" ty::"T" bind xs in ty
+*)
 
 (* example 9 from Peter Sewell's bestiary *)
 (* run out of steam at the moment *)