src/Pure/Isar/interpretation.ML
author wenzelm
Tue, 16 May 2023 17:08:31 +0200
changeset 78064 4e865c45458b
parent 78047 c8c084bd7e12
child 78065 11d6a1e62841
permissions -rw-r--r--
clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context; clarified signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
     1
(*  Title:      Pure/Isar/interpretation.ML
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
     2
    Author:     Clemens Ballarin, TU Muenchen
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
     3
    Author:     Florian Haftmann, TU Muenchen
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
     4
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
     5
Locale interpretation.
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
     6
*)
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
     7
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
     8
signature INTERPRETATION =
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
     9
sig
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    10
  type 'a defines = (Attrib.binding * ((binding * mixfix) * 'a)) list
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    11
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    12
  (*interpretation in proofs*)
67777
2d3c1091527b Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents: 67740
diff changeset
    13
  val interpret: Expression.expression_i -> Proof.state -> Proof.state
2d3c1091527b Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents: 67740
diff changeset
    14
  val interpret_cmd: Expression.expression -> Proof.state -> Proof.state
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    15
61890
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
    16
  (*interpretation in local theories*)
67777
2d3c1091527b Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents: 67740
diff changeset
    17
  val interpretation: Expression.expression_i -> local_theory -> Proof.state
2d3c1091527b Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents: 67740
diff changeset
    18
  val interpretation_cmd: Expression.expression -> local_theory -> Proof.state
61890
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
    19
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
    20
  (*interpretation into global theories*)
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    21
  val global_interpretation: Expression.expression_i ->
67777
2d3c1091527b Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents: 67740
diff changeset
    22
    term defines -> local_theory -> Proof.state
61890
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
    23
  val global_interpretation_cmd: Expression.expression ->
67777
2d3c1091527b Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents: 67740
diff changeset
    24
    string defines -> local_theory -> Proof.state
61890
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
    25
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
    26
  (*interpretation between locales*)
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    27
  val sublocale: Expression.expression_i ->
67777
2d3c1091527b Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents: 67740
diff changeset
    28
    term defines -> local_theory -> Proof.state
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    29
  val sublocale_cmd: Expression.expression ->
67777
2d3c1091527b Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents: 67740
diff changeset
    30
    string defines -> local_theory -> Proof.state
61890
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
    31
  val global_sublocale: string -> Expression.expression_i ->
67777
2d3c1091527b Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents: 67740
diff changeset
    32
    term defines -> theory -> Proof.state
61890
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
    33
  val global_sublocale_cmd: xstring * Position.T -> Expression.expression ->
67777
2d3c1091527b Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents: 67740
diff changeset
    34
    string defines -> theory -> Proof.state
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    35
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    36
  (*mixed Isar interface*)
67777
2d3c1091527b Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents: 67740
diff changeset
    37
  val isar_interpretation: Expression.expression_i -> local_theory -> Proof.state
2d3c1091527b Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents: 67740
diff changeset
    38
  val isar_interpretation_cmd: Expression.expression -> local_theory -> Proof.state
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
    39
end;
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
    40
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
    41
structure Interpretation : INTERPRETATION =
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
    42
struct
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
    43
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    44
(** common interpretation machinery **)
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    45
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    46
type 'a defines = (Attrib.binding * ((binding * mixfix) * 'a)) list
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    47
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    48
(* reading of locale expressions with rewrite morphisms *)
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
    49
61672
87203a0f0041 tuned -- share implementations as far as appropriate
haftmann
parents: 61670
diff changeset
    50
local
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
    51
67450
b0ae74b86ef3 Experimental support for rewrite morphisms in locale instances.
ballarin
parents: 66334
diff changeset
    52
fun augment_with_def prep_term ((name, atts), ((b, mx), raw_rhs)) lthy =
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
    53
  let
61775
ec11275fb263 alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents: 61774
diff changeset
    54
    val rhs = prep_term lthy raw_rhs;
ec11275fb263 alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents: 61774
diff changeset
    55
    val lthy' = Variable.declare_term rhs lthy;
ec11275fb263 alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents: 61774
diff changeset
    56
    val ((_, (_, def)), lthy'') =
ec11275fb263 alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents: 61774
diff changeset
    57
      Local_Theory.define ((b, mx), ((Thm.def_binding_optional b name, atts), rhs)) lthy';
69699
82f57315cade dedicated combinator for declarations nested in a local theory block
haftmann
parents: 69058
diff changeset
    58
  in (Thm.symmetric def, lthy'') end;
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
    59
69699
82f57315cade dedicated combinator for declarations nested in a local theory block
haftmann
parents: 69058
diff changeset
    60
fun augment_with_defs _ [] _ = pair []
61691
91854ba66adb clarified contexts by factoring out reading and definition of mixins
haftmann
parents: 61684
diff changeset
    61
      (*quasi-inhomogeneous type: definitions demand local theory rather than bare proof context*)
69699
82f57315cade dedicated combinator for declarations nested in a local theory block
haftmann
parents: 69058
diff changeset
    62
  | augment_with_defs prep_term raw_defs deps =
72451
e51f1733618d replaced combinators by more conventional nesting pattern
haftmann
parents: 70314
diff changeset
    63
      Local_Theory.begin_nested
e51f1733618d replaced combinators by more conventional nesting pattern
haftmann
parents: 70314
diff changeset
    64
      #> snd
e51f1733618d replaced combinators by more conventional nesting pattern
haftmann
parents: 70314
diff changeset
    65
      #> fold Locale.activate_declarations deps
e51f1733618d replaced combinators by more conventional nesting pattern
haftmann
parents: 70314
diff changeset
    66
      #> fold_map (augment_with_def prep_term) raw_defs
e51f1733618d replaced combinators by more conventional nesting pattern
haftmann
parents: 70314
diff changeset
    67
      #> Local_Theory.end_nested_result Morphism.fact;
61775
ec11275fb263 alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents: 61774
diff changeset
    68
67777
2d3c1091527b Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents: 67740
diff changeset
    69
fun prep_interpretation prep_expr prep_term
2d3c1091527b Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents: 67740
diff changeset
    70
  expression raw_defs initial_ctxt =
61691
91854ba66adb clarified contexts by factoring out reading and definition of mixins
haftmann
parents: 61684
diff changeset
    71
  let
67450
b0ae74b86ef3 Experimental support for rewrite morphisms in locale instances.
ballarin
parents: 66334
diff changeset
    72
    val ((propss, eq_propss, deps, eqnss, export), expr_ctxt) = prep_expr expression initial_ctxt;
61775
ec11275fb263 alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents: 61774
diff changeset
    73
    val (def_eqns, def_ctxt) =
ec11275fb263 alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents: 61774
diff changeset
    74
      augment_with_defs prep_term raw_defs deps expr_ctxt;
70314
6d6839a948cf proper Proof_Context.export_morphism corresponding to Proof_Context.augment (see 7f568724d67e);
wenzelm
parents: 69699
diff changeset
    75
    val export' = Proof_Context.export_morphism def_ctxt expr_ctxt;
67777
2d3c1091527b Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents: 67740
diff changeset
    76
  in (((propss, eq_propss, deps, eqnss, export, export'), def_eqns), def_ctxt) end;
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
    77
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
    78
in
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
    79
61698
c4a6edbfec49 make SML/NJ happy;
wenzelm
parents: 61691
diff changeset
    80
fun cert_interpretation expression =
67777
2d3c1091527b Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents: 67740
diff changeset
    81
  prep_interpretation Expression.cert_goal_expression Syntax.check_term expression;
61672
87203a0f0041 tuned -- share implementations as far as appropriate
haftmann
parents: 61670
diff changeset
    82
61698
c4a6edbfec49 make SML/NJ happy;
wenzelm
parents: 61691
diff changeset
    83
fun read_interpretation expression =
67777
2d3c1091527b Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents: 67740
diff changeset
    84
  prep_interpretation Expression.read_goal_expression Syntax.read_term expression;
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
    85
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
    86
end;
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
    87
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
    88
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
    89
(* interpretation machinery *)
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
    90
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
    91
local
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
    92
68854
wenzelm
parents: 68852
diff changeset
    93
fun abs_def_rule eqns ctxt =
63381
823660593928 tuned whitespace;
wenzelm
parents: 63380
diff changeset
    94
  (map (Local_Defs.abs_def_rule ctxt) (maps snd eqns), ctxt);
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
    95
68855
59ce31e15c33 more careful treatment position: existing facts refer to interpretation command, future facts refer to themselves (see also 4270da306442);
wenzelm
parents: 68854
diff changeset
    96
fun note_eqns_register note add_registration
68849
wenzelm
parents: 67777
diff changeset
    97
    deps eqnss witss def_eqns thms export export' ctxt =
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
    98
  let
68849
wenzelm
parents: 67777
diff changeset
    99
    val factss = thms
wenzelm
parents: 67777
diff changeset
   100
      |> unflat ((map o map) #1 eqnss)
78041
1828b174768e proper Thm.trim_context / Thm.transfer;
wenzelm
parents: 73845
diff changeset
   101
      |> map2 (map2 (fn b => fn eq =>
1828b174768e proper Thm.trim_context / Thm.transfer;
wenzelm
parents: 73845
diff changeset
   102
          (b, [([Morphism.thm export (Thm.transfer' ctxt eq)], [])]))) ((map o map) #1 eqnss);
68849
wenzelm
parents: 67777
diff changeset
   103
    val (eqnss', ctxt') =
68854
wenzelm
parents: 68852
diff changeset
   104
      fold_map (fn facts => note Thm.theoremK facts #-> abs_def_rule) factss ctxt;
67777
2d3c1091527b Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents: 67740
diff changeset
   105
    val defs = (Binding.empty_atts, [(map (Morphism.thm (export' $> export)) def_eqns, [])]);
68854
wenzelm
parents: 68852
diff changeset
   106
    val (eqns', ctxt'') = ctxt' |> note Thm.theoremK [defs] |-> abs_def_rule;
78064
4e865c45458b clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
wenzelm
parents: 78047
diff changeset
   107
    val transform_witness = Element.transform_witness (Morphism.set_trim_context' ctxt' export');
68854
wenzelm
parents: 68852
diff changeset
   108
    val deps' =
wenzelm
parents: 68852
diff changeset
   109
      (deps ~~ witss) |> map (fn ((dep, morph), wits) =>
78047
c8c084bd7e12 proper trim_context / transfer;
wenzelm
parents: 78041
diff changeset
   110
        (dep, morph $> Element.satisfy_morphism (map transform_witness wits)));
68854
wenzelm
parents: 68852
diff changeset
   111
    fun register (dep, eqns) ctxt =
68851
6c9825c1e26b clarified signature: explicit type Locale.registration;
wenzelm
parents: 68850
diff changeset
   112
      ctxt |> add_registration
69058
f4fb93197670 tuned signature;
wenzelm
parents: 69050
diff changeset
   113
        {inst = dep,
68851
6c9825c1e26b clarified signature: explicit type Locale.registration;
wenzelm
parents: 68850
diff changeset
   114
          mixin =
6c9825c1e26b clarified signature: explicit type Locale.registration;
wenzelm
parents: 68850
diff changeset
   115
            Option.map (rpair true)
6c9825c1e26b clarified signature: explicit type Locale.registration;
wenzelm
parents: 68850
diff changeset
   116
              (Element.eq_morphism (Proof_Context.theory_of ctxt) (eqns @ eqns')),
6c9825c1e26b clarified signature: explicit type Locale.registration;
wenzelm
parents: 68850
diff changeset
   117
          export = export};
68854
wenzelm
parents: 68852
diff changeset
   118
  in ctxt'' |> fold register (deps' ~~ eqnss') end;
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   119
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   120
in
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   121
63380
wenzelm
parents: 63379
diff changeset
   122
fun generic_interpretation prep_interpretation setup_proof note add_registration
67777
2d3c1091527b Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents: 67740
diff changeset
   123
    expression raw_defs initial_ctxt =
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   124
  let
67777
2d3c1091527b Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents: 67740
diff changeset
   125
    val (((propss, eq_propss, deps, eqnss, export, export'), def_eqns), goal_ctxt) =
2d3c1091527b Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents: 67740
diff changeset
   126
      prep_interpretation expression raw_defs initial_ctxt;
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   127
    fun after_qed witss eqns =
68855
59ce31e15c33 more careful treatment position: existing facts refer to interpretation command, future facts refer to themselves (see also 4270da306442);
wenzelm
parents: 68854
diff changeset
   128
      note_eqns_register note add_registration deps eqnss witss def_eqns eqns export export';
67777
2d3c1091527b Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents: 67740
diff changeset
   129
  in setup_proof after_qed propss (flat eq_propss) goal_ctxt end;
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   130
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   131
end;
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   132
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   133
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   134
(** interfaces **)
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   135
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   136
(* interpretation in proofs *)
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   137
61672
87203a0f0041 tuned -- share implementations as far as appropriate
haftmann
parents: 61670
diff changeset
   138
local
87203a0f0041 tuned -- share implementations as far as appropriate
haftmann
parents: 61670
diff changeset
   139
68850
wenzelm
parents: 68849
diff changeset
   140
fun setup_proof state after_qed propss eqns goal_ctxt =
wenzelm
parents: 68849
diff changeset
   141
  Element.witness_local_proof_eqs
wenzelm
parents: 68849
diff changeset
   142
    (fn witss => fn eqns => Proof.map_context (after_qed witss eqns) #> Proof.reset_facts)
wenzelm
parents: 68849
diff changeset
   143
    "interpret" propss eqns goal_ctxt state;
wenzelm
parents: 68849
diff changeset
   144
73845
bfce186331be more succint interfaces
haftmann
parents: 72953
diff changeset
   145
fun add_registration_proof registration ctxt = ctxt
bfce186331be more succint interfaces
haftmann
parents: 72953
diff changeset
   146
  |> Proof_Context.set_stmt false
bfce186331be more succint interfaces
haftmann
parents: 72953
diff changeset
   147
  |> Context.proof_map (Locale.add_registration registration)
bfce186331be more succint interfaces
haftmann
parents: 72953
diff changeset
   148
  |> Proof_Context.restore_stmt ctxt;
bfce186331be more succint interfaces
haftmann
parents: 72953
diff changeset
   149
67777
2d3c1091527b Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents: 67740
diff changeset
   150
fun gen_interpret prep_interpretation expression state =
68850
wenzelm
parents: 68849
diff changeset
   151
  Proof.assert_forward_or_chain state
wenzelm
parents: 68849
diff changeset
   152
  |> Proof.context_of
wenzelm
parents: 68849
diff changeset
   153
  |> generic_interpretation prep_interpretation (setup_proof state)
73845
bfce186331be more succint interfaces
haftmann
parents: 72953
diff changeset
   154
    Attrib.local_notes add_registration_proof expression [];
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   155
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   156
in
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   157
63379
wenzelm
parents: 63352
diff changeset
   158
val interpret = gen_interpret cert_interpretation;
wenzelm
parents: 63352
diff changeset
   159
val interpret_cmd = gen_interpret read_interpretation;
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   160
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   161
end;
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   162
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   163
61890
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   164
(* interpretation in local theories *)
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   165
72953
90ada01470cb clarified scope of concept
haftmann
parents: 72536
diff changeset
   166
val add_registration_local_theory =
73845
bfce186331be more succint interfaces
haftmann
parents: 72953
diff changeset
   167
  Named_Target.revoke_reinitializability oo Generic_Target.local_interpretation;
72953
90ada01470cb clarified scope of concept
haftmann
parents: 72536
diff changeset
   168
61890
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   169
fun interpretation expression =
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   170
  generic_interpretation cert_interpretation Element.witness_proof_eqs
72953
90ada01470cb clarified scope of concept
haftmann
parents: 72536
diff changeset
   171
    Local_Theory.notes_kind add_registration_local_theory expression [];
61890
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   172
63380
wenzelm
parents: 63379
diff changeset
   173
fun interpretation_cmd expression =
61890
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   174
  generic_interpretation read_interpretation Element.witness_proof_eqs
72953
90ada01470cb clarified scope of concept
haftmann
parents: 72536
diff changeset
   175
    Local_Theory.notes_kind add_registration_local_theory expression [];
61890
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   176
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   177
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   178
(* interpretation into global theories *)
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   179
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   180
fun global_interpretation expression =
63380
wenzelm
parents: 63379
diff changeset
   181
  generic_interpretation cert_interpretation Element.witness_proof_eqs
61890
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   182
    Local_Theory.notes_kind Local_Theory.theory_registration expression;
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   183
63380
wenzelm
parents: 63379
diff changeset
   184
fun global_interpretation_cmd expression =
wenzelm
parents: 63379
diff changeset
   185
  generic_interpretation read_interpretation Element.witness_proof_eqs
wenzelm
parents: 63379
diff changeset
   186
    Local_Theory.notes_kind Local_Theory.theory_registration expression;
61890
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   187
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   188
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   189
(* interpretation between locales *)
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   190
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   191
fun sublocale expression =
63380
wenzelm
parents: 63379
diff changeset
   192
  generic_interpretation cert_interpretation Element.witness_proof_eqs
61890
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   193
    Local_Theory.notes_kind Local_Theory.locale_dependency expression;
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   194
63380
wenzelm
parents: 63379
diff changeset
   195
fun sublocale_cmd expression =
wenzelm
parents: 63379
diff changeset
   196
  generic_interpretation read_interpretation Element.witness_proof_eqs
wenzelm
parents: 63379
diff changeset
   197
    Local_Theory.notes_kind Local_Theory.locale_dependency expression;
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   198
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   199
local
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   200
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   201
fun gen_global_sublocale prep_loc prep_interpretation
67777
2d3c1091527b Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents: 67740
diff changeset
   202
    raw_locale expression raw_defs thy =
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   203
  let
72536
589645894305 bundle mixins for locale and class specifications
haftmann
parents: 72505
diff changeset
   204
    val lthy = Named_Target.init [] (prep_loc thy raw_locale) thy;
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   205
    fun setup_proof after_qed =
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   206
      Element.witness_proof_eqs
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   207
        (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit);
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   208
  in
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   209
    lthy |>
63380
wenzelm
parents: 63379
diff changeset
   210
      generic_interpretation prep_interpretation setup_proof
67777
2d3c1091527b Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents: 67740
diff changeset
   211
        Local_Theory.notes_kind Local_Theory.locale_dependency expression raw_defs
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   212
  end;
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   213
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   214
in
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   215
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   216
fun global_sublocale expression =
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   217
  gen_global_sublocale (K I) cert_interpretation expression;
61890
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   218
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   219
fun global_sublocale_cmd raw_expression =
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   220
  gen_global_sublocale Locale.check read_interpretation raw_expression;
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   221
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   222
end;
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   223
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   224
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   225
(* mixed Isar interface *)
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   226
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   227
local
61670
301e0b4ecd45 coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents: 61669
diff changeset
   228
61890
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   229
fun register_or_activate lthy =
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   230
  if Named_Target.is_theory lthy
61890
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   231
  then Local_Theory.theory_registration
72953
90ada01470cb clarified scope of concept
haftmann
parents: 72536
diff changeset
   232
  else add_registration_local_theory;
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   233
67777
2d3c1091527b Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents: 67740
diff changeset
   234
fun gen_isar_interpretation prep_interpretation expression lthy =
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   235
  generic_interpretation prep_interpretation Element.witness_proof_eqs
67777
2d3c1091527b Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents: 67740
diff changeset
   236
    Local_Theory.notes_kind (register_or_activate lthy) expression [] lthy;
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   237
61673
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   238
in
fd4ac1530d63 represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents: 61672
diff changeset
   239
61890
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   240
fun isar_interpretation expression =
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   241
  gen_isar_interpretation cert_interpretation expression;
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   242
fun isar_interpretation_cmd raw_expression =
f6ded81f5690 abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents: 61823
diff changeset
   243
  gen_isar_interpretation read_interpretation raw_expression;
61669
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   244
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   245
end;
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   246
27ca6147e3b3 separate ML module for interpretation
haftmann
parents:
diff changeset
   247
end;