# HG changeset patch # User ballarin # Date 1220369480 -7200 # Node ID 914183e229e95fa6e7b368cb15979d5ed716f71e # Parent a05ca48ef263bdc990b38f88428bb0402d4018b2 Interpretation commands no longer accept interpretation attributes. diff -r a05ca48ef263 -r 914183e229e9 NEWS --- a/NEWS Tue Sep 02 16:55:33 2008 +0200 +++ b/NEWS Tue Sep 02 17:31:20 2008 +0200 @@ -24,10 +24,13 @@ * Dropped "locale (open)". INCOMPATBILITY. -* Command 'interpretation' no longer attempts to simplify goal. +* Interpretation commands no longer attempt to simplify goal. INCOMPATIBILITY: in rare situations the generated goal differs. Use methods intro_locales and unfold_locales to clarify. +* Interpretation commands no longer accept interpretation attributes. +INCOMPATBILITY. + * Command 'instance': attached definitions no longer accepted. INCOMPATIBILITY, use proper 'instantiation' target. diff -r a05ca48ef263 -r 914183e229e9 doc-src/IsarRef/Thy/Spec.thy --- a/doc-src/IsarRef/Thy/Spec.thy Tue Sep 02 16:55:33 2008 +0200 +++ b/doc-src/IsarRef/Thy/Spec.thy Tue Sep 02 17:31:20 2008 +0200 @@ -468,7 +468,7 @@ ; instantiation: ('[' (inst+) ']')? ; - interp: thmdecl? \\ (contextexpr instantiation | + interp: (name ':')? \\ (contextexpr instantiation | name instantiation 'where' (thmdecl? prop + 'and')) ; \end{rail} @@ -497,18 +497,18 @@ restricted to a locale name. The command is aware of interpretations already active in the - theory. No proof obligations are generated for those, neither is - post-processing applied to their facts. This avoids duplication of - interpreted facts, in particular. Note that, in the case of a - locale with import, parts of the interpretation may already be - active. The command will only generate proof obligations and - process facts for new parts. + theory, but does not simplify the goal automatically. In order to + simplify the proof obligations use methods @{method intro_locales} + or @{method unfold_locales}. Post-processing is not applied to + facts of interpretations that are already active. This avoids + duplication of interpreted facts, in particular. Note that, in the + case of a locale with import, parts of the interpretation may + already be active. The command will only process facts for new + parts. - The context expression may be preceded by a name and/or attributes. - These take effect in the post-processing of facts. The name is used - to prefix fact names, for example to avoid accidental hiding of - other facts. Attributes are applied after attributes of the - interpreted facts. + The context expression may be preceded by a name, which takes effect + in the post-processing of facts. It is used to prefix fact names, + for example to avoid accidental hiding of other facts. Adding facts to locales has the effect of adding interpreted facts to the theory for all active interpretations also. That is, diff -r a05ca48ef263 -r 914183e229e9 doc-src/IsarRef/Thy/document/Spec.tex --- a/doc-src/IsarRef/Thy/document/Spec.tex Tue Sep 02 16:55:33 2008 +0200 +++ b/doc-src/IsarRef/Thy/document/Spec.tex Tue Sep 02 17:31:20 2008 +0200 @@ -481,7 +481,7 @@ ; instantiation: ('[' (inst+) ']')? ; - interp: thmdecl? \\ (contextexpr instantiation | + interp: (name ':')? \\ (contextexpr instantiation | name instantiation 'where' (thmdecl? prop + 'and')) ; \end{rail} @@ -509,18 +509,18 @@ restricted to a locale name. The command is aware of interpretations already active in the - theory. No proof obligations are generated for those, neither is - post-processing applied to their facts. This avoids duplication of - interpreted facts, in particular. Note that, in the case of a - locale with import, parts of the interpretation may already be - active. The command will only generate proof obligations and - process facts for new parts. + theory, but does not simplify the goal automatically. In order to + simplify the proof obligations use methods \hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}} + or \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}. Post-processing is not applied to + facts of interpretations that are already active. This avoids + duplication of interpreted facts, in particular. Note that, in the + case of a locale with import, parts of the interpretation may + already be active. The command will only process facts for new + parts. - The context expression may be preceded by a name and/or attributes. - These take effect in the post-processing of facts. The name is used - to prefix fact names, for example to avoid accidental hiding of - other facts. Attributes are applied after attributes of the - interpreted facts. + The context expression may be preceded by a name, which takes effect + in the post-processing of facts. It is used to prefix fact names, + for example to avoid accidental hiding of other facts. Adding facts to locales has the effect of adding interpreted facts to the theory for all active interpretations also. That is, diff -r a05ca48ef263 -r 914183e229e9 src/FOL/ex/LocaleTest.thy --- a/src/FOL/ex/LocaleTest.thy Tue Sep 02 16:55:33 2008 +0200 +++ b/src/FOL/ex/LocaleTest.thy Tue Sep 02 17:31:20 2008 +0200 @@ -82,12 +82,12 @@ locale IL locale IM = fixes a and b and c -interpretation test [simp]: IL + IM a b c [x y z] . +interpretation test: IL + IM a b c [x y z] . print_interps IL (* output: test *) print_interps IM (* output: test *) -interpretation test [simp]: IL print_interps IM . +interpretation test: IL print_interps IM . interpretation IL . @@ -252,12 +252,6 @@ locale IL11 = notes rev_conjI = conjI [THEN iffD1 [OF conj_commute]] -lemma "[| P; Q |] ==> P & Q" -proof - - interpret [intro]: IL11 . txt {* Attribute supplied at instantiation. *} - assume Q and P - then show "P & Q" .. -qed subsection {* Simple locale with assumptions *} diff -r a05ca48ef263 -r 914183e229e9 src/HOL/Algebra/IntRing.thy --- a/src/HOL/Algebra/IntRing.thy Tue Sep 02 16:55:33 2008 +0200 +++ b/src/HOL/Algebra/IntRing.thy Tue Sep 02 17:31:20 2008 +0200 @@ -204,7 +204,7 @@ "(True ==> PROP R) == PROP R" by simp_all -interpretation int [unfolded UNIV]: +interpretation int (* FIXME [unfolded UNIV] *) : partial_order ["(| carrier = UNIV::int set, eq = op =, le = op \ |)"] where "carrier (| carrier = UNIV::int set, eq = op =, le = op \ |) = UNIV" and "le (| carrier = UNIV::int set, eq = op =, le = op \ |) x y = (x \ y)" @@ -220,7 +220,7 @@ by (simp add: lless_def) auto qed -interpretation int [unfolded UNIV]: +interpretation int (* FIXME [unfolded UNIV] *) : lattice ["(| carrier = UNIV::int set, eq = op =, le = op \ |)"] where "join (| carrier = UNIV::int set, eq = op =, le = op \ |) x y = max x y" and "meet (| carrier = UNIV::int set, eq = op =, le = op \ |) x y = min x y" @@ -246,7 +246,7 @@ done qed -interpretation int [unfolded UNIV]: +interpretation int (* [unfolded UNIV] *) : total_order ["(| carrier = UNIV::int set, eq = op =, le = op \ |)"] by unfold_locales clarsimp diff -r a05ca48ef263 -r 914183e229e9 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Tue Sep 02 16:55:33 2008 +0200 +++ b/src/Pure/Isar/class.ML Tue Sep 02 17:31:20 2008 +0200 @@ -373,7 +373,7 @@ in thy |> fold2 add_constraint (map snd consts) no_constraints - |> prove_interpretation tac ((false, prfx), []) (Locale.Locale class) + |> prove_interpretation tac (false, prfx) (Locale.Locale class) (inst, map (fn def => (Attrib.no_binding, def)) defs) |> fold2 add_constraint (map snd consts) constraints end; diff -r a05ca48ef263 -r 914183e229e9 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Tue Sep 02 16:55:33 2008 +0200 +++ b/src/Pure/Isar/isar_syn.ML Tue Sep 02 17:31:20 2008 +0200 @@ -390,24 +390,26 @@ (begin ? Toplevel.print) o Toplevel.begin_local_theory begin (Locale.add_locale "" name expr elems #-> TheoryTarget.begin))); +val opt_prefix = Scan.optional (P.binding --| P.$$$ ":") Name.no_binding; + val _ = OuterSyntax.command "interpretation" "prove and register interpretation of locale expression in theory or locale" K.thy_goal (P.xname --| (P.$$$ "\\" || P.$$$ "<") -- P.!!! SpecParse.locale_expr >> (Toplevel.print oo (Toplevel.theory_to_proof o Locale.interpretation_in_locale I)) || - SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts - >> (fn (((name, atts), expr), insts) => Toplevel.print o + opt_prefix -- SpecParse.locale_expr -- SpecParse.locale_insts + >> (fn ((name, expr), insts) => Toplevel.print o Toplevel.theory_to_proof - (Locale.interpretation I ((true, Name.name_of name), atts) expr insts))); + (Locale.interpretation I (true, Name.name_of name) expr insts))); val _ = OuterSyntax.command "interpret" "prove and register interpretation of locale expression in proof context" (K.tag_proof K.prf_goal) - (SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts - >> (fn (((name, atts), expr), insts) => Toplevel.print o + (opt_prefix -- SpecParse.locale_expr -- SpecParse.locale_insts + >> (fn ((name, expr), insts) => Toplevel.print o Toplevel.proof' - (Locale.interpret Seq.single ((true, Name.name_of name), atts) expr insts))); + (Locale.interpret Seq.single (true, Name.name_of name) expr insts))); (* classes *) diff -r a05ca48ef263 -r 914183e229e9 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Tue Sep 02 16:55:33 2008 +0200 +++ b/src/Pure/Isar/locale.ML Tue Sep 02 17:31:20 2008 +0200 @@ -97,21 +97,21 @@ val add_declaration: string -> declaration -> Proof.context -> Proof.context val interpretation_i: (Proof.context -> Proof.context) -> - (bool * string) * Attrib.src list -> expr -> + bool * string -> expr -> term option list * (Attrib.binding * term) list -> theory -> Proof.state val interpretation: (Proof.context -> Proof.context) -> - (bool * string) * Attrib.src list -> expr -> + bool * string -> expr -> string option list * (Attrib.binding * string) list -> theory -> Proof.state val interpretation_in_locale: (Proof.context -> Proof.context) -> xstring * expr -> theory -> Proof.state val interpret_i: (Proof.state -> Proof.state Seq.seq) -> - (bool * string) * Attrib.src list -> expr -> + bool * string -> expr -> term option list * (Attrib.binding * term) list -> bool -> Proof.state -> Proof.state val interpret: (Proof.state -> Proof.state Seq.seq) -> - (bool * string) * Attrib.src list -> expr -> + bool * string -> expr -> string option list * (Attrib.binding * string) list -> bool -> Proof.state -> Proof.state end; @@ -202,7 +202,7 @@ (** management of registrations in theories and proof contexts **) type registration = - {attn: (bool * string) * Attrib.src list, + {prfx: bool * string, (* 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.) *) @@ -223,20 +223,18 @@ val join: T * T -> T val dest: theory -> T -> (term list * - (((bool * string) * Attrib.src list) * + ((bool * string) * (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Element.witness list * thm Termtab.table)) list 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) -> + ((bool * string) * Element.witness list * thm Termtab.table) option + val insert: theory -> term list -> (bool * string) -> (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 + T * (term list * ((bool * string) * Element.witness list)) list val add_witness: term list -> Element.witness -> T -> T val add_equation: term list -> thm -> T -> T end = @@ -245,14 +243,14 @@ NB: index is exported whereas content is internalised. *) type T = registration Termtab.table; - fun mk_reg attn exp imp wits eqns = - {attn = attn, exp = exp, imp = imp, wits = wits, eqns = eqns}; + fun mk_reg prfx exp imp wits eqns = + {prfx = prfx, exp = exp, imp = imp, wits = wits, eqns = eqns}; fun map_reg f reg = let - val {attn, exp, imp, wits, eqns} = reg; - val (attn', exp', imp', wits', eqns') = f (attn, exp, imp, wits, eqns); - in mk_reg attn' exp' imp' wits' eqns' end; + val {prfx, exp, imp, wits, eqns} = reg; + val (prfx', exp', imp', wits', eqns') = f (prfx, exp, imp, wits, eqns); + in mk_reg prfx' exp' imp' wits' eqns' end; val empty = Termtab.empty; @@ -265,11 +263,11 @@ in ut t [] end; (* joining of registrations: - - prefix, attributes and morphisms of right theory; + - prefix 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 ({eqns = e1, ...}, {attn = n, exp, imp, wits = w, eqns = e2}) => + fun join (r1, r2) = Termtab.join (fn _ => fn ({eqns = e1, ...}, {prfx = n, exp, imp, wits = w, eqns = e2}) => mk_reg n exp imp w (Termtab.join (fn _ => fn (_, e) => e) (e1, e2))) (r1, r2); fun dest_transfer thy regs = @@ -277,7 +275,7 @@ (n, e, i, map (Element.transfer_witness thy) ws, Termtab.map (transfer thy) es)))); fun dest thy regs = dest_transfer thy regs |> map (apfst untermify) |> - map (apsnd (fn {attn, exp, imp, wits, eqns} => (attn, (exp, imp), wits, eqns))); + map (apsnd (fn {prfx, exp, imp, wits, eqns} => (prfx, (exp, imp), wits, eqns))); (* registrations that subsume t *) fun subsumers thy t regs = @@ -295,7 +293,7 @@ in (case subs of [] => NONE - | ((t', {attn = (prfx, atts), exp = exp', imp = ((impT', domT'), (imp', dom')), wits, eqns}) :: _) => + | ((t', {prfx, exp = exp', imp = ((impT', domT'), (imp', dom')), wits, eqns}) :: _) => let val (tinst, inst) = Pattern.match thy (t', t) (Vartab.empty, Vartab.empty); val tinst' = domT' |> map (fn (T as TFree (x, _)) => @@ -305,7 +303,7 @@ (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), + in SOME (prfx, map (Element.morph_witness inst'_morph) wits, Termtab.map (Morphism.thm inst'_morph) eqns) end) @@ -313,7 +311,7 @@ (* add registration if not subsumed by ones already present, additionally returns registrations that are strictly subsumed *) - fun insert thy ts attn (exp, imp) regs = + fun insert thy ts prfx (exp, imp) regs = let val t = termify ts; val subs = subsumers thy t regs ; @@ -321,8 +319,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, {attn, wits, ...}) => (ts, (attn, wits))) - in (Termtab.update (t, mk_reg attn exp imp [] Termtab.empty) regs, sups') end + val sups' = map (apfst untermify) sups |> map (fn (ts, {prfx, wits, ...}) => (ts, (prfx, wits))) + in (Termtab.update (t, mk_reg prfx exp imp [] Termtab.empty) regs, sups') end | _ => (regs, [])) end; @@ -458,24 +456,24 @@ (* add registration to theory or context, ignored if subsumed *) -fun put_registration (name, ps) attn morphs (* wits *) ctxt = +fun put_registration (name, ps) prfx morphs (* wits *) 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 morphs (* wits *) reg; + val (reg', sups) = Registrations.insert thy ps prfx morphs (* wits *) reg; val _ = if not (null sups) then warning ("Subsumed interpretation(s) of locale " ^ quote (extern thy name) ^ "\nwith the following prefix(es):" ^ - commas_quote (map (fn (_, (((_, s), _), _)) => s) sups)) + commas_quote (map (fn (_, ((_, s), _)) => s) sups)) else (); in Symtab.update (name, reg') regs end) ctxt; -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_global_registration id prfx morphs = + Context.theory_map (put_registration id prfx morphs); +fun put_local_registration id prfx morphs = + Context.proof_map (put_registration id prfx morphs); fun put_registration_in_locale name id = @@ -522,11 +520,8 @@ val prt_thm = prt_term o prop_of; fun prt_inst ts = Pretty.enclose "(" ")" (Pretty.breaks (map prt_term' ts)); - fun prt_attn ((false, prfx), atts) = - Pretty.breaks (Pretty.str prfx :: Pretty.str "(optional)" :: - Attrib.pretty_attribs ctxt atts) - | prt_attn ((true, prfx), atts) = - Pretty.breaks (Pretty.str prfx :: Attrib.pretty_attribs ctxt atts); + fun prt_prfx (false, prfx) = [Pretty.str prfx, Pretty.brk 1, Pretty.str "(optional)"] + | prt_prfx (true, prfx) = [Pretty.str prfx]; fun prt_eqns [] = Pretty.str "no equations." | prt_eqns eqns = Pretty.block (Pretty.str "equations:" :: Pretty.brk 1 :: Pretty.breaks (map prt_thm eqns)); @@ -535,15 +530,15 @@ 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, (prfx, _, witns, eqns)) = if show_wits - then Pretty.block ((prt_attn attn @ [Pretty.str ":", Pretty.brk 1] @ + then Pretty.block ((prt_prfx prfx @ [Pretty.str ":", Pretty.brk 1] @ prt_core ts eqns @ [Pretty.fbrk, prt_witns witns])) - else Pretty.block ((prt_attn attn @ + else Pretty.block ((prt_prfx prfx @ [Pretty.str ":", Pretty.brk 1] @ prt_core ts eqns)); val loc_int = intern thy loc; @@ -554,7 +549,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; @@ -996,7 +991,7 @@ 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, ""), []) + val ctxt'' = put_local_registration (name, ps') (true, "") (Morphism.identity, ((Vartab.empty, []), (Vartab.empty, []) )) ctxt' in case mode of Assumed axs => @@ -1652,7 +1647,7 @@ (* compute morphism and apply to args *) -fun interpret_args thy prfx insts prems eqns atts2 exp attrib args = +fun interpret_args thy prfx insts prems eqns exp attrib args = let val inst = Morphism.name_morphism (Name.map_name (NameSpace.qualified prfx)) $> (* need to add parameter prefix *) (* FIXME *) @@ -1662,8 +1657,6 @@ in args |> Element.facts_map (morph_ctxt' inst) |> (* suppresses application of name morphism: workaroud for class package *) (* FIXME *) - map (fn (attn, bs) => (attn, - bs |> map (fn (ths, atts) => (ths, (atts @ atts2))))) |> standardize thy exp |> Attrib.map_facts attrib end; @@ -1680,12 +1673,12 @@ val regs = get_global_registrations thy target; (* add args to thy for all registrations *) - fun activate (vts, (((fully_qualified, prfx), atts2), (exp, imp), _, _)) thy = + fun activate (vts, ((fully_qualified, prfx), (exp, imp), _, _)) thy = let val (insts, prems, eqns) = collect_global_witnesses thy imp parms ids vts; val attrib = Attrib.attribute_i thy; val args' = args - |> interpret_args thy prfx insts prems eqns atts2 exp attrib + |> interpret_args thy prfx insts prems eqns exp attrib |> add_param_prefixss (space_implode "_" (map fst parms)); in global_note_prefix_i kind target (fully_qualified, prfx) args' thy |> snd end; in fold activate regs thy end; @@ -2059,7 +2052,7 @@ 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 put_reg test_reg add_wit add_eqn - attn all_elemss propss eq_attns (exp, imp) thmss thy_ctxt = + prfx all_elemss propss eq_attns (exp, imp) thmss thy_ctxt = let val ctxt = mk_ctxt thy_ctxt; val (all_propss, eq_props) = chop (length all_elemss) propss; @@ -2073,8 +2066,8 @@ val thy_ctxt' = thy_ctxt (* add registrations *) -(* |> fold (fn ((id, _), _) => put_reg id attn (exp, imp)) new_elemss *) - |> fold (fn (id, _) => put_reg id attn (exp, imp)) new_propss +(* |> fold (fn ((id, _), _) => put_reg id prfx (exp, imp)) new_elemss *) + |> fold (fn (id, _) => put_reg id prfx (exp, imp)) new_propss (* add witnesses of Assumed elements (only those generate proof obligations) *) |> fold (fn (id, thms) => fold (add_wit id) thms) (map fst new_propss ~~ new_thmss) (* add equations *) @@ -2086,22 +2079,21 @@ (fn ((id, Assumed _), _) => Option.map #2 (get_reg thy_ctxt' imp id) | ((_, Derived _), _) => NONE) all_elemss); - fun activate_elem eqns loc ((fully_qualified, prfx), atts) (Notes (kind, facts)) thy_ctxt = + fun activate_elem eqns loc (fully_qualified, prfx) (Notes (kind, facts)) thy_ctxt = let val ctxt = mk_ctxt thy_ctxt; val facts' = interpret_args (ProofContext.theory_of ctxt) prfx - (Symtab.empty, Symtab.empty) prems eqns atts - exp (attrib thy_ctxt) facts; + (Symtab.empty, Symtab.empty) prems eqns exp (attrib thy_ctxt) facts; in snd (note_interp kind loc (fully_qualified, prfx) facts' thy_ctxt) end | activate_elem _ _ _ _ thy_ctxt = thy_ctxt; fun activate_elems all_eqns ((id, _), elems) thy_ctxt = let - val (prfx_atts, _, _) = case get_reg thy_ctxt imp id + val (prfx, _, _) = 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 all_eqns id)) (fst id) prfx_atts) elems thy_ctxt end; + in fold (activate_elem (the (Idtab.lookup all_eqns id)) (fst id) prfx) elems thy_ctxt end; val thy_ctxt'' = thy_ctxt' (* add witnesses of Derived elements *) @@ -2209,7 +2201,7 @@ fun gen_prep_registration mk_ctxt test_reg activate prep_attr prep_expr prep_insts - thy_ctxt raw_attn raw_expr raw_insts = + thy_ctxt prfx raw_expr raw_insts = let val ctxt = mk_ctxt thy_ctxt; val thy = ProofContext.theory_of ctxt; @@ -2217,7 +2209,6 @@ fun prep_attn attn = (apsnd o map) (Attrib.crude_closure ctxt o Args.assignable o prep_attr thy) attn; - val attn = prep_attn raw_attn; val expr = prep_expr thy raw_expr; val pts = params_of_expr ctxt' [] expr ([], Symtab.empty, Symtab.empty); @@ -2274,7 +2265,7 @@ val propss = map extract_asms_elems inst_elemss @ eqn_elems; - in (propss, activate attn inst_elemss propss eq_attns morphs) end; + in (propss, activate prfx inst_elemss propss eq_attns morphs) end; fun gen_prep_global_registration mk_ctxt = gen_prep_registration ProofContext.init test_global_registration @@ -2333,7 +2324,7 @@ |> fold (add_witness_in_locale target id) thms | activate_id _ thy = thy; - fun activate_reg (vts, (((fully_qualified, prfx), atts2), (exp, imp), _, _)) thy = + fun activate_reg (vts, ((fully_qualified, prfx), (exp, imp), _, _)) thy = let val (insts, wits, _) = collect_global_witnesses thy imp fixed target_ids vts; fun inst_parms ps = map @@ -2348,7 +2339,7 @@ if test_global_registration thy (name, ps') then thy else thy - |> put_global_registration (name, ps') ((fully_qualified, prfx), atts2) (exp, imp) + |> put_global_registration (name, ps') (fully_qualified, prfx) (exp, imp) |> fold (fn witn => fn thy => add_global_witness (name, ps') (Element.morph_witness (Element.inst_morphism thy insts) witn) thy) thms end; @@ -2360,7 +2351,7 @@ if test_global_registration thy (name, ps') then thy else thy - |> put_global_registration (name, ps') ((fully_qualified, prfx), atts2) (exp, imp) + |> put_global_registration (name, ps') (fully_qualified, prfx) (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, @@ -2376,7 +2367,6 @@ Morphism.thm_morphism disch; val facts' = facts |> Attrib.map_facts (Attrib.attribute_i thy o Args.morph_values att_morphism) - |> map (apfst (apsnd (fn a => a @ map (Attrib.attribute thy) atts2))) |> map (apsnd (map (apfst (map (disch o Element.inst_thm thy insts o satisfy))))) in thy @@ -2403,10 +2393,10 @@ fun prep_result propps thmss = ListPair.map (fn ((_, props), thms) => map2 Element.make_witness props thms) (propps, thmss); -fun gen_interpretation prep_registration after_qed (prfx, raw_atts) raw_expr raw_insts thy = +fun gen_interpretation prep_registration after_qed prfx raw_expr raw_insts thy = (* prfx = (flag indicating full qualification, name prefix) *) let - val (propss, activate) = prep_registration thy (prfx, raw_atts) raw_expr raw_insts; + val (propss, activate) = prep_registration thy prfx raw_expr raw_insts; fun after_qed' results = ProofContext.theory (activate (prep_result propss results)) #> after_qed; @@ -2418,12 +2408,12 @@ |> Seq.hd end; -fun gen_interpret prep_registration after_qed (prfx, atts) expr insts int state = +fun gen_interpret prep_registration after_qed prfx expr insts int state = (* prfx = (flag indicating full qualification, name prefix) *) let val _ = Proof.assert_forward_or_chain state; val ctxt = Proof.context_of state; - val (propss, activate) = prep_registration ctxt (prfx, atts) expr insts; + val (propss, activate) = prep_registration ctxt prfx expr insts; fun after_qed' results = Proof.map_context (K (ctxt |> activate (prep_result propss results))) #> Proof.put_facts NONE