# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1265037827 -3600
# Node ID e63838c26f28018c2af5dc0363d1d611734dd71d
# Parent  83d5a7cd2cc682820dd9cc730778ad3c795dfa2d
updated from huffman

diff -r 83d5a7cd2cc6 -r e63838c26f28 Quot/Nominal/Nominal2_Base.thy
--- a/Quot/Nominal/Nominal2_Base.thy	Mon Feb 01 16:13:24 2010 +0100
+++ b/Quot/Nominal/Nominal2_Base.thy	Mon Feb 01 16:23:47 2010 +0100
@@ -433,6 +433,17 @@
 unfolding permute_fun_def permute_bool_def
 unfolding vimage_def Collect_def mem_def ..
 
+lemma swap_set_not_in:
+  assumes a: "a \<notin> S" "b \<notin> S"
+  shows "(a \<rightleftharpoons> b) \<bullet> S = S"
+  using a by (auto simp add: permute_set_eq swap_atom)
+
+lemma swap_set_in:
+  assumes a: "a \<in> S" "b \<notin> S" "sort_of a = sort_of b"
+  shows "(a \<rightleftharpoons> b) \<bullet> S \<noteq> S"
+  using a by (auto simp add: permute_set_eq swap_atom)
+
+
 subsection {* Permutations for units *}
 
 instantiation unit :: pt
@@ -954,8 +965,7 @@
 apply (simp_all add: supp_Nil supp_Cons finite_supp)
 done
 
-
-section {* support and freshness for applications *}
+section {* Support and freshness for applications *}
 
 lemma supp_fun_app:
   shows "supp (f x) \<subseteq> (supp f) \<union> (supp x)"
diff -r 83d5a7cd2cc6 -r e63838c26f28 Quot/Nominal/Nominal2_Supp.thy
--- a/Quot/Nominal/Nominal2_Supp.thy	Mon Feb 01 16:13:24 2010 +0100
+++ b/Quot/Nominal/Nominal2_Supp.thy	Mon Feb 01 16:23:47 2010 +0100
@@ -66,12 +66,6 @@
   which 'translates' between both sets.
 *}
 
-lemma swap_set_fresh:
-  assumes a: "a \<notin> S" "b \<notin> S"
-  shows "(a \<rightleftharpoons> b) \<bullet> S = S"
-  using a
-  by (auto simp add: permute_set_eq swap_atom)
-
 lemma at_set_avoiding_aux:
   fixes Xs::"atom set"
   and   As::"atom set"
@@ -107,7 +101,7 @@
       unfolding insert_eqvt
       using `p \<bullet> x = x` `sort_of y = sort_of x`
       using `x \<notin> p \<bullet> Xs` `y \<notin> p \<bullet> Xs`
-      by (simp add: swap_atom swap_set_fresh)
+      by (simp add: swap_atom swap_set_not_in)
     have "?q \<bullet> insert x Xs \<inter> As = {}"
       using `y \<notin> As` `p \<bullet> Xs \<inter> As = {}`
       unfolding q by simp
@@ -353,9 +347,9 @@
   shows "supp S = S"
   apply(rule finite_supp_unique)
   apply(simp add: supports_def)
-  apply(auto simp add: permute_set_eq_vimage vimage_def swap_atom)[1]
+  apply(simp add: swap_set_not_in)
   apply(rule assms)
-  apply(auto simp add: permute_set_eq swap_atom)[1]
+  apply(simp add: swap_set_in)
 done