author | wenzelm |
Tue, 16 May 2023 17:08:31 +0200 | |
changeset 78064 | 4e865c45458b |
parent 78047 | c8c084bd7e12 |
child 78065 | 11d6a1e62841 |
permissions | -rw-r--r-- |
61669 | 1 |
(* Title: Pure/Isar/interpretation.ML |
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 | 4 |
|
5 |
Locale interpretation. |
|
6 |
*) |
|
7 |
||
8 |
signature INTERPRETATION = |
|
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 | 39 |
end; |
40 |
||
41 |
structure Interpretation : INTERPRETATION = |
|
42 |
struct |
|
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 | 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 | 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 | 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 | 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 | 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 | 85 |
|
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
86 |
end; |
61669 | 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 | 93 |
fun abs_def_rule eqns ctxt = |
63381 | 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 | 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 | 99 |
val factss = thms |
100 |
|> unflat ((map o map) #1 eqnss) |
|
78041 | 101 |
|> map2 (map2 (fn b => fn eq => |
102 |
(b, [([Morphism.thm export (Thm.transfer' ctxt eq)], [])]))) ((map o map) #1 eqnss); |
|
68849 | 103 |
val (eqnss', ctxt') = |
68854 | 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 | 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 | 108 |
val deps' = |
109 |
(deps ~~ witss) |> map (fn ((dep, morph), wits) => |
|
78047 | 110 |
(dep, morph $> Element.satisfy_morphism (map transform_witness wits))); |
68854 | 111 |
fun register (dep, eqns) ctxt = |
68851
6c9825c1e26b
clarified signature: explicit type Locale.registration;
wenzelm
parents:
68850
diff
changeset
|
112 |
ctxt |> add_registration |
69058 | 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 | 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 | 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 | 140 |
fun setup_proof state after_qed propss eqns goal_ctxt = |
141 |
Element.witness_local_proof_eqs |
|
142 |
(fn witss => fn eqns => Proof.map_context (after_qed witss eqns) #> Proof.reset_facts) |
|
143 |
"interpret" propss eqns goal_ctxt state; |
|
144 |
||
73845 | 145 |
fun add_registration_proof registration ctxt = ctxt |
146 |
|> Proof_Context.set_stmt false |
|
147 |
|> Context.proof_map (Locale.add_registration registration) |
|
148 |
|> Proof_Context.restore_stmt ctxt; |
|
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 | 151 |
Proof.assert_forward_or_chain state |
152 |
|> Proof.context_of |
|
153 |
|> generic_interpretation prep_interpretation (setup_proof state) |
|
73845 | 154 |
Attrib.local_notes add_registration_proof expression []; |
61669 | 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 | 158 |
val interpret = gen_interpret cert_interpretation; |
159 |
val interpret_cmd = gen_interpret read_interpretation; |
|
61669 | 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 | 166 |
val add_registration_local_theory = |
73845 | 167 |
Named_Target.revoke_reinitializability oo Generic_Target.local_interpretation; |
72953 | 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 | 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 | 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 | 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 | 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 | 184 |
fun global_interpretation_cmd expression = |
185 |
generic_interpretation read_interpretation Element.witness_proof_eqs |
|
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 | 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 | 195 |
fun sublocale_cmd expression = |
196 |
generic_interpretation read_interpretation Element.witness_proof_eqs |
|
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 | 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 | 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 | 213 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
214 |
in |
61669 | 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 | 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 | 232 |
else add_registration_local_theory; |
61669 | 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 | 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 | 244 |
|
245 |
end; |
|
246 |
||
247 |
end; |