# HG changeset patch
# User urbanc
# Date 1176701543 -7200
# Node ID 381e6c45f13b3c0e0f474b2ab7a69a9997a0d8ed
# Parent  ca804eb70d3940ed5e3336edf309925d76ddc1e5
improved the equivariance lemmas for the quantifiers; had to export the lemma eqvt_force_add and eqvt_force_del in the thmdecls

diff -r ca804eb70d39 -r 381e6c45f13b src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Mon Apr 16 06:45:22 2007 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Mon Apr 16 07:32:23 2007 +0200
@@ -1716,7 +1716,7 @@
   and     x :: "'a"
   assumes pt: "pt TYPE('a) TYPE('x)"
   and     at: "at TYPE('x)"
-  shows "pi\<bullet>(\<forall>(x::'a). P x) = (\<forall>(x::'a). (pi\<bullet>P) x)"
+  shows "pi\<bullet>(\<forall>(x::'a). P x) = (\<forall>(x::'a). pi\<bullet>(P ((rev pi)\<bullet>x)))"
 apply(auto simp add: perm_bool perm_fun_def)
 apply(drule_tac x="pi\<bullet>x" in spec)
 apply(simp add: pt_rev_pi[OF pt, OF at])
@@ -1727,7 +1727,7 @@
   and     x :: "'a"
   assumes pt: "pt TYPE('a) TYPE('x)"
   and     at: "at TYPE('x)"
-  shows "pi\<bullet>(\<exists>(x::'a). P x) = (\<exists>(x::'a). (pi\<bullet>P) x)"
+  shows "pi\<bullet>(\<exists>(x::'a). P x) = (\<exists>(x::'a). pi\<bullet>(P ((rev pi)\<bullet>x)))"
 apply(auto simp add: perm_bool perm_fun_def)
 apply(rule_tac x="pi\<bullet>x" in exI) 
 apply(simp add: pt_rev_pi[OF pt, OF at])
diff -r ca804eb70d39 -r 381e6c45f13b src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Mon Apr 16 06:45:22 2007 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Mon Apr 16 07:32:23 2007 +0200
@@ -802,8 +802,8 @@
             ||>> PureThy.add_thmss [(("supp_atm", (inst_at [at_supp]) @ (inst_dj [dj_supp])),[])]
             ||>> PureThy.add_thmss [(("exists_fresh", inst_at [at_exists_fresh]),[])]
             ||>> PureThy.add_thmss [(("exists_fresh'", inst_at [at_exists_fresh']),[])]
-            ||>> PureThy.add_thmss [(("all_eqvt", inst_pt_at [all_eqvt]),[NominalThmDecls.eqvt_add])] 
-            ||>> PureThy.add_thmss [(("ex_eqvt", inst_pt_at [ex_eqvt]),[NominalThmDecls.eqvt_add])]
+            ||>> PureThy.add_thmss [(("all_eqvt", inst_pt_at [all_eqvt]),[NominalThmDecls.eqvt_force_add])] 
+            ||>> PureThy.add_thmss [(("ex_eqvt", inst_pt_at [ex_eqvt]),[NominalThmDecls.eqvt_force_add])]
             ||>> PureThy.add_thmss 
 	      let val thms1 = inst_at [at_fresh]
 		  val thms2 = inst_dj [at_fresh_ineq]
diff -r ca804eb70d39 -r 381e6c45f13b src/HOL/Nominal/nominal_thmdecls.ML
--- a/src/HOL/Nominal/nominal_thmdecls.ML	Mon Apr 16 06:45:22 2007 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML	Mon Apr 16 07:32:23 2007 +0200
@@ -15,6 +15,8 @@
   val print_data: Proof.context -> unit
   val eqvt_add: attribute
   val eqvt_del: attribute
+  val eqvt_force_add: attribute
+  val eqvt_force_del: attribute
   val setup: theory -> theory
   val get_eqvt_thms: theory -> thm list
   val get_fresh_thms: theory -> thm list
@@ -205,19 +207,22 @@
 
 val eqvt_add  = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.add_rule)); 
 val eqvt_del  = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.del_rule)); 
+val eqvt_force_add  = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Drule.add_rule)); 
+val eqvt_force_del  = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Drule.del_rule)); 
+
 val bij_add   = Thm.declaration_attribute (bij_add_del_aux (bij_map Drule.add_rule)); 
 val bij_del   = Thm.declaration_attribute (bij_add_del_aux (bij_map Drule.del_rule));
 val fresh_add = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Drule.add_rule)); 
 val fresh_del = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Drule.del_rule));
 
-val eqvt_force_add  = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Drule.add_rule)); 
-val eqvt_force_del  = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Drule.del_rule)); 
+
 
 val setup =
   Data.init #>
   Attrib.add_attributes 
      [("eqvt",  Attrib.add_del_args eqvt_add eqvt_del,   "equivariance theorem declaration"),
-      ("eqvt_force",  Attrib.add_del_args eqvt_force_add eqvt_force_del,"equivariance theorem declaration (without checking the form of the lemma)"),
+      ("eqvt_force", Attrib.add_del_args eqvt_force_add eqvt_force_del,
+                             "equivariance theorem declaration (without checking the form of the lemma)"),
       ("fresh", Attrib.add_del_args fresh_add fresh_del, "freshness theorem declaration"),
       ("bij",   Attrib.add_del_args bij_add bij_del,     "bijection theorem declaration")];