# HG changeset patch # User ballarin # Date 1194281331 -3600 # Node ID 35e954ff67f84bd27e8ea8e7e6605bee869c115f # Parent 774d2dc351617c3c1b5b5d85ed6194a54a81f05b Use of export rather than standard in interpretation. diff -r 774d2dc35161 -r 35e954ff67f8 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Mon Nov 05 17:48:34 2007 +0100 +++ b/src/Pure/Isar/locale.ML Mon Nov 05 17:48:51 2007 +0100 @@ -187,6 +187,35 @@ +(** substitutions on Frees and Vars -- clone from element.ML **) + +(* instantiate types *) + +fun var_instT_type env = + if Vartab.is_empty env then I + else Term.map_type_tvar (fn (x, S) => the_default (TVar (x, S)) (Vartab.lookup env x)); + +fun var_instT_term env = + if Vartab.is_empty env then I + else Term.map_types (var_instT_type env); + +fun var_inst_term (envT, env) = + if Vartab.is_empty env then var_instT_term envT + else + let + val instT = var_instT_type envT; + fun inst (Const (x, T)) = Const (x, instT T) + | inst (Free (x, T)) = Free(x, instT T) + | inst (Var (xi, T)) = + (case Vartab.lookup env xi of + NONE => Var (xi, instT T) + | SOME t => t) + | inst (b as Bound _) = b + | inst (Abs (x, T, t)) = Abs (x, instT T, inst t) + | inst (t $ u) = inst t $ inst u; + in Envir.beta_norm o inst end; + + (** management of registrations in theories and proof contexts **) structure Registrations : @@ -196,12 +225,18 @@ val join: T * T -> T val dest: theory -> T -> (term list * - (((bool * string) * Attrib.src list) * Element.witness list * + (((bool * string) * Attrib.src list) * + (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * + Element.witness list * thm Termtab.table)) list - val lookup: theory -> T * term list -> - (((bool * string) * Attrib.src list) * Element.witness list * - thm Termtab.table) option - val insert: theory -> term list * ((bool * string) * Attrib.src list) -> T -> + val test: theory -> T * term list -> bool + val lookup: theory -> + T * (term list * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) -> + (((bool * string) * Attrib.src list) * + Element.witness list * + thm Termtab.table) option + val insert: theory -> term list -> ((bool * string) * Attrib.src list) -> + (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) -> T -> T * (term list * (((bool * string) * Attrib.src list) * Element.witness list)) list val add_witness: term list -> Element.witness -> T -> T val add_equation: term list -> thm -> T -> T @@ -211,10 +246,15 @@ - parameters and prefix (if the Boolean flag is set, only accesses containing the prefix are generated, otherwise the prefix may be omitted when accessing theorems etc.) + - pair of export and import morphisms, export maps content to its originating + context, import is its inverse - theorems (actually witnesses) instantiating locale assumptions - - theorems (equations) interpreting derived concepts and indexed by lhs + - theorems (equations) interpreting derived concepts and indexed by lhs. + NB: index is exported while content is internalised. *) - type T = (((bool * string) * Attrib.src list) * Element.witness list * + type T = (((bool * string) * Attrib.src list) * + (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * + Element.witness list * thm Termtab.table) Termtab.table; val empty = Termtab.empty; @@ -228,16 +268,16 @@ in ut t [] end; (* joining of registrations: - - prefix and attributes of right theory; + - prefix, attributes and morphisms of right theory; - witnesses are equal, no attempt to subsumption testing; - union of equalities, if conflicting (i.e. two eqns with equal lhs) eqn of right theory takes precedence *) - fun join (r1, r2) = Termtab.join (fn _ => fn ((_, _, e1), (n, w, e2)) => - (n, w, Termtab.join (fn _ => fn (_, e) => e) (e1, e2))) (r1, r2); + fun join (r1, r2) = Termtab.join (fn _ => fn ((_, _, _, e1), (n, m, w, e2)) => + (n, m, w, Termtab.join (fn _ => fn (_, e) => e) (e1, e2))) (r1, r2); fun dest_transfer thy regs = - Termtab.dest regs |> map (apsnd (fn (n, ws, es) => - (n, map (Element.transfer_witness thy) ws, Termtab.map (transfer thy) es))); + Termtab.dest regs |> map (apsnd (fn (n, m, ws, es) => + (n, m, map (Element.transfer_witness thy) ws, Termtab.map (transfer thy) es))); fun dest thy regs = dest_transfer thy regs |> map (apfst untermify); @@ -245,33 +285,37 @@ fun subsumers thy t regs = filter (fn (t', _) => Pattern.matches thy (t', t)) (dest_transfer thy regs); + (* test if registration that subsumes the query is present *) + fun test thy (regs, ts) = + not (null (subsumers thy (termify ts) regs)); + (* look up registration, pick one that subsumes the query *) - fun lookup thy (regs, ts) = + fun lookup thy (regs, (ts, ((impT, _), (imp, _)))) = let val t = termify ts; val subs = subsumers thy t regs; in (case subs of [] => NONE - | ((t', (attn, thms, eqns)) :: _) => + | ((t', ((prfx, atts), (exp', ((impT', domT'), (imp', dom'))), thms, eqns)) :: _) => let val (tinst, inst) = Pattern.match thy (t', t) (Vartab.empty, Vartab.empty); - (* thms contain Frees, not Vars *) - val tinst' = tinst |> Vartab.dest (* FIXME Vartab.map (!?) *) - |> map (fn ((x, 0), (_, T)) => (x, Logic.legacy_unvarifyT T)) - |> Symtab.make; - val inst' = inst |> Vartab.dest - |> map (fn ((x, 0), (_, t)) => (x, Logic.legacy_unvarify t)) - |> Symtab.make; - val inst_morph = Element.inst_morphism thy (tinst', inst'); - in SOME (attn, map (Element.morph_witness inst_morph) thms, - Termtab.map (Morphism.thm inst_morph) eqns) + val tinst' = domT' |> map (fn (T as TFree (x, _)) => + (x, T |> Morphism.typ exp' |> Envir.typ_subst_TVars tinst + |> var_instT_type impT)) |> Symtab.make; + val inst' = dom' |> map (fn (t as Free (x, _)) => + (x, t |> Morphism.term exp' |> Envir.subst_vars (tinst, inst) + |> var_inst_term (impT, imp))) |> Symtab.make; + val inst'_morph = Element.inst_morphism thy (tinst', inst'); + in SOME ((prfx, map (Args.morph_values inst'_morph) atts), + map (Element.morph_witness inst'_morph) thms, + Termtab.map (Morphism.thm inst'_morph) eqns) end) end; (* add registration if not subsumed by ones already present, additionally returns registrations that are strictly subsumed *) - fun insert thy (ts, attn) regs = + fun insert thy ts attn m regs = let val t = termify ts; val subs = subsumers thy t regs ; @@ -279,8 +323,8 @@ [] => let val sups = filter (fn (t', _) => Pattern.matches thy (t, t')) (dest_transfer thy regs); - val sups' = map (apfst untermify) sups |> map (fn (ts, (n, w, d)) => (ts, (n, w))) - in (Termtab.update (t, (attn, [], Termtab.empty)) regs, sups') end + val sups' = map (apfst untermify) sups |> map (fn (ts, (n, _, w, _)) => (ts, (n, w))) + in (Termtab.update (t, (attn, m, [], Termtab.empty)) regs, sups') end | _ => (regs, [])) end; @@ -294,14 +338,14 @@ (* add witness theorem to registration, only if instantiation is exact, otherwise exception Option raised *) fun add_witness ts thm regs = - gen_add (fn thm => fn (x, thms, eqns) => (x, thm::thms, eqns)) ts thm regs; + gen_add (fn thm => fn (x, m, thms, eqns) => (x, m, thm::thms, eqns)) ts thm regs; (* add equation to registration, replaces previous equation with same lhs; only if instantiation is exact, otherwise exception Option raised; exception TERM raised if not a meta equality *) fun add_equation ts thm regs = - gen_add (fn thm => fn (x, thms, eqns) => - (x, thms, Termtab.update (thm |> prop_of |> Logic.dest_equals |> fst, thm) eqns)) + gen_add (fn thm => fn (x, m, thms, eqns) => + (x, m, thms, Termtab.update (thm |> prop_of |> Logic.dest_equals |> fst, thm) eqns)) ts thm regs; end; @@ -389,11 +433,6 @@ (* access registrations *) -(* Ids of global registrations are varified, - Ids of local registrations are not. - Witness thms of registrations are never varified. - Varification of eqns as varification of ids. *) - (* retrieve registration from theory or context *) fun get_registrations ctxt name = @@ -405,25 +444,32 @@ fun get_local_registrations ctxt = get_registrations (Context.Proof ctxt); -fun get_registration ctxt (name, ps) = +fun get_registration ctxt import (name, ps) = case Symtab.lookup (RegistrationsData.get ctxt) name of NONE => NONE - | SOME reg => Registrations.lookup (Context.theory_of ctxt) (reg, ps); + | SOME reg => Registrations.lookup (Context.theory_of ctxt) (reg, (ps, import)); fun get_global_registration thy = get_registration (Context.Theory thy); fun get_local_registration ctxt = get_registration (Context.Proof ctxt); -val test_global_registration = is_some oo get_global_registration; -val test_local_registration = is_some oo get_local_registration; + +fun test_registration ctxt (name, ps) = + case Symtab.lookup (RegistrationsData.get ctxt) name of + NONE => false + | SOME reg => Registrations.test (Context.theory_of ctxt) (reg, ps); + +fun test_global_registration thy = test_registration (Context.Theory thy); +fun test_local_registration ctxt = test_registration (Context.Proof ctxt); + (* add registration to theory or context, ignored if subsumed *) -fun put_registration (name, ps) attn ctxt = +fun put_registration (name, ps) attn morphs ctxt = RegistrationsData.map (fn regs => let val thy = Context.theory_of ctxt; val reg = the_default Registrations.empty (Symtab.lookup regs name); - val (reg', sups) = Registrations.insert thy (ps, attn) reg; + val (reg', sups) = Registrations.insert thy ps attn morphs reg; val _ = if not (null sups) then warning ("Subsumed interpretation(s) of locale " ^ quote (extern thy name) ^ @@ -432,8 +478,10 @@ else (); in Symtab.update (name, reg') regs end) ctxt; -fun put_global_registration id attn = Context.theory_map (put_registration id attn); -fun put_local_registration id attn = Context.proof_map (put_registration id attn); +fun put_global_registration id attn morphs = + Context.theory_map (put_registration id attn morphs); +fun put_local_registration id attn morphs = + Context.proof_map (put_registration id attn morphs); fun put_registration_in_locale name id = @@ -493,11 +541,11 @@ fun prt_witns [] = Pretty.str "no witnesses." | prt_witns witns = Pretty.block (Pretty.str "witnesses:" :: Pretty.brk 1 :: Pretty.breaks (map (Element.pretty_witness ctxt) witns)) - fun prt_reg (ts, (((_, ""), []), witns, eqns)) = + fun prt_reg (ts, (((_, ""), []), _, witns, eqns)) = if show_wits then Pretty.block (prt_core ts eqns @ [Pretty.fbrk, prt_witns witns]) else Pretty.block (prt_core ts eqns) - | prt_reg (ts, (attn, witns, eqns)) = + | prt_reg (ts, (attn, _, witns, eqns)) = if show_wits then Pretty.block ((prt_attn attn @ [Pretty.str ":", Pretty.brk 1] @ prt_core ts eqns @ [Pretty.fbrk, prt_witns witns])) @@ -512,7 +560,7 @@ NONE => Pretty.str ("no interpretations") | SOME r => let val r' = Registrations.dest thy r; - val r'' = Library.sort_wrt (fn (_, (((_, prfx), _), _, _)) => prfx) r'; + val r'' = Library.sort_wrt (fn (_, (((_, prfx), _), _, _, _)) => prfx) r'; in Pretty.big_list ("interpretations:") (map prt_reg r'') end) |> Pretty.writeln end; @@ -960,7 +1008,8 @@ val ps' = map (fn (n, SOME T) => Free (n, T)) ps; in if test_local_registration ctxt' (name, ps') then ctxt' else let - val ctxt'' = put_local_registration (name, ps') ((true, ""), []) ctxt' + val ctxt'' = put_local_registration (name, ps') ((true, ""), []) + (Morphism.identity, ((Vartab.empty, []), (Vartab.empty, []) )) ctxt' in case mode of Assumed axs => fold (add_local_witness (name, ps') o @@ -1557,7 +1606,7 @@ registration; requires parameters and flattened list of identifiers instead of recomputing it from the target *) -fun collect_global_witnesses thy parms ids vts = let +fun collect_global_witnesses thy import parms ids vts = let val ts = map Logic.unvarify vts; val (parms, parmTs) = split_list parms; val parmvTs = map Logic.varifyT parmTs; @@ -1570,16 +1619,54 @@ val inst = Symtab.make (parms ~~ ts); val inst_ids = map (apfst (apsnd vinst_names)) ids; val assumed_ids' = map_filter (fn (id, (_, Assumed _)) => SOME id | _ => NONE) inst_ids; - val wits = maps (#2 o the o get_global_registration thy) assumed_ids'; + val wits = maps (#2 o the o get_global_registration thy import) assumed_ids'; val ids' = map fst inst_ids; val eqns = - fold_map (join_eqns (get_global_registration thy) I (ProofContext.init thy)) + fold_map (join_eqns (get_global_registration thy import) I (ProofContext.init thy)) ids' Termtab.empty |> snd |> Termtab.dest |> map snd; - - val tinst' = fold (Sign.typ_match thy) (parmvTs ~~ map Term.fastype_of vts) Vartab.empty - |> Vartab.dest |> map (fn ((x, 0), (_, T)) => (x, T)) |> Symtab.make; - in ((tinst', vinst), (tinst, inst), wits, eqns) end; + in ((tinst, inst), wits, eqns) end; + + +(* standardise export morphism *) + +(* clone from Element.generalize_facts *) +fun standardize thy export facts = + let + val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export; + val exp_term = TermSubst.zero_var_indexes o Morphism.term export; + (* FIXME sync with exp_fact *) + val exp_typ = Logic.type_map exp_term; + val morphism = + Morphism.morphism {name = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact}; + in Element.facts_map (Element.morph_ctxt morphism) facts end; + + +(* suppress application of name morphism: workaroud for class package *) (* FIXME *) + +fun morph_ctxt' phi = Element.map_ctxt + {name = I, + var = Morphism.var phi, + typ = Morphism.typ phi, + term = Morphism.term phi, + fact = Morphism.fact phi, + attrib = Args.morph_values phi}; + + +(* compute morphism and apply to args *) + +fun interpret_args thy prfx insts prems eqns atts2 exp attrib args = + let + val inst = Morphism.name_morphism (NameSpace.qualified prfx) $> + Element.inst_morphism thy insts $> Element.satisfy_morphism prems $> + Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $> + Morphism.thm_morphism (MetaSimplifier.rewrite_rule eqns) + in + args |> Element.facts_map (morph_ctxt' inst) |> + map (fn (attn, bs) => (attn, + bs |> map (fn (ths, atts) => (ths, (atts @ atts2))))) |> + standardize thy exp |> Attrib.map_facts attrib + end; (* store instantiations of args for all registered interpretations @@ -1592,27 +1679,13 @@ (([], Symtab.empty), Expr (Locale target)) |> fst |> fst; val regs = get_global_registrations thy target; - (* add args to thy for all registrations *) - fun activate (vts, (((fully_qualified, prfx), atts2), _, _)) thy = + fun activate (vts, (((fully_qualified, prfx), atts2), (exp, imp), _, _)) thy = let - val (vinsts, insts, prems, eqns) = collect_global_witnesses thy parms ids vts; + val (insts, prems, eqns) = collect_global_witnesses thy imp parms ids vts; val attrib = Attrib.attribute_i thy; - val inst_atts = Args.morph_values - (Morphism.name_morphism (NameSpace.qualified prfx) $> - Element.inst_morphism' thy vinsts insts $> - Element.satisfy_morphism prems $> - Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $> - Morphism.thm_morphism (MetaSimplifier.rewrite_rule eqns #> Drule.standard)); - val inst_thm = - Element.inst_thm thy insts #> Element.satisfy_thm prems #> - MetaSimplifier.rewrite_rule eqns #> - Drule.standard; - val args' = args |> map (fn ((name, atts), bs) => - ((name, map (attrib o inst_atts) atts), - bs |> map (fn (ths, more_atts) => - (map inst_thm ths, map attrib (map inst_atts more_atts @ atts2))))); + val args' = interpret_args thy prfx insts prems eqns atts2 exp attrib args; in global_note_prefix_i kind (fully_qualified, prfx) args' thy |> snd end; in fold activate regs thy end; @@ -1941,17 +2014,16 @@ let val thy = ProofContext.theory_of ctxt; fun get registrations = Symtab.fold (fn (_, regs) => fn thms => - (Registrations.dest thy regs |> map (fn (_, (_, wits, _)) => - map Element.conclude_witness wits) |> flat) @ thms) + (Registrations.dest thy regs |> map (fn (_, (_, (exp, _), wits, _)) => + map (Element.conclude_witness #> Morphism.thm exp) wits) |> flat) @ thms) registrations []; in get (RegistrationsData.get (Context.Proof ctxt)) end; -(* FIXME: proper varification *) in fun intro_locales_tac eager ctxt facts st = let - val wits = all_witnesses ctxt |> map Thm.varifyT; + val wits = all_witnesses ctxt; val thy = ProofContext.theory_of ctxt; val intros = locale_base_intros thy @ (if eager then locale_assm_intros thy else []); in @@ -1985,45 +2057,33 @@ TableFun(type key = string * term list val ord = prod_ord string_ord (list_ord Term.fast_term_ord)); -fun gen_activate_facts_elemss mk_ctxt get_reg note note_interp attrib std put_reg add_wit add_eqn - attn all_elemss new_elemss propss eq_attns thmss thy_ctxt = +fun gen_activate_facts_elemss mk_ctxt get_reg note note_interp attrib put_reg add_wit add_eqn + attn all_elemss new_elemss propss eq_attns (exp, imp) thmss thy_ctxt = let val ctxt = mk_ctxt thy_ctxt; val (propss, eq_props) = chop (length new_elemss) propss; val (thmss, eq_thms) = chop (length new_elemss) thmss; - fun activate_elem eqns disch ((fully_qualified, prfx), atts) (Notes (kind, facts)) thy_ctxt = + fun activate_elem prems eqns exp ((fully_qualified, prfx), atts) (Notes (kind, facts)) thy_ctxt = let val ctxt = mk_ctxt thy_ctxt; - val fact_morphism = - Morphism.name_morphism (NameSpace.qualified prfx) - $> Morphism.term_morphism (MetaSimplifier.rewrite_term - (ProofContext.theory_of ctxt) eqns []) - $> Morphism.thm_morphism (disch #> MetaSimplifier.rewrite_rule eqns); - val facts' = facts - (* discharge hyps in attributes *) - |> Attrib.map_facts - (attrib thy_ctxt o Args.morph_values fact_morphism) - (* append interpretation attributes *) - |> map (apfst (apsnd (fn a => a @ map (attrib thy_ctxt) atts))) - (* discharge hyps *) - |> map (apsnd (map (apfst (map disch)))) - (* unfold eqns *) - |> map (apsnd (map (apfst (map (MetaSimplifier.rewrite_rule eqns))))) + val facts' = interpret_args (ProofContext.theory_of ctxt) prfx + (Symtab.empty, Symtab.empty) prems eqns atts + exp (attrib thy_ctxt) facts; in snd (note_interp kind (fully_qualified, prfx) facts' thy_ctxt) end - | activate_elem _ _ _ _ thy_ctxt = thy_ctxt; - - fun activate_elems eqns disch ((id, _), elems) thy_ctxt = + | activate_elem _ _ _ _ _ thy_ctxt = thy_ctxt; + + fun activate_elems prems eqns exp ((id, _), elems) thy_ctxt = let - val (prfx_atts, _, _) = case get_reg thy_ctxt id + val (prfx_atts, _, _) = case get_reg thy_ctxt imp id of SOME x => x | NONE => sys_error ("Unknown registration of " ^ quote (fst id) ^ " while activating facts."); - in fold (activate_elem (the (Idtab.lookup eqns id)) disch prfx_atts) elems thy_ctxt end; + in fold (activate_elem prems (the (Idtab.lookup eqns id)) exp prfx_atts) elems thy_ctxt end; val thy_ctxt' = thy_ctxt (* add registrations *) - |> fold (fn ((id, _), _) => put_reg id attn) new_elemss + |> fold (fn ((id, _), _) => put_reg id attn (exp, imp)) new_elemss (* add witnesses of Assumed elements (only those generate proof obligations) *) |> fold (fn (id, thms) => fold (add_wit id) thms) (map fst propss ~~ thmss) (* add equations *) @@ -2032,25 +2092,22 @@ Element.conclude_witness) eq_thms); val prems = flat (map_filter - (fn ((id, Assumed _), _) => Option.map #2 (get_reg thy_ctxt' id) + (fn ((id, Assumed _), _) => Option.map #2 (get_reg thy_ctxt' imp id) | ((_, Derived _), _) => NONE) all_elemss); - val satisfy = Element.satisfy_morphism prems; val thy_ctxt'' = thy_ctxt' (* add witnesses of Derived elements *) - |> fold (fn (id, thms) => fold (add_wit id o Element.morph_witness satisfy) thms) + |> fold (fn (id, thms) => fold (add_wit id o Element.morph_witness (Element.satisfy_morphism prems)) thms) (map_filter (fn ((_, Assumed _), _) => NONE | ((id, Derived thms), _) => SOME (id, thms)) new_elemss) (* Accumulate equations *) val all_eqns = - fold_map (join_eqns (get_reg thy_ctxt'') (fst o fst) ctxt) all_elemss Termtab.empty + fold_map (join_eqns (get_reg thy_ctxt'' imp) (fst o fst) ctxt) all_elemss Termtab.empty |> fst |> map (apsnd (map snd o Termtab.dest)) |> (fn xs => fold Idtab.update xs Idtab.empty) (* Idtab.make wouldn't work here: can have conflicting duplicates, because instantiation may equate ids and equations are accumulated! *) - - val disch' = std o Morphism.thm satisfy; (* FIXME *) in thy_ctxt'' (* add equations *) @@ -2060,21 +2117,16 @@ [([Element.conclude_witness thm], [])])] #> snd) (attns ~~ thms)) (unflat eq_thms eq_attns ~~ eq_thms) (* add facts *) - |> fold (activate_elems all_eqns disch') new_elemss + |> fold (activate_elems prems all_eqns exp) new_elemss end; fun global_activate_facts_elemss x = gen_activate_facts_elemss ProofContext.init - (fn thy => fn (name, ps) => - get_global_registration thy (name, map Logic.varify ps)) + get_global_registration PureThy.note_thmss_i global_note_prefix_i - Attrib.attribute_i Drule.standard - (fn (name, ps) => put_global_registration (name, map Logic.varify ps)) - (fn (n, ps) => add_global_witness (n, map Logic.varify ps) o - Element.map_witness (fn (t, th) => (Logic.legacy_unvarify t, legacy_unvarify th)) - (* FIXME *)) - (fn (n, ps) => add_global_equation (n, map Logic.varify ps)) + Attrib.attribute_i + put_global_registration add_global_witness add_global_equation x; fun local_activate_facts_elemss x = gen_activate_facts_elemss @@ -2082,7 +2134,7 @@ get_local_registration ProofContext.note_thmss_i local_note_prefix_i - (Attrib.attribute_i o ProofContext.theory_of) I + (Attrib.attribute_i o ProofContext.theory_of) put_local_registration add_local_witness add_local_equation @@ -2112,20 +2164,34 @@ val given_insts' = map (parse_term ctxt) given_insts; val eqns' = map (parse_prop ctxt) eqns; - (* type inference etc. *) - val res = Syntax.check_terms ctxt - (type_parms @ - map2 TypeInfer.constrain given_parm_types given_insts' @ - eqns'); + (* type inference and contexts *) + val arg = type_parms @ map2 TypeInfer.constrain given_parm_types given_insts' @ eqns'; + val res = Syntax.check_terms ctxt arg; val ctxt' = ctxt |> fold Variable.auto_fixes res; - (* results *) + (* instantiation *) val (type_parms'', res') = chop (length type_parms) res; val (given_insts'', eqns'') = chop (length given_insts) res'; val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms''); val inst = Symtab.make (given_parm_names ~~ given_insts''); - val standard = Variable.export_morphism ctxt' ctxt; - in ((instT, inst), eqns'') end; + + (* export from eigencontext *) + val export = Variable.export_morphism ctxt' ctxt; + + (* import, its inverse *) + val domT = fold Term.add_tfrees res [] |> map TFree; + val importT = domT |> map (fn x => (Morphism.typ export x, x)) + |> map_filter (fn (TFree _, _) => NONE (* fixed point of export *) + | (TVar y, x) => SOME (fst y, x) + | _ => error "internal: illegal export in interpretation") + |> Vartab.make; + val dom = fold Term.add_frees res [] |> map Free; + val import = dom |> map (fn x => (Morphism.term export x, x)) + |> map_filter (fn (Free _, _) => NONE (* fixed point of export *) + | (Var y, x) => SOME (fst y, x) + | _ => error "internal: illegal export in interpretation") + |> Vartab.make; + in (((instT, inst), eqns''), (export, ((importT, domT), (import, dom)))) end; val read_instantiations = prep_instantiations Syntax.parse_term Syntax.parse_prop; val check_instantiations = prep_instantiations (K I) (K I); @@ -2162,7 +2228,7 @@ (* read or certify instantiation *) val (raw_insts', raw_eqns) = raw_insts; val (raw_eq_attns, raw_eqns') = split_list raw_eqns; - val ((instT, inst1), eqns) = prep_insts ctxt parms (raw_insts', raw_eqns'); + val (((instT, inst1), eqns), morphs) = prep_insts ctxt parms (raw_insts', raw_eqns'); val eq_attns = map prep_attn raw_eq_attns; (* defined params without given instantiation *) @@ -2187,14 +2253,13 @@ val (_, all_elemss') = chop (length raw_params_elemss) all_elemss (* instantiate ids and elements *) val inst_elemss = (ids' ~~ all_elemss') |> map (fn (((n, ps), _), ((_, mode), elems)) => - ((n, map (Morphism.term inst_morphism) ps), + ((n, map (Morphism.term (inst_morphism $> fst morphs)) ps), map (fn Int e => Element.morph_ctxt inst_morphism e) elems) |> apfst (fn id => (id, map_mode (map (Element.morph_witness inst_morphism)) mode))); (* remove fragments already registered with theory or context *) val new_inst_elemss = filter_out (fn ((id, _), _) => test_reg thy_ctxt id) inst_elemss; -(* val new_ids = map #1 new_inst_elemss; *) (* equations *) val eqn_elems = if null eqns then [] @@ -2202,10 +2267,10 @@ val propss = map extract_asms_elems new_inst_elemss @ eqn_elems; - in (propss, activate attn inst_elemss new_inst_elemss propss eq_attns) end; + in (propss, activate attn inst_elemss new_inst_elemss propss eq_attns morphs) end; fun gen_prep_global_registration mk_ctxt = gen_prep_registration ProofContext.init - (fn thy => fn (name, ps) => test_global_registration thy (name, map Logic.varify ps)) + test_global_registration global_activate_facts_elemss mk_ctxt; fun gen_prep_local_registration mk_ctxt = gen_prep_registration I @@ -2261,9 +2326,9 @@ |> fold (add_witness_in_locale target id) thms | activate_id _ thy = thy; - fun activate_reg (vts, (((fully_qualified, prfx), atts2), _, _)) thy = + fun activate_reg (vts, (((fully_qualified, prfx), atts2), (exp, imp), _, _)) thy = let - val (vinsts, insts, wits, _) = collect_global_witnesses thy fixed target_ids vts; + val (insts, wits, _) = collect_global_witnesses thy imp fixed target_ids vts; fun inst_parms ps = map (the o AList.lookup (op =) (map #1 fixed ~~ vts)) ps; val disch = Element.satisfy_thm wits; @@ -2276,9 +2341,9 @@ if test_global_registration thy (name, ps') then thy else thy - |> put_global_registration (name, ps') ((fully_qualified, prfx), atts2) + |> put_global_registration (name, ps') ((fully_qualified, prfx), atts2) (exp, imp) |> fold (fn witn => fn thy => add_global_witness (name, ps') - (Element.morph_witness (Element.inst_morphism' thy vinsts insts) witn) thy) thms + (Element.morph_witness (Element.inst_morphism thy insts) witn) thy) thms end; fun activate_derived_id ((_, Assumed _), _) thy = thy @@ -2288,7 +2353,7 @@ if test_global_registration thy (name, ps') then thy else thy - |> put_global_registration (name, ps') ((fully_qualified, prfx), atts2) + |> put_global_registration (name, ps') ((fully_qualified, prfx), atts2) (exp, imp) |> fold (fn witn => fn thy => add_global_witness (name, ps') (witn |> Element.map_witness (fn (t, th) => (* FIXME *) (Element.inst_term insts t,