Interpretation command (theory/proof context) no longer simplifies goal.
authorballarin
Wed Aug 06 16:41:40 2008 +0200 (2008-08-06)
changeset 27761b95e9ba0ca1d
parent 27760 3aa86edac080
child 27762 4936264477f2
Interpretation command (theory/proof context) no longer simplifies goal.
NEWS
src/FOL/ex/LocaleTest.thy
src/Pure/Isar/class.ML
src/Pure/Isar/locale.ML
     1.1 --- a/NEWS	Wed Aug 06 13:57:25 2008 +0200
     1.2 +++ b/NEWS	Wed Aug 06 16:41:40 2008 +0200
     1.3 @@ -19,7 +19,11 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 -* dropped "locale (open)".  INCOMPATBILITY.
     1.8 +* Dropped "locale (open)".  INCOMPATBILITY.
     1.9 +
    1.10 +* Command 'interpretation' no longer attempts to simplify goal.
    1.11 +INCOMPATIBILITY: in rare situations the generated goal differs.  Use
    1.12 +methods intro_locales and unfold_locales to clarify.
    1.13  
    1.14  * Command 'instance': attached definitions no longer accepted.
    1.15  INCOMPATIBILITY, use proper 'instantiation' target.
     2.1 --- a/src/FOL/ex/LocaleTest.thy	Wed Aug 06 13:57:25 2008 +0200
     2.2 +++ b/src/FOL/ex/LocaleTest.thy	Wed Aug 06 16:41:40 2008 +0200
     2.3 @@ -120,7 +120,7 @@
     2.4  
     2.5  (* without prefix *)
     2.6  
     2.7 -interpretation IC ["W::i" "Z::i"] .  (* subsumed by i1: IC *)
     2.8 +interpretation IC ["W::i" "Z::i"] by intro_locales  (* subsumed by i1: IC *)
     2.9  interpretation IC ["W::'a" "Z::i"] by unfold_locales auto
    2.10    (* subsumes i1: IA and i1: IC *)
    2.11  
    2.12 @@ -151,7 +151,7 @@
    2.13  print_interps ID  (* output: i2, i3 *)
    2.14  
    2.15  
    2.16 -interpretation i10: ID + ID a' b' d' [X "Y::i" _ u "v::i" _] .
    2.17 +interpretation i10: ID + ID a' b' d' [X "Y::i" _ u "v::i" _] by intro_locales
    2.18  
    2.19  corollary (in ID) th_x: True ..
    2.20  
    2.21 @@ -184,7 +184,7 @@
    2.22  proof -
    2.23    fix alpha::i and beta
    2.24    have alpha_A: "IA(alpha)" by unfold_locales
    2.25 -  interpret i5: IA [alpha] .  (* subsumed *)
    2.26 +  interpret i5: IA [alpha] by intro_locales  (* subsumed *)
    2.27    print_interps IA  (* output: <no prefix>, i1 *)
    2.28    interpret i6: IC [alpha beta] by unfold_locales auto
    2.29    print_interps IA   (* output: <no prefix>, i1 *)
     3.1 --- a/src/Pure/Isar/class.ML	Wed Aug 06 13:57:25 2008 +0200
     3.2 +++ b/src/Pure/Isar/class.ML	Wed Aug 06 16:41:40 2008 +0200
     3.3 @@ -65,7 +65,7 @@
     3.4  fun prove_interpretation tac prfx_atts expr inst =
     3.5    Locale.interpretation_i I prfx_atts expr inst
     3.6    #> Proof.global_terminal_proof
     3.7 -      (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
     3.8 +      (Method.Basic (fn ctxt => Method.SIMPLE_METHOD (tac ctxt), Position.none), NONE)
     3.9    #> ProofContext.theory_of;
    3.10  
    3.11  fun prove_interpretation_in tac after_qed (name, expr) =
    3.12 @@ -367,7 +367,8 @@
    3.13      val no_constraints = map (map_atyps (K (TFree (Name.aT, [])))) constraints;
    3.14      fun add_constraint c T = Sign.add_const_constraint (c, SOME T);
    3.15      val inst = (#inst o the_class_data thy) class;
    3.16 -    val tac = ALLGOALS (ProofContext.fact_tac facts);
    3.17 +    fun tac ctxt = ALLGOALS (ProofContext.fact_tac facts
    3.18 +      ORELSE' (fn n => SELECT_GOAL (Locale.intro_locales_tac false ctxt []) n));
    3.19      val prfx = class_prefix class;
    3.20    in
    3.21      thy
     4.1 --- a/src/Pure/Isar/locale.ML	Wed Aug 06 13:57:25 2008 +0200
     4.2 +++ b/src/Pure/Isar/locale.ML	Wed Aug 06 16:41:40 2008 +0200
     4.3 @@ -167,7 +167,7 @@
     4.4    intros: thm list * thm list,
     4.5      (* Introduction rules: of delta predicate and locale predicate. *)
     4.6    dests: thm list}
     4.7 -    (* Destruction rules relative to canonical order in locale context. *)
     4.8 +    (* Destruction rules: projections from locale predicate to predicates of fragments. *)
     4.9  
    4.10  (* CB: an internal (Int) locale element was either imported or included,
    4.11     an external (Ext) element appears directly in the locale text. *)
    4.12 @@ -176,7 +176,7 @@
    4.13  
    4.14  
    4.15  
    4.16 -(** substitutions on Frees and Vars -- clone from element.ML **)
    4.17 +(** substitutions on Vars -- clone from element.ML **)
    4.18  
    4.19  (* instantiate types *)
    4.20  
    4.21 @@ -239,7 +239,7 @@
    4.22         context, import is its inverse
    4.23       - theorems (actually witnesses) instantiating locale assumptions
    4.24       - theorems (equations) interpreting derived concepts and indexed by lhs.
    4.25 -     NB: index is exported while content is internalised.
    4.26 +     NB: index is exported whereas content is internalised.
    4.27    *)
    4.28    type T = (((bool * string) * Attrib.src list) *
    4.29              (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) *
    4.30 @@ -2040,12 +2040,18 @@
    4.31    TableFun(type key = string * term list
    4.32      val ord = prod_ord string_ord (list_ord Term.fast_term_ord));
    4.33  
    4.34 -fun gen_activate_facts_elemss mk_ctxt get_reg note note_interp attrib put_reg add_wit add_eqn
    4.35 -        attn all_elemss new_elemss propss eq_attns (exp, imp) thmss thy_ctxt =
    4.36 +fun gen_activate_facts_elemss mk_ctxt get_reg note note_interp attrib put_reg test_reg add_wit add_eqn
    4.37 +        attn all_elemss propss eq_attns (exp, imp) thmss thy_ctxt =
    4.38    let
    4.39      val ctxt = mk_ctxt thy_ctxt;
    4.40 -    val (propss, eq_props) = chop (length new_elemss) propss;
    4.41 -    val (thmss, eq_thms) = chop (length new_elemss) thmss;
    4.42 +    val (propss, eq_props) = chop (length all_elemss) propss;
    4.43 +    val (thmss, eq_thms) = chop (length all_elemss) thmss;
    4.44 +
    4.45 +    (* Filter out fragments already registered. *)
    4.46 +
    4.47 +    val (new_elemss, xs) = split_list (filter_out (fn (((id, _), _), _) =>
    4.48 +          test_reg thy_ctxt id) (all_elemss ~~ (propss ~~ thmss)));
    4.49 +    val (propss, thmss) = split_list xs;
    4.50  
    4.51      fun activate_elem prems eqns exp loc ((fully_qualified, prfx), atts) (Notes (kind, facts)) thy_ctxt =
    4.52          let
    4.53 @@ -2077,6 +2083,7 @@
    4.54      val prems = flat (map_filter
    4.55            (fn ((id, Assumed _), _) => Option.map #2 (get_reg thy_ctxt' imp id)
    4.56              | ((_, Derived _), _) => NONE) all_elemss);
    4.57 +
    4.58      val thy_ctxt'' = thy_ctxt'
    4.59        (* add witnesses of Derived elements *)
    4.60        |> fold (fn (id, thms) => fold (add_wit id o Element.morph_witness (Element.satisfy_morphism prems)) thms)
    4.61 @@ -2091,6 +2098,7 @@
    4.62        |> (fn xs => fold Idtab.update xs Idtab.empty)
    4.63        (* Idtab.make wouldn't work here: can have conflicting duplicates,
    4.64           because instantiation may equate ids and equations are accumulated! *)
    4.65 +
    4.66    in
    4.67      thy_ctxt''
    4.68      (* add equations *)
    4.69 @@ -2109,7 +2117,7 @@
    4.70        PureThy.note_thmss
    4.71        global_note_prefix_i
    4.72        Attrib.attribute_i
    4.73 -      put_global_registration add_global_witness add_global_equation
    4.74 +      put_global_registration test_global_registration add_global_witness add_global_equation
    4.75        x;
    4.76  
    4.77  fun local_activate_facts_elemss x = gen_activate_facts_elemss
    4.78 @@ -2119,6 +2127,7 @@
    4.79        local_note_prefix_i
    4.80        (Attrib.attribute_i o ProofContext.theory_of)
    4.81        put_local_registration
    4.82 +      test_local_registration
    4.83        add_local_witness
    4.84        add_local_equation
    4.85        x;
    4.86 @@ -2239,18 +2248,13 @@
    4.87        ((n, map (Morphism.term (inst_morphism $> fst morphs)) ps),
    4.88          map (fn Int e => Element.morph_ctxt inst_morphism e) elems)
    4.89        |> apfst (fn id => (id, map_mode (map (Element.morph_witness inst_morphism)) mode)));
    4.90 -
    4.91 -    (* remove fragments already registered with theory or context *)
    4.92 -    val new_inst_elemss = filter_out (fn ((id, _), _) =>
    4.93 -          test_reg thy_ctxt id) inst_elemss;
    4.94 -
    4.95      (* equations *)
    4.96      val eqn_elems = if null eqns then []
    4.97        else [(Library.last_elem inst_elemss |> fst |> fst, eqns)];
    4.98  
    4.99 -    val propss = map extract_asms_elems new_inst_elemss @ eqn_elems;
   4.100 -
   4.101 -  in (propss, activate attn inst_elemss new_inst_elemss propss eq_attns morphs) end;
   4.102 +    val propss = map extract_asms_elems inst_elemss @ eqn_elems;
   4.103 +
   4.104 +  in (propss, activate attn inst_elemss propss eq_attns morphs) end;
   4.105  
   4.106  fun gen_prep_global_registration mk_ctxt = gen_prep_registration ProofContext.init
   4.107    test_global_registration