src/Pure/Isar/interpretation.ML
author wenzelm
Thu Aug 30 12:36:26 2018 +0200 (14 months ago)
changeset 68850 6d2735ca0271
parent 68849 0f9b2fa0556f
child 68851 6c9825c1e26b
permissions -rw-r--r--
tuned;
haftmann@61669
     1
(*  Title:      Pure/Isar/interpretation.ML
haftmann@61669
     2
    Author:     Clemens Ballarin, TU Muenchen
haftmann@61670
     3
    Author:     Florian Haftmann, TU Muenchen
haftmann@61669
     4
haftmann@61669
     5
Locale interpretation.
haftmann@61669
     6
*)
haftmann@61669
     7
haftmann@61669
     8
signature INTERPRETATION =
haftmann@61669
     9
sig
haftmann@61673
    10
  type 'a defines = (Attrib.binding * ((binding * mixfix) * 'a)) list
haftmann@61673
    11
haftmann@61673
    12
  (*interpretation in proofs*)
ballarin@67777
    13
  val interpret: Expression.expression_i -> Proof.state -> Proof.state
ballarin@67777
    14
  val interpret_cmd: Expression.expression -> Proof.state -> Proof.state
haftmann@61673
    15
haftmann@61890
    16
  (*interpretation in local theories*)
ballarin@67777
    17
  val interpretation: Expression.expression_i -> local_theory -> Proof.state
ballarin@67777
    18
  val interpretation_cmd: Expression.expression -> local_theory -> Proof.state
haftmann@61890
    19
haftmann@61890
    20
  (*interpretation into global theories*)
haftmann@61673
    21
  val global_interpretation: Expression.expression_i ->
ballarin@67777
    22
    term defines -> local_theory -> Proof.state
haftmann@61890
    23
  val global_interpretation_cmd: Expression.expression ->
ballarin@67777
    24
    string defines -> local_theory -> Proof.state
haftmann@61890
    25
haftmann@61890
    26
  (*interpretation between locales*)
haftmann@61673
    27
  val sublocale: Expression.expression_i ->
ballarin@67777
    28
    term defines -> local_theory -> Proof.state
haftmann@61673
    29
  val sublocale_cmd: Expression.expression ->
ballarin@67777
    30
    string defines -> local_theory -> Proof.state
haftmann@61890
    31
  val global_sublocale: string -> Expression.expression_i ->
ballarin@67777
    32
    term defines -> theory -> Proof.state
haftmann@61890
    33
  val global_sublocale_cmd: xstring * Position.T -> Expression.expression ->
ballarin@67777
    34
    string defines -> theory -> Proof.state
haftmann@61673
    35
haftmann@61673
    36
  (*mixed Isar interface*)
ballarin@67777
    37
  val isar_interpretation: Expression.expression_i -> local_theory -> Proof.state
ballarin@67777
    38
  val isar_interpretation_cmd: Expression.expression -> local_theory -> Proof.state
haftmann@61669
    39
end;
haftmann@61669
    40
haftmann@61669
    41
structure Interpretation : INTERPRETATION =
haftmann@61669
    42
struct
haftmann@61669
    43
haftmann@61673
    44
(** common interpretation machinery **)
haftmann@61673
    45
haftmann@61673
    46
type 'a defines = (Attrib.binding * ((binding * mixfix) * 'a)) list
haftmann@61673
    47
haftmann@61673
    48
(* reading of locale expressions with rewrite morphisms *)
haftmann@61670
    49
haftmann@61672
    50
local
haftmann@61669
    51
ballarin@67450
    52
fun augment_with_def prep_term ((name, atts), ((b, mx), raw_rhs)) lthy =
haftmann@61670
    53
  let
haftmann@61775
    54
    val rhs = prep_term lthy raw_rhs;
haftmann@61775
    55
    val lthy' = Variable.declare_term rhs lthy;
haftmann@61775
    56
    val ((_, (_, def)), lthy'') =
haftmann@61775
    57
      Local_Theory.define ((b, mx), ((Thm.def_binding_optional b name, atts), rhs)) lthy';
haftmann@61775
    58
  in (def, lthy'') end;
haftmann@61669
    59
ballarin@67450
    60
fun augment_with_defs _ [] _ ctxt = ([], ctxt)
haftmann@61691
    61
      (*quasi-inhomogeneous type: definitions demand local theory rather than bare proof context*)
haftmann@61775
    62
  | augment_with_defs prep_term raw_defs deps lthy =
haftmann@61691
    63
      let
haftmann@61775
    64
        val (_, inner_lthy) =
haftmann@61775
    65
          Local_Theory.open_target lthy
haftmann@61775
    66
          ||> fold Locale.activate_declarations deps;
haftmann@61775
    67
        val (inner_defs, inner_lthy') =
ballarin@67450
    68
          fold_map (augment_with_def prep_term) raw_defs inner_lthy;
haftmann@61775
    69
        val lthy' =
haftmann@61775
    70
          inner_lthy'
haftmann@61708
    71
          |> Local_Theory.close_target;
haftmann@61708
    72
        val def_eqns =
haftmann@61775
    73
          map (singleton (Proof_Context.export inner_lthy' lthy') o Thm.symmetric) inner_defs
haftmann@61775
    74
      in (def_eqns, lthy') end;
haftmann@61775
    75
ballarin@67777
    76
fun prep_interpretation prep_expr prep_term
ballarin@67777
    77
  expression raw_defs initial_ctxt =
haftmann@61691
    78
  let
ballarin@67450
    79
    val ((propss, eq_propss, deps, eqnss, export), expr_ctxt) = prep_expr expression initial_ctxt;
haftmann@61775
    80
    val (def_eqns, def_ctxt) =
haftmann@61775
    81
      augment_with_defs prep_term raw_defs deps expr_ctxt;
ballarin@67777
    82
    val export' = Variable.export_morphism def_ctxt expr_ctxt;
ballarin@67777
    83
  in (((propss, eq_propss, deps, eqnss, export, export'), def_eqns), def_ctxt) end;
haftmann@61669
    84
haftmann@61670
    85
in
haftmann@61670
    86
wenzelm@61698
    87
fun cert_interpretation expression =
ballarin@67777
    88
  prep_interpretation Expression.cert_goal_expression Syntax.check_term expression;
haftmann@61672
    89
wenzelm@61698
    90
fun read_interpretation expression =
ballarin@67777
    91
  prep_interpretation Expression.read_goal_expression Syntax.read_term expression;
haftmann@61669
    92
haftmann@61670
    93
end;
haftmann@61669
    94
haftmann@61670
    95
haftmann@61673
    96
(* interpretation machinery *)
haftmann@61670
    97
haftmann@61670
    98
local
haftmann@61670
    99
wenzelm@63381
   100
fun meta_rewrite eqns ctxt =
wenzelm@63381
   101
  (map (Local_Defs.abs_def_rule ctxt) (maps snd eqns), ctxt);
haftmann@61670
   102
wenzelm@68849
   103
fun note_eqns_register pos note add_registration
wenzelm@68849
   104
    deps eqnss witss def_eqns thms export export' ctxt =
haftmann@61670
   105
  let
wenzelm@68849
   106
    val factss = thms
wenzelm@68849
   107
      |> unflat ((map o map) #1 eqnss)
wenzelm@68849
   108
      |> map2 (map2 (fn b => fn eq => (b, [([Morphism.thm export eq], [])]))) ((map o map) #1 eqnss);
wenzelm@68849
   109
    val (eqnss', ctxt') =
wenzelm@68849
   110
      fold_map (fn facts => note Thm.theoremK facts #-> meta_rewrite) factss ctxt;
ballarin@67777
   111
    val defs = (Binding.empty_atts, [(map (Morphism.thm (export' $> export)) def_eqns, [])]);
ballarin@67450
   112
    val (eqns', ctxt'') = ctxt'
ballarin@67777
   113
      |> note Thm.theoremK [defs]
haftmann@61670
   114
      |-> meta_rewrite;
wenzelm@63381
   115
    val dep_morphs =
wenzelm@63381
   116
      map2 (fn (dep, morph) => fn wits =>
wenzelm@63382
   117
        let val morph' = morph
wenzelm@63382
   118
          $> Element.satisfy_morphism (map (Element.transform_witness export') wits)
wenzelm@63382
   119
          $> Morphism.binding_morphism "position" (Binding.set_pos pos)
wenzelm@63382
   120
        in (dep, morph') end) deps witss;
wenzelm@68849
   121
    fun register (dep_morph, eqns) ctxt =
wenzelm@68849
   122
      add_registration dep_morph
ballarin@67450
   123
        (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) (eqns @ eqns')))
wenzelm@63381
   124
        export ctxt;
wenzelm@68849
   125
  in ctxt'' |> fold register (dep_morphs ~~ eqnss') end;
haftmann@61670
   126
haftmann@61670
   127
in
haftmann@61670
   128
wenzelm@63380
   129
fun generic_interpretation prep_interpretation setup_proof note add_registration
ballarin@67777
   130
    expression raw_defs initial_ctxt =
haftmann@61670
   131
  let
ballarin@67777
   132
    val (((propss, eq_propss, deps, eqnss, export, export'), def_eqns), goal_ctxt) =
ballarin@67777
   133
      prep_interpretation expression raw_defs initial_ctxt;
wenzelm@63382
   134
    val pos = Position.thread_data ();
haftmann@61670
   135
    fun after_qed witss eqns =
ballarin@67777
   136
      note_eqns_register pos note add_registration deps eqnss witss def_eqns eqns export export';
ballarin@67777
   137
  in setup_proof after_qed propss (flat eq_propss) goal_ctxt end;
haftmann@61670
   138
haftmann@61670
   139
end;
haftmann@61670
   140
haftmann@61670
   141
haftmann@61673
   142
(** interfaces **)
haftmann@61673
   143
haftmann@61673
   144
(* interpretation in proofs *)
haftmann@61670
   145
haftmann@61672
   146
local
haftmann@61672
   147
wenzelm@68850
   148
fun setup_proof state after_qed propss eqns goal_ctxt =
wenzelm@68850
   149
  Element.witness_local_proof_eqs
wenzelm@68850
   150
    (fn witss => fn eqns => Proof.map_context (after_qed witss eqns) #> Proof.reset_facts)
wenzelm@68850
   151
    "interpret" propss eqns goal_ctxt state;
wenzelm@68850
   152
wenzelm@68850
   153
fun add_registration reg mixin export ctxt = ctxt
wenzelm@68850
   154
  |> Proof_Context.set_stmt false
wenzelm@68850
   155
  |> Context.proof_map (Locale.add_registration reg mixin export)
wenzelm@68850
   156
  |> Proof_Context.restore_stmt ctxt;
wenzelm@68850
   157
ballarin@67777
   158
fun gen_interpret prep_interpretation expression state =
wenzelm@68850
   159
  Proof.assert_forward_or_chain state
wenzelm@68850
   160
  |> Proof.context_of
wenzelm@68850
   161
  |> generic_interpretation prep_interpretation (setup_proof state)
wenzelm@68850
   162
    Attrib.local_notes add_registration expression [];
haftmann@61669
   163
haftmann@61673
   164
in
haftmann@61670
   165
wenzelm@63379
   166
val interpret = gen_interpret cert_interpretation;
wenzelm@63379
   167
val interpret_cmd = gen_interpret read_interpretation;
haftmann@61669
   168
haftmann@61673
   169
end;
haftmann@61670
   170
haftmann@61670
   171
haftmann@61890
   172
(* interpretation in local theories *)
haftmann@61890
   173
haftmann@61890
   174
fun interpretation expression =
haftmann@61890
   175
  generic_interpretation cert_interpretation Element.witness_proof_eqs
wenzelm@63380
   176
    Local_Theory.notes_kind Locale.activate_fragment expression [];
haftmann@61890
   177
wenzelm@63380
   178
fun interpretation_cmd expression =
haftmann@61890
   179
  generic_interpretation read_interpretation Element.witness_proof_eqs
wenzelm@63380
   180
    Local_Theory.notes_kind Locale.activate_fragment expression [];
haftmann@61890
   181
haftmann@61890
   182
haftmann@61890
   183
(* interpretation into global theories *)
haftmann@61890
   184
haftmann@61890
   185
fun global_interpretation expression =
wenzelm@63380
   186
  generic_interpretation cert_interpretation Element.witness_proof_eqs
haftmann@61890
   187
    Local_Theory.notes_kind Local_Theory.theory_registration expression;
haftmann@61890
   188
wenzelm@63380
   189
fun global_interpretation_cmd expression =
wenzelm@63380
   190
  generic_interpretation read_interpretation Element.witness_proof_eqs
wenzelm@63380
   191
    Local_Theory.notes_kind Local_Theory.theory_registration expression;
haftmann@61890
   192
haftmann@61890
   193
haftmann@61890
   194
(* interpretation between locales *)
haftmann@61890
   195
haftmann@61890
   196
fun sublocale expression =
wenzelm@63380
   197
  generic_interpretation cert_interpretation Element.witness_proof_eqs
haftmann@61890
   198
    Local_Theory.notes_kind Local_Theory.locale_dependency expression;
haftmann@61890
   199
wenzelm@63380
   200
fun sublocale_cmd expression =
wenzelm@63380
   201
  generic_interpretation read_interpretation Element.witness_proof_eqs
wenzelm@63380
   202
    Local_Theory.notes_kind Local_Theory.locale_dependency expression;
haftmann@61673
   203
haftmann@61673
   204
local
haftmann@61669
   205
haftmann@61673
   206
fun gen_global_sublocale prep_loc prep_interpretation
ballarin@67777
   207
    raw_locale expression raw_defs thy =
haftmann@61673
   208
  let
haftmann@66334
   209
    val lthy = Named_Target.init (prep_loc thy raw_locale) thy;
haftmann@61673
   210
    fun setup_proof after_qed =
haftmann@61673
   211
      Element.witness_proof_eqs
haftmann@61673
   212
        (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit);
haftmann@61673
   213
  in
haftmann@61673
   214
    lthy |>
wenzelm@63380
   215
      generic_interpretation prep_interpretation setup_proof
ballarin@67777
   216
        Local_Theory.notes_kind Local_Theory.locale_dependency expression raw_defs
haftmann@61673
   217
  end;
haftmann@61669
   218
haftmann@61673
   219
in
haftmann@61669
   220
haftmann@61673
   221
fun global_sublocale expression =
haftmann@61673
   222
  gen_global_sublocale (K I) cert_interpretation expression;
haftmann@61890
   223
haftmann@61673
   224
fun global_sublocale_cmd raw_expression =
haftmann@61673
   225
  gen_global_sublocale Locale.check read_interpretation raw_expression;
haftmann@61669
   226
haftmann@61673
   227
end;
haftmann@61673
   228
haftmann@61673
   229
haftmann@61673
   230
(* mixed Isar interface *)
haftmann@61673
   231
haftmann@61673
   232
local
haftmann@61670
   233
haftmann@61890
   234
fun register_or_activate lthy =
haftmann@61673
   235
  if Named_Target.is_theory lthy
haftmann@61890
   236
  then Local_Theory.theory_registration
haftmann@61673
   237
  else Locale.activate_fragment;
haftmann@61669
   238
ballarin@67777
   239
fun gen_isar_interpretation prep_interpretation expression lthy =
haftmann@61673
   240
  generic_interpretation prep_interpretation Element.witness_proof_eqs
ballarin@67777
   241
    Local_Theory.notes_kind (register_or_activate lthy) expression [] lthy;
haftmann@61669
   242
haftmann@61673
   243
in
haftmann@61673
   244
haftmann@61890
   245
fun isar_interpretation expression =
haftmann@61890
   246
  gen_isar_interpretation cert_interpretation expression;
haftmann@61890
   247
fun isar_interpretation_cmd raw_expression =
haftmann@61890
   248
  gen_isar_interpretation read_interpretation raw_expression;
haftmann@61669
   249
haftmann@61669
   250
end;
haftmann@61669
   251
haftmann@61669
   252
end;