--- a/Nominal/Test.thy	Wed Mar 03 12:45:55 2010 +0100
+++ b/Nominal/Test.thy	Wed Mar 03 12:47:06 2010 +0100
@@ -13,11 +13,53 @@
 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. *)
 
-abbreviation "fv_weird \<equiv> fv_weird_raw"
-abbreviation "alpha_weird \<equiv> alpha_weird_raw"
+lemma "alpha_weird_raw a b \<Longrightarrow> alpha_weird_raw (p \<bullet> a) (p \<bullet> b)"
+apply (erule alpha_weird_raw.induct)
+defer
+apply (simp add: alpha_weird_raw.intros)
+apply (simp add: alpha_weird_raw.intros)
+apply (simp only: permute_weird_raw.simps)
+apply (rule alpha_weird_raw.intros)
+apply (erule exi[of _ _ "p"])
+apply (erule exi[of _ _ "p"])
+apply (erule exi[of _ _ "p"])
+apply (erule exi[of _ _ "p"])
+apply (erule conjE)+
+apply (rule conjI)
+apply (erule alpha_gen_compose_eqvt[of _ _ _ _ "p"])
+apply (simp add: eqvts)
+apply (simp add: eqvts)
+apply (rule conjI)
+defer
+apply (erule alpha_gen_compose_eqvt[of _ _ _ _ "p"])
+apply (simp add: eqvts)
+apply (simp add: eqvts)
+apply (rule conjI)
+defer
+apply (simp add: supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt)
+apply(simp add: alpha_gen.simps)
+apply(erule conjE)+
+  apply(rule conjI)
+  apply(rule_tac ?p1="- p" in permute_eq_iff[THEN iffD1])
+apply (simp add: eqvts)
+  apply(rule conjI)
+  apply(rule_tac ?p1="- p" in fresh_star_permute_iff[THEN iffD1])
+apply (simp add: eqvts add_perm_eqvt)
+apply (simp add: permute_eqvt[symmetric])
+done
 
-(*
+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
@@ -29,55 +71,38 @@
   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" 
+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_raw.intros)
+apply(rule_tac alpha_weird.intros)
 unfolding alpha_gen
 using a
 apply(simp)
 apply(rule_tac x="(x \<leftrightarrow> y)" in exI)
-apply(rule conjI)
-apply(simp add: flip_def)
+apply(rule_tac x="(x \<leftrightarrow> y)" in exI)
 apply(simp add: fresh_star_def)
-defer
-apply(rule conjI)
-apply(simp)
-apply(rule alpha_weird_raw.intros)
-apply(simp add: alpha_weird_raw.intros(2))
-apply(simp add: fresh_star_def)
-apply(rule conjI)
-apply(rule_tac x="(x \<leftrightarrow> y)" in exI)
-apply(rule_tac x="0" in exI)
+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_raw.intros)
-apply(simp add: alpha_weird_raw.intros(2))
-apply(rule conjI)
-apply(auto)[1]
-apply(rule_tac x="(x \<leftrightarrow> y)" in exI)
-apply(rule conjI)
-apply(simp add: flip_def)
-apply(auto)[1]
-defer
+apply(rule alpha_weird.intros)
 apply(simp)
-apply(rule alpha_weird_raw.intros)
-apply(simp add: alpha_weird_raw.intros(2))
-apply(simp add: fresh_perm)
-defer
-apply(simp add: fresh_perm)
-apply(simp add: atom_eqvt)
-unfolding flip_def[symmetric]
+apply(simp add: alpha_gen)
+using a
 apply(simp)
-done
-
-
+*)
 
 text {* example 1 *}
 
@@ -219,14 +244,15 @@
 
 (* example 4 from Terms.thy *)
 
-(* fv_eqvt does not work, we need to repaire defined permute functions...
-nominal_datatype trm4 =
+(* fv_eqvt does not work, we need to repaire defined permute functions
+   defined fv and defined alpha... *)
+(*nominal_datatype trm4 =
   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]
+thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]*)
 
 (* example 5 from Terms.thy *)