# HG changeset patch # User Cezary Kaliszyk # Date 1265364583 -3600 # Node ID ffae51f14367919717721ba0bf509b1e0634d4ba # Parent 62e54830590f300672e8503f3d4e712684253dd6# Parent 8d4d52f51e0d52c5ad0d132f8a1aff7410d32d39 merge diff -r 62e54830590f -r ffae51f14367 Quot/Nominal/Nominal2_Eqvt.thy --- a/Quot/Nominal/Nominal2_Eqvt.thy Fri Feb 05 10:45:49 2010 +0100 +++ b/Quot/Nominal/Nominal2_Eqvt.thy Fri Feb 05 11:09:43 2010 +0100 @@ -226,6 +226,8 @@ use "nominal_thmdecls.ML" setup "Nominal_ThmDecls.setup" + + lemmas [eqvt] = (* connectives *) eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt @@ -233,8 +235,7 @@ imp_eqvt [folded induct_implies_def] (* nominal *) - permute_eqvt supp_eqvt fresh_eqvt - permute_pure + supp_eqvt fresh_eqvt permute_pure (* datatypes *) permute_prod.simps @@ -244,6 +245,8 @@ empty_eqvt UNIV_eqvt union_eqvt inter_eqvt Diff_eqvt Compl_eqvt insert_eqvt +lemmas [eqvt_raw] = permute_eqvt + thm eqvts thm eqvts_raw diff -r 62e54830590f -r ffae51f14367 Quot/Nominal/nominal_permeq.ML --- a/Quot/Nominal/nominal_permeq.ML Fri Feb 05 10:45:49 2010 +0100 +++ b/Quot/Nominal/nominal_permeq.ML Fri Feb 05 11:09:43 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_raw_thms ctxt), + More_Conv.rewrs_conv (Nominal_ThmDecls.get_eqvts_raw_thms ctxt), Conv.all_conv ] ct diff -r 62e54830590f -r ffae51f14367 Quot/Nominal/nominal_thmdecls.ML --- a/Quot/Nominal/nominal_thmdecls.ML Fri Feb 05 10:45:49 2010 +0100 +++ b/Quot/Nominal/nominal_thmdecls.ML Fri Feb 05 11:09:43 2010 +0100 @@ -3,18 +3,18 @@ Infrastructure for the lemma collection "eqvts". - Provides the attributes [eqvt] and [eqvt_force], and the theorem - 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 + Provides the attributes [eqvt] and [eqvt_raw], and the theorem + 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 is stored in the form + and it is stored in the form p o c == c - The [eqvt_force] attribute just adds the theorem to eqvts. + The [eqvt_raw] attribute just adds the theorem to eqvts_raw. TODO: @@ -27,36 +27,41 @@ sig val eqvt_add: attribute val eqvt_del: attribute - val eqvt_force_add: attribute - val eqvt_force_del: attribute + val eqvt_raw_add: attribute + val eqvt_raw_del: attribute val setup: theory -> theory - val get_eqvt_thms: Proof.context -> thm list - val get_eqvt_raw_thms: Proof.context -> thm list + val get_eqvts_thms: Proof.context -> thm list + val get_eqvts_raw_thms: Proof.context -> thm list end; structure Nominal_ThmDecls: NOMINAL_THMDECLS = struct + structure EqvtData = Generic_Data -( - 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) +( type T = thm Item_Net.T; + val empty = Thm.full_rules; val extend = I; - val merge = Item_Net.merge; -); + val merge = Item_Net.merge ); -val eqvts = (map fst) o Item_Net.content o EqvtData.get; -val eqvts_raw = (map_filter snd) o Item_Net.content o EqvtData.get; +structure EqvtRawData = Generic_Data +( type T = thm Item_Net.T; + val empty = Thm.full_rules; + val extend = I; + val merge = Item_Net.merge ); -val get_eqvt_thms = eqvts o Context.Proof; -val get_eqvt_raw_thms = eqvts_raw o Context.Proof; +val eqvts = Item_Net.content o EqvtData.get; +val eqvts_raw = Item_Net.content o EqvtRawData.get; + +val get_eqvts_thms = eqvts o Context.Proof; +val get_eqvts_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; -val add_force_thm = EqvtData.map o Item_Net.update; -val del_force_thm = EqvtData.map o Item_Net.remove; +val add_raw_thm = EqvtRawData.map o Item_Net.update; +val del_raw_thm = EqvtRawData.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,7 +99,7 @@ (fn _ => eqvt_transform_tac thm 1) end -fun transform addel_fn thm context = +fun transform addel_fun thm context = let val ctxt = Context.proof_of context val trm = HOLogic.dest_Trueprop (prop_of thm) @@ -102,27 +107,28 @@ case trm of Const (@{const_name "op ="}, _) $ lhs $ rhs => let - val thm2 = transform_eq ctxt thm lhs rhs RS @{thm eq_reflection} + val thm' = transform_eq ctxt thm lhs rhs RS @{thm eq_reflection} in - addel_fn (thm, SOME thm2) context + addel_fun thm' 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_add = Thm.declaration_attribute (fn thm => (add_thm thm) o (transform add_raw_thm thm)); +val eqvt_del = Thm.declaration_attribute (fn thm => (del_thm thm) o (transform del_raw_thm 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 eqvt_raw_add = Thm.declaration_attribute add_raw_thm; +val eqvt_raw_del = Thm.declaration_attribute del_raw_thm; 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"]) #> - Attrib.setup @{binding "eqvt_force"} (Attrib.add_del eqvt_force_add eqvt_force_del) + Attrib.setup @{binding "eqvt_raw"} (Attrib.add_del eqvt_raw_add eqvt_raw_del) (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;