author | haftmann |
Sat, 24 Oct 2020 15:16:54 +0000 | |
changeset 72505 | 974071d873ba |
parent 72451 | e51f1733618d |
child 72536 | 589645894305 |
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) |
|
101 |
|> map2 (map2 (fn b => fn eq => (b, [([Morphism.thm export eq], [])]))) ((map o map) #1 eqnss); |
|
102 |
val (eqnss', ctxt') = |
|
68854 | 103 |
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
|
104 |
val defs = (Binding.empty_atts, [(map (Morphism.thm (export' $> export)) def_eqns, [])]); |
68854 | 105 |
val (eqns', ctxt'') = ctxt' |> note Thm.theoremK [defs] |-> abs_def_rule; |
106 |
val deps' = |
|
107 |
(deps ~~ witss) |> map (fn ((dep, morph), wits) => |
|
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
|
108 |
(dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))); |
68854 | 109 |
fun register (dep, eqns) ctxt = |
68851
6c9825c1e26b
clarified signature: explicit type Locale.registration;
wenzelm
parents:
68850
diff
changeset
|
110 |
ctxt |> add_registration |
69058 | 111 |
{inst = dep, |
68851
6c9825c1e26b
clarified signature: explicit type Locale.registration;
wenzelm
parents:
68850
diff
changeset
|
112 |
mixin = |
6c9825c1e26b
clarified signature: explicit type Locale.registration;
wenzelm
parents:
68850
diff
changeset
|
113 |
Option.map (rpair true) |
6c9825c1e26b
clarified signature: explicit type Locale.registration;
wenzelm
parents:
68850
diff
changeset
|
114 |
(Element.eq_morphism (Proof_Context.theory_of ctxt) (eqns @ eqns')), |
6c9825c1e26b
clarified signature: explicit type Locale.registration;
wenzelm
parents:
68850
diff
changeset
|
115 |
export = export}; |
68854 | 116 |
in ctxt'' |> fold register (deps' ~~ eqnss') end; |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
117 |
|
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
118 |
in |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
119 |
|
63380 | 120 |
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
|
121 |
expression raw_defs initial_ctxt = |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
122 |
let |
67777
2d3c1091527b
Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents:
67740
diff
changeset
|
123 |
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
|
124 |
prep_interpretation expression raw_defs initial_ctxt; |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
125 |
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
|
126 |
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
|
127 |
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
|
128 |
|
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
129 |
end; |
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 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
132 |
(** interfaces **) |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
133 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
134 |
(* interpretation in proofs *) |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
135 |
|
61672
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
136 |
local |
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
137 |
|
68850 | 138 |
fun setup_proof state after_qed propss eqns goal_ctxt = |
139 |
Element.witness_local_proof_eqs |
|
140 |
(fn witss => fn eqns => Proof.map_context (after_qed witss eqns) #> Proof.reset_facts) |
|
141 |
"interpret" propss eqns goal_ctxt state; |
|
142 |
||
67777
2d3c1091527b
Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents:
67740
diff
changeset
|
143 |
fun gen_interpret prep_interpretation expression state = |
68850 | 144 |
Proof.assert_forward_or_chain state |
145 |
|> Proof.context_of |
|
146 |
|> generic_interpretation prep_interpretation (setup_proof state) |
|
68852 | 147 |
Attrib.local_notes Locale.add_registration_proof expression []; |
61669 | 148 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
149 |
in |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
150 |
|
63379 | 151 |
val interpret = gen_interpret cert_interpretation; |
152 |
val interpret_cmd = gen_interpret read_interpretation; |
|
61669 | 153 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
154 |
end; |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
155 |
|
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
156 |
|
61890
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
157 |
(* interpretation in local theories *) |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
158 |
|
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
159 |
fun interpretation expression = |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
160 |
generic_interpretation cert_interpretation Element.witness_proof_eqs |
72505 | 161 |
Local_Theory.notes_kind Locale.add_registration_local_theory expression []; |
61890
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
162 |
|
63380 | 163 |
fun interpretation_cmd expression = |
61890
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
164 |
generic_interpretation read_interpretation Element.witness_proof_eqs |
72505 | 165 |
Local_Theory.notes_kind Locale.add_registration_local_theory expression []; |
61890
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
166 |
|
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
167 |
|
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
168 |
(* interpretation into global theories *) |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
169 |
|
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
170 |
fun global_interpretation expression = |
63380 | 171 |
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
|
172 |
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
|
173 |
|
63380 | 174 |
fun global_interpretation_cmd expression = |
175 |
generic_interpretation read_interpretation Element.witness_proof_eqs |
|
176 |
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
|
177 |
|
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
178 |
|
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
179 |
(* interpretation between locales *) |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
180 |
|
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
181 |
fun sublocale expression = |
63380 | 182 |
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
|
183 |
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
|
184 |
|
63380 | 185 |
fun sublocale_cmd expression = |
186 |
generic_interpretation read_interpretation Element.witness_proof_eqs |
|
187 |
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
|
188 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
189 |
local |
61669 | 190 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
191 |
fun gen_global_sublocale prep_loc prep_interpretation |
67777
2d3c1091527b
Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents:
67740
diff
changeset
|
192 |
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
|
193 |
let |
66334
b210ae666a42
provide explicit variant initializers for regular named target vs. almost-named target
haftmann
parents:
63402
diff
changeset
|
194 |
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
|
195 |
fun setup_proof after_qed = |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
196 |
Element.witness_proof_eqs |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
197 |
(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
|
198 |
in |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
199 |
lthy |> |
63380 | 200 |
generic_interpretation prep_interpretation setup_proof |
67777
2d3c1091527b
Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents:
67740
diff
changeset
|
201 |
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
|
202 |
end; |
61669 | 203 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
204 |
in |
61669 | 205 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
206 |
fun global_sublocale expression = |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
207 |
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
|
208 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
209 |
fun global_sublocale_cmd raw_expression = |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
210 |
gen_global_sublocale Locale.check read_interpretation raw_expression; |
61669 | 211 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
212 |
end; |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
213 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
214 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
215 |
(* mixed Isar interface *) |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
216 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
217 |
local |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
218 |
|
61890
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
219 |
fun register_or_activate lthy = |
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
220 |
if Named_Target.is_theory lthy |
61890
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
221 |
then Local_Theory.theory_registration |
72505 | 222 |
else Locale.add_registration_local_theory; |
61669 | 223 |
|
67777
2d3c1091527b
Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents:
67740
diff
changeset
|
224 |
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
|
225 |
generic_interpretation prep_interpretation Element.witness_proof_eqs |
67777
2d3c1091527b
Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents:
67740
diff
changeset
|
226 |
Local_Theory.notes_kind (register_or_activate lthy) expression [] lthy; |
61669 | 227 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
228 |
in |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
229 |
|
61890
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
230 |
fun isar_interpretation expression = |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
231 |
gen_isar_interpretation cert_interpretation expression; |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
232 |
fun isar_interpretation_cmd raw_expression = |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
233 |
gen_isar_interpretation read_interpretation raw_expression; |
61669 | 234 |
|
235 |
end; |
|
236 |
||
237 |
end; |