--- a/Quot/Nominal/Abs.thy	Tue Feb 02 09:51:39 2010 +0100
+++ b/Quot/Nominal/Abs.thy	Tue Feb 02 10:20:54 2010 +0100
@@ -9,6 +9,20 @@
 apply(simp add: permute_bool_def) 
 done
 
+lemma fresh_plus:
+  fixes p q::perm
+  shows "\<lbrakk>a \<sharp> p;  a \<sharp> q\<rbrakk> \<Longrightarrow> a \<sharp> (p + q)"
+  unfolding fresh_def
+  using supp_plus_perm
+  by(auto)
+
+lemma fresh_star_plus:
+  fixes p q::perm
+  shows "\<lbrakk>a \<sharp>* p;  a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)"
+  unfolding fresh_star_def
+  by (simp add: fresh_plus)
+
+
 lemma fresh_star_permute_iff:
   shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x"
 apply(simp add: fresh_star_def)
@@ -25,6 +39,12 @@
 apply(simp)
 done
 
+lemma fresh_minus_perm:
+  fixes p::perm
+  shows "a \<sharp> (- p) \<longleftrightarrow> a \<sharp> p"
+  apply(simp add: fresh_def)
+  apply(simp only: supp_minus_perm)
+  done
 
 fun
   alpha_gen 
@@ -49,6 +69,22 @@
   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_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>
+        \<exists>pi. ({atom b}, s) \<approx>gen R f pi ({atom a}, t)"
+  apply(erule exE)
+  apply(rule_tac x="- pi" in exI)
+  apply(simp add: alpha_gen.simps)
+  apply(erule conjE)+
+  apply(rule conjI)
+  apply(simp add: fresh_star_def fresh_minus_perm)
+  apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))")
+  apply simp
+  apply(rule a)
+  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)"
@@ -59,6 +95,27 @@
   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);
+        \<exists>pi\<Colon>perm. ({atom aa}, ta) \<approx>gen R f pi ({atom ba}, sa)\<rbrakk>
+    \<Longrightarrow> \<exists>pi\<Colon>perm. ({atom a}, t) \<approx>gen R f pi ({atom ba}, sa)"
+  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)
+  apply(rotate_tac 4)
+  apply(drule_tac pi="- pia" in a)
+  apply(simp)
+  apply(rotate_tac 6)
+  apply(drule_tac pi="pia" in a)
+  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)"