# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1295356309 -32400
# Node ID eef49daac6c8644abc2af9a8120537d9f00c413c
# Parent  3c493c9513880e61a96c58f9ee104588a58b0ce0
alpha_abs_set_stronger1

diff -r 3c493c951388 -r eef49daac6c8 Nominal/Nominal2_Abs.thy
--- a/Nominal/Nominal2_Abs.thy	Tue Jan 18 21:12:25 2011 +0900
+++ b/Nominal/Nominal2_Abs.thy	Tue Jan 18 22:11:49 2011 +0900
@@ -344,7 +344,7 @@
 
 lemma alpha_abs_res_stronger1:
   fixes x::"'a::fs"
-  assumes asm: "(as, x) \<approx>res (op =) supp p' (as', x')" 
+  assumes asm: "(as, x) \<approx>res (op =) supp p' (as', x')"
   shows "\<exists>p. (as, x) \<approx>res (op =) supp p (as', x') \<and> supp p \<subseteq> (supp x \<inter> as) \<union> (supp x' \<inter> as')" 
 proof -
   from asm have 0: "(supp x - as) \<sharp>* p'" by  (auto simp only: alphas)
@@ -377,6 +377,49 @@
   show "\<exists>p. (as, x) \<approx>res (op =) supp p (as', x') \<and> supp p \<subseteq> (supp x \<inter> as) \<union> (supp x' \<inter> as')" by blast
 qed
 
+lemma alpha_abs_set_stronger1:
+  fixes x::"'a::fs"
+  assumes  fin: "finite as"
+  and     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
+  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)
+  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)
+  then have 2: "(supp x - as) \<inter> supp p = {}"
+    by (auto simp add: fresh_star_def fresh_def)
+  have b: "supp x = (supp x - as) \<union> (supp x \<inter> as)" by auto
+  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 \<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
+  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 
+  have "(as, x) \<approx>set (op =) supp p (as', x')" using asm 1 a zb by (simp add: alphas)
+  ultimately 
+  show "\<exists>p. (as, x) \<approx>set (op =) supp p (as', x') \<and> supp p \<subseteq> as \<union> as'" using zc by blast
+qed
+
 
 
 section {* Quotient types *}