# HG changeset patch # User Cezary Kaliszyk # Date 1265377947 -3600 # Node ID b2f32114e8a63a3ef0f6920a6ed41a0f2dad0c99 # Parent 7a42cc191111ca1164bc714b1005b868e87aca78# Parent 6deecec6795f3e35111260f0e555cf63a823ea88 merge diff -r 7a42cc191111 -r b2f32114e8a6 Quot/Nominal/Nominal2_Eqvt.thy --- a/Quot/Nominal/Nominal2_Eqvt.thy Fri Feb 05 10:32:21 2010 +0100 +++ b/Quot/Nominal/Nominal2_Eqvt.thy Fri Feb 05 14:52:27 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 7a42cc191111 -r b2f32114e8a6 Quot/Nominal/nominal_permeq.ML --- a/Quot/Nominal/nominal_permeq.ML Fri Feb 05 10:32:21 2010 +0100 +++ b/Quot/Nominal/nominal_permeq.ML Fri Feb 05 14:52:27 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 7a42cc191111 -r b2f32114e8a6 Quot/Nominal/nominal_thmdecls.ML --- a/Quot/Nominal/nominal_thmdecls.ML Fri Feb 05 10:32:21 2010 +0100 +++ b/Quot/Nominal/nominal_thmdecls.ML Fri Feb 05 14:52:27 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; diff -r 7a42cc191111 -r b2f32114e8a6 Quot/QuotMain.thy --- a/Quot/QuotMain.thy Fri Feb 05 10:32:21 2010 +0100 +++ b/Quot/QuotMain.thy Fri Feb 05 14:52:27 2010 +0100 @@ -150,7 +150,6 @@ text {* Tactics for proving the lifted theorems *} use "quotient_tacs.ML" - section {* Methods / Interface *} ML {* @@ -181,5 +180,9 @@ {* Scan.succeed (mk_method2 Quotient_Tacs.clean_tac) *} {* Proves automatically the cleaning goals from the lifting procedure. *} +attribute_setup quot_lifted = + {* Scan.succeed Quotient_Tacs.lifted_attr *} + {* Lifting of theorems to quotient types. *} + end diff -r 7a42cc191111 -r b2f32114e8a6 Quot/quotient_tacs.ML --- a/Quot/quotient_tacs.ML Fri Feb 05 10:32:21 2010 +0100 +++ b/Quot/quotient_tacs.ML Fri Feb 05 14:52:27 2010 +0100 @@ -15,6 +15,7 @@ val lift_tac: Proof.context -> thm list -> int -> tactic val quotient_tac: Proof.context -> int -> tactic val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic + val lifted_attr: attribute end; structure Quotient_Tacs: QUOTIENT_TACS = @@ -647,4 +648,15 @@ THEN' RANGE (map mk_tac rthms) end +(* The attribute *) +fun lifted_attr_pre ctxt thm = +let + val gl = (quotient_lift_all ctxt o Logic.unvarify o prop_of) thm + val glc = Syntax.check_term ctxt gl +in + (Goal.prove ctxt (Term.add_free_names glc []) [] glc (fn x => lift_tac (#context x) [thm] 1)) +end; + +val lifted_attr = Thm.rule_attribute (fn ctxt => fn t => lifted_attr_pre (Context.proof_of ctxt) t) + end; (* structure *) diff -r 7a42cc191111 -r b2f32114e8a6 Quot/quotient_term.ML --- a/Quot/quotient_term.ML Fri Feb 05 10:32:21 2010 +0100 +++ b/Quot/quotient_term.ML Fri Feb 05 14:52:27 2010 +0100 @@ -689,48 +689,74 @@ inj_repabs_trm ctxt (rtrm, qtrm) |> Syntax.check_term ctxt -(* Finds subterms of a term that are lifted to constants and replaces - those as well as occurrences of the equivalence relation and replaces - those by equality. - Currently types are not checked so because of the dummyTs it may - not be complete *) +(*** Translating the goal automatically + +Finds subterms of a term that can be lifted and: +* replaces subterms matching lifted constants by the lifted constants +* replaces equivalence relations by equalities +* In constants, frees and schematic variables replaces + subtypes matching lifted types by those types *) + +fun subst_ty thy ty (rty, qty) r = + if r <> NONE then r else + case try (Sign.typ_match thy (ty, rty)) Vartab.empty of + SOME inst => SOME (Envir.subst_type inst qty) + | NONE => NONE +fun subst_tys thy substs ty = + case fold (subst_ty thy ty) substs NONE of + SOME ty => ty + | NONE => + (case ty of + Type (s, tys) => Type (s, map (subst_tys thy substs) tys) + | x => x) + +fun subst_trm thy t (rt, qt) s = + if s <> NONE then s else + case try (Pattern.match thy (t, rt)) (Vartab.empty, Vartab.empty) of + SOME inst => SOME (Envir.subst_term inst qt) + | NONE => NONE; +fun subst_trms thy substs t = fold (subst_trm thy t) substs NONE + +fun get_ty_trm_substs ctxt = +let + val thy = ProofContext.theory_of ctxt + val quot_infos = Quotient_Info.quotdata_dest ctxt + val ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos + val const_infos = Quotient_Info.qconsts_dest ctxt + val const_substs = map (fn ci => (#rconst ci, #qconst ci)) const_infos + fun rel_eq rel = HOLogic.eq_const (subst_tys thy ty_substs (domain_type (fastype_of rel))) + val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos +in + (ty_substs, (const_substs @ rel_substs)) +end + fun quotient_lift_all ctxt t = let val thy = ProofContext.theory_of ctxt - val const_infos = Quotient_Info.qconsts_dest ctxt - val rel_infos = Quotient_Info.quotdata_dest ctxt - fun treat_const_info t qc_info s = - if s <> NONE then s else - case try (Pattern.match thy (t, #rconst qc_info)) (Vartab.empty, Vartab.empty) of - SOME inst => SOME (Envir.subst_term inst (#qconst qc_info)) - | NONE => NONE; - fun treat_const t = fold (treat_const_info t) const_infos NONE - fun treat_rel_info t rel_info s = - if s <> NONE then s else - if Pattern.matches thy (t, #equiv_rel rel_info) then SOME (Const ("op =", dummyT)) - else NONE - fun treat_rel t = fold (treat_rel_info t) rel_infos NONE + val (ty_substs, substs) = get_ty_trm_substs ctxt fun lift_aux t = - case treat_const t of + case subst_trms thy substs t of SOME x => x | NONE => - (case treat_rel t of - SOME x => x - | NONE => - (case t of - a $ b => lift_aux a $ lift_aux b - | Abs(a, T, s) => - let val (y, s') = Term.dest_abs (a, T, s) in - Abs(y, dummyT, abstract_over (Free (y, dummyT), (lift_aux s'))) - end - | Free(n, _) => Free(n, dummyT) - | Var(n, _) => Var(n, dummyT) - | Bound i => Bound i - | Const(s, _) => Const(s, dummyT))) + (case t of + a $ b => lift_aux a $ lift_aux b + | Abs(a, ty, s) => + let + val (y, s') = Term.dest_abs (a, ty, s) + val nty = subst_tys thy ty_substs ty + in + Abs(y, nty, abstract_over (Free (y, nty), (lift_aux s'))) + end + | Free(n, ty) => Free(n, subst_tys thy ty_substs ty) + | Var(n, ty) => Var(n, subst_tys thy ty_substs ty) + | Bound i => Bound i + | Const(s, ty) => Const(s, subst_tys thy ty_substs ty)) in lift_aux t end + + end; (* structure *)