--- a/Nominal/Abs.thy	Tue Mar 02 15:05:50 2010 +0100
+++ b/Nominal/Abs.thy	Tue Mar 02 15:07:27 2010 +0100
@@ -75,12 +75,11 @@
   done
 
 lemma alpha_gen_compose_sym:
-  assumes b: "\<exists>pi. (aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)"
+  fixes pi
+  assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)"
   and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
-  shows "\<exists>pi. (ab, s) \<approx>gen R f pi (aa, t)"
+  shows "(ab, s) \<approx>gen R f (- pi) (aa, t)"
   using b apply -
-  apply(erule exE)
-  apply(rule_tac x="- pi" in exI)
   apply(simp add: alpha_gen.simps)
   apply(erule conjE)+
   apply(rule conjI)
@@ -92,16 +91,14 @@
   done
 
 lemma alpha_gen_compose_trans:
-  assumes b: "\<exists>pi\<Colon>perm. (aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)"
-  and c: "\<exists>pi\<Colon>perm. (ab, ta) \<approx>gen R f pi (ac, sa)"
+  fixes pi pia
+  assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)"
+  and c: "(ab, ta) \<approx>gen R f pia (ac, sa)"
   and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
-  shows "\<exists>pi\<Colon>perm. (aa, t) \<approx>gen R f pi (ac, sa)"
+  shows "(aa, t) \<approx>gen R f (pia + pi) (ac, sa)"
   using b c apply -
   apply(simp add: alpha_gen.simps)
   apply(erule conjE)+
-  apply(erule exE)+
-  apply(erule conjE)+
-  apply(rule_tac x="pia + pi" in exI)
   apply(simp add: fresh_star_plus)
   apply(drule_tac x="- pia \<bullet> sa" in spec)
   apply(drule mp)
@@ -114,14 +111,13 @@
   done
 
 lemma alpha_gen_compose_eqvt:
-  assumes b: "\<exists>pia. (g d, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia (g e, s)"
+  fixes  pia
+  assumes b: "(g d, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia (g e, s)"
   and     c: "\<And>y. pi \<bullet> (g y) = g (pi \<bullet> y)"
   and     a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)"
-  shows  "\<exists>pia. (g (pi \<bullet> d), pi \<bullet> t) \<approx>gen R f pia (g (pi \<bullet> e), pi \<bullet> s)"
+  shows  "(g (pi \<bullet> d), pi \<bullet> t) \<approx>gen R f (pi \<bullet> pia) (g (pi \<bullet> e), pi \<bullet> s)"
   using b
   apply -
-  apply(erule exE)
-  apply(rule_tac x="pi \<bullet> pia" in exI)
   apply(simp add: alpha_gen.simps)
   apply(erule conjE)+
   apply(rule conjI)
@@ -351,6 +347,8 @@
 notation 
   alpha1 ("_ \<approx>abs1 _")
 
+thm swap_set_not_in
+
 lemma qq:
   fixes S::"atom set"
   assumes a: "supp p \<inter> S = {}"
@@ -417,6 +415,7 @@
 apply(simp add: supp_swap)
 done
 
+(*
 thm supp_perm
 
 lemma perm_induct_test:
@@ -500,15 +499,6 @@
 apply(simp)
 oops
 
-fun
-  distinct_perms 
-where
-  "distinct_perms [] = True"
-| "distinct_perms (p # ps) = (supp p \<inter> supp ps = {} \<and> distinct_perms ps)"
-
-
-
-
-
+*)
 end