interpretation: distinguish theories and proofs by explicit parameter rather than generic context;
authorhaftmann
Sun Apr 21 16:29:40 2013 +0200 (2013-04-21)
changeset 51730dffc57bfc653
parent 51729 106bd5a4af22
child 51731 f27e22880cc3
interpretation: distinguish theories and proofs by explicit parameter rather than generic context;
formal initialisation of theory target during interpretation;
prefer Local_Theory.notes_kind to register mixin equations during interpretation;
more uniformity between note_eqns_register and note_eqns_dependency
src/Pure/Isar/expression.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Sun Apr 21 10:41:18 2013 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Sun Apr 21 16:29:40 2013 +0200
     1.3 @@ -819,26 +819,26 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun note_eqns_register deps witss attrss eqns export export' context =
     1.8 +fun note_eqns_register note add_registration deps witss attrss eqns export export' ctxt =
     1.9    let
    1.10      val facts = 
    1.11        (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns);
    1.12 -    val (eqns', context') = context 
    1.13 -      |> Attrib.generic_notes Thm.lemmaK facts
    1.14 -      |-> (fn facts' => `(fn context'' => meta_rewrite (Context.proof_of context'') (maps snd facts')));
    1.15 +    val (eqns', ctxt') = ctxt
    1.16 +      |> note Thm.lemmaK facts
    1.17 +      |-> (fn facts' => `(fn ctxt'' => meta_rewrite ctxt'' (maps snd facts')));
    1.18    in
    1.19 -    context'
    1.20 -    |> fold2 (fn (dep, morph) => fn wits => fn context'' =>
    1.21 -      Locale.add_registration
    1.22 +    ctxt'
    1.23 +    |> fold2 (fn (dep, morph) => fn wits => fn ctxt'' =>
    1.24 +      add_registration
    1.25          (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))
    1.26 -        (Element.eq_morphism (Context.theory_of context'') eqns' |> Option.map (rpair true))
    1.27 -        export context'') deps witss
    1.28 +        (Element.eq_morphism (Proof_Context.theory_of ctxt'') eqns' |> Option.map (rpair true))
    1.29 +        export ctxt'') deps witss
    1.30    end;
    1.31  
    1.32  fun gen_interpretation prep_expr parse_prop prep_attr
    1.33      expression equations thy =
    1.34    let
    1.35 -    val initial_ctxt = Proof_Context.init_global thy;
    1.36 +    val initial_ctxt = Named_Target.theory_init thy;
    1.37  
    1.38      val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
    1.39      val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
    1.40 @@ -847,9 +847,10 @@
    1.41      val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
    1.42      val export' = Variable.export_morphism goal_ctxt expr_ctxt;
    1.43  
    1.44 +    val note = Local_Theory.notes_kind;
    1.45 +    val add_registration = Proof_Context.background_theory o Context.theory_map ooo Locale.add_registration;
    1.46      fun after_qed witss eqns =
    1.47 -      (Proof_Context.background_theory o Context.theory_map)
    1.48 -        (note_eqns_register deps witss attrss eqns export export');
    1.49 +      note_eqns_register note add_registration deps witss attrss eqns export export';
    1.50  
    1.51    in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
    1.52  
    1.53 @@ -867,10 +868,12 @@
    1.54      val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
    1.55      val export' = Variable.export_morphism goal_ctxt expr_ctxt;
    1.56  
    1.57 +    val note = Attrib.local_notes;
    1.58 +    val add_registration = Context.proof_map ooo Locale.add_registration;
    1.59      fun after_qed witss eqns =
    1.60 -      (Proof.map_context o Context.proof_map)
    1.61 -        (note_eqns_register deps witss attrss eqns export export')
    1.62 +      Proof.map_context (note_eqns_register note add_registration deps witss attrss eqns export export')
    1.63        #> Proof.reset_facts;
    1.64 +
    1.65    in
    1.66      state
    1.67      |> Element.witness_local_proof_eqs after_qed "interpret" propss eqns goal_ctxt int
    1.68 @@ -902,12 +905,11 @@
    1.69        |-> (fn facts' => `(fn ctxt'' => meta_rewrite ctxt'' (maps snd facts')));
    1.70    in
    1.71      ctxt'
    1.72 -    |> Proof_Context.background_theory (fold2 (fn (dep, morph) => fn wits =>
    1.73 -      fn thy =>
    1.74 -        Locale.add_dependency target
    1.75 -          (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))
    1.76 -          (Element.eq_morphism thy eqns' |> Option.map (rpair true))
    1.77 -          export thy) deps witss)
    1.78 +    |> fold2 (fn (dep, morph) => fn wits => fn ctxt'' =>
    1.79 +      (Proof_Context.background_theory ooo Locale.add_dependency target)
    1.80 +        (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))
    1.81 +        (Element.eq_morphism (Proof_Context.theory_of ctxt'') eqns' |> Option.map (rpair true))
    1.82 +        export ctxt'') deps witss
    1.83    end;
    1.84  
    1.85  fun gen_sublocale prep_expr prep_loc parse_prop prep_attr