src/Tools/interpretation_with_defs.ML
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 47249 c0481c3c2a6c
child 55599 6535c537b243
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41582
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
     1
(*  Title:      Tools/interpretation_with_defs.ML
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
     2
    Author:     Florian Haftmann, TU Muenchen
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
     3
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
     4
Interpretation accompanied with mixin definitions.  EXPERIMENTAL.
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
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
     7
signature INTERPRETATION_WITH_DEFS =
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
     8
sig
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
     9
  val interpretation: Expression.expression_i ->
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 ->
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    11
    theory -> Proof.state
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    12
  val interpretation_cmd: Expression.expression ->
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 ->
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    14
    theory -> Proof.state
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
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    17
structure Interpretation_With_Defs : INTERPRETATION_WITH_DEFS =
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
46858
wenzelm
parents: 45290
diff changeset
    20
fun note_eqns_register deps witss def_eqns attrss eqns export export' =
41582
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    21
  let
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    22
    fun meta_rewrite context =
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    23
      map (Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def) o
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    24
        maps snd;
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    25
  in
47249
c0481c3c2a6c added Attrib.global_notes/local_notes/generic_notes convenience;
wenzelm
parents: 46961
diff changeset
    26
    Attrib.generic_notes Thm.lemmaK
41582
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    27
      (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns)
46858
wenzelm
parents: 45290
diff changeset
    28
    #-> (fn facts => `(fn context => meta_rewrite context facts))
wenzelm
parents: 45290
diff changeset
    29
    #-> (fn eqns => fold (fn ((dep, morph), wits) =>
41582
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    30
      fn context =>
46858
wenzelm
parents: 45290
diff changeset
    31
        Locale.add_registration
wenzelm
parents: 45290
diff changeset
    32
          (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))
41582
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    33
          (Element.eq_morphism (Context.theory_of context) (def_eqns @ eqns) |>
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    34
            Option.map (rpair true))
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    35
          export context) (deps ~~ witss))
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    36
  end;
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    37
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    38
local
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    39
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    40
fun gen_interpretation prep_expr prep_decl parse_term parse_prop prep_attr
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    41
    expression raw_defs raw_eqns theory =
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    42
  let
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    43
    val (_, (_, defs_ctxt)) =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 41582
diff changeset
    44
      prep_decl expression I [] (Proof_Context.init_global theory);
41582
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    45
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    46
    val rhss = map (parse_term defs_ctxt o snd o snd) raw_defs
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    47
      |> Syntax.check_terms defs_ctxt;
46909
3c73a121a387 more explicit indication of def names;
wenzelm
parents: 46858
diff changeset
    48
    val defs = map2 (fn ((name, atts), ((b, mx), _)) => fn rhs =>
3c73a121a387 more explicit indication of def names;
wenzelm
parents: 46858
diff changeset
    49
      ((b, mx), ((Thm.def_binding_optional b name, atts), rhs))) raw_defs rhss;
41582
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    50
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    51
    val (def_eqns, theory') = theory
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    52
      |> Named_Target.theory_init
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    53
      |> fold_map (Local_Theory.define) defs
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    54
      |>> map (Thm.symmetric o snd o snd)
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    55
      |> Local_Theory.exit_result_global (map o Morphism.thm);
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    56
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    57
    val ((propss, deps, export), expr_ctxt) = theory'
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 41582
diff changeset
    58
      |> Proof_Context.init_global
41582
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    59
      |> prep_expr expression;
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    60
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    61
    val eqns = map (parse_prop expr_ctxt o snd) raw_eqns
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    62
      |> Syntax.check_terms expr_ctxt;
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    63
    val attrss = map ((apsnd o map) (prep_attr theory) o fst) raw_eqns;
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    64
    val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    65
    val export' = Variable.export_morphism goal_ctxt expr_ctxt;
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    66
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    67
    fun after_qed witss eqns =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 41582
diff changeset
    68
      (Proof_Context.background_theory o Context.theory_map)
41582
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    69
        (note_eqns_register deps witss def_eqns attrss eqns export export');
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    70
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    71
  in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    72
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    73
in
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    74
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    75
fun interpretation x = gen_interpretation Expression.cert_goal_expression
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    76
  Expression.cert_declaration (K I) (K I) (K I) x;
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    77
fun interpretation_cmd x = gen_interpretation Expression.read_goal_expression
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    78
  Expression.read_declaration Syntax.parse_term Syntax.parse_prop Attrib.intern_src x;
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    79
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    80
end;
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    81
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    82
val _ =
46961
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46949
diff changeset
    83
  Outer_Syntax.command @{command_spec "interpretation"}
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46949
diff changeset
    84
    "prove interpretation of locale expression in theory"
41582
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    85
    (Parse.!!! (Parse_Spec.locale_expression true) --
46949
94aa7b81bcf6 prefer formally checked @{keyword} parser;
wenzelm
parents: 46947
diff changeset
    86
      Scan.optional (@{keyword "defines"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
94aa7b81bcf6 prefer formally checked @{keyword} parser;
wenzelm
parents: 46947
diff changeset
    87
        -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "is"} -- Parse.term))) [] --
41582
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    88
      Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    89
      >> (fn ((expr, defs), equations) => Toplevel.print o
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    90
          Toplevel.theory_to_proof (interpretation_cmd expr defs equations)));
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    91
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    92
end;