author | wenzelm |
Thu, 30 Aug 2018 12:36:26 +0200 | |
changeset 68850 | 6d2735ca0271 |
parent 68849 | 0f9b2fa0556f |
child 68851 | 6c9825c1e26b |
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'; |
ec11275fb263
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents:
61774
diff
changeset
|
58 |
in (def, lthy'') end; |
61669 | 59 |
|
67450
b0ae74b86ef3
Experimental support for rewrite morphisms in locale instances.
ballarin
parents:
66334
diff
changeset
|
60 |
fun augment_with_defs _ [] _ ctxt = ([], ctxt) |
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*) |
61775
ec11275fb263
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents:
61774
diff
changeset
|
62 |
| augment_with_defs prep_term raw_defs deps lthy = |
61691
91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset
|
63 |
let |
61775
ec11275fb263
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents:
61774
diff
changeset
|
64 |
val (_, inner_lthy) = |
ec11275fb263
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents:
61774
diff
changeset
|
65 |
Local_Theory.open_target lthy |
ec11275fb263
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents:
61774
diff
changeset
|
66 |
||> fold Locale.activate_declarations deps; |
ec11275fb263
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents:
61774
diff
changeset
|
67 |
val (inner_defs, inner_lthy') = |
67450
b0ae74b86ef3
Experimental support for rewrite morphisms in locale instances.
ballarin
parents:
66334
diff
changeset
|
68 |
fold_map (augment_with_def prep_term) raw_defs inner_lthy; |
61775
ec11275fb263
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents:
61774
diff
changeset
|
69 |
val lthy' = |
ec11275fb263
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents:
61774
diff
changeset
|
70 |
inner_lthy' |
61708
4de2380ae3ab
explicit nested local theory for definitions, however retaining arcane low-level fiddling with background theory
haftmann
parents:
61698
diff
changeset
|
71 |
|> Local_Theory.close_target; |
4de2380ae3ab
explicit nested local theory for definitions, however retaining arcane low-level fiddling with background theory
haftmann
parents:
61698
diff
changeset
|
72 |
val def_eqns = |
61775
ec11275fb263
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents:
61774
diff
changeset
|
73 |
map (singleton (Proof_Context.export inner_lthy' lthy') o Thm.symmetric) inner_defs |
ec11275fb263
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents:
61774
diff
changeset
|
74 |
in (def_eqns, lthy') end; |
ec11275fb263
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents:
61774
diff
changeset
|
75 |
|
67777
2d3c1091527b
Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents:
67740
diff
changeset
|
76 |
fun prep_interpretation prep_expr prep_term |
2d3c1091527b
Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents:
67740
diff
changeset
|
77 |
expression raw_defs initial_ctxt = |
61691
91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset
|
78 |
let |
67450
b0ae74b86ef3
Experimental support for rewrite morphisms in locale instances.
ballarin
parents:
66334
diff
changeset
|
79 |
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
|
80 |
val (def_eqns, def_ctxt) = |
ec11275fb263
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents:
61774
diff
changeset
|
81 |
augment_with_defs prep_term raw_defs deps expr_ctxt; |
67777
2d3c1091527b
Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents:
67740
diff
changeset
|
82 |
val export' = Variable.export_morphism def_ctxt expr_ctxt; |
2d3c1091527b
Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents:
67740
diff
changeset
|
83 |
in (((propss, eq_propss, deps, eqnss, export, export'), def_eqns), def_ctxt) end; |
61669 | 84 |
|
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
85 |
in |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
86 |
|
61698 | 87 |
fun cert_interpretation expression = |
67777
2d3c1091527b
Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents:
67740
diff
changeset
|
88 |
prep_interpretation Expression.cert_goal_expression Syntax.check_term expression; |
61672
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
89 |
|
61698 | 90 |
fun read_interpretation expression = |
67777
2d3c1091527b
Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents:
67740
diff
changeset
|
91 |
prep_interpretation Expression.read_goal_expression Syntax.read_term expression; |
61669 | 92 |
|
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
93 |
end; |
61669 | 94 |
|
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
95 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
96 |
(* interpretation machinery *) |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
97 |
|
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
98 |
local |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
99 |
|
63381 | 100 |
fun meta_rewrite eqns ctxt = |
101 |
(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
|
102 |
|
68849 | 103 |
fun note_eqns_register pos note add_registration |
104 |
deps eqnss witss def_eqns thms export export' ctxt = |
|
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
105 |
let |
68849 | 106 |
val factss = thms |
107 |
|> unflat ((map o map) #1 eqnss) |
|
108 |
|> map2 (map2 (fn b => fn eq => (b, [([Morphism.thm export eq], [])]))) ((map o map) #1 eqnss); |
|
109 |
val (eqnss', ctxt') = |
|
110 |
fold_map (fn facts => note Thm.theoremK facts #-> meta_rewrite) factss ctxt; |
|
67777
2d3c1091527b
Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents:
67740
diff
changeset
|
111 |
val defs = (Binding.empty_atts, [(map (Morphism.thm (export' $> export)) def_eqns, [])]); |
67450
b0ae74b86ef3
Experimental support for rewrite morphisms in locale instances.
ballarin
parents:
66334
diff
changeset
|
112 |
val (eqns', ctxt'') = ctxt' |
67777
2d3c1091527b
Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents:
67740
diff
changeset
|
113 |
|> note Thm.theoremK [defs] |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
114 |
|-> meta_rewrite; |
63381 | 115 |
val dep_morphs = |
116 |
map2 (fn (dep, morph) => fn wits => |
|
63382
4270da306442
clarified positions, e.g. for reports on literal facts;
wenzelm
parents:
63381
diff
changeset
|
117 |
let val morph' = morph |
4270da306442
clarified positions, e.g. for reports on literal facts;
wenzelm
parents:
63381
diff
changeset
|
118 |
$> Element.satisfy_morphism (map (Element.transform_witness export') wits) |
4270da306442
clarified positions, e.g. for reports on literal facts;
wenzelm
parents:
63381
diff
changeset
|
119 |
$> Morphism.binding_morphism "position" (Binding.set_pos pos) |
4270da306442
clarified positions, e.g. for reports on literal facts;
wenzelm
parents:
63381
diff
changeset
|
120 |
in (dep, morph') end) deps witss; |
68849 | 121 |
fun register (dep_morph, eqns) ctxt = |
122 |
add_registration dep_morph |
|
67450
b0ae74b86ef3
Experimental support for rewrite morphisms in locale instances.
ballarin
parents:
66334
diff
changeset
|
123 |
(Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) (eqns @ eqns'))) |
63381 | 124 |
export ctxt; |
68849 | 125 |
in ctxt'' |> fold register (dep_morphs ~~ eqnss') end; |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
126 |
|
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
127 |
in |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
128 |
|
63380 | 129 |
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
|
130 |
expression raw_defs initial_ctxt = |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
131 |
let |
67777
2d3c1091527b
Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents:
67740
diff
changeset
|
132 |
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
|
133 |
prep_interpretation expression raw_defs initial_ctxt; |
63382
4270da306442
clarified positions, e.g. for reports on literal facts;
wenzelm
parents:
63381
diff
changeset
|
134 |
val pos = Position.thread_data (); |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
135 |
fun after_qed witss eqns = |
67777
2d3c1091527b
Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents:
67740
diff
changeset
|
136 |
note_eqns_register pos note add_registration deps eqnss witss def_eqns eqns export export'; |
2d3c1091527b
Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents:
67740
diff
changeset
|
137 |
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
|
138 |
|
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
139 |
end; |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
140 |
|
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
141 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
142 |
(** interfaces **) |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
143 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
144 |
(* interpretation in proofs *) |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
145 |
|
61672
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
146 |
local |
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
147 |
|
68850 | 148 |
fun setup_proof state after_qed propss eqns goal_ctxt = |
149 |
Element.witness_local_proof_eqs |
|
150 |
(fn witss => fn eqns => Proof.map_context (after_qed witss eqns) #> Proof.reset_facts) |
|
151 |
"interpret" propss eqns goal_ctxt state; |
|
152 |
||
153 |
fun add_registration reg mixin export ctxt = ctxt |
|
154 |
|> Proof_Context.set_stmt false |
|
155 |
|> Context.proof_map (Locale.add_registration reg mixin export) |
|
156 |
|> Proof_Context.restore_stmt ctxt; |
|
157 |
||
67777
2d3c1091527b
Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents:
67740
diff
changeset
|
158 |
fun gen_interpret prep_interpretation expression state = |
68850 | 159 |
Proof.assert_forward_or_chain state |
160 |
|> Proof.context_of |
|
161 |
|> generic_interpretation prep_interpretation (setup_proof state) |
|
162 |
Attrib.local_notes add_registration expression []; |
|
61669 | 163 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
164 |
in |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
165 |
|
63379 | 166 |
val interpret = gen_interpret cert_interpretation; |
167 |
val interpret_cmd = gen_interpret read_interpretation; |
|
61669 | 168 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
169 |
end; |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
170 |
|
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
171 |
|
61890
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
172 |
(* interpretation in local theories *) |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
173 |
|
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
174 |
fun interpretation expression = |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
175 |
generic_interpretation cert_interpretation Element.witness_proof_eqs |
63380 | 176 |
Local_Theory.notes_kind Locale.activate_fragment expression []; |
61890
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
177 |
|
63380 | 178 |
fun interpretation_cmd expression = |
61890
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
179 |
generic_interpretation read_interpretation Element.witness_proof_eqs |
63380 | 180 |
Local_Theory.notes_kind Locale.activate_fragment expression []; |
61890
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
181 |
|
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
182 |
|
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
183 |
(* interpretation into global theories *) |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
184 |
|
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
185 |
fun global_interpretation expression = |
63380 | 186 |
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
|
187 |
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
|
188 |
|
63380 | 189 |
fun global_interpretation_cmd expression = |
190 |
generic_interpretation read_interpretation Element.witness_proof_eqs |
|
191 |
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
|
192 |
|
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
193 |
|
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
194 |
(* interpretation between locales *) |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
195 |
|
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
196 |
fun sublocale expression = |
63380 | 197 |
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
|
198 |
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
|
199 |
|
63380 | 200 |
fun sublocale_cmd expression = |
201 |
generic_interpretation read_interpretation Element.witness_proof_eqs |
|
202 |
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
|
203 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
204 |
local |
61669 | 205 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
206 |
fun gen_global_sublocale prep_loc prep_interpretation |
67777
2d3c1091527b
Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents:
67740
diff
changeset
|
207 |
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
|
208 |
let |
66334
b210ae666a42
provide explicit variant initializers for regular named target vs. almost-named target
haftmann
parents:
63402
diff
changeset
|
209 |
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
|
210 |
fun setup_proof after_qed = |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
211 |
Element.witness_proof_eqs |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
212 |
(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
|
213 |
in |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
214 |
lthy |> |
63380 | 215 |
generic_interpretation prep_interpretation setup_proof |
67777
2d3c1091527b
Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents:
67740
diff
changeset
|
216 |
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
|
217 |
end; |
61669 | 218 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
219 |
in |
61669 | 220 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
221 |
fun global_sublocale expression = |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
222 |
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
|
223 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
224 |
fun global_sublocale_cmd raw_expression = |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
225 |
gen_global_sublocale Locale.check read_interpretation raw_expression; |
61669 | 226 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
227 |
end; |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
228 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
229 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
230 |
(* mixed Isar interface *) |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
231 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
232 |
local |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
233 |
|
61890
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
234 |
fun register_or_activate lthy = |
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
235 |
if Named_Target.is_theory lthy |
61890
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
236 |
then Local_Theory.theory_registration |
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
237 |
else Locale.activate_fragment; |
61669 | 238 |
|
67777
2d3c1091527b
Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents:
67740
diff
changeset
|
239 |
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
|
240 |
generic_interpretation prep_interpretation Element.witness_proof_eqs |
67777
2d3c1091527b
Drop rewrite rule arguments of sublocale and interpretation implementations.
ballarin
parents:
67740
diff
changeset
|
241 |
Local_Theory.notes_kind (register_or_activate lthy) expression [] lthy; |
61669 | 242 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
243 |
in |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
244 |
|
61890
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
245 |
fun isar_interpretation expression = |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
246 |
gen_isar_interpretation cert_interpretation expression; |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
247 |
fun isar_interpretation_cmd raw_expression = |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
248 |
gen_isar_interpretation read_interpretation raw_expression; |
61669 | 249 |
|
250 |
end; |
|
251 |
||
252 |
end; |