--- a/Nominal/Nominal2_Abs.thy	Mon Jan 17 17:20:21 2011 +0100
+++ b/Nominal/Nominal2_Abs.thy	Tue Jan 18 06:55:18 2011 +0100
@@ -250,6 +250,102 @@
   apply(rule_tac [!] x="p \<bullet> pa" in exI)
   by (auto simp add: fresh_star_permute_iff permute_eqvt[symmetric])
 
+
+section {* Strengthening the equivalence *}
+
+lemma disjoint_right_eq:
+  assumes a: "A \<union> B1 = A \<union> B2"
+  and     b: "A \<inter> B1 = {}" "A \<inter> B2 = {}"
+  shows "B1 = B2"
+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'"
+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_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
+
+
+
+section {* Quotient types *}
+
 quotient_type 
     'a abs_set = "(atom set \<times> 'a::pt)" / "alpha_abs_set"
 and 'b abs_res = "(atom set \<times> 'b::pt)" / "alpha_abs_res"
@@ -550,7 +646,8 @@
   shows "\<exists>q. [bs]set. x = [p \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
 proof -
   from b set_renaming_perm 
-  obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by blast
+  obtain q where *: "\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by blast
+  have ***: "q \<bullet> bs = p \<bullet> bs" using b * by (induct) (simp add: permute_set_eq, simp add: insert_eqvt)
   have "[bs]set. x =  q \<bullet> ([bs]set. x)"
     apply(rule perm_supp_eq[symmetric])
     using a **
@@ -558,8 +655,8 @@
     unfolding fresh_star_def
     by auto
   also have "\<dots> = [q \<bullet> bs]set. (q \<bullet> x)" by simp
-  finally have "[bs]set. x = [p \<bullet> bs]set. (q \<bullet> x)" by (simp add: *)
-  then show "\<exists>q. [bs]set. x = [p \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" using * by metis
+  finally have "[bs]set. x = [p \<bullet> bs]set. (q \<bullet> x)" by (simp add: ***)
+  then show "\<exists>q. [bs]set. x = [p \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" using *** by metis
 qed
 
 lemma Abs_rename_res:
@@ -569,7 +666,8 @@
   shows "\<exists>q. [bs]res. x = [p \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
 proof -
   from b set_renaming_perm 
-  obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by blast
+  obtain q where *: "\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by blast
+  have ***: "q \<bullet> bs = p \<bullet> bs" using b * by (induct) (simp add: permute_set_eq, simp add: insert_eqvt)
   have "[bs]res. x =  q \<bullet> ([bs]res. x)"
     apply(rule perm_supp_eq[symmetric])
     using a **
@@ -577,8 +675,8 @@
     unfolding fresh_star_def
     by auto
   also have "\<dots> = [q \<bullet> bs]res. (q \<bullet> x)" by simp
-  finally have "[bs]res. x = [p \<bullet> bs]res. (q \<bullet> x)" by (simp add: *)
-  then show "\<exists>q. [bs]res. x = [p \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" using * by metis
+  finally have "[bs]res. x = [p \<bullet> bs]res. (q \<bullet> x)" by (simp add: ***)
+  then show "\<exists>q. [bs]res. x = [p \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" using *** by metis
 qed
 
 lemma Abs_rename_lst:
@@ -587,7 +685,8 @@
   shows "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
 proof -
   from a list_renaming_perm 
-  obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" by blast
+  obtain q where *: "\<forall>b \<in> set bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" by blast
+  have ***: "q \<bullet> bs = p \<bullet> bs" using * by (induct bs) (simp_all add: insert_eqvt)
   have "[bs]lst. x =  q \<bullet> ([bs]lst. x)"
     apply(rule perm_supp_eq[symmetric])
     using a **
@@ -595,8 +694,8 @@
     unfolding fresh_star_def
     by auto
   also have "\<dots> = [q \<bullet> bs]lst. (q \<bullet> x)" by simp
-  finally have "[bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x)" by (simp add: *)
-  then show "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" using * by metis
+  finally have "[bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x)" by (simp add: ***)
+  then show "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" using *** by metis
 qed