--- a/Nominal/Test.thy	Tue Mar 02 21:43:27 2010 +0100
+++ b/Nominal/Test.thy	Wed Mar 03 11:50:25 2010 +0100
@@ -13,18 +13,11 @@
 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)"
+abbreviation "fv_weird \<equiv> fv_weird_raw"
+abbreviation "alpha_weird \<equiv> alpha_weird_raw"
 
+(*
 inductive
   alpha_weird
 where
@@ -36,38 +29,55 @@
   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.intros)
+apply(rule_tac alpha_weird_raw.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(rule conjI)
 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 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)
-apply(rule alpha_weird.intros)
+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(simp)
-apply(simp add: alpha_gen)
-using a
+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)
-*)
+done
+
+
 
 text {* example 1 *}