--- a/Nominal/Abs.thy	Tue Mar 16 20:07:13 2010 +0100
+++ b/Nominal/Abs.thy	Wed Mar 17 06:49:33 2010 +0100
@@ -2,11 +2,27 @@
 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "../Quotient_Product"
 begin
 
+lemma permute_boolI:
+  fixes P::"bool"
+  shows "p \<bullet> P \<Longrightarrow> P"
+apply(simp add: permute_bool_def)
+done
+
+lemma permute_boolE:
+  fixes P::"bool"
+  shows "P \<Longrightarrow> p \<bullet> P"
+apply(simp add: permute_bool_def)
+done
+
 fun
   alpha_gen 
 where
   alpha_gen[simp del]:
-  "alpha_gen (bs, x) R f pi (cs, y) \<longleftrightarrow> f x - bs = f y - cs \<and> (f x - bs) \<sharp>* pi \<and> R (pi \<bullet> x) y"
+  "alpha_gen (bs, x) R f pi (cs, y) \<longleftrightarrow> 
+     f x - bs = f y - cs \<and> 
+     (f x - bs) \<sharp>* pi \<and> 
+     R (pi \<bullet> x) y \<and>
+     pi \<bullet> bs = cs"
 
 notation
   alpha_gen ("_ \<approx>gen _ _ _ _" [100, 100, 100, 100, 100] 100)
@@ -23,7 +39,11 @@
   assumes a: "(bs, x) \<approx>gen R f p (cs, y)"
   and     b: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x"
   shows "(cs, y) \<approx>gen R f (- p) (bs, x)"
-  using a b by (simp add: alpha_gen fresh_star_def fresh_def supp_minus_perm)
+  using a b 
+  apply (simp add: alpha_gen fresh_star_def fresh_def supp_minus_perm)
+  apply(clarify)
+  apply(simp)
+  done
 
 lemma alpha_gen_trans:
   assumes a: "(bs, x) \<approx>gen R f p1 (cs, y)"
@@ -60,6 +80,8 @@
   apply(simp add: fresh_star_def fresh_minus_perm)
   apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))")
   apply simp
+  apply(clarify)
+  apply(simp)
   apply(rule a)
   apply assumption
   done
@@ -76,10 +98,10 @@
   apply(simp add: fresh_star_plus)
   apply(drule_tac x="- pia \<bullet> sa" in spec)
   apply(drule mp)
-  apply(rotate_tac 4)
+  apply(rotate_tac 5)
   apply(drule_tac pi="- pia" in a)
   apply(simp)
-  apply(rotate_tac 6)
+  apply(rotate_tac 7)
   apply(drule_tac pi="pia" in a)
   apply(simp)
   done
@@ -102,7 +124,7 @@
   apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric])
   apply(subst permute_eqvt[symmetric])
   apply(simp)
-  done
+  sorry
 
 fun
   alpha_abs 
@@ -112,6 +134,8 @@
 notation
   alpha_abs ("_ \<approx>abs _")
 
+
+
 lemma alpha_abs_swap:
   assumes a1: "a \<notin> (supp x) - bs"
   and     a2: "b \<notin> (supp x) - bs"
@@ -346,23 +370,6 @@
 notation 
   alpha2 ("_ \<approx>abs2 _")
 
-lemma qq:
-  fixes S::"atom set"
-  assumes a: "supp p \<inter> S = {}"
-  shows "p \<bullet> S = S"
-using a
-apply(simp add: supp_perm permute_set_eq)
-apply(auto)
-apply(simp only: disjoint_iff_not_equal)
-apply(simp)
-apply (metis permute_atom_def_raw)
-apply(rule_tac x="(- p) \<bullet> x" in exI)
-apply(simp)
-apply(simp only: disjoint_iff_not_equal)
-apply(simp)
-apply(metis permute_minus_cancel)
-done
-
 lemma alpha_old_new:
   assumes a: "(a, x) \<approx>abs1 (b, y)" "sort_of a = sort_of b"
   shows "({a}, x) \<approx>abs ({b}, y)"
@@ -385,6 +392,7 @@
 apply(simp)
 apply(simp)
 apply(simp add: permute_set_eq)
+apply(rule conjI)
 apply(rule_tac ?p1="(a \<rightleftharpoons> b)" in fresh_star_permute_iff[THEN iffD1])
 apply(simp add: permute_self)
 apply(simp add: Diff_eqvt supp_eqvt)
@@ -393,6 +401,7 @@
 apply(simp add: fresh_star_def fresh_def)
 apply(blast)
 apply(simp add: supp_swap)
+apply(simp add: eqvts)
 done
 
 lemma perm_zero:
@@ -532,9 +541,42 @@
 apply(simp add: zero)
 apply(rotate_tac 3)
 oops
-lemma tt:
-  "(supp x) \<sharp>* p \<Longrightarrow> p \<bullet> x = x"
-oops
+
+lemma ii:
+  assumes "\<forall>x \<in> A. p \<bullet> x = x"
+  shows "p \<bullet> A = A"
+using assms
+apply(auto)
+apply (metis Collect_def Collect_mem_eq Int_absorb assms eqvt_bound inf_Int_eq mem_def mem_permute_iff)
+apply (metis Collect_def Collect_mem_eq Int_absorb assms eqvt_apply eqvt_bound eqvt_lambda inf_Int_eq mem_def mem_permute_iff permute_minus_cancel(2) permute_pure)
+done
+
+
+
+lemma alpha_abs_Pair:
+  shows "(bs, (x1, x2)) \<approx>gen (\<lambda>(x1,x2) (y1,y2). x1=y1 \<and> x2=y2) (\<lambda>(x,y). supp x \<union> supp y) p (cs, (y1, y2))
+         \<longleftrightarrow> ((bs, x1) \<approx>gen (op=) supp p (cs, y1) \<and> (bs, x2) \<approx>gen (op=) supp p (cs, y2))"         
+  apply(simp add: alpha_gen)
+  apply(simp add: fresh_star_def)
+  apply(simp add: ball_Un Un_Diff)
+  apply(rule iffI)
+  apply(simp)
+  defer
+  apply(simp)
+  apply(rule conjI)
+  apply(clarify)
+  apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric])
+  apply(rule sym)
+  apply(rule ii)
+  apply(simp add: fresh_def supp_perm)
+  apply(clarify)
+  apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric])
+  apply(simp add: fresh_def supp_perm)
+  apply(rule sym)
+  apply(rule ii)
+  apply(simp)
+  done
+
 
 lemma yy:
   assumes "S1 - {x} = S2 - {x}" "x \<in> S1" "x \<in> S2"
@@ -543,18 +585,6 @@
 apply (metis insert_Diff_single insert_absorb)
 done
 
-lemma permute_boolI:
-  fixes P::"bool"
-  shows "p \<bullet> P \<Longrightarrow> P"
-apply(simp add: permute_bool_def)
-done
-
-lemma permute_boolE:
-  fixes P::"bool"
-  shows "P \<Longrightarrow> p \<bullet> P"
-apply(simp add: permute_bool_def)
-done
-
 lemma kk:
   assumes a: "p \<bullet> x = y"
   shows "\<forall>a \<in> supp x. (p \<bullet> a) \<in> supp y"