src/Tools/interpretation_with_defs.ML
author wenzelm
Sat, 10 Mar 2012 20:02:15 +0100
changeset 46858 05f30c796f95
parent 45290 f599ac41e7f5
child 46909 3c73a121a387
permissions -rw-r--r--
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
46858
wenzelm
parents: 45290
diff changeset
    26
    Element.generic_note_thmss 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;
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    48
    val defs = map2 (fn (binding_thm, (binding_syn, _)) => fn rhs =>
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    49
      (binding_syn, (binding_thm, rhs))) raw_defs rhss;
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 definesK = "defines";
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    83
val _ = Keyword.keyword definesK;
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    84
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    85
val _ =
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    86
  Outer_Syntax.command "interpretation"
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    87
    "prove interpretation of locale expression in theory" Keyword.thy_goal
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    88
    (Parse.!!! (Parse_Spec.locale_expression true) --
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    89
      Scan.optional (Parse.$$$ definesK |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    90
        -- ((Parse.binding -- Parse.opt_mixfix') --| Parse.$$$ "is" -- Parse.term))) [] --
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    91
      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
    92
      >> (fn ((expr, defs), equations) => Toplevel.print o
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    93
          Toplevel.theory_to_proof (interpretation_cmd expr defs equations)));
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;