# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1295368247 -3600
# Node ID 87ebc706df67478085bec0b74f6a9fd4927e9806
# Parent  7e76628904773360f2f28b3ab9c3e3cf728802a8
made alpha_abs_set_stronger1 stronger

diff -r 7e7662890477 -r 87ebc706df67 Nominal/Nominal2_Abs.thy
--- a/Nominal/Nominal2_Abs.thy	Tue Jan 18 17:19:50 2011 +0100
+++ b/Nominal/Nominal2_Abs.thy	Tue Jan 18 17:30:47 2011 +0100
@@ -350,9 +350,8 @@
   from asm have 0: "(supp x - as) \<sharp>* p'" by  (auto simp only: alphas)
   then have #: "p' \<bullet> (supp x - as) = (supp x - as)" 
     by (simp add: atom_set_perm_eq)
-  have "finite (supp x)" by (simp add: finite_supp)
-  then obtain p where *: "\<forall>b \<in> supp x. p \<bullet> b = p' \<bullet> b" and **: "supp p \<subseteq> supp x \<union> p' \<bullet> supp x"
-    using set_renaming_perm by blast
+  obtain p where *: "\<forall>b \<in> supp x. p \<bullet> b = p' \<bullet> b" and **: "supp p \<subseteq> supp x \<union> p' \<bullet> supp x"
+    using set_renaming_perm2 by blast
   from * have a: "p \<bullet> x = p' \<bullet> x" using supp_perm_perm_eq by auto
   from 0 have 1: "(supp x - as) \<sharp>* p" using *
     by (auto simp add: fresh_star_def fresh_perm)
@@ -379,20 +378,23 @@
 
 lemma alpha_abs_set_stronger1:
   fixes x::"'a::fs"
-  assumes  fin: "finite as"
-  and     asm: "(as, x) \<approx>set (op =) supp p' (as', x')"
+  assumes asm: "(as, x) \<approx>set (op =) supp p' (as', x')"
   shows "\<exists>p. (as, x) \<approx>set (op =) supp p (as', x') \<and> supp p \<subseteq> as \<union> as'"
 proof -
   from asm have 0: "(supp x - as) \<sharp>* p'" by  (auto simp only: alphas)
   then have #: "p' \<bullet> (supp x - as) = (supp x - as)" 
     by (simp add: atom_set_perm_eq)
-  have za: "finite ((supp x) \<union> as)" using fin by (simp add: finite_supp)
-  obtain p where *: "\<forall>b \<in> ((supp x) \<union> as). p \<bullet> b = p' \<bullet> b" and **: "supp p \<subseteq> ((supp x) \<union> as) \<union> p' \<bullet> ((supp x) \<union> as)"
-    using set_renaming_perm[OF za] by blast
+  obtain p where *: "\<forall>b \<in> (supp x \<union> as). p \<bullet> b = p' \<bullet> b" 
+    and **: "supp p \<subseteq> (supp x \<union> as) \<union> p' \<bullet> (supp x \<union> as)"
+    using set_renaming_perm2 by blast
   from * have "\<forall>b \<in> supp x. p \<bullet> b = p' \<bullet> b" by blast
   then have a: "p \<bullet> x = p' \<bullet> x" using supp_perm_perm_eq by auto
   from * have "\<forall>b \<in> as. p \<bullet> b = p' \<bullet> b" by blast
-  then have zb: "p \<bullet> as = p' \<bullet> as" using supp_perm_perm_eq by (metis fin supp_finite_atom_set)
+  then have zb: "p \<bullet> as = p' \<bullet> as" 
+    apply(auto simp add: permute_set_eq)
+    apply(rule_tac x="xa" in exI)
+    apply(simp)
+    done
   have zc: "p' \<bullet> as = as'" using asm by (simp add: alphas)
   from 0 have 1: "(supp x - as) \<sharp>* p" using *
     by (auto simp add: fresh_star_def fresh_perm)
@@ -402,16 +404,15 @@
   have "supp p \<subseteq> supp x \<union> as \<union> p' \<bullet> supp x \<union> p' \<bullet> as" using ** using union_eqvt by blast
   also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> as \<union> (p' \<bullet> ((supp x - as) \<union> (supp x \<inter> as))) \<union> p' \<bullet> as" 
     using b by simp
-  also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> as \<union> ((p' \<bullet> (supp x - as)) \<union> (p' \<bullet> (supp x \<inter> as))) \<union> p' \<bullet> as"
-    by (simp add: union_eqvt)
+  also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> as \<union> 
+    ((p' \<bullet> (supp x - as)) \<union> (p' \<bullet> (supp x \<inter> as))) \<union> p' \<bullet> as" by (simp add: union_eqvt)
   also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> as \<union> (p' \<bullet> (supp x \<inter> as)) \<union> p' \<bullet> as"
     using # by auto
   also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> as \<union> p' \<bullet> ((supp x \<inter> as) \<union> as)" using union_eqvt
     by auto
   also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> as \<union> p' \<bullet> as" 
     by (metis Int_commute Un_commute sup_inf_absorb)
-  also have "\<dots> = (supp x - as) \<union> as \<union> p' \<bullet> as" 
-    by blast
+  also have "\<dots> = (supp x - as) \<union> as \<union> p' \<bullet> as" by blast
   finally have "supp p \<subseteq> (supp x - as) \<union> as \<union> p' \<bullet> as" .
   then have "supp p \<subseteq> as \<union> p' \<bullet> as" using 2 by blast
   moreover