--- a/Quot/Nominal/Abs.thy	Tue Feb 09 11:40:32 2010 +0100
+++ b/Quot/Nominal/Abs.thy	Tue Feb 09 15:20:40 2010 +0100
@@ -51,6 +51,30 @@
   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)
 
+lemma alpha_gen_trans:
+  assumes a: "(bs, x) \<approx>gen R f p1 (cs, y)"
+  and     b: "(cs, y) \<approx>gen R f p2 (ds, z)"
+  and     c: "\<lbrakk>R (p1 \<bullet> x) y; R (p2 \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((p2 + p1) \<bullet> x) z"
+  shows "(bs, x) \<approx>gen R f (p2 + p1) (ds, z)"
+  using a b c using supp_plus_perm
+  apply(simp add: alpha_gen fresh_star_def fresh_def)
+  apply(blast)
+  done
+
+lemma alpha_gen_eqvt:
+  assumes a: "(bs, x) \<approx>gen R f q (cs, y)"
+  and     b: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)"
+  and     c: "p \<bullet> (f x) = f (p \<bullet> x)"
+  and     d: "p \<bullet> (f y) = f (p \<bullet> y)"
+  shows "(p \<bullet> bs, p \<bullet> x) \<approx>gen R f (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
+  using a b
+  apply(simp add: alpha_gen c[symmetric] d[symmetric] Diff_eqvt[symmetric])
+  apply(simp add: permute_eqvt[symmetric])
+  apply(simp add: fresh_star_permute_iff)
+  apply(clarsimp)
+  done
+
+(* introduced for examples *)
 lemma alpha_gen_atom_sym:
   assumes a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
   shows "\<exists>pi. ({atom a}, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi ({atom b}, s) \<Longrightarrow>
@@ -67,16 +91,6 @@
   apply assumption
   done
 
-lemma alpha_gen_trans:
-  assumes a: "(bs, x) \<approx>gen R f p1 (cs, y)"
-  and     b: "(cs, y) \<approx>gen R f p2 (ds, z)"
-  and     c: "\<lbrakk>R (p1 \<bullet> x) y; R (p2 \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((p2 + p1) \<bullet> x) z"
-  shows "(bs, x) \<approx>gen R f (p2 + p1) (ds, z)"
-  using a b c using supp_plus_perm
-  apply(simp add: alpha_gen fresh_star_def fresh_def)
-  apply(blast)
-  done
-
 lemma alpha_gen_atom_trans:
   assumes a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
   shows "\<lbrakk>\<exists>pi\<Colon>perm. ({atom a}, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi ({atom aa}, ta);
@@ -98,19 +112,6 @@
   apply(simp)
   done
 
-lemma alpha_gen_eqvt:
-  assumes a: "(bs, x) \<approx>gen R f q (cs, y)"
-  and     b: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)"
-  and     c: "p \<bullet> (f x) = f (p \<bullet> x)"
-  and     d: "p \<bullet> (f y) = f (p \<bullet> y)"
-  shows "(p \<bullet> bs, p \<bullet> x) \<approx>gen R f (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
-  using a b
-  apply(simp add: alpha_gen c[symmetric] d[symmetric] Diff_eqvt[symmetric])
-  apply(simp add: permute_eqvt[symmetric])
-  apply(simp add: fresh_star_permute_iff)
-  apply(clarsimp)
-  done
-
 lemma alpha_gen_atom_eqvt:
   assumes a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)"
   and     b: "\<exists>pia. ({atom a}, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia ({atom b}, s)"
@@ -259,11 +260,8 @@
   shows "supp_Abs_fun (Abs bs x) = (supp x) - bs"
   by (lifting supp_abs_fun.simps(1))
 
-lemma supp_Abs_fun_eqvt:
-  shows "(p \<bullet> supp_Abs_fun) = supp_Abs_fun"
-  apply(subst permute_fun_def)
-  apply(subst expand_fun_eq)
-  apply(rule allI)
+lemma supp_Abs_fun_eqvt [eqvt]:
+  shows "(p \<bullet> supp_Abs_fun x) = supp_Abs_fun (p \<bullet> x)"
   apply(induct_tac x rule: abs_induct)
   apply(simp add: supp_Abs_fun_simp supp_eqvt Diff_eqvt)
   done
@@ -271,7 +269,7 @@
 lemma supp_Abs_fun_fresh:
   shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_Abs_fun (Abs bs x)"
   apply(rule fresh_fun_eqvt_app)
-  apply(simp add: supp_Abs_fun_eqvt)
+  apply(simp add: eqvts_raw)
   apply(simp)
   done
 
@@ -326,14 +324,14 @@
 
 lemma Abs_fresh_iff:
   fixes x::"'a::fs"
-  shows "a \<sharp> Abs bs x = (a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x))"
+  shows "a \<sharp> Abs bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
   apply(simp add: fresh_def)
   apply(simp add: supp_Abs)
   apply(auto)
   done
 
 lemma Abs_eq_iff:
-  shows "(Abs bs x) = (Abs cs y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
+  shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
   by (lifting alpha_abs.simps(1))
 
 
@@ -347,11 +345,47 @@
 fun
   alpha1
 where
-  "alpha1 (a, x) (b, y) \<longleftrightarrow> ((a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y))"
+  "alpha1 (a, x) (b, y) \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)"
 
 notation 
   alpha1 ("_ \<approx>abs1 _")
 
+thm swap_set_not_in
+
+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_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)"
@@ -384,6 +418,60 @@
 apply(simp add: supp_swap)
 done
 
+thm supp_perm
+
+lemma perm_induct_test:
+  fixes P :: "perm => bool"
+  assumes zero: "P 0"
+  assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)"
+  assumes plus: "\<And>p1 p2. \<lbrakk>supp (p1 + p2) = (supp p1 \<union> supp p2); P p1; P p2\<rbrakk> \<Longrightarrow> P (p1 + p2)"
+  shows "P p"
+sorry
+
+
+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
+
+lemma yy:
+  assumes "S1 - {x} = S2 - {x}" "x \<in> S1" "x \<in> S2"
+  shows "S1 = S2"
+using assms
+apply (metis insert_Diff_single insert_absorb)
+done
+
+
+lemma
+  assumes a: "({a}, x) \<approx>abs ({b}, y)" "sort_of a = sort_of b"
+  shows "(a, x) \<approx>abs1 (b, y)"
+using a
+apply(case_tac "a = b")
+apply(simp)
+oops
+
 
 end