--- a/Nominal/Test.thy	Tue Mar 02 19:48:44 2010 +0100
+++ b/Nominal/Test.thy	Tue Mar 02 20:14:21 2010 +0100
@@ -2,6 +2,73 @@
 imports "Parser"
 begin
 
+text {* weirdo example from Peter Sewell's bestiary *}
+
+nominal_datatype weird =
+  WBind x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird"
+    bind x in p1, bind x in p2, bind y in p2, bind y in p3
+| WV "name"
+| WP "weird" "weird"
+
+thm permute_weird_raw.simps[no_vars]
+thm alpha_weird_raw.intros[no_vars]
+thm fv_weird_raw.simps[no_vars]
+(* Potential problem: Is it correct that in the fv-function 
+the first two terms are created? Should be ommitted. Also
+something wrong with the permutations. *)
+
+primrec 
+  fv_weird
+where
+  "fv_weird (WBind_raw x y p1 p2 p3) = 
+    (fv_weird p1 - {atom x}) \<union> (fv_weird p2 - ({atom x} \<union> {atom y})) \<union> (fv_weird p3 - {atom y})"
+| "fv_weird (WV_raw x) = {atom x}"
+| "fv_weird (WP_raw p1 p2) = (fv_weird p1 \<union> fv_weird p2)"
+
+inductive
+  alpha_weird
+where
+  "\<exists>p1 p2.  
+  ({atom y}, w3) \<approx>gen alpha_weird fv_weird p2 ({atom ya}, w3a) \<and>
+  ({atom x} \<union> {atom y}, w2) \<approx>gen alpha_weird fv_weird (p1 + p2) ({atom xa} \<union> {atom ya}, w2a) \<and>
+  ({atom x}, w1) \<approx>gen alpha_weird fv_weird p1 ({atom xa}, w1a) \<and>
+  supp p1 \<inter> supp p2 = {} \<Longrightarrow>
+  alpha_weird (WBind_raw x y w1 w2 w3) (WBind_raw xa ya w1a w2a w3a)"
+| "x = xa \<Longrightarrow> alpha_weird (WV_raw x) (WV_raw xa)"
+| "alpha_weird w2 w2a \<and> alpha_weird w1 w1a \<Longrightarrow> alpha_weird (WP_raw w1 w2) (WP_raw w1a w2a)"
+
+(*
+abbreviation "WBind \<equiv> WBind_raw"
+abbreviation "WP \<equiv> WP_raw"
+abbreviation "WV \<equiv> WV_raw"
+
+lemma test:
+  assumes a: "distinct [x, y, z]"
+  shows "alpha_weird (WBind x y (WP (WV x) (WV z)) (WP (WV x) (WV y)) (WP (WV z) (WV y)))  
+                     (WBind y x (WP (WV y) (WV z)) (WP (WV y) (WV x)) (WP (WV z) (WV x)))"
+apply(rule_tac alpha_weird.intros)
+unfolding alpha_gen
+using a
+apply(simp)
+apply(rule_tac x="(x \<leftrightarrow> y)" in exI)
+apply(rule_tac x="(x \<leftrightarrow> y)" in exI)
+apply(simp add: fresh_star_def)
+apply(simp add: flip_def)
+apply(auto)
+prefer 2
+apply(rule alpha_weird.intros)
+apply(simp add: alpha_weird.intros(2))
+prefer 2
+apply(rule alpha_weird.intros)
+apply(simp add: alpha_weird.intros(2))
+apply(simp)
+apply(rule alpha_weird.intros)
+apply(simp)
+apply(simp add: alpha_gen)
+using a
+apply(simp)
+*)
+
 text {* example 1 *}
 
 (* ML {* set show_hyps *} *)
@@ -24,8 +91,8 @@
 term Test.BP_raw
 thm bi_raw.simps
 thm permute_lam_raw_permute_bp_raw.simps
-thm alpha_lam_raw_alpha_bp_raw.intros
-thm fv_lam_raw_fv_bp_raw.simps
+thm alpha_lam_raw_alpha_bp_raw.intros[no_vars]
+thm fv_lam_raw_fv_bp_raw.simps[no_vars]
 thm eqvts
 
 print_theorems
@@ -48,6 +115,9 @@
 | "f (PS x) = {atom x}"
 | "f (PD x y) = {atom x, atom y}"
 
+
+thm alpha_trm'_raw_alpha_pat'_raw.intros[no_vars]
+thm fv_trm'_raw_fv_pat'_raw.simps[no_vars]
 thm f_raw.simps
 
 nominal_datatype trm0 =
@@ -144,7 +214,9 @@
   Vr4 "name"
 | Ap4 "trm4" "trm4 list"
 | Lm4 x::"name" t::"trm4"  bind x in t
-*)
+
+thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars]
+thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]
 
 (* example 5 from Terms.thy *)
 
@@ -225,7 +297,12 @@
 |  AndL1 n::"name" t::"phd" "name"                              bind n in t
 |  AndL2 n::"name" t::"phd" "name"                              bind n in t
 |  ImpL c::"coname" t1::"phd" n::"name" t2::"phd" "name"        bind c in t1, bind n in t2
-|  ImpR c::"coname" n::"name" t::"phd" "coname"                 bind n in 1, bind c in t
+|  ImpR c::"coname" n::"name" t::"phd" "coname"                 bind n in t, bind c in t
+
+(* PROBLEM?: why does it create for the Cut AndR ImpL cases
+two permutations, but only one is used *)
+thm alpha_phd_raw.intros[no_vars]
+thm fv_phd_raw.simps[no_vars]
 
 (* example form Leroy 96 about modules; OTT *)
 
@@ -340,14 +417,14 @@
 
 (* example 3 from Peter Sewell's bestiary *)
 nominal_datatype exp =
-  Var name
-| App exp exp
-| Lam x::name e::exp bind x in e
-| Let x::name p::pat e1::exp e2::exp bind x in e2, bind "bp p" in e1
+  Var "name"
+| App "exp" "exp"
+| Lam x::"name" e::"exp" bind x in e
+| Let x::"name" p::"pat" e1::"exp" e2::"exp" bind x in e2, bind "bp p" in e1
 and pat =
-  PVar name
+  PVar "name"
 | PUnit
-| PPair pat pat
+| PPair "pat" "pat"
 binder
   bp :: "pat \<Rightarrow> atom set"
 where