# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1265291721 -3600
# Node ID 090fa3f21380c521efe9fcada0c99bcae2c1a8c9
# Parent  f81b506f62a78c075da1c9ecf4816a046937c263
restored the old behaviour of having an eqvts list; the transformed theorems are stored in eqvts_raw

diff -r f81b506f62a7 -r 090fa3f21380 Quot/Nominal/Nominal2_Eqvt.thy
--- a/Quot/Nominal/Nominal2_Eqvt.thy	Wed Feb 03 17:36:25 2010 +0100
+++ b/Quot/Nominal/Nominal2_Eqvt.thy	Thu Feb 04 14:55:21 2010 +0100
@@ -11,6 +11,7 @@
 
 section {* Logical Operators *}
 
+
 lemma eq_eqvt:
   shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)"
   unfolding permute_eq_iff permute_bool_def ..
@@ -233,6 +234,7 @@
 
   (* nominal *)
   permute_eqvt supp_eqvt fresh_eqvt
+  permute_pure
 
   (* datatypes *)
   permute_prod.simps
@@ -242,9 +244,8 @@
   empty_eqvt UNIV_eqvt union_eqvt inter_eqvt
   Diff_eqvt Compl_eqvt insert_eqvt
 
-declare permute_pure [eqvt]
-
-(* thm eqvts *)
+thm eqvts
+thm eqvts_raw
 
 text {* helper lemmas for the eqvt_tac *}
 
diff -r f81b506f62a7 -r 090fa3f21380 Quot/Nominal/nominal_permeq.ML
--- a/Quot/Nominal/nominal_permeq.ML	Wed Feb 03 17:36:25 2010 +0100
+++ b/Quot/Nominal/nominal_permeq.ML	Thu Feb 04 14:55:21 2010 +0100
@@ -59,7 +59,7 @@
         then_conv Conv.comb_conv (eqvt_conv ctxt),
       eqvt_lambda_conv ctxt
         then_conv Conv.abs_conv (fn (v, ctxt) => eqvt_conv ctxt) ctxt,
-      More_Conv.rewrs_conv (Nominal_ThmDecls.get_eqvt_thms ctxt),
+      More_Conv.rewrs_conv (Nominal_ThmDecls.get_eqvt_raw_thms ctxt),
       Conv.all_conv
     ] ct
 
diff -r f81b506f62a7 -r 090fa3f21380 Quot/Nominal/nominal_thmdecls.ML
--- a/Quot/Nominal/nominal_thmdecls.ML	Wed Feb 03 17:36:25 2010 +0100
+++ b/Quot/Nominal/nominal_thmdecls.ML	Thu Feb 04 14:55:21 2010 +0100
@@ -4,18 +4,21 @@
   Infrastructure for the lemma collection "eqvts".
 
   Provides the attributes [eqvt] and [eqvt_force], and the theorem
-  list eqvt. In contrast to eqvt-force, the eqvt-lemmas that will be 
-  stored are expected to be of the form
+  lists eqvts and eqvts_raw. The first attribute will store the theorem
+  in the eqvts list and also in the eqvts_raw list. For the latter 
+  the theorem is expected to be of the form
 
     p o (c x1 x2 ...) = c (p o x1) (p o x2) ...
 
-  and are transformed into the form
+  and is stored in the form
 
     p o c == c
 
-  TODO
+  The [eqvt_force] attribute just adds the theorem to eqvts.
 
-   - deal with eqvt-lemmas of the for 
+  TODO:
+
+   - deal with eqvt-lemmas of the form 
 
        c x1 x2 ... ==> c (p o x1) (p o x2) ..
 *)
@@ -28,6 +31,7 @@
   val eqvt_force_del: attribute
   val setup: theory -> theory
   val get_eqvt_thms: Proof.context -> thm list
+  val get_eqvt_raw_thms: Proof.context -> thm list
 
 end;
 
@@ -36,14 +40,17 @@
 
 structure EqvtData = Generic_Data
 (
-  type T = thm Item_Net.T;
-  val empty = Thm.full_rules;
+  type T = (thm * thm option) Item_Net.T;
+  val empty = Item_Net.init (eq_fst Thm.eq_thm_prop) (single o Thm.full_prop_of o fst)
   val extend = I;
   val merge = Item_Net.merge;
 );
 
-val content = Item_Net.content o EqvtData.get;
-val get_eqvt_thms = content o Context.Proof; 
+val eqvts = (map fst) o Item_Net.content o EqvtData.get;
+val eqvts_raw = (map_filter snd) o Item_Net.content o EqvtData.get;
+
+val get_eqvt_thms = eqvts o Context.Proof; 
+val get_eqvt_raw_thms = eqvts_raw o Context.Proof; 
 
 val add_thm = EqvtData.map o Item_Net.update;
 val del_thm = EqvtData.map o Item_Net.remove;
@@ -51,7 +58,6 @@
 val add_force_thm = EqvtData.map o Item_Net.update;
 val del_force_thm = EqvtData.map o Item_Net.remove;
 
-
 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)
   | dest_perm t = raise TERM("dest_perm", [t])
 
@@ -94,26 +100,29 @@
   val trm = HOLogic.dest_Trueprop (prop_of thm)
 in
   case trm of
-    Const (@{const_name "op ="}, _) $ lhs $ rhs => 
-      addel_fn (transform_eq ctxt thm lhs rhs RS @{thm eq_reflection}) context
-  | _ => raise (error "no other cases yet implemented")
+    Const (@{const_name "op ="}, _) $ lhs $ rhs =>
+      let 
+        val thm2 = transform_eq ctxt thm lhs rhs RS @{thm eq_reflection}
+      in
+        addel_fn (thm, SOME thm2) context
+      end
+  | _ => raise (error "only (op=) case implemented yet")
 end 
 
-
 val eqvt_add = Thm.declaration_attribute (transform add_thm);
 val eqvt_del = Thm.declaration_attribute (transform del_thm);
 
-val eqvt_force_add = Thm.declaration_attribute add_force_thm;
-val eqvt_force_del = Thm.declaration_attribute del_force_thm;
+val eqvt_force_add = Thm.declaration_attribute (add_force_thm o rpair NONE);
+val eqvt_force_del = Thm.declaration_attribute (del_force_thm o rpair NONE);
 
 val setup =
   Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del) 
     (cat_lines ["declaration of equivariance lemmas - they will automtically be",  
-                "brought into the form p o c = c"]) #>
+       "brought into the form p o c = c"]) #>
   Attrib.setup @{binding "eqvt_force"} (Attrib.add_del eqvt_force_add eqvt_force_del) 
-    (cat_lines ["declaration of equivariance lemmas - they will will be", 
-                "added/deleted directly to the eqvt thm-list"]) #>
-  PureThy.add_thms_dynamic (@{binding "eqvts"}, content);
-
+    (cat_lines ["declaration of equivariance lemmas - no",
+       "transformation is performed"]) #>
+  PureThy.add_thms_dynamic (@{binding "eqvts"}, eqvts) #>
+  PureThy.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw);
 
 end;