# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1272831352 -3600
# Node ID a48a6f88f76ed733670c1eec28eb77d448e75e81
# Parent  12ce87b55f974b0b69e5b1355b37de63080a22ae
simplified the supp-of-finite-sets proof

diff -r 12ce87b55f97 -r a48a6f88f76e Nominal-General/Nominal2_Supp.thy
--- a/Nominal-General/Nominal2_Supp.thy	Sun May 02 16:02:27 2010 +0100
+++ b/Nominal-General/Nominal2_Supp.thy	Sun May 02 21:15:52 2010 +0100
@@ -22,7 +22,7 @@
 
 lemma fresh_star_prod:
   fixes as::"atom set"
-  shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)"
+  shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)" 
   by (auto simp add: fresh_star_def fresh_Pair)
 
 lemma fresh_star_union:
@@ -67,7 +67,7 @@
 lemma fresh_star_permute_iff:
   shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x"
   unfolding fresh_star_def
-  by (metis mem_permute_iff permute_minus_cancel fresh_permute_iff)
+  by (metis mem_permute_iff permute_minus_cancel(1) fresh_permute_iff)
 
 lemma fresh_star_eqvt[eqvt]:
   shows "(p \<bullet> (as \<sharp>* x)) = (p \<bullet> as) \<sharp>* (p \<bullet> x)"
@@ -166,7 +166,7 @@
     using at_set_avoiding2[of "{a}" "c" "x"] assms a by blast
   have c: "(p \<bullet> a) \<sharp> c" using p1
     unfolding fresh_star_def Ball_def 
-    by (erule_tac x="p \<bullet> a" in allE) (simp add: eqvts)
+    by(erule_tac x="p \<bullet> a" in allE) (simp add: permute_set_eq)
   hence "p \<bullet> a \<sharp> c \<and> supp x \<sharp>* p" using p2 by blast
   then show "\<exists>p. (p \<bullet> a) \<sharp> c \<and> supp x \<sharp>* p" by blast
 qed
@@ -481,23 +481,15 @@
 
 lemma Union_supports_set:
   shows "(\<Union>x \<in> S. supp x) supports S"
-  apply(simp add: supports_def fresh_def[symmetric])
-  apply(rule allI)+
-  apply(rule impI)
-  apply(erule conjE)
-  apply(simp add: permute_set_eq)
-  apply(auto)
-  apply(subgoal_tac "(a \<rightleftharpoons> b) \<bullet> xa = xa")(*A*)
-  apply(simp)
-  apply(rule swap_fresh_fresh)
-  apply(force)
-  apply(force)
-  apply(rule_tac x="x" in exI)
-  apply(simp)
-  apply(rule sym)
-  apply(rule swap_fresh_fresh)
-  apply(auto)
-  done
+proof -
+  { fix a b
+    have "\<forall>x \<in> S. (a \<rightleftharpoons> b) \<bullet> x = x \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> S = S"
+      unfolding permute_set_eq by force
+  }
+  then show "(\<Union>x \<in> S. supp x) supports S"
+    unfolding supports_def 
+    by (simp add: fresh_def[symmetric] swap_fresh_fresh)
+qed
 
 lemma Union_of_fin_supp_sets:
   fixes S::"('a::fs set)"
@@ -512,8 +504,7 @@
 proof -
   have "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)"
     apply(rule supp_finite_atom_set[symmetric])
-    apply(rule Union_of_fin_supp_sets)
-    apply(rule fin)
+    apply(rule Union_of_fin_supp_sets[OF fin])
     done
   also have "\<dots> \<subseteq> supp S"
     apply(rule supp_subset_fresh)