improved the equivariance lemmas for the quantifiers; had to export the lemma eqvt_force_add and eqvt_force_del in the thmdecls
--- 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])
--- 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]
--- 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")];