# HG changeset patch # User Christian Urban # Date 1258768179 -3600 # Node ID f46dc0ca08c3201d9001ae43efba75ea0268d429 # Parent 7d3d86beacd6e2b1949a09f659d8c7db91af0921 simplified get_fun so that it uses directly rty and qty, instead of qenv diff -r 7d3d86beacd6 -r f46dc0ca08c3 IntEx.thy --- a/IntEx.thy Fri Nov 20 13:03:01 2009 +0100 +++ b/IntEx.thy Sat Nov 21 02:49:39 2009 +0100 @@ -8,10 +8,13 @@ "intrel (x, y) (u, v) = (x + v = u + y)" quotient my_int = "nat \ nat" / intrel + and my_int' = "nat \ nat" / intrel apply(unfold EQUIV_def) apply(auto simp add: mem_def expand_fun_eq) done +thm my_int_equiv + print_theorems print_quotients @@ -98,6 +101,7 @@ term LE thm LE_def + definition LESS :: "my_int \ my_int \ bool" where @@ -149,12 +153,33 @@ val test = lift_thm_my_int @{context} @{thm plus_sym_pre} *} - ML {* - val aqtrm = HOLogic.dest_Trueprop (prop_of (atomize_thm test)) - val artrm = HOLogic.dest_Trueprop (prop_of (atomize_thm @{thm plus_sym_pre})) + val aqtrm = (prop_of (atomize_thm test)) + val artrm = (prop_of (atomize_thm @{thm plus_sym_pre})) + val reg_artm = mk_REGULARIZE_goal @{context} artrm aqtrm *} +prove {* reg_artm *} +apply(tactic {* ObjectLogic.full_atomize_tac 1 *}) +apply(tactic {* REGULARIZE_tac' @{context} @{thm "TrueI"} @{thm my_int_equiv} *}) +done + +(* +ML {* +fun inj_REPABS lthy rtrm qtrm = + case (rtrm, qtrm) of + (Abs (x, T, t), Abs (x', T', t')) => + if T = T' + then Abs (x, T, inj_REPABS lthy t t') + else + let + + in + + end + | _ => rtrm +*} +*) lemma plus_assoc_pre: shows "my_plus (my_plus i j) k \ my_plus i (my_plus j k)" @@ -164,8 +189,17 @@ apply (simp) done -ML {* lift_thm_my_int @{context} @{thm plus_assoc_pre} *} +ML {* val test2 = lift_thm_my_int @{context} @{thm plus_assoc_pre} *} +ML {* + val aqtrm = (prop_of (atomize_thm test2)) + val artrm = (prop_of (atomize_thm @{thm plus_assoc_pre})) +*} + +prove {* mk_REGULARIZE_goal @{context} artrm aqtrm *} +apply(tactic {* ObjectLogic.full_atomize_tac 1 *}) +apply(tactic {* REGULARIZE_tac' @{context} @{thm "TrueI"} @{thm my_int_equiv} *}) +done diff -r 7d3d86beacd6 -r f46dc0ca08c3 QuotMain.thy --- a/QuotMain.thy Fri Nov 20 13:03:01 2009 +0100 +++ b/QuotMain.thy Sat Nov 21 02:49:39 2009 +0100 @@ -557,7 +557,62 @@ *} ML {* -fun get_fun_new flag (rty, qty) lthy ty = +fun negF absF = repF + | negF repF = absF + +fun get_fun flag qenv lthy ty = +let + + fun get_fun_aux s fs = + (case (maps_lookup (ProofContext.theory_of lthy) s) of + SOME info => list_comb (Const (#mapfun info, dummyT), fs) + | NONE => error ("no map association for type " ^ s)) + + fun get_const flag qty = + let + val thy = ProofContext.theory_of lthy + val qty_name = Long_Name.base_name (fst (dest_Type qty)) + in + case flag of + absF => Const (Sign.full_bname thy ("ABS_" ^ qty_name), dummyT) + | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT) + end + + fun mk_identity ty = Abs ("", ty, Bound 0) + +in + if (AList.defined (op=) qenv ty) + then (get_const flag ty) + else (case ty of + TFree _ => mk_identity ty + | Type (_, []) => mk_identity ty + | Type ("fun" , [ty1, ty2]) => + let + val fs_ty1 = get_fun (negF flag) qenv lthy ty1 + val fs_ty2 = get_fun flag qenv lthy ty2 + in + get_fun_aux "fun" [fs_ty1, fs_ty2] + end + | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys) + | _ => error ("no type variables allowed")) +end + +(* returns all subterms where two types differ *) +fun diff (T, S) Ds = + case (T, S) of + (TVar v, TVar u) => if v = u then Ds else (T, S)::Ds + | (TFree x, TFree y) => if x = y then Ds else (T, S)::Ds + | (Type (a, Ts), Type (b, Us)) => + if a = b then diffs (Ts, Us) Ds else (T, S)::Ds + | _ => (T, S)::Ds +and diffs (T::Ts, U::Us) Ds = diffs (Ts, Us) (diff (T, U) Ds) + | diffs ([], []) Ds = Ds + | diffs _ _ = error "Unequal length of type arguments" + +*} + +ML {* +fun get_fun_OLD flag (rty, qty) lthy ty = let val tys = find_matching_types rty ty; val qenv = map (fn t => (exchange_ty lthy rty qty t, t)) tys; @@ -657,11 +712,11 @@ fun mk_abs tm = let val ty = fastype_of tm - in Syntax.check_term lthy ((get_fun_new absF (rty, qty) lthy ty) $ tm) end + in Syntax.check_term lthy ((get_fun_OLD absF (rty, qty) lthy ty) $ tm) end fun mk_repabs tm = let val ty = fastype_of tm - in Syntax.check_term lthy ((get_fun_new repF (rty, qty) lthy ty) $ (mk_abs tm)) end + in Syntax.check_term lthy ((get_fun_OLD repF (rty, qty) lthy ty) $ (mk_abs tm)) end fun is_lifted_const (Const (x, _)) = member (op =) consts x | is_lifted_const _ = false; @@ -1008,11 +1063,11 @@ fun mk_rep tm = let val ty = exchange_ty lthy qty rty (fastype_of tm) - in Syntax.check_term lthy ((get_fun_new repF (rty, qty) lthy ty) $ tm) end; + in Syntax.check_term lthy ((get_fun_OLD repF (rty, qty) lthy ty) $ tm) end; fun mk_abs tm = let val ty = fastype_of tm - in Syntax.check_term lthy ((get_fun_new absF (rty, qty) lthy ty) $ tm) end + in Syntax.check_term lthy ((get_fun_OLD absF (rty, qty) lthy ty) $ tm) end val (l, ltl) = Term.strip_type ty; val nl = map absty l; val vs = map (fn _ => "x") l; @@ -1149,7 +1204,6 @@ (******************************************) (* exception for when qtrm and rtrm do not match *) -ML {* exception LIFT_MATCH of string *} ML {* fun mk_resp_arg lthy (rty, qty) = @@ -1161,7 +1215,7 @@ if s = s' then let val SOME map_info = maps_lookup thy s - val args = map (mk_resp_arg lthy) (tys ~~tys') + val args = map (mk_resp_arg lthy) (tys ~~ tys') in list_comb (Const (#relfun map_info, dummyT), args) end @@ -1192,12 +1246,28 @@ fun qnt_typ ty = domain_type (domain_type ty) *} +(* +Regularizing an rterm means: + - Quantifiers over a type that needs lifting are replaced by + bounded quantifiers, for example: + \x. P \ \x\(Respects R). P + - Abstractions over a type that needs lifting are replaced + by bounded abstractions: + \x. P \ Ball (Respects R) (\x. P) + + - Equalities over the type being lifted are replaced by + appropriate relations: + A = B \ A \ B + Example with more complicated types of A, B: + A = B \ (op = \ op \) A B +*) + ML {* -fun REGULARIZE_aux lthy rtrm qtrm = +fun REGULARIZE_trm lthy rtrm qtrm = case (rtrm, qtrm) of (Abs (x, T, t), Abs (x', T', t')) => let - val subtrm = REGULARIZE_aux lthy t t' + val subtrm = REGULARIZE_trm lthy t t' in if T = T' then Abs (x, T, subtrm) @@ -1205,7 +1275,7 @@ end | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => let - val subtrm = apply_subt (REGULARIZE_aux lthy) t t' + val subtrm = apply_subt (REGULARIZE_trm lthy) t t' in if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm @@ -1213,7 +1283,7 @@ end | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => let - val subtrm = apply_subt (REGULARIZE_aux lthy) t t' + val subtrm = apply_subt (REGULARIZE_trm lthy) t t' in if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm @@ -1222,14 +1292,14 @@ (* FIXME: why is there a case for equality? is it correct? *) | (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') => let - val subtrm = REGULARIZE_aux lthy t t' + val subtrm = REGULARIZE_trm lthy t t' in if ty = ty' then Const (@{const_name "op ="}, ty) $ subtrm else mk_resp_arg lthy (ty, ty') $ subtrm end | (t1 $ t2, t1' $ t2') => - (REGULARIZE_aux lthy t1 t1') $ (REGULARIZE_aux lthy t2 t2') + (REGULARIZE_trm lthy t1 t1') $ (REGULARIZE_trm lthy t2 t2') | (Free (x, ty), Free (x', ty')) => if x = x' then rtrm @@ -1246,11 +1316,98 @@ *} ML {* -fun REGULARIZE_trm lthy rtrm qtrm = - REGULARIZE_aux lthy rtrm qtrm - |> Syntax.check_term lthy - +fun mk_REGULARIZE_goal lthy rtrm qtrm = + Logic.mk_implies (rtrm, REGULARIZE_trm lthy rtrm qtrm |> Syntax.check_term lthy) *} +(* +To prove that the old theorem implies the new one, we first +atomize it and then try: + - Reflexivity of the relation + - Assumption + - Elimnating quantifiers on both sides of toplevel implication + - Simplifying implications on both sides of toplevel implication + - Ball (Respects ?E) ?P = All ?P + - (\x. ?R x \ ?P x \ ?Q x) \ All ?P \ Ball ?R ?Q + +*) + +lemma my_equiv_res_forall2: + fixes P::"'a \ bool" + fixes Q::"'b \ bool" + assumes a: "(All Q) \ (All P)" + shows "(All Q) \ Ball (Respects E) P" +using a by auto + +lemma my_equiv_res_exists: + fixes P::"'a \ bool" + fixes Q::"'b \ bool" + assumes a: "EQUIV E" + and b: "(Ex Q) \ (Ex P)" + shows "(Ex Q) \ Bex (Respects E) P" +apply(subst equiv_res_exists) +apply(rule a) +apply(rule b) +done + +ML {* +fun REGULARIZE_tac lthy rel_refl rel_eqv = + ObjectLogic.full_atomize_tac THEN' + REPEAT_ALL_NEW (FIRST' + [rtac rel_refl, + atac, + rtac @{thm universal_twice}, + rtac @{thm impI} THEN' atac, + rtac @{thm implication_twice}, + rtac @{thm my_equiv_res_forall2}, + rtac (rel_eqv RS @{thm my_equiv_res_exists}), + (* For a = b \ a \ b *) + rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl, + rtac @{thm RIGHT_RES_FORALL_REGULAR}]) +*} + +(* same version including debugging information *) +ML {* +fun my_print_tac ctxt s thm = +let + val prems_str = prems_of thm + |> map (Syntax.string_of_term ctxt) + |> cat_lines + val _ = tracing (s ^ "\n" ^ prems_str) +in + Seq.single thm +end + +fun DT ctxt s tac = EVERY' [tac, K (my_print_tac ctxt ("after " ^ s))] +*} + +ML {* +fun REGULARIZE_tac' lthy rel_refl rel_eqv = + (REPEAT1 o FIRST1) + [(K (print_tac "start")) THEN' (K no_tac), + DT lthy "1" (rtac rel_refl), + DT lthy "2" atac, + DT lthy "3" (rtac @{thm universal_twice}), + DT lthy "4" (rtac @{thm impI} THEN' atac), + DT lthy "5" (rtac @{thm implication_twice}), + DT lthy "6" (rtac @{thm my_equiv_res_forall2}), + DT lthy "7" (rtac (rel_eqv RS @{thm my_equiv_res_exists})), + (* For a = b \ a \ b *) + DT lthy "8" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl), + DT lthy "9" (rtac @{thm RIGHT_RES_FORALL_REGULAR})] +*} + +ML {* +fun REGULARIZE_prove rtrm qtrm rel_eqv rel_refl lthy = + let + val goal = mk_REGULARIZE_goal lthy rtrm qtrm + val cthm = Goal.prove lthy [] [] goal + (fn {context, ...} => REGULARIZE_tac context rel_refl rel_eqv 1) + in + cthm + end +*} + + end diff -r 7d3d86beacd6 -r f46dc0ca08c3 quotient.ML --- a/quotient.ML Fri Nov 20 13:03:01 2009 +0100 +++ b/quotient.ML Sat Nov 21 02:49:39 2009 +0100 @@ -1,5 +1,7 @@ signature QUOTIENT = sig + exception LIFT_MATCH of string + val quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state val quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state @@ -9,6 +11,9 @@ structure Quotient: QUOTIENT = struct +(* exception for when quotient and lifted things do not match *) +exception LIFT_MATCH of string + (* wrappers for define, note and theorem_i *) fun define (name, mx, rhs) lthy = let @@ -150,15 +155,17 @@ val _ = tracing ("storing under: " ^ qty_str) val lthy3 = quotdata_update qty_str (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2 (* FIXME: varifyT should not be used *) + (* storing of the equiv_thm under a name *) + val (_, lthy4) = note (Binding.suffix_name "_equiv" qty_name, equiv_thm) lthy3 (* interpretation *) val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list)) - val ((_, [eqn1pre]), lthy4) = Variable.import true [ABS_def] lthy3; + val ((_, [eqn1pre]), lthy5) = Variable.import true [ABS_def] lthy4; val eqn1i = Thm.prop_of (symmetric eqn1pre) - val ((_, [eqn2pre]), lthy5) = Variable.import true [REP_def] lthy4; + val ((_, [eqn2pre]), lthy6) = Variable.import true [REP_def] lthy5; val eqn2i = Thm.prop_of (symmetric eqn2pre) - val exp_morphism = ProofContext.export_morphism lthy5 (ProofContext.init (ProofContext.theory_of lthy5)); + val exp_morphism = ProofContext.export_morphism lthy6 (ProofContext.init (ProofContext.theory_of lthy6)); val exp_term = Morphism.term exp_morphism; val exp = Morphism.thm exp_morphism; @@ -169,14 +176,14 @@ val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true), Expression.Named [("R", rel), ("Abs", abs), ("Rep", rep) ]))] in - lthy5 + lthy6 |> note (quot_thm_name, quot_thm) ||>> note (quotient_thm_name, quotient_thm) ||> Local_Theory.theory (fn thy => let val global_eqns = map exp_term [eqn2i, eqn1i]; (* Not sure if the following context should not be used *) - val (global_eqns2, lthy6) = Variable.import_terms true global_eqns lthy5; + val (global_eqns2, lthy7) = Variable.import_terms true global_eqns lthy6; val global_eqns3 = map (fn t => (bindd, t)) global_eqns2; in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end) end diff -r 7d3d86beacd6 -r f46dc0ca08c3 quotient_def.ML --- a/quotient_def.ML Fri Nov 20 13:03:01 2009 +0100 +++ b/quotient_def.ML Sat Nov 21 02:49:39 2009 +0100 @@ -2,7 +2,7 @@ signature QUOTIENT_DEF = sig datatype flag = absF | repF - val get_fun: flag -> (typ * typ) list -> Proof.context -> typ -> term + val get_fun: flag -> Proof.context -> typ * typ -> term val make_def: binding -> typ -> mixfix -> Attrib.binding -> term -> Proof.context -> (term * thm) * local_theory @@ -10,7 +10,6 @@ local_theory -> (term * thm) * local_theory val quotdef_cmd: (binding * string * mixfix) * (Attrib.binding * string) -> local_theory -> local_theory - val diff: (typ * typ) -> (typ * typ) list -> (typ * typ) list end; structure Quotient_Def: QUOTIENT_DEF = @@ -25,7 +24,6 @@ ((rhs, thm), lthy') end - (* calculates the aggregate abs and rep functions for a given type; repF is for constants' arguments; absF is for constants; function types need to be treated specially, since repF and absF @@ -36,99 +34,65 @@ fun negF absF = repF | negF repF = absF -fun get_fun flag qenv lthy ty = -let - - fun get_fun_aux s fs = - (case (maps_lookup (ProofContext.theory_of lthy) s) of - SOME info => list_comb (Const (#mapfun info, dummyT), fs) - | NONE => error ("no map association for type " ^ s)) - - fun get_const flag qty = - let - val thy = ProofContext.theory_of lthy - val qty_name = Long_Name.base_name (fst (dest_Type qty)) - in - case flag of - absF => Const (Sign.full_bname thy ("ABS_" ^ qty_name), dummyT) - | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT) - end +fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) - fun mk_identity ty = Abs ("", ty, Bound 0) - +fun ty_lift_error lthy rty qty = +let + val rty_str = quote (Syntax.string_of_typ lthy rty) + val qty_str = quote (Syntax.string_of_typ lthy qty) + val msg = ["quotient type", qty_str, "and lifted type", rty_str, "do not match."] in - if (AList.defined (op=) qenv ty) - then (get_const flag ty) - else (case ty of - TFree _ => mk_identity ty - | Type (_, []) => mk_identity ty - | Type ("fun" , [ty1, ty2]) => - let - val fs_ty1 = get_fun (negF flag) qenv lthy ty1 - val fs_ty2 = get_fun flag qenv lthy ty2 - in - get_fun_aux "fun" [fs_ty1, fs_ty2] - end - | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys) - | _ => error ("no type variables allowed")) + raise LIFT_MATCH (space_implode " " msg) end -(* returns all subterms where two types differ *) -fun diff (T, S) Ds = - case (T, S) of - (TVar v, TVar u) => if v = u then Ds else (T, S)::Ds - | (TFree x, TFree y) => if x = y then Ds else (T, S)::Ds - | (Type (a, Ts), Type (b, Us)) => - if a = b then diffs (Ts, Us) Ds else (T, S)::Ds - | _ => (T, S)::Ds -and diffs (T::Ts, U::Us) Ds = diffs (Ts, Us) (diff (T, U) Ds) - | diffs ([], []) Ds = Ds - | diffs _ _ = error "Unequal length of type arguments" +fun get_fun_aux lthy s fs = + case (maps_lookup (ProofContext.theory_of lthy) s) of + SOME info => list_comb (Const (#mapfun info, dummyT), fs) + | NONE => raise LIFT_MATCH ("no map association for type " ^ s) - -(* sanity check that the calculated quotient environment - matches with the stored quotient environment. *) -fun sanity_chk qenv lthy = -let - val global_qenv = Quotient_Info.mk_qenv lthy +fun get_const flag lthy _ qty = +(* FIXME: check here that _ and qty are related *) +let val thy = ProofContext.theory_of lthy + val qty_name = Long_Name.base_name (fst (dest_Type qty)) +in + case flag of + absF => Const (Sign.full_bname thy ("ABS_" ^ qty_name), dummyT) + | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT) +end - fun error_msg lthy (qty, rty) = - let - val qtystr = quote (Syntax.string_of_typ lthy qty) - val rtystr = quote (Syntax.string_of_typ lthy rty) - in - error (implode ["Quotient type ", qtystr, " does not match with ", rtystr]) - end - - fun is_inst (qty, rty) (qty', rty') = - if Sign.typ_instance thy (qty, qty') - then let - val inst = Sign.typ_match thy (qty', qty) Vartab.empty - in - rty = Envir.subst_type inst rty' - end - else false - - fun chk_inst (qty, rty) = - if exists (is_inst (qty, rty)) global_qenv - then true - else error_msg lthy (qty, rty) -in - map chk_inst qenv -end +fun get_fun flag lthy (rty, qty) = + case (rty, qty) of + (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) => + let + val fs_ty1 = get_fun (negF flag) lthy (ty1, ty1') + val fs_ty2 = get_fun flag lthy (ty2, ty2') + in + get_fun_aux lthy "fun" [fs_ty1, fs_ty2] + end + | (Type (s, []), Type (s', [])) => + if s = s' + then mk_identity qty + else get_const flag lthy rty qty + | (Type (s, tys), Type (s', tys')) => + if s = s' + then get_fun_aux lthy s' (map (get_fun flag lthy) (tys ~~ tys')) + else get_const flag lthy rty qty + | (TFree x, TFree x') => + if x = x' + then mk_identity qty + else ty_lift_error lthy rty qty + | (TVar _, TVar _) => raise LIFT_MATCH "no type variables allowed" + | _ => ty_lift_error lthy rty qty fun make_def nconst_bname qty mx attr rhs lthy = let - val (arg_tys, res_ty) = strip_type qty - val rty = fastype_of rhs - val qenv = distinct (op=) (diff (qty, rty) []) - - val _ = sanity_chk qenv lthy - - val rep_fns = map (get_fun repF qenv lthy) arg_tys - val abs_fn = (get_fun absF qenv lthy) res_ty + val (arg_rtys, res_rty) = strip_type rty + val (arg_qtys, res_qty) = strip_type qty + + val rep_fns = map (get_fun repF lthy) (arg_rtys ~~ arg_qtys) + val abs_fn = get_fun absF lthy (res_rty, res_qty) fun mk_fun_map t s = Const (@{const_name "fun_map"}, dummyT) $ t $ s @@ -139,10 +103,9 @@ val ((trm, thm), lthy') = define nconst_bname mx attr absrep_trm lthy val nconst_str = Binding.name_of nconst_bname - val qcinfo = {qconst = trm, rconst = rhs} + fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs} val lthy'' = Local_Theory.declaration true - (fn phi => qconsts_update_generic nconst_str - (qconsts_transfer phi qcinfo)) lthy' + (fn phi => qconsts_update_gen nconst_str (qcinfo phi)) lthy' in ((trm, thm), lthy'') end @@ -186,3 +149,5 @@ end; (* structure *) open Quotient_Def; + + diff -r 7d3d86beacd6 -r f46dc0ca08c3 quotient_info.ML --- a/quotient_info.ML Fri Nov 20 13:03:01 2009 +0100 +++ b/quotient_info.ML Sat Nov 21 02:49:39 2009 +0100 @@ -20,7 +20,7 @@ val qconsts_transfer: morphism -> qconsts_info -> qconsts_info val qconsts_lookup: theory -> string -> qconsts_info option val qconsts_update_thy: string -> qconsts_info -> theory -> theory - val qconsts_update_generic: string -> qconsts_info -> Context.generic -> Context.generic + val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic val print_qconstinfo: Proof.context -> unit end; @@ -147,7 +147,7 @@ val qconsts_lookup = Symtab.lookup o QConstsData.get fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo)) -fun qconsts_update_generic k qcinfo = +fun qconsts_update_gen k qcinfo = Context.mapping (qconsts_update_thy k qcinfo) I fun print_qconstinfo ctxt =