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