# HG changeset patch # User ballarin # Date 1218033700 -7200 # Node ID b95e9ba0ca1de2f8928ef1242ab41638771e55ab # Parent 3aa86edac08048fcd13b8bff944dcffeec60fcad Interpretation command (theory/proof context) no longer simplifies goal. diff -r 3aa86edac080 -r b95e9ba0ca1d NEWS --- a/NEWS Wed Aug 06 13:57:25 2008 +0200 +++ b/NEWS Wed Aug 06 16:41:40 2008 +0200 @@ -19,7 +19,11 @@ *** Pure *** -* dropped "locale (open)". INCOMPATBILITY. +* Dropped "locale (open)". INCOMPATBILITY. + +* Command 'interpretation' no longer attempts to simplify goal. +INCOMPATIBILITY: in rare situations the generated goal differs. Use +methods intro_locales and unfold_locales to clarify. * Command 'instance': attached definitions no longer accepted. INCOMPATIBILITY, use proper 'instantiation' target. diff -r 3aa86edac080 -r b95e9ba0ca1d src/FOL/ex/LocaleTest.thy --- a/src/FOL/ex/LocaleTest.thy Wed Aug 06 13:57:25 2008 +0200 +++ b/src/FOL/ex/LocaleTest.thy Wed Aug 06 16:41:40 2008 +0200 @@ -120,7 +120,7 @@ (* without prefix *) -interpretation IC ["W::i" "Z::i"] . (* subsumed by i1: IC *) +interpretation IC ["W::i" "Z::i"] by intro_locales (* subsumed by i1: IC *) interpretation IC ["W::'a" "Z::i"] by unfold_locales auto (* subsumes i1: IA and i1: IC *) @@ -151,7 +151,7 @@ print_interps ID (* output: i2, i3 *) -interpretation i10: ID + ID a' b' d' [X "Y::i" _ u "v::i" _] . +interpretation i10: ID + ID a' b' d' [X "Y::i" _ u "v::i" _] by intro_locales corollary (in ID) th_x: True .. @@ -184,7 +184,7 @@ proof - fix alpha::i and beta have alpha_A: "IA(alpha)" by unfold_locales - interpret i5: IA [alpha] . (* subsumed *) + interpret i5: IA [alpha] by intro_locales (* subsumed *) print_interps IA (* output: , i1 *) interpret i6: IC [alpha beta] by unfold_locales auto print_interps IA (* output: , i1 *) diff -r 3aa86edac080 -r b95e9ba0ca1d src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Wed Aug 06 13:57:25 2008 +0200 +++ b/src/Pure/Isar/class.ML Wed Aug 06 16:41:40 2008 +0200 @@ -65,7 +65,7 @@ fun prove_interpretation tac prfx_atts expr inst = Locale.interpretation_i I prfx_atts expr inst #> Proof.global_terminal_proof - (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE) + (Method.Basic (fn ctxt => Method.SIMPLE_METHOD (tac ctxt), Position.none), NONE) #> ProofContext.theory_of; fun prove_interpretation_in tac after_qed (name, expr) = @@ -367,7 +367,8 @@ val no_constraints = map (map_atyps (K (TFree (Name.aT, [])))) constraints; fun add_constraint c T = Sign.add_const_constraint (c, SOME T); val inst = (#inst o the_class_data thy) class; - val tac = ALLGOALS (ProofContext.fact_tac facts); + fun tac ctxt = ALLGOALS (ProofContext.fact_tac facts + ORELSE' (fn n => SELECT_GOAL (Locale.intro_locales_tac false ctxt []) n)); val prfx = class_prefix class; in thy diff -r 3aa86edac080 -r b95e9ba0ca1d src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Wed Aug 06 13:57:25 2008 +0200 +++ b/src/Pure/Isar/locale.ML Wed Aug 06 16:41:40 2008 +0200 @@ -167,7 +167,7 @@ intros: thm list * thm list, (* Introduction rules: of delta predicate and locale predicate. *) dests: thm list} - (* Destruction rules relative to canonical order in locale context. *) + (* Destruction rules: projections from locale predicate to predicates of fragments. *) (* CB: an internal (Int) locale element was either imported or included, an external (Ext) element appears directly in the locale text. *) @@ -176,7 +176,7 @@ -(** substitutions on Frees and Vars -- clone from element.ML **) +(** substitutions on Vars -- clone from element.ML **) (* instantiate types *) @@ -239,7 +239,7 @@ context, import is its inverse - theorems (actually witnesses) instantiating locale assumptions - theorems (equations) interpreting derived concepts and indexed by lhs. - NB: index is exported while content is internalised. + NB: index is exported whereas content is internalised. *) type T = (((bool * string) * Attrib.src list) * (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * @@ -2040,12 +2040,18 @@ 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 put_reg add_wit add_eqn - attn all_elemss new_elemss propss eq_attns (exp, imp) thmss thy_ctxt = +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 = 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; + val (propss, eq_props) = chop (length all_elemss) propss; + val (thmss, eq_thms) = chop (length all_elemss) thmss; + + (* Filter out fragments already registered. *) + + val (new_elemss, xs) = split_list (filter_out (fn (((id, _), _), _) => + test_reg thy_ctxt id) (all_elemss ~~ (propss ~~ thmss))); + val (propss, thmss) = split_list xs; fun activate_elem prems eqns exp loc ((fully_qualified, prfx), atts) (Notes (kind, facts)) thy_ctxt = let @@ -2077,6 +2083,7 @@ val prems = flat (map_filter (fn ((id, Assumed _), _) => Option.map #2 (get_reg thy_ctxt' imp id) | ((_, Derived _), _) => NONE) all_elemss); + val thy_ctxt'' = thy_ctxt' (* add witnesses of Derived elements *) |> fold (fn (id, thms) => fold (add_wit id o Element.morph_witness (Element.satisfy_morphism prems)) thms) @@ -2091,6 +2098,7 @@ |> (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! *) + in thy_ctxt'' (* add equations *) @@ -2109,7 +2117,7 @@ PureThy.note_thmss global_note_prefix_i Attrib.attribute_i - put_global_registration add_global_witness add_global_equation + put_global_registration test_global_registration add_global_witness add_global_equation x; fun local_activate_facts_elemss x = gen_activate_facts_elemss @@ -2119,6 +2127,7 @@ local_note_prefix_i (Attrib.attribute_i o ProofContext.theory_of) put_local_registration + test_local_registration add_local_witness add_local_equation x; @@ -2239,18 +2248,13 @@ ((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; - (* equations *) val eqn_elems = if null eqns then [] else [(Library.last_elem inst_elemss |> fst |> fst, eqns)]; - val propss = map extract_asms_elems new_inst_elemss @ eqn_elems; - - in (propss, activate attn inst_elemss new_inst_elemss propss eq_attns morphs) end; + val propss = map extract_asms_elems inst_elemss @ eqn_elems; + + in (propss, activate attn inst_elemss propss eq_attns morphs) end; fun gen_prep_global_registration mk_ctxt = gen_prep_registration ProofContext.init test_global_registration