src/Pure/Isar/interpretation.ML
author haftmann
Mon Nov 16 19:08:38 2015 +0100 (2015-11-16 ago)
changeset 61691 91854ba66adb
parent 61684 048ba34613bb
child 61698 c4a6edbfec49
permissions -rw-r--r--
clarified contexts by factoring out reading and definition of mixins
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
  type 'a rewrites = (Attrib.binding * 'a) list
haftmann@61673
    12
haftmann@61673
    13
  (*interpretation in proofs*)
haftmann@61673
    14
  val interpret: Expression.expression_i -> term rewrites -> bool -> Proof.state -> Proof.state
haftmann@61673
    15
  val interpret_cmd: Expression.expression -> string rewrites -> bool -> Proof.state -> Proof.state
haftmann@61673
    16
haftmann@61673
    17
  (*algebraic-view*)
haftmann@61673
    18
  val global_interpretation: Expression.expression_i ->
haftmann@61673
    19
    term defines -> term rewrites -> theory -> Proof.state
haftmann@61673
    20
  val global_sublocale: string -> Expression.expression_i ->
haftmann@61676
    21
    term defines -> term rewrites -> theory -> Proof.state
haftmann@61673
    22
  val global_sublocale_cmd: xstring * Position.T -> Expression.expression ->
haftmann@61673
    23
    string defines -> string rewrites -> theory -> Proof.state
haftmann@61673
    24
  val sublocale: Expression.expression_i ->
haftmann@61673
    25
    term defines -> term rewrites -> local_theory -> Proof.state
haftmann@61673
    26
  val sublocale_cmd: Expression.expression ->
haftmann@61673
    27
    string defines -> string rewrites -> local_theory -> Proof.state
haftmann@61673
    28
haftmann@61673
    29
  (*local-theory-based view*)
haftmann@61673
    30
  val ephemeral_interpretation: Expression.expression_i ->
haftmann@61673
    31
    term rewrites -> local_theory -> Proof.state
haftmann@61670
    32
  val permanent_interpretation: Expression.expression_i ->
haftmann@61673
    33
    term defines -> term rewrites -> local_theory -> Proof.state
haftmann@61670
    34
  val permanent_interpretation_cmd: Expression.expression ->
haftmann@61673
    35
    string defines -> string rewrites -> local_theory -> Proof.state
haftmann@61673
    36
haftmann@61673
    37
  (*mixed Isar interface*)
haftmann@61673
    38
  val interpretation: Expression.expression_i -> term rewrites -> local_theory -> Proof.state
haftmann@61673
    39
  val interpretation_cmd: Expression.expression -> string rewrites ->
haftmann@61670
    40
    local_theory -> Proof.state
haftmann@61669
    41
end;
haftmann@61669
    42
haftmann@61669
    43
structure Interpretation : INTERPRETATION =
haftmann@61669
    44
struct
haftmann@61669
    45
haftmann@61673
    46
(** common interpretation machinery **)
haftmann@61673
    47
haftmann@61673
    48
type 'a defines = (Attrib.binding * ((binding * mixfix) * 'a)) list
haftmann@61673
    49
type 'a rewrites = (Attrib.binding * 'a) list
haftmann@61673
    50
haftmann@61673
    51
(* reading of locale expressions with rewrite morphisms *)
haftmann@61670
    52
haftmann@61672
    53
local
haftmann@61669
    54
haftmann@61691
    55
fun prep_mixins prep_term prep_prop expr_ctxt deps_ctxt raw_defs raw_eqns =
haftmann@61670
    56
  let
haftmann@61684
    57
    val prep = Syntax.check_terms deps_ctxt #> Variable.export_terms deps_ctxt expr_ctxt;
haftmann@61670
    58
    val rhss = (prep o map (prep_term deps_ctxt o snd o snd)) raw_defs;
haftmann@61670
    59
    val pre_defs = map2 (fn ((name, atts), ((b, mx), _)) => fn rhs =>
haftmann@61670
    60
      ((b, mx), ((Thm.def_binding_optional b name, atts), rhs))) raw_defs rhss;
haftmann@61691
    61
    val eqns = (prep o map (prep_prop deps_ctxt o snd)) raw_eqns;
haftmann@61691
    62
  in (pre_defs, eqns) end;
haftmann@61669
    63
haftmann@61691
    64
fun define_mixins [] expr_ctxt = ([], expr_ctxt)
haftmann@61691
    65
      (*quasi-inhomogeneous type: definitions demand local theory rather than bare proof context*)
haftmann@61691
    66
  | define_mixins pre_defs expr_lthy =
haftmann@61691
    67
      let
haftmann@61691
    68
        val (defs, forked_lthy) = fold_map Local_Theory.define pre_defs expr_lthy;
haftmann@61691
    69
        val def_lthy =
haftmann@61691
    70
          Proof_Context.transfer (Proof_Context.theory_of forked_lthy) expr_lthy;
haftmann@61691
    71
        val def_eqns = defs
haftmann@61691
    72
          |> map (Thm.symmetric o
haftmann@61691
    73
              Morphism.thm (Local_Theory.standard_morphism forked_lthy def_lthy) o snd o snd);
haftmann@61691
    74
      in (def_eqns, def_lthy) end;
haftmann@61691
    75
haftmann@61691
    76
fun prep_interpretation prep_expr prep_term prep_prop prep_attr
haftmann@61691
    77
  expression raw_defs raw_eqns initial_ctxt =
haftmann@61691
    78
  let
haftmann@61691
    79
    val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
haftmann@61691
    80
    val (pre_defs, eqns) =
haftmann@61691
    81
      prep_mixins prep_term prep_prop expr_ctxt
haftmann@61691
    82
        (fold Locale.activate_declarations deps expr_ctxt) raw_defs raw_eqns;
haftmann@61691
    83
    val (def_eqns, def_ctxt) = define_mixins pre_defs expr_ctxt;
haftmann@61672
    84
    val attrss = map (apsnd (map (prep_attr def_ctxt)) o fst) raw_eqns;
haftmann@61672
    85
    val goal_ctxt = fold Variable.auto_fixes eqns def_ctxt;
haftmann@61672
    86
    val export' = Variable.export_morphism goal_ctxt def_ctxt;
haftmann@61672
    87
  in (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end;
haftmann@61669
    88
haftmann@61670
    89
in
haftmann@61670
    90
haftmann@61672
    91
val cert_interpretation =
haftmann@61672
    92
  prep_interpretation Expression.cert_goal_expression (K I) (K I) (K I);
haftmann@61672
    93
haftmann@61672
    94
val read_interpretation =
haftmann@61672
    95
  prep_interpretation Expression.read_goal_expression Syntax.parse_term Syntax.parse_prop Attrib.check_src;
haftmann@61669
    96
haftmann@61670
    97
end;
haftmann@61669
    98
haftmann@61670
    99
haftmann@61673
   100
(* interpretation machinery *)
haftmann@61670
   101
haftmann@61670
   102
local
haftmann@61670
   103
haftmann@61672
   104
fun meta_rewrite eqns ctxt =
haftmann@61672
   105
  (map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns), ctxt);
haftmann@61670
   106
haftmann@61670
   107
fun note_eqns_register note activate deps witss def_eqns eqns attrss export export' ctxt =
haftmann@61670
   108
  let
haftmann@61670
   109
    val facts = (Attrib.empty_binding, [(map (Morphism.thm (export' $> export)) def_eqns, [])])
haftmann@61670
   110
      :: map2 (fn attrs => fn eqn => (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns;
haftmann@61670
   111
    val (eqns', ctxt') = ctxt
haftmann@61670
   112
      |> note Thm.theoremK facts
haftmann@61670
   113
      |-> meta_rewrite;
haftmann@61670
   114
    val dep_morphs = map2 (fn (dep, morph) => fn wits =>
haftmann@61670
   115
      (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))) deps witss;
haftmann@61670
   116
    fun activate' dep_morph ctxt = activate dep_morph
haftmann@61670
   117
      (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt;
haftmann@61670
   118
  in
haftmann@61670
   119
    ctxt'
haftmann@61670
   120
    |> fold activate' dep_morphs
haftmann@61670
   121
  end;
haftmann@61670
   122
haftmann@61670
   123
in
haftmann@61670
   124
haftmann@61670
   125
fun generic_interpretation_with_defs prep_interpretation setup_proof note add_registration
haftmann@61670
   126
    expression raw_defs raw_eqns initial_ctxt =
haftmann@61670
   127
  let
haftmann@61670
   128
    val (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) =
haftmann@61670
   129
      prep_interpretation expression raw_defs raw_eqns initial_ctxt;
haftmann@61670
   130
    fun after_qed witss eqns =
haftmann@61670
   131
      note_eqns_register note add_registration deps witss def_eqns eqns attrss export export';
haftmann@61670
   132
  in setup_proof after_qed propss eqns goal_ctxt end;
haftmann@61670
   133
haftmann@61672
   134
fun generic_interpretation prep_interpretation setup_proof note add_registration expression =
haftmann@61672
   135
  generic_interpretation_with_defs prep_interpretation setup_proof note add_registration expression [];
haftmann@61672
   136
haftmann@61670
   137
end;
haftmann@61670
   138
haftmann@61670
   139
haftmann@61673
   140
(** interfaces **)
haftmann@61673
   141
haftmann@61673
   142
(* interpretation in proofs *)
haftmann@61670
   143
haftmann@61672
   144
local
haftmann@61672
   145
haftmann@61669
   146
fun gen_interpret prep_interpretation expression raw_eqns int state =
haftmann@61669
   147
  let
haftmann@61669
   148
    val _ = Proof.assert_forward_or_chain state;
haftmann@61669
   149
    val ctxt = Proof.context_of state;
haftmann@61669
   150
    fun lift_after_qed after_qed witss eqns =
haftmann@61669
   151
      Proof.map_context (after_qed witss eqns) #> Proof.reset_facts;
haftmann@61669
   152
    fun setup_proof after_qed propss eqns goal_ctxt =
haftmann@61669
   153
      Element.witness_local_proof_eqs (lift_after_qed after_qed) "interpret"
haftmann@61669
   154
        propss eqns goal_ctxt int state;
haftmann@61669
   155
  in
haftmann@61669
   156
    generic_interpretation prep_interpretation setup_proof
haftmann@61669
   157
      Attrib.local_notes (Context.proof_map ooo Locale.add_registration) expression raw_eqns ctxt
haftmann@61669
   158
  end;
haftmann@61669
   159
haftmann@61673
   160
in
haftmann@61670
   161
haftmann@61673
   162
fun interpret expression = gen_interpret cert_interpretation expression;
haftmann@61673
   163
fun interpret_cmd raw_expression = gen_interpret read_interpretation raw_expression;
haftmann@61669
   164
haftmann@61673
   165
end;
haftmann@61670
   166
haftmann@61670
   167
haftmann@61673
   168
(* algebraic-view *)
haftmann@61673
   169
haftmann@61673
   170
local
haftmann@61669
   171
haftmann@61673
   172
fun gen_global_interpretation prep_interpretation expression
haftmann@61673
   173
    raw_defs raw_eqns thy = 
haftmann@61673
   174
  let
haftmann@61673
   175
    val lthy = Named_Target.theory_init thy;
haftmann@61673
   176
    fun setup_proof after_qed =
haftmann@61673
   177
      Element.witness_proof_eqs
haftmann@61673
   178
        (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit);
haftmann@61673
   179
  in
haftmann@61673
   180
    lthy |>
haftmann@61673
   181
      generic_interpretation_with_defs prep_interpretation setup_proof
haftmann@61673
   182
        Local_Theory.notes_kind Local_Theory.subscription expression raw_defs raw_eqns
haftmann@61673
   183
  end;
haftmann@61673
   184
haftmann@61673
   185
fun gen_global_sublocale prep_loc prep_interpretation
haftmann@61673
   186
    raw_locale expression raw_defs raw_eqns thy =
haftmann@61673
   187
  let
haftmann@61673
   188
    val lthy = Named_Target.init (prep_loc thy raw_locale) thy;
haftmann@61673
   189
    fun setup_proof after_qed =
haftmann@61673
   190
      Element.witness_proof_eqs
haftmann@61673
   191
        (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit);
haftmann@61673
   192
  in
haftmann@61673
   193
    lthy |>
haftmann@61673
   194
      generic_interpretation_with_defs prep_interpretation setup_proof
haftmann@61673
   195
        Local_Theory.notes_kind Local_Theory.subscription expression raw_defs raw_eqns
haftmann@61673
   196
  end;
haftmann@61669
   197
haftmann@61669
   198
fun subscribe_locale_only lthy =
haftmann@61669
   199
  let
haftmann@61669
   200
    val _ =
haftmann@61669
   201
      if Named_Target.is_theory lthy
haftmann@61669
   202
      then error "Not possible on level of global theory"
haftmann@61669
   203
      else ();
haftmann@61669
   204
  in Local_Theory.subscription end;
haftmann@61669
   205
haftmann@61673
   206
fun gen_sublocale prep_interpretation expression raw_defs raw_eqns lthy =
haftmann@61673
   207
  generic_interpretation_with_defs prep_interpretation Element.witness_proof_eqs
haftmann@61673
   208
    Local_Theory.notes_kind (subscribe_locale_only lthy) expression raw_defs raw_eqns lthy;
haftmann@61669
   209
haftmann@61673
   210
in
haftmann@61669
   211
haftmann@61673
   212
fun global_interpretation expression =
haftmann@61673
   213
  gen_global_interpretation cert_interpretation expression;
haftmann@61673
   214
fun global_sublocale expression =
haftmann@61673
   215
  gen_global_sublocale (K I) cert_interpretation expression;
haftmann@61673
   216
fun global_sublocale_cmd raw_expression =
haftmann@61673
   217
  gen_global_sublocale Locale.check read_interpretation raw_expression;
haftmann@61673
   218
fun sublocale expression =
haftmann@61673
   219
  gen_sublocale cert_interpretation expression;
haftmann@61673
   220
fun sublocale_cmd raw_expression =
haftmann@61673
   221
  gen_sublocale read_interpretation raw_expression;
haftmann@61673
   222
haftmann@61673
   223
end;
haftmann@61673
   224
haftmann@61673
   225
haftmann@61673
   226
(* local-theory-based view *)
haftmann@61673
   227
haftmann@61673
   228
local
haftmann@61673
   229
haftmann@61673
   230
fun gen_permanent_interpretation prep_interpretation expression raw_defs raw_eqns =
haftmann@61673
   231
  Local_Theory.assert_bottom true
haftmann@61673
   232
  #> generic_interpretation_with_defs prep_interpretation Element.witness_proof_eqs
haftmann@61673
   233
    Local_Theory.notes_kind Local_Theory.subscription expression raw_defs raw_eqns
haftmann@61669
   234
haftmann@61669
   235
in
haftmann@61669
   236
haftmann@61673
   237
fun ephemeral_interpretation expression =
haftmann@61673
   238
  generic_interpretation cert_interpretation Element.witness_proof_eqs
haftmann@61673
   239
    Local_Theory.notes_kind Locale.activate_fragment expression;
haftmann@61669
   240
haftmann@61673
   241
fun permanent_interpretation expression =
haftmann@61673
   242
  gen_permanent_interpretation cert_interpretation expression;
haftmann@61673
   243
fun permanent_interpretation_cmd raw_expression =
haftmann@61673
   244
  gen_permanent_interpretation read_interpretation raw_expression;
haftmann@61669
   245
haftmann@61673
   246
end;
haftmann@61673
   247
haftmann@61673
   248
haftmann@61673
   249
(* mixed Isar interface *)
haftmann@61673
   250
haftmann@61673
   251
local
haftmann@61670
   252
haftmann@61673
   253
fun subscribe_or_activate lthy =
haftmann@61673
   254
  if Named_Target.is_theory lthy
haftmann@61673
   255
  then Local_Theory.subscription
haftmann@61673
   256
  else Locale.activate_fragment;
haftmann@61669
   257
haftmann@61673
   258
fun gen_local_theory_interpretation prep_interpretation expression raw_eqns lthy =
haftmann@61673
   259
  generic_interpretation prep_interpretation Element.witness_proof_eqs
haftmann@61673
   260
    Local_Theory.notes_kind (subscribe_or_activate lthy) expression raw_eqns lthy;
haftmann@61669
   261
haftmann@61673
   262
in
haftmann@61673
   263
haftmann@61673
   264
fun interpretation expression =
haftmann@61673
   265
  gen_local_theory_interpretation cert_interpretation expression;
haftmann@61673
   266
fun interpretation_cmd raw_expression =
haftmann@61673
   267
  gen_local_theory_interpretation read_interpretation raw_expression;
haftmann@61669
   268
haftmann@61669
   269
end;
haftmann@61669
   270
haftmann@61669
   271
end;