--- a/Nominal/Nominal2_Base.thy	Wed Jan 19 07:06:47 2011 +0100
+++ b/Nominal/Nominal2_Base.thy	Wed Jan 19 17:11:10 2011 +0100
@@ -225,9 +225,10 @@
   by (rule Rep_perm_ext) (simp add: Rep_perm_simps)
 
 lemma swap_cancel:
-  "(a \<rightleftharpoons> b) + (a \<rightleftharpoons> b) = 0"
-  by (rule Rep_perm_ext) 
-     (simp add: Rep_perm_simps fun_eq_iff)
+  shows "(a \<rightleftharpoons> b) + (a \<rightleftharpoons> b) = 0"
+  and   "(a \<rightleftharpoons> b) + (b \<rightleftharpoons> a) = 0"
+  by (rule_tac [!] Rep_perm_ext) 
+     (simp_all add: Rep_perm_simps fun_eq_iff)
 
 lemma swap_self [simp]:
   "(a \<rightleftharpoons> a) = 0"
@@ -235,7 +236,7 @@
 
 lemma minus_swap [simp]:
   "- (a \<rightleftharpoons> b) = (a \<rightleftharpoons> b)"
-  by (rule minus_unique [OF swap_cancel])
+  by (rule minus_unique [OF swap_cancel(1)])
 
 lemma swap_commute:
   "(a \<rightleftharpoons> b) = (b \<rightleftharpoons> a)"
@@ -1396,6 +1397,14 @@
   unfolding fresh_def
   by (simp add: supp_finite_atom_set[OF assms])
 
+lemma fresh_minus_atom_set:
+  fixes S::"atom set"
+  assumes "finite S"
+  shows "a \<sharp> S - T \<longleftrightarrow> (a \<notin> T \<longrightarrow> a \<sharp> S)"
+  unfolding fresh_def
+  by (auto simp add: supp_finite_atom_set assms)
+
+
 lemma Union_fresh:
   shows "a \<sharp> S \<Longrightarrow> a \<sharp> (\<Union>x \<in> S. supp x)"
   unfolding Union_image_eq[symmetric]
@@ -1610,6 +1619,15 @@
 apply(simp add: supp_finite_atom_set fin fresh)
 done
 
+lemma fresh_star_atom_set_conv:
+  fixes p::"perm"
+  assumes fresh: "as \<sharp>* bs"
+  and     fin: "finite as" "finite bs"
+  shows "bs \<sharp>* as"
+using fresh
+unfolding fresh_star_def fresh_def
+by (auto simp add: supp_finite_atom_set fin)
+
 
 lemma fresh_star_Pair:
   shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)" 
@@ -1772,6 +1790,32 @@
 by (rule_tac S="supp p" in perm_struct_induct2)
    (auto intro: zero swap plus)
 
+lemma supp_perm_singleton:
+  fixes p::"perm"
+  shows "supp p \<subseteq> {b} \<longleftrightarrow> p = 0"
+proof -
+  { assume "supp p \<subseteq> {b}"
+    then have "p = 0"
+      by (induct p rule: perm_struct_induct) (simp_all)
+  }
+  then show "supp p \<subseteq> {b} \<longleftrightarrow> p = 0" by (auto simp add: supp_zero_perm)
+qed
+
+lemma supp_perm_pair:
+  fixes p::"perm"
+  shows "supp p \<subseteq> {a, b} \<longleftrightarrow> p = 0 \<or> p = (b \<rightleftharpoons> a)"
+proof -
+  { assume "supp p \<subseteq> {a, b}"
+    then have "p = 0 \<or> p = (b \<rightleftharpoons> a)"
+      apply (induct p rule: perm_struct_induct) 
+      apply (auto simp add: swap_cancel supp_zero_perm supp_swap)
+      apply (simp add: swap_commute)
+      done
+  }
+  then show "supp p \<subseteq> {a, b} \<longleftrightarrow> p = 0 \<or> p = (b \<rightleftharpoons> a)" 
+    by (auto simp add: supp_zero_perm supp_swap split: if_splits)
+qed
+
 lemma supp_perm_eq:
   assumes "(supp x) \<sharp>* p"
   shows "p \<bullet> x = x"