src/Tools/permanent_interpretation.ML
author wenzelm
Fri Aug 15 18:02:34 2014 +0200 (2014-08-15)
changeset 57944 fff8d328da56
parent 57224 2a7a789ed510
child 59936 b8ffc3dc9e24
permissions -rw-r--r--
more informative Token.Name with history of morphisms;
tuned signature;
     1 (*  Title:   Tools/permanent_interpretation.ML
     2     Author:  Florian Haftmann, TU Muenchen
     3 
     4 Permanent interpretation accompanied with mixin definitions.
     5 *)
     6 
     7 signature PERMANENT_INTERPRETATION =
     8 sig
     9   val permanent_interpretation: Expression.expression_i ->
    10     (Attrib.binding * ((binding * mixfix) * term)) list -> (Attrib.binding * term) list ->
    11     local_theory -> Proof.state
    12   val permanent_interpretation_cmd: Expression.expression ->
    13     (Attrib.binding * ((binding * mixfix) * string)) list -> (Attrib.binding * string) list ->
    14     local_theory -> Proof.state
    15 end;
    16 
    17 structure Permanent_Interpretation : PERMANENT_INTERPRETATION =
    18 struct
    19 
    20 local
    21 
    22 (* reading *)
    23 
    24 fun prep_interpretation prep_expr prep_term prep_prop prep_attr expression raw_defs raw_eqns initial_ctxt =
    25   let
    26     (*reading*)
    27     val ((propss, deps, export), expr_ctxt1) = prep_expr expression initial_ctxt;
    28     val deps_ctxt = fold Locale.activate_declarations deps expr_ctxt1;
    29     val prep = Syntax.check_terms deps_ctxt #> Variable.export_terms deps_ctxt deps_ctxt;
    30     val rhss = (prep o map (prep_term deps_ctxt o snd o snd)) raw_defs;
    31     val eqns = (prep o map (prep_prop deps_ctxt o snd)) raw_eqns;
    32 
    33     (*defining*)
    34     val pre_defs = map2 (fn ((name, atts), ((b, mx), _)) => fn rhs =>
    35       ((b, mx), ((Thm.def_binding_optional b name, atts), rhs))) raw_defs rhss;
    36     val (defs, defs_ctxt) = fold_map Local_Theory.define pre_defs expr_ctxt1;
    37     val def_eqns = map (Thm.symmetric o Morphism.thm (Local_Theory.standard_morphism defs_ctxt expr_ctxt1) o snd o snd) defs;
    38     val expr_ctxt2 = Proof_Context.transfer (Proof_Context.theory_of defs_ctxt) expr_ctxt1;
    39 
    40     (*setting up*)
    41     val attrss = map (apsnd (map (prep_attr expr_ctxt2)) o fst) raw_eqns;
    42     val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt2;
    43     val export' = Variable.export_morphism goal_ctxt expr_ctxt2;
    44   in (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end;
    45 
    46 val cert_interpretation =
    47   prep_interpretation Expression.cert_goal_expression (K I) (K I) (K I);
    48 
    49 val read_interpretation =
    50   prep_interpretation Expression.read_goal_expression Syntax.parse_term Syntax.parse_prop Attrib.check_src;
    51 
    52 
    53 (* generic interpretation machinery *)
    54 
    55 fun meta_rewrite eqns ctxt = (map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns), ctxt);
    56 
    57 fun note_eqns_register note activate deps witss def_eqns eqns attrss export export' ctxt =
    58   let
    59     val facts = (Attrib.empty_binding, [(map (Morphism.thm (export' $> export)) def_eqns, [])])
    60       :: map2 (fn attrs => fn eqn => (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns;
    61     val (eqns', ctxt') = ctxt
    62       |> note Thm.lemmaK facts
    63       |-> meta_rewrite;
    64     val dep_morphs = map2 (fn (dep, morph) => fn wits =>
    65       (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))) deps witss;
    66     fun activate' dep_morph ctxt = activate dep_morph
    67       (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt;
    68   in
    69     ctxt'
    70     |> fold activate' dep_morphs
    71   end;
    72 
    73 fun generic_interpretation prep_interpretation setup_proof note add_registration
    74     expression raw_defs raw_eqns initial_ctxt = 
    75   let
    76     val (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) = 
    77       prep_interpretation expression raw_defs raw_eqns initial_ctxt;
    78     fun after_qed witss eqns =
    79       note_eqns_register note add_registration deps witss def_eqns eqns attrss export export';
    80   in setup_proof after_qed propss eqns goal_ctxt end;
    81 
    82 
    83 (* interpretation with permanent registration *)
    84 
    85 fun gen_permanent_interpretation prep_interpretation expression raw_defs raw_eqns =
    86   Local_Theory.assert_bottom true
    87   #> generic_interpretation prep_interpretation Element.witness_proof_eqs
    88     Local_Theory.notes_kind Local_Theory.subscription expression raw_defs raw_eqns
    89 
    90 in
    91 
    92 fun permanent_interpretation x = gen_permanent_interpretation cert_interpretation x;
    93 fun permanent_interpretation_cmd x = gen_permanent_interpretation read_interpretation x;
    94 
    95 end;
    96 
    97 val _ =
    98   Outer_Syntax.local_theory_to_proof @{command_spec "permanent_interpretation"}
    99     "prove interpretation of locale expression into named theory"
   100     (Parse.!!! (Parse_Spec.locale_expression true) --
   101       Scan.optional (@{keyword "defining"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
   102         -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "="} -- Parse.term))) [] --
   103       Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
   104       >> (fn ((expr, defs), eqns) => permanent_interpretation_cmd expr defs eqns));
   105 
   106 end;