diff -r 1803104d76c9 -r 0d7a1703fe28 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Fri Dec 17 01:01:44 2010 +0000
+++ b/Nominal/Nominal2_Base.thy	Sun Dec 19 07:43:32 2010 +0000
@@ -1070,6 +1070,33 @@
   qed
 qed
 
+lemma supp_plus_perm_eq:
+  fixes p q::perm
+  assumes asm: "supp p \<inter> supp q = {}"
+  shows "supp (p + q) = supp p \<union> supp q"
+proof -
+  { fix a::"atom"
+    assume "a \<in> supp p"
+    then have "a \<notin> supp q" using asm by auto
+    then have "a \<in> supp (p + q)" using `a \<in> supp p` 
+      by (simp add: supp_perm)
+  }
+  moreover
+  { fix a::"atom"
+    assume "a \<in> supp q"
+    then have "a \<notin> supp p" using asm by auto
+    then have "a \<in> supp (q + p)" using `a \<in> supp q` 
+      by (simp add: supp_perm)
+    then have "a \<in> supp (p + q)" using asm plus_perm_eq
+      by metis
+  }
+  ultimately have "supp p \<union> supp q \<subseteq> supp (p + q)"
+    by blast
+  then show "supp (p + q) = supp p \<union> supp q" using supp_plus_perm
+    by blast
+qed
+
+
 section {* Finite Support instances for other types *}
 
 
@@ -1606,7 +1633,7 @@
   and   As::"atom set"
   assumes b: "Xs \<subseteq> As"
   and     c: "finite As"
-  shows "\<exists>p. (p \<bullet> Xs) \<inter> As = {} \<and> (supp p) \<subseteq> (Xs \<union> (p \<bullet> Xs))"
+  shows "\<exists>p. (p \<bullet> Xs) \<inter> As = {} \<and> (supp p) = (Xs \<union> (p \<bullet> Xs))"
 proof -
   from b c have "finite Xs" by (rule finite_subset)
   then show ?thesis using b
@@ -1614,23 +1641,25 @@
     case empty
     have "0 \<bullet> {} \<inter> As = {}" by simp
     moreover
-    have "supp (0::perm) \<subseteq> {} \<union> 0 \<bullet> {}" by (simp add: supp_zero_perm)
+    have "supp (0::perm) = {} \<union> 0 \<bullet> {}" by (simp add: supp_zero_perm)
     ultimately show ?case by blast
   next
     case (insert x Xs)
     then obtain p where
       p1: "(p \<bullet> Xs) \<inter> As = {}" and 
-      p2: "supp p \<subseteq> (Xs \<union> (p \<bullet> Xs))" by blast
+      p2: "supp p = (Xs \<union> (p \<bullet> Xs))" by blast
     from `x \<in> As` p1 have "x \<notin> p \<bullet> Xs" by fast
     with `x \<notin> Xs` p2 have "x \<notin> supp p" by fast
     hence px: "p \<bullet> x = x" unfolding supp_perm by simp
-    have "finite (As \<union> p \<bullet> Xs)"
+    have "finite (As \<union> p \<bullet> Xs \<union> supp p)"
       using `finite As` `finite Xs`
-      by (simp add: permute_set_eq_image)
-    then obtain y where "y \<notin> (As \<union> p \<bullet> Xs)" "sort_of y = sort_of x"
+      by (simp add: permute_set_eq_image finite_supp)
+    then obtain y where "y \<notin> (As \<union> p \<bullet> Xs \<union> supp p)" "sort_of y = sort_of x"
       by (rule obtain_atom)
-    hence y: "y \<notin> As" "y \<notin> p \<bullet> Xs" "sort_of y = sort_of x"
+    hence y: "y \<notin> As" "y \<notin> p \<bullet> Xs" "y \<notin> supp p" "sort_of y = sort_of x"
       by simp_all
+    hence py: "p \<bullet> y = y" "x \<noteq> y" using `x \<in> As`
+      by (auto simp add: supp_perm)
     let ?q = "(x \<rightleftharpoons> y) + p"
     have q: "?q \<bullet> insert x Xs = insert y (p \<bullet> Xs)"
       unfolding insert_eqvt
@@ -1641,10 +1670,13 @@
       using `y \<notin> As` `p \<bullet> Xs \<inter> As = {}`
       unfolding q by simp
     moreover
-    have "supp ?q \<subseteq> insert x Xs \<union> ?q \<bullet> insert x Xs"
-      using p2 unfolding q
-      by (intro subset_trans [OF supp_plus_perm])
-         (auto simp add: supp_swap)
+    have "supp (x \<rightleftharpoons> y) \<inter> supp p = {}" using px py `sort_of y = sort_of x`
+      unfolding supp_swap by (simp add: supp_perm)
+    then have "supp ?q = (supp (x \<rightleftharpoons> y) \<union> supp p)" 
+      by (simp add: supp_plus_perm_eq)
+    then have "supp ?q = insert x Xs \<union> ?q \<bullet> insert x Xs"
+      using p2 `sort_of y = sort_of x` `x \<noteq> y` unfolding q supp_swap
+      by auto
     ultimately show ?case by blast
   qed
 qed
@@ -1652,7 +1684,7 @@
 lemma at_set_avoiding:
   assumes a: "finite Xs"
   and     b: "finite (supp c)"
-  obtains p::"perm" where "(p \<bullet> Xs)\<sharp>*c" and "(supp p) \<subseteq> (Xs \<union> (p \<bullet> Xs))"
+  obtains p::"perm" where "(p \<bullet> Xs)\<sharp>*c" and "(supp p) = (Xs \<union> (p \<bullet> Xs))"
   using a b at_set_avoiding_aux [where Xs="Xs" and As="Xs \<union> supp c"]
   unfolding fresh_star_def fresh_def by blast
 
@@ -1683,7 +1715,7 @@
   assumes "finite xs"
   and     "finite (supp c)" "finite (supp x)"
   and     "xs \<sharp>* x"
-  shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp x \<sharp>* p \<and> supp p \<subseteq> xs \<union> (p \<bullet> xs)"
+  shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp x \<sharp>* p \<and> supp p = xs \<union> (p \<bullet> xs)"
 using assms
 apply(erule_tac c="(c, x)" in at_set_avoiding)
 apply(simp add: supp_Pair)
@@ -1693,7 +1725,6 @@
 apply(auto simp add: fresh_star_def)
 done
 
-
 lemma at_set_avoiding2_atom:
   assumes "finite (supp c)" "finite (supp x)"
   and     b: "a \<sharp> x"
@@ -1709,6 +1740,7 @@
   then show "\<exists>p. (p \<bullet> a) \<sharp> c \<and> supp x \<sharp>* p" by blast
 qed
 
+
 section {* Renaming permutations *}
 
 lemma set_renaming_perm: