--- a/Nominal/Abs.thy	Wed Mar 10 12:48:55 2010 +0100
+++ b/Nominal/Abs.thy	Wed Mar 10 16:50:42 2010 +0100
@@ -347,7 +347,15 @@
 notation 
   alpha1 ("_ \<approx>abs1 _")
 
-thm swap_set_not_in
+fun
+  alpha2
+where
+  "alpha2 (a, x) (b, y) \<longleftrightarrow> (\<exists>c. c \<sharp> (a,b,x,y) \<and> ((c \<rightleftharpoons> a) \<bullet> x) = ((c \<rightleftharpoons> b) \<bullet> y))"
+
+notation 
+  alpha2 ("_ \<approx>abs2 _")
+
+
 
 lemma qq:
   fixes S::"atom set"
@@ -366,23 +374,6 @@
 apply(metis permute_minus_cancel)
 done
 
-lemma alpha_abs_swap:
-  assumes a1: "(supp x - bs) \<sharp>* p"
-  and     a2: "(supp x - bs) \<sharp>* p"
-  shows "(bs, x) \<approx>abs (p \<bullet> bs, p \<bullet> x)"
-  apply(simp)
-  apply(rule_tac x="p" in exI)
-  apply(simp add: alpha_gen)
-  apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric])
-  apply(rule conjI)
-  apply(rule sym)
-  apply(rule qq)
-  using a1 a2
-  apply(auto)[1]
-  oops
-
-
-
 lemma
   assumes a: "(a, x) \<approx>abs1 (b, y)" "sort_of a = sort_of b"
   shows "({a}, x) \<approx>abs ({b}, y)"
@@ -551,37 +542,11 @@
 apply(drule perm_zero)
 apply(simp add: zero)
 apply(rotate_tac 3)
-sorry
-
-
-(*
+oops
 lemma tt:
   "(supp x) \<sharp>* p \<Longrightarrow> p \<bullet> x = x"
-apply(induct p rule: perm_induct_test)
-apply(simp)
-apply(rule swap_fresh_fresh)
-apply(case_tac "a \<in> supp x")
-apply(simp add: fresh_star_def)
-apply(drule_tac x="a" in bspec)
-apply(simp)
-apply(simp add: fresh_def)
-apply(simp add: supp_swap)
-apply(simp add: fresh_def)
-apply(case_tac "b \<in> supp x")
-apply(simp add: fresh_star_def)
-apply(drule_tac x="b" in bspec)
-apply(simp)
-apply(simp add: fresh_def)
-apply(simp add: supp_swap)
-apply(simp add: fresh_def)
-apply(simp)
-apply(drule meta_mp)
-apply(simp add: fresh_star_def fresh_def)
-apply(drule meta_mp)
-apply(simp add: fresh_star_def fresh_def)
-apply(simp)
-done
-*)
+oops
+
 lemma yy:
   assumes "S1 - {x} = S2 - {x}" "x \<in> S1" "x \<in> S2"
   shows "S1 = S2"
@@ -589,6 +554,54 @@
 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 fresh_star_eqvt:
+  shows "(p \<bullet> (as \<sharp>* x)) = (p \<bullet> as) \<sharp>* (p \<bullet> x)"
+apply(simp add: permute_bool_def)
+apply(auto simp add: fresh_star_def)
+apply(drule_tac x="(- p) \<bullet> xa" in bspec)
+apply(rule_tac p="p" in permute_boolI)
+apply(simp add: mem_eqvt)
+apply(rule_tac p="- p" in permute_boolI)
+apply(simp add: fresh_eqvt)
+apply(drule_tac x="p \<bullet> xa" in bspec)
+apply(rule_tac p="- p" in permute_boolI)
+apply(simp add: mem_eqvt)
+apply(rule_tac p="p" in permute_boolI)
+apply(simp add: fresh_eqvt)
+done
+
+lemma kk:
+  assumes a: "p \<bullet> x = y"
+  shows "\<forall>a \<in> supp x. (p \<bullet> a) \<in> supp y"
+using a
+apply(auto)
+apply(rule_tac p="- p" in permute_boolI)
+apply(simp add: mem_eqvt supp_eqvt)
+done
+
+lemma ww:
+  assumes "a \<notin> supp x" "b \<in> supp x" "a \<noteq> b"
+  shows "((a \<rightleftharpoons> b) \<bullet> x) \<noteq> x"
+apply(subgoal_tac "(supp x) supports x")
+apply(simp add: supports_def)
+using assms
+apply -
+apply(drule_tac x="a" in spec)
+apply(simp)
+sorry
+
 
 lemma
   assumes a: "({a}, x) \<approx>abs ({b}, y)" "sort_of a = sort_of b"
@@ -596,6 +609,91 @@
 using a
 apply(case_tac "a = b")
 apply(simp)
+apply(erule exE)
+apply(simp add: alpha_gen)
+apply(erule conjE)+
+apply(case_tac "b \<notin> supp x \<and> b \<notin> supp y")
+apply(simp)
+apply(drule tt1)
+apply(clarify)
+apply(simp)
+apply(simp)
+apply(erule disjE)
+apply(case_tac "b \<in> supp y")
+apply(drule_tac yy)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(case_tac "b \<sharp> p")
+apply(subgoal_tac "supp y \<sharp>* p")
+apply(drule tt1)
+apply(clarify)
+apply(drule sym)
+apply(drule sym)
+apply(simp)
+apply(auto simp add: fresh_star_def)[1]
+apply(frule_tac kk)
+apply(drule_tac x="b" in bspec)
+apply(simp)
+apply(simp add: fresh_def)
+apply(simp add: supp_perm)
+apply(subgoal_tac "((p \<bullet> b) \<sharp> p)")
+apply(simp add: fresh_def supp_perm)
+apply(simp add: fresh_star_def)
+apply(simp)
+apply(drule tt1)
+apply(clarify)
+apply(drule sym)
+apply(drule sym)
+apply(simp)
+apply(case_tac "b \<in> supp x")
+apply(drule_tac yy)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(case_tac "b \<sharp> p")
+apply(subgoal_tac "supp y \<sharp>* p")
+apply(drule tt1)
+apply(clarify)
+apply(drule sym)
+apply(drule sym)
+apply(simp)
+apply(auto simp add: fresh_star_def)[1]
+apply(frule_tac kk)
+apply(drule_tac x="b" in bspec)
+apply(simp)
+apply(simp add: fresh_def)
+apply(simp add: supp_perm)
+apply(subgoal_tac "((p \<bullet> b) \<sharp> p)")
+apply(simp add: fresh_def supp_perm)
+apply(simp add: fresh_star_def)
+apply(simp)
+apply(drule sym)
+apply(drule sym)
+apply(subgoal_tac "supp x \<sharp>* p")
+apply(drule tt1)
+apply(clarify)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(erule exE)
+apply(simp add: alpha_gen)
+apply(erule conjE)+
+apply(simp add: fresh_def)
+apply(rule conjI)
+defer
+apply(clarify)
+apply(subgoal_tac "a=b")
+prefer 2
+apply(blast)
+apply(simp)
+apply(clarify)
+apply(subgoal_tac "b \<notin> supp x")
+prefer 2
+apply(blast)
+apply(subgoal_tac "a \<notin> supp (p \<bullet> x)")
+prefer 2
+apply(blast)
 oops