diff -r 87dbeba4b25a -r ea327a4c4f43 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Mon Jul 01 09:56:58 2013 +0100
+++ b/Nominal/Nominal2_Base.thy	Wed Jul 31 13:15:29 2013 +0100
@@ -1513,6 +1513,10 @@
   shows "supp (a \<rightleftharpoons> b) = (if a = b \<or> sort_of a \<noteq> sort_of b then {} else {a, b})"
   by (auto simp add: supp_perm swap_atom)
 
+lemma fresh_swap:
+  shows "a \<sharp> (b \<rightleftharpoons> c) \<longleftrightarrow> (sort_of b \<noteq> sort_of c) \<or> b = c \<or> (a \<sharp> b \<and> a \<sharp> c)"
+  by (simp add: fresh_def supp_swap supp_atom)
+
 lemma fresh_zero_perm: 
   shows "a \<sharp> (0::perm)"
   unfolding fresh_perm by simp
@@ -2067,6 +2071,14 @@
   using fin1 fin2
   by (simp add: supp_of_finite_sets)
 
+lemma fresh_finite_union:
+  fixes S T::"('a::fs) set"
+  assumes fin1: "finite S"
+  and     fin2: "finite T"
+  shows "a \<sharp> (S \<union> T) \<longleftrightarrow> a \<sharp> S \<and> a \<sharp> T"
+  unfolding fresh_def
+  by (simp add: supp_of_finite_union[OF fin1 fin2])
+
 lemma supp_of_finite_insert:
   fixes S::"('a::fs) set"
   assumes fin:  "finite S"
@@ -2583,9 +2595,6 @@
   qed
 qed
 
-
-
-
 lemma supp_perm_perm_eq:
   assumes a: "\<forall>a \<in> supp x. p \<bullet> a = q \<bullet> a"
   shows "p \<bullet> x = q \<bullet> x"
@@ -3055,6 +3064,10 @@
   unfolding atom_eqvt[symmetric]
   by (simp only: fresh_permute_iff)
 
+lemma fresh_at_base_permI: 
+  shows "atom a \<sharp> p \<Longrightarrow> p \<bullet> a = a"
+by (simp add: fresh_def supp_perm)
+
 
 section {* Infrastructure for concrete atom types *}