src/Tools/permanent_interpretation.ML
author blanchet
Mon, 15 Sep 2014 10:49:07 +0200
changeset 58335 a5a3b576fcfb
parent 57224 2a7a789ed510
child 59936 b8ffc3dc9e24
permissions -rw-r--r--
generate 'code' attribute only if 'code' plugin is enabled
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
55601
b7f4da504b75 offical tool
haftmann
parents: 55600
diff changeset
     1
(*  Title:   Tools/permanent_interpretation.ML
b7f4da504b75 offical tool
haftmann
parents: 55600
diff changeset
     2
    Author:  Florian Haftmann, TU Muenchen
41582
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
     3
55601
b7f4da504b75 offical tool
haftmann
parents: 55600
diff changeset
     4
Permanent interpretation accompanied with mixin definitions.
41582
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
     5
*)
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
     6
55601
b7f4da504b75 offical tool
haftmann
parents: 55600
diff changeset
     7
signature PERMANENT_INTERPRETATION =
41582
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
     8
sig
55599
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
     9
  val permanent_interpretation: Expression.expression_i ->
41582
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    10
    (Attrib.binding * ((binding * mixfix) * term)) list -> (Attrib.binding * term) list ->
55599
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    11
    local_theory -> Proof.state
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    12
  val permanent_interpretation_cmd: Expression.expression ->
41582
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    13
    (Attrib.binding * ((binding * mixfix) * string)) list -> (Attrib.binding * string) list ->
55599
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    14
    local_theory -> Proof.state
41582
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    15
end;
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    16
55601
b7f4da504b75 offical tool
haftmann
parents: 55600
diff changeset
    17
structure Permanent_Interpretation : PERMANENT_INTERPRETATION =
41582
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    18
struct
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    19
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    20
local
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    21
55599
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    22
(* reading *)
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    23
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    24
fun prep_interpretation prep_expr prep_term prep_prop prep_attr expression raw_defs raw_eqns initial_ctxt =
41582
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    25
  let
55599
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    26
    (*reading*)
57223
fe3f1ca1200a proper proof context transfer wrt. background theory avoids ad-hoc restore operation
haftmann
parents: 56809
diff changeset
    27
    val ((propss, deps, export), expr_ctxt1) = prep_expr expression initial_ctxt;
fe3f1ca1200a proper proof context transfer wrt. background theory avoids ad-hoc restore operation
haftmann
parents: 56809
diff changeset
    28
    val deps_ctxt = fold Locale.activate_declarations deps expr_ctxt1;
55599
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    29
    val prep = Syntax.check_terms deps_ctxt #> Variable.export_terms deps_ctxt deps_ctxt;
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    30
    val rhss = (prep o map (prep_term deps_ctxt o snd o snd)) raw_defs;
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    31
    val eqns = (prep o map (prep_prop deps_ctxt o snd)) raw_eqns;
41582
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    32
55599
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    33
    (*defining*)
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    34
    val pre_defs = map2 (fn ((name, atts), ((b, mx), _)) => fn rhs =>
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    35
      ((b, mx), ((Thm.def_binding_optional b name, atts), rhs))) raw_defs rhss;
57224
2a7a789ed510 mixin definitions are within scope of "for"s of import expression
haftmann
parents: 57223
diff changeset
    36
    val (defs, defs_ctxt) = fold_map Local_Theory.define pre_defs expr_ctxt1;
2a7a789ed510 mixin definitions are within scope of "for"s of import expression
haftmann
parents: 57223
diff changeset
    37
    val def_eqns = map (Thm.symmetric o Morphism.thm (Local_Theory.standard_morphism defs_ctxt expr_ctxt1) o snd o snd) defs;
57223
fe3f1ca1200a proper proof context transfer wrt. background theory avoids ad-hoc restore operation
haftmann
parents: 56809
diff changeset
    38
    val expr_ctxt2 = Proof_Context.transfer (Proof_Context.theory_of defs_ctxt) expr_ctxt1;
41582
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    39
55599
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    40
    (*setting up*)
57223
fe3f1ca1200a proper proof context transfer wrt. background theory avoids ad-hoc restore operation
haftmann
parents: 56809
diff changeset
    41
    val attrss = map (apsnd (map (prep_attr expr_ctxt2)) o fst) raw_eqns;
fe3f1ca1200a proper proof context transfer wrt. background theory avoids ad-hoc restore operation
haftmann
parents: 56809
diff changeset
    42
    val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt2;
fe3f1ca1200a proper proof context transfer wrt. background theory avoids ad-hoc restore operation
haftmann
parents: 56809
diff changeset
    43
    val export' = Variable.export_morphism goal_ctxt expr_ctxt2;
55599
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    44
  in (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end;
41582
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    45
55997
9dc5ce83202c modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents: 55601
diff changeset
    46
val cert_interpretation =
9dc5ce83202c modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents: 55601
diff changeset
    47
  prep_interpretation Expression.cert_goal_expression (K I) (K I) (K I);
9dc5ce83202c modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents: 55601
diff changeset
    48
9dc5ce83202c modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents: 55601
diff changeset
    49
val read_interpretation =
9dc5ce83202c modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents: 55601
diff changeset
    50
  prep_interpretation Expression.read_goal_expression Syntax.parse_term Syntax.parse_prop Attrib.check_src;
55599
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    51
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    52
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    53
(* generic interpretation machinery *)
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    54
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    55
fun meta_rewrite eqns ctxt = (map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns), ctxt);
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    56
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    57
fun note_eqns_register note activate deps witss def_eqns eqns attrss export export' ctxt =
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    58
  let
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    59
    val facts = (Attrib.empty_binding, [(map (Morphism.thm (export' $> export)) def_eqns, [])])
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    60
      :: map2 (fn attrs => fn eqn => (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns;
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    61
    val (eqns', ctxt') = ctxt
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    62
      |> note Thm.lemmaK facts
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    63
      |-> meta_rewrite;
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    64
    val dep_morphs = map2 (fn (dep, morph) => fn wits =>
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    65
      (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))) deps witss;
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    66
    fun activate' dep_morph ctxt = activate dep_morph
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    67
      (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt;
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    68
  in
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    69
    ctxt'
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    70
    |> fold activate' dep_morphs
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    71
  end;
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    72
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    73
fun generic_interpretation prep_interpretation setup_proof note add_registration
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    74
    expression raw_defs raw_eqns initial_ctxt = 
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    75
  let
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    76
    val (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) = 
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    77
      prep_interpretation expression raw_defs raw_eqns initial_ctxt;
41582
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    78
    fun after_qed witss eqns =
55599
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    79
      note_eqns_register note add_registration deps witss def_eqns eqns attrss export export';
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    80
  in setup_proof after_qed propss eqns goal_ctxt end;
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    81
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    82
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    83
(* interpretation with permanent registration *)
41582
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    84
56809
b60009672a65 prevent subscription in nested contexts explicitly -- at foundational and user level
haftmann
parents: 56723
diff changeset
    85
fun gen_permanent_interpretation prep_interpretation expression raw_defs raw_eqns =
b60009672a65 prevent subscription in nested contexts explicitly -- at foundational and user level
haftmann
parents: 56723
diff changeset
    86
  Local_Theory.assert_bottom true
b60009672a65 prevent subscription in nested contexts explicitly -- at foundational and user level
haftmann
parents: 56723
diff changeset
    87
  #> generic_interpretation prep_interpretation Element.witness_proof_eqs
b60009672a65 prevent subscription in nested contexts explicitly -- at foundational and user level
haftmann
parents: 56723
diff changeset
    88
    Local_Theory.notes_kind Local_Theory.subscription expression raw_defs raw_eqns
41582
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    89
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    90
in
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    91
55599
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    92
fun permanent_interpretation x = gen_permanent_interpretation cert_interpretation x;
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    93
fun permanent_interpretation_cmd x = gen_permanent_interpretation read_interpretation x;
41582
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    94
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    95
end;
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    96
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    97
val _ =
55599
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    98
  Outer_Syntax.local_theory_to_proof @{command_spec "permanent_interpretation"}
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
    99
    "prove interpretation of locale expression into named theory"
41582
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
   100
    (Parse.!!! (Parse_Spec.locale_expression true) --
55600
3c7610b8dcfc more convenient syntax for permanent interpretation
haftmann
parents: 55599
diff changeset
   101
      Scan.optional (@{keyword "defining"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
3c7610b8dcfc more convenient syntax for permanent interpretation
haftmann
parents: 55599
diff changeset
   102
        -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "="} -- Parse.term))) [] --
41582
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
   103
      Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
55599
6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents: 47249
diff changeset
   104
      >> (fn ((expr, defs), eqns) => permanent_interpretation_cmd expr defs eqns));
41582
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
   105
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
   106
end;