# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1295330118 -3600
# Node ID 92c001d932258402bdd0b8cb3f9853a02407ab43
# Parent  e3f8673085b15418d394ef030098f0658ecde093
modified the renaming_perm lemmas

diff -r e3f8673085b1 -r 92c001d93225 Nominal/Nominal2_Abs.thy
--- 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
 
 
diff -r e3f8673085b1 -r 92c001d93225 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Mon Jan 17 17:20:21 2011 +0100
+++ b/Nominal/Nominal2_Base.thy	Tue Jan 18 06:55:18 2011 +0100
@@ -1785,7 +1785,22 @@
     by (metis permute_minus_cancel permute_plus)
 qed
     
-
+lemma atom_set_perm_eq:
+  assumes a: "as \<sharp>* p"
+  shows "p \<bullet> as = as"
+proof -
+  from a have "supp p \<subseteq> {a. a \<notin> as}"
+    unfolding supp_perm fresh_star_def fresh_def by auto
+  then show "p \<bullet> as = as"
+  proof (induct p rule: perm_struct_induct)
+    case zero
+    show "0 \<bullet> as = as" by simp
+  next
+    case (swap p a b)
+    then have "a \<notin> as" "b \<notin> as" "p \<bullet> as = as" by simp_all
+    then show "((a \<rightleftharpoons> b) + p) \<bullet> as = as" by (simp add: swap_set_not_in)
+  qed
+qed
 
 section {* Avoiding of atom sets *}
 
@@ -1910,38 +1925,34 @@
 
 section {* Renaming permutations *}
 
+
 lemma set_renaming_perm:
   assumes b: "finite bs"
-  shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)"
+  shows "\<exists>q. (\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)"
 using b
 proof (induct)
   case empty
-  have "0 \<bullet> {} = p \<bullet> {} \<and> supp (0::perm) \<subseteq> {} \<union> p \<bullet> {}"
+  have "(\<forall>b \<in> {}. 0 \<bullet> b = p \<bullet> b) \<and> supp (0::perm) \<subseteq> {} \<union> p \<bullet> {}"
     by (simp add: permute_set_eq supp_perm)
-  then show "\<exists>q. q \<bullet> {} = p \<bullet> {} \<and> supp q \<subseteq> {} \<union> p \<bullet> {}" by blast
+  then show "\<exists>q. (\<forall>b \<in> {}. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> {} \<union> p \<bullet> {}" by blast
 next
   case (insert a bs)
-  then have " \<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> p \<bullet> bs" 
-    by (simp add: insert_eqvt) 
-  then obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> p \<bullet> bs" by blast 
+  then have " \<exists>q. (\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> bs \<union> p \<bullet> bs" by simp 
+  then obtain q where *: "\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> bs \<union> p \<bullet> bs"
+    by (metis empty_subsetI insert(3) supp_swap) 
   { assume 1: "q \<bullet> a = p \<bullet> a"
-    have "q \<bullet> insert a bs = p \<bullet> insert a bs" using 1 * by (simp add: insert_eqvt)
+    have "\<forall>b \<in> (insert a bs). q \<bullet> b = p \<bullet> b" using 1 * by simp
     moreover 
     have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" 
       using ** by (auto simp add: insert_eqvt)
     ultimately 
-    have "\<exists>q. q \<bullet> insert a bs = p \<bullet> insert a bs \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by blast
+    have "\<exists>q. (\<forall>b \<in> insert a bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by blast
   }
   moreover
   { assume 2: "q \<bullet> a \<noteq> p \<bullet> a"
     def q' \<equiv> "((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q"
-    { have "(q \<bullet> a) \<notin> (p \<bullet> bs)" using `a \<notin> bs` *[symmetric] by (simp add: mem_permute_iff)
-      moreover 
-      have "(p \<bullet> a) \<notin> (p \<bullet> bs)" using `a \<notin> bs` by (simp add: mem_permute_iff)
-      ultimately 
-      have "q' \<bullet> insert a bs = p \<bullet> insert a bs" using 2 * unfolding q'_def 
-        by (simp add: insert_eqvt  swap_set_not_in) 
-    }
+    have "\<forall>b \<in> insert a bs. q' \<bullet> b = p \<bullet> b" using 2 * `a \<notin> bs` unfolding q'_def
+      by (auto simp add: swap_atom)
     moreover 
     { have "{q \<bullet> a, p \<bullet> a} \<subseteq> insert a bs \<union> p \<bullet> insert a bs"
 	using ** 
@@ -1961,45 +1972,38 @@
         unfolding q'_def using supp_plus_perm by blast
     }
     ultimately 
-    have "\<exists>q. q \<bullet> insert a bs = p \<bullet> insert a bs \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by blast
+    have "\<exists>q. (\<forall>b \<in> insert a bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by blast
   }
-  ultimately show "\<exists>q. q \<bullet> insert a bs = p \<bullet> insert a bs \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs"
+  ultimately show "\<exists>q. (\<forall>b \<in> insert a bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs"
     by blast
 qed
 
+
 lemma list_renaming_perm:
-  fixes bs::"atom list"
-  shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> (set bs) \<union> (p \<bullet> (set bs))"
+  shows "\<exists>q. (\<forall>b \<in> set bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set bs \<union> (p \<bullet> set bs)"
 proof (induct bs)
   case Nil
-  have "0 \<bullet> [] = p \<bullet> [] \<and> supp (0::perm) \<subseteq> set [] \<union> p \<bullet> set []"
-    by (simp add: permute_set_eq supp_perm)
-  then show "\<exists>q. q \<bullet> [] = p \<bullet> [] \<and> supp q \<subseteq> set [] \<union> p \<bullet> (set [])" by blast
+  have "(\<forall>b \<in> set []. 0 \<bullet> b = p \<bullet> b) \<and> supp (0::perm) \<subseteq> set [] \<union> p \<bullet> set []" 
+    by (simp add: supp_zero_perm)
+  then show "\<exists>q. (\<forall>b \<in> set []. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set [] \<union> p \<bullet> (set [])" by blast
 next
   case (Cons a bs)
-  then have " \<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> set bs \<union> p \<bullet> (set bs)" 
-    by (simp add: insert_eqvt) 
-  then obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> p \<bullet> (set bs)" by blast 
+  then have " \<exists>q. (\<forall>b \<in> set bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set bs \<union> p \<bullet> (set bs)"  by simp
+  then 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)
   { assume 1: "a \<in> set bs"
     have "q \<bullet> a = p \<bullet> a" using * 1 by (induct bs) (auto)
-    then have "q \<bullet> (a # bs) = p \<bullet> (a # bs)" using * by simp 
+    then have "\<forall>b \<in> set (a # bs). q \<bullet> b = p \<bullet> b" using * by simp 
     moreover 
     have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" using ** by (auto simp add: insert_eqvt)
     ultimately 
-    have "\<exists>q. q \<bullet> (a # bs) = p \<bullet> (a # bs) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" by blast
+    have "\<exists>q. (\<forall>b \<in> set (a # bs). q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" by blast
   }
   moreover
   { assume 2: "a \<notin> set bs"
     def q' \<equiv> "((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q"
-    { have "(q \<bullet> a) \<sharp> (p \<bullet> bs)" using `a \<notin> set bs` *[symmetric] 
-	by (simp add: fresh_permute_iff) (simp add: fresh_def supp_of_atom_list)
-      moreover 
-      have "(p \<bullet> a) \<sharp> (p \<bullet> bs)" using `a \<notin> set bs` 
-	by (simp add: fresh_permute_iff) (simp add: fresh_def supp_of_atom_list)
-      ultimately 
-      have "q' \<bullet> (a # bs) = p \<bullet> (a # bs)" using 2 * unfolding q'_def 
-        by (simp add: swap_fresh_fresh) 
-    }
+    have "\<forall>b \<in> set (a # bs). q' \<bullet> b = p \<bullet> b" 
+      unfolding q'_def using 2 * `a \<notin> set bs` by (auto simp add: swap_atom)
     moreover 
     { have "{q \<bullet> a, p \<bullet> a} \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))"
 	using **
@@ -2019,14 +2023,13 @@
         unfolding q'_def using supp_plus_perm by blast
     }
     ultimately 
-    have "\<exists>q. q \<bullet> (a # bs) = p \<bullet> (a # bs) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" by blast
+    have "\<exists>q. (\<forall>b \<in> set (a # bs).  q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" by blast
   }
-  ultimately show "\<exists>q. q \<bullet> (a # bs) = p \<bullet> (a # bs) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))"
+  ultimately show "\<exists>q. (\<forall>b \<in> set (a # bs). q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))"
     by blast
 qed
 
 
-
 section {* Concrete Atoms Types *}
 
 text {*
diff -r e3f8673085b1 -r 92c001d93225 Nominal/Nominal2_Eqvt.thy
--- a/Nominal/Nominal2_Eqvt.thy	Mon Jan 17 17:20:21 2011 +0100
+++ b/Nominal/Nominal2_Eqvt.thy	Tue Jan 18 06:55:18 2011 +0100
@@ -113,11 +113,6 @@
   shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. p \<bullet> P (- p \<bullet> x))"
   by (perm_simp add: permute_minus_cancel) (rule refl)
 
-lemma ex1_eqvt[eqvt]:
-  shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. (p \<bullet> P) x)"
-  unfolding Ex1_def
-  by (perm_simp) (rule refl)
-
 lemma ex1_eqvt2:
   shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. p \<bullet> P (- p \<bullet> x))"
   by (perm_simp add: permute_minus_cancel) (rule refl)