src/Pure/Isar/interpretation.ML
author wenzelm
Thu Aug 30 14:38:24 2018 +0200 (14 months ago)
changeset 68854 404e04f649d4
parent 68852 becaeaa334ae
child 68855 59ce31e15c33
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@68854
   100
fun abs_def_rule 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@68854
   110
      fold_map (fn facts => note Thm.theoremK facts #-> abs_def_rule) factss ctxt;
ballarin@67777
   111
    val defs = (Binding.empty_atts, [(map (Morphism.thm (export' $> export)) def_eqns, [])]);
wenzelm@68854
   112
    val (eqns', ctxt'') = ctxt' |> note Thm.theoremK [defs] |-> abs_def_rule;
wenzelm@68854
   113
    val deps' =
wenzelm@68854
   114
      (deps ~~ witss) |> map (fn ((dep, morph), wits) =>
wenzelm@63382
   115
        let val morph' = morph
wenzelm@63382
   116
          $> Element.satisfy_morphism (map (Element.transform_witness export') wits)
wenzelm@63382
   117
          $> Morphism.binding_morphism "position" (Binding.set_pos pos)
wenzelm@68854
   118
        in (dep, morph') end);
wenzelm@68854
   119
    fun register (dep, eqns) ctxt =
wenzelm@68851
   120
      ctxt |> add_registration
wenzelm@68854
   121
        {dep = dep,
wenzelm@68851
   122
          mixin =
wenzelm@68851
   123
            Option.map (rpair true)
wenzelm@68851
   124
              (Element.eq_morphism (Proof_Context.theory_of ctxt) (eqns @ eqns')),
wenzelm@68851
   125
          export = export};
wenzelm@68854
   126
  in ctxt'' |> fold register (deps' ~~ eqnss') end;
haftmann@61670
   127
haftmann@61670
   128
in
haftmann@61670
   129
wenzelm@63380
   130
fun generic_interpretation prep_interpretation setup_proof note add_registration
ballarin@67777
   131
    expression raw_defs initial_ctxt =
haftmann@61670
   132
  let
ballarin@67777
   133
    val (((propss, eq_propss, deps, eqnss, export, export'), def_eqns), goal_ctxt) =
ballarin@67777
   134
      prep_interpretation expression raw_defs initial_ctxt;
wenzelm@63382
   135
    val pos = Position.thread_data ();
haftmann@61670
   136
    fun after_qed witss eqns =
ballarin@67777
   137
      note_eqns_register pos note add_registration deps eqnss witss def_eqns eqns export export';
ballarin@67777
   138
  in setup_proof after_qed propss (flat eq_propss) goal_ctxt end;
haftmann@61670
   139
haftmann@61670
   140
end;
haftmann@61670
   141
haftmann@61670
   142
haftmann@61673
   143
(** interfaces **)
haftmann@61673
   144
haftmann@61673
   145
(* interpretation in proofs *)
haftmann@61670
   146
haftmann@61672
   147
local
haftmann@61672
   148
wenzelm@68850
   149
fun setup_proof state after_qed propss eqns goal_ctxt =
wenzelm@68850
   150
  Element.witness_local_proof_eqs
wenzelm@68850
   151
    (fn witss => fn eqns => Proof.map_context (after_qed witss eqns) #> Proof.reset_facts)
wenzelm@68850
   152
    "interpret" propss eqns goal_ctxt state;
wenzelm@68850
   153
ballarin@67777
   154
fun gen_interpret prep_interpretation expression state =
wenzelm@68850
   155
  Proof.assert_forward_or_chain state
wenzelm@68850
   156
  |> Proof.context_of
wenzelm@68850
   157
  |> generic_interpretation prep_interpretation (setup_proof state)
wenzelm@68852
   158
    Attrib.local_notes Locale.add_registration_proof expression [];
haftmann@61669
   159
haftmann@61673
   160
in
haftmann@61670
   161
wenzelm@63379
   162
val interpret = gen_interpret cert_interpretation;
wenzelm@63379
   163
val interpret_cmd = gen_interpret read_interpretation;
haftmann@61669
   164
haftmann@61673
   165
end;
haftmann@61670
   166
haftmann@61670
   167
haftmann@61890
   168
(* interpretation in local theories *)
haftmann@61890
   169
haftmann@61890
   170
fun interpretation expression =
haftmann@61890
   171
  generic_interpretation cert_interpretation Element.witness_proof_eqs
wenzelm@63380
   172
    Local_Theory.notes_kind Locale.activate_fragment expression [];
haftmann@61890
   173
wenzelm@63380
   174
fun interpretation_cmd expression =
haftmann@61890
   175
  generic_interpretation read_interpretation Element.witness_proof_eqs
wenzelm@63380
   176
    Local_Theory.notes_kind Locale.activate_fragment expression [];
haftmann@61890
   177
haftmann@61890
   178
haftmann@61890
   179
(* interpretation into global theories *)
haftmann@61890
   180
haftmann@61890
   181
fun global_interpretation expression =
wenzelm@63380
   182
  generic_interpretation cert_interpretation Element.witness_proof_eqs
haftmann@61890
   183
    Local_Theory.notes_kind Local_Theory.theory_registration expression;
haftmann@61890
   184
wenzelm@63380
   185
fun global_interpretation_cmd expression =
wenzelm@63380
   186
  generic_interpretation read_interpretation Element.witness_proof_eqs
wenzelm@63380
   187
    Local_Theory.notes_kind Local_Theory.theory_registration expression;
haftmann@61890
   188
haftmann@61890
   189
haftmann@61890
   190
(* interpretation between locales *)
haftmann@61890
   191
haftmann@61890
   192
fun sublocale expression =
wenzelm@63380
   193
  generic_interpretation cert_interpretation Element.witness_proof_eqs
haftmann@61890
   194
    Local_Theory.notes_kind Local_Theory.locale_dependency expression;
haftmann@61890
   195
wenzelm@63380
   196
fun sublocale_cmd expression =
wenzelm@63380
   197
  generic_interpretation read_interpretation Element.witness_proof_eqs
wenzelm@63380
   198
    Local_Theory.notes_kind Local_Theory.locale_dependency expression;
haftmann@61673
   199
haftmann@61673
   200
local
haftmann@61669
   201
haftmann@61673
   202
fun gen_global_sublocale prep_loc prep_interpretation
ballarin@67777
   203
    raw_locale expression raw_defs thy =
haftmann@61673
   204
  let
haftmann@66334
   205
    val lthy = Named_Target.init (prep_loc thy raw_locale) thy;
haftmann@61673
   206
    fun setup_proof after_qed =
haftmann@61673
   207
      Element.witness_proof_eqs
haftmann@61673
   208
        (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit);
haftmann@61673
   209
  in
haftmann@61673
   210
    lthy |>
wenzelm@63380
   211
      generic_interpretation prep_interpretation setup_proof
ballarin@67777
   212
        Local_Theory.notes_kind Local_Theory.locale_dependency expression raw_defs
haftmann@61673
   213
  end;
haftmann@61669
   214
haftmann@61673
   215
in
haftmann@61669
   216
haftmann@61673
   217
fun global_sublocale expression =
haftmann@61673
   218
  gen_global_sublocale (K I) cert_interpretation expression;
haftmann@61890
   219
haftmann@61673
   220
fun global_sublocale_cmd raw_expression =
haftmann@61673
   221
  gen_global_sublocale Locale.check read_interpretation raw_expression;
haftmann@61669
   222
haftmann@61673
   223
end;
haftmann@61673
   224
haftmann@61673
   225
haftmann@61673
   226
(* mixed Isar interface *)
haftmann@61673
   227
haftmann@61673
   228
local
haftmann@61670
   229
haftmann@61890
   230
fun register_or_activate lthy =
haftmann@61673
   231
  if Named_Target.is_theory lthy
haftmann@61890
   232
  then Local_Theory.theory_registration
haftmann@61673
   233
  else Locale.activate_fragment;
haftmann@61669
   234
ballarin@67777
   235
fun gen_isar_interpretation prep_interpretation expression lthy =
haftmann@61673
   236
  generic_interpretation prep_interpretation Element.witness_proof_eqs
ballarin@67777
   237
    Local_Theory.notes_kind (register_or_activate lthy) expression [] lthy;
haftmann@61669
   238
haftmann@61673
   239
in
haftmann@61673
   240
haftmann@61890
   241
fun isar_interpretation expression =
haftmann@61890
   242
  gen_isar_interpretation cert_interpretation expression;
haftmann@61890
   243
fun isar_interpretation_cmd raw_expression =
haftmann@61890
   244
  gen_isar_interpretation read_interpretation raw_expression;
haftmann@61669
   245
haftmann@61669
   246
end;
haftmann@61669
   247
haftmann@61669
   248
end;