# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1295370280 -3600
# Node ID 3c79dfec1cf0f7a8d7af10dc0225f86b35ff91ae
# Parent  87ebc706df67478085bec0b74f6a9fd4927e9806
derived stronger Abs_eq_iff2 theorems

diff -r 87ebc706df67 -r 3c79dfec1cf0 Nominal/Nominal2_Abs.thy
--- a/Nominal/Nominal2_Abs.thy	Tue Jan 18 17:30:47 2011 +0100
+++ b/Nominal/Nominal2_Abs.thy	Tue Jan 18 18:04:40 2011 +0100
@@ -260,33 +260,6 @@
 using a b
 by (metis Int_Un_distrib2 Int_absorb2 Int_commute Un_upper2)
 
-lemma supp_property_set:
-  assumes a: "(as, x) \<approx>set (op =) supp p (as', x')"
-  shows "p \<bullet> (supp x \<inter> as) = supp x' \<inter> as'"
-proof -
-  from a have "(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 "(supp x' - as') \<union> (supp x' \<inter> as') = supp x'" by auto
-  also have "\<dots> = supp (p \<bullet> x)" using a by (simp add: alphas)
-  also have "\<dots> = p \<bullet> (supp x)" by (simp add: supp_eqvt)
-  also have "\<dots> = p \<bullet> ((supp x - as) \<union> (supp x \<inter> as))" by auto
-  also have "\<dots> = (p \<bullet> (supp x - as)) \<union> (p \<bullet> (supp x \<inter> as))" by (simp add: union_eqvt)
-  also have "\<dots> = (supp x - as) \<union> (p \<bullet> (supp x \<inter> as))" using * by simp
-  also have "\<dots> = (supp x' - as') \<union> (p \<bullet> (supp x \<inter> as))" using a by (simp add: alphas)
-  finally have "(supp x' - as') \<union> (supp x' \<inter> as') = (supp x' - as') \<union> (p \<bullet> (supp x \<inter> as))" .
-  moreover 
-  have "(supp x' - as') \<inter> (supp x' \<inter> as') = {}" by auto
-  moreover 
-  have "(supp x - as) \<inter> (supp x \<inter> as) = {}" by auto
-  then have "p \<bullet> ((supp x - as) \<inter> (supp x \<inter> as) = {})" by (simp add: permute_bool_def)
-  then have "(p \<bullet> (supp x - as)) \<inter> (p \<bullet> (supp x \<inter> as)) = {}" by (perm_simp) (simp)
-  then have "(supp x - as) \<inter> (p \<bullet> (supp x \<inter> as)) = {}" using * by simp
-  then have "(supp x' - as') \<inter> (p \<bullet> (supp x \<inter> as)) = {}" using a by (simp add: alphas)
-  ultimately show "p \<bullet> (supp x \<inter> as) = supp x' \<inter> as'"
-    by (auto dest: disjoint_right_eq)
-qed
-  
 lemma supp_property_res:
   assumes a: "(as, x) \<approx>res (op =) supp p (as', x')"
   shows "p \<bullet> (supp x \<inter> as) = supp x' \<inter> as'"
@@ -314,36 +287,7 @@
     by (auto dest: disjoint_right_eq)
 qed 
 
-lemma supp_property_list:
-  assumes a: "(as, x) \<approx>lst (op =) supp p (as', x')"
-  shows "p \<bullet> (supp x \<inter> set as) = supp x' \<inter> set as'"
-proof -
-  from a have "(supp x - set as) \<sharp>* p" by  (auto simp only: alphas)
-  then have *: "p \<bullet> (supp x - set as) = (supp x - set as)" 
-    by (simp add: atom_set_perm_eq)
-  have "(supp x' - set as') \<union> (supp x' \<inter> set as') = supp x'" by auto
-  also have "\<dots> = supp (p \<bullet> x)" using a by (simp add: alphas)
-  also have "\<dots> = p \<bullet> (supp x)" by (simp add: supp_eqvt)
-  also have "\<dots> = p \<bullet> ((supp x - set as) \<union> (supp x \<inter> set as))" by auto
-  also have "\<dots> = (p \<bullet> (supp x - set as)) \<union> (p \<bullet> (supp x \<inter> set as))" by (simp add: union_eqvt)
-  also have "\<dots> = (supp x - set as) \<union> (p \<bullet> (supp x \<inter> set as))" using * by simp
-  also have "\<dots> = (supp x' - set as') \<union> (p \<bullet> (supp x \<inter> set as))" using a by (simp add: alphas)
-  finally 
-  have "(supp x' - set as') \<union> (supp x' \<inter> set as') = (supp x' - set as') \<union> (p \<bullet> (supp x \<inter> set as))" .
-  moreover 
-  have "(supp x' - set as') \<inter> (supp x' \<inter> set as') = {}" by auto
-  moreover 
-  have "(supp x - set as) \<inter> (supp x \<inter> set as) = {}" by auto
-  then have "p \<bullet> ((supp x - set as) \<inter> (supp x \<inter> set as) = {})" by (simp add: permute_bool_def)
-  then have "(p \<bullet> (supp x - set as)) \<inter> (p \<bullet> (supp x \<inter> set as)) = {}" by (perm_simp) (simp)
-  then have "(supp x - set as) \<inter> (p \<bullet> (supp x \<inter> set as)) = {}" using * by simp
-  then have "(supp x' - set as') \<inter> (p \<bullet> (supp x \<inter> set as)) = {}" using a by (simp add: alphas)
-  ultimately show "p \<bullet> (supp x \<inter> set as) = supp x' \<inter> set as'"
-    by (auto dest: disjoint_right_eq)
-qed
-
-lemma alpha_abs_res_stronger1:
-  fixes x::"'a::fs"
+lemma alpha_abs_res_stronger1_aux:
   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 -
@@ -376,8 +320,12 @@
   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_res_stronger1:
+  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> as \<union> as'"
+using alpha_abs_res_stronger1_aux[OF asm] by auto
+
 lemma alpha_abs_set_stronger1:
-  fixes x::"'a::fs"
   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 -
@@ -421,7 +369,61 @@
   show "\<exists>p. (as, x) \<approx>set (op =) supp p (as', x') \<and> supp p \<subseteq> as \<union> as'" using zc by blast
 qed
 
+lemma alpha_abs_lst_stronger1:
+  assumes asm: "(as, x) \<approx>lst (op =) supp p' (as', x')"
+  shows "\<exists>p. (as, x) \<approx>lst (op =) supp p (as', x') \<and> supp p \<subseteq> set as \<union> set as'"
+proof -
+  from asm have 0: "(supp x - set as) \<sharp>* p'" by  (auto simp only: alphas)
+  then have #: "p' \<bullet> (supp x - set as) = (supp x - set as)" 
+    by (simp add: atom_set_perm_eq)
+  obtain p where *: "\<forall>b \<in> (supp x \<union> set as). p \<bullet> b = p' \<bullet> b" 
+    and **: "supp p \<subseteq> (supp x \<union> set as) \<union> p' \<bullet> (supp x \<union> set 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> set as. p \<bullet> b = p' \<bullet> b" by blast
+  then have zb: "p \<bullet> as = p' \<bullet> as" by (induct as) (auto)
+  have zc: "p' \<bullet> set as = set as'" using asm by (simp add: alphas set_eqvt)
+  from 0 have 1: "(supp x - set as) \<sharp>* p" using *
+    by (auto simp add: fresh_star_def fresh_perm)
+  then have 2: "(supp x - set as) \<inter> supp p = {}"
+    by (auto simp add: fresh_star_def fresh_def)
+  have b: "supp x = (supp x - set as) \<union> (supp x \<inter> set as)" by auto
+  have "supp p \<subseteq> supp x \<union> set as \<union> p' \<bullet> supp x \<union> p' \<bullet> set as" using ** using union_eqvt by blast
+  also have "\<dots> = (supp x - set as) \<union> (supp x \<inter> set as) \<union> set as \<union> 
+    (p' \<bullet> ((supp x - set as) \<union> (supp x \<inter> set as))) \<union> p' \<bullet> set as" using b by simp
+  also have "\<dots> = (supp x - set as) \<union> (supp x \<inter> set as) \<union> set as \<union> 
+    ((p' \<bullet> (supp x - set as)) \<union> (p' \<bullet> (supp x \<inter> set as))) \<union> p' \<bullet> set as" by (simp add: union_eqvt)
+  also have "\<dots> = (supp x - set as) \<union> (supp x \<inter> set as) \<union> set as \<union> 
+    (p' \<bullet> (supp x \<inter> set as)) \<union> p' \<bullet> set as" using # by auto
+  also have "\<dots> = (supp x - set as) \<union> (supp x \<inter> set as) \<union> set as \<union> p' \<bullet> ((supp x \<inter> set as) \<union> set as)" 
+    using union_eqvt by auto
+  also have "\<dots> = (supp x - set as) \<union> (supp x \<inter> set as) \<union> set as \<union> p' \<bullet> set as" 
+    by (metis Int_commute Un_commute sup_inf_absorb)
+  also have "\<dots> = (supp x - set as) \<union> set as \<union> p' \<bullet> set as" by blast
+  finally have "supp p \<subseteq> (supp x - set as) \<union> set as \<union> p' \<bullet> set as" .
+  then have "supp p \<subseteq> set as \<union> p' \<bullet> set as" using 2 by blast
+  moreover 
+  have "(as, x) \<approx>lst (op =) supp p (as', x')" using asm 1 a zb by (simp add: alphas)
+  ultimately 
+  show "\<exists>p. (as, x) \<approx>lst (op =) supp p (as', x') \<and> supp p \<subseteq> set as \<union> set as'" using zc by blast 
+qed
 
+lemma alphas_abs_stronger:
+  shows "(as, x) \<approx>abs_set (as', x') \<longleftrightarrow> (\<exists>p. (as, x) \<approx>set (op =) supp p (as', x') \<and> supp p \<subseteq> as \<union> as')"
+  and   "(as, x) \<approx>abs_res (as', x') \<longleftrightarrow> (\<exists>p. (as, x) \<approx>res (op =) supp p (as', x') \<and> supp p \<subseteq> as \<union> as')"
+  and   "(bs, x) \<approx>abs_lst (bs', x') \<longleftrightarrow> 
+   (\<exists>p. (bs, x) \<approx>lst (op =) supp p (bs', x') \<and> supp p \<subseteq> set bs \<union> set bs')"
+apply(rule iffI)
+apply(auto simp add: alphas_abs alpha_abs_set_stronger1)[1]
+apply(auto simp add: alphas_abs)[1]
+apply(rule iffI)
+apply(auto simp add: alphas_abs alpha_abs_res_stronger1)[1]
+apply(auto simp add: alphas_abs)[1]
+apply(rule iffI)
+apply(auto simp add: alphas_abs alpha_abs_lst_stronger1)[1]
+apply(auto simp add: alphas_abs)[1]
+done
 
 section {* Quotient types *}
 
@@ -474,6 +476,13 @@
   and   "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))"
   by (lifting alphas_abs)
 
+lemma Abs_eq_iff2:
+  shows "Abs_set bs x = Abs_set cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op =) supp p (cs, y) \<and> supp p \<subseteq> bs \<union> cs)"
+  and   "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y) \<and> supp p \<subseteq> bs \<union> cs)"
+  and   "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> 
+    (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y) \<and> supp p \<subseteq> set bsl \<union> set csl)"
+  by (lifting alphas_abs_stronger)
+
 lemma Abs_exhausts:
   shows "(\<And>as (x::'a::pt). y1 = Abs_set as x \<Longrightarrow> P1) \<Longrightarrow> P1"
   and   "(\<And>as (x::'a::pt). y2 = Abs_res as x \<Longrightarrow> P2) \<Longrightarrow> P2"
@@ -717,6 +726,7 @@
 
 subsection {* Renaming of bodies of abstractions *}
 
+(* FIXME: finiteness assumption is not needed *)
 
 lemma Abs_rename_set:
   fixes x::"'a::fs"