author | wenzelm |
Wed, 06 Jul 2016 11:29:51 +0200 | |
changeset 63402 | f199837304d7 |
parent 63382 | 4270da306442 |
child 66334 | b210ae666a42 |
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 |
type 'a rewrites = (Attrib.binding * 'a) list |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
12 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
13 |
(*interpretation in proofs*) |
62680
646b84666a56
eliminated unused argument (see also 58110c1e02bc);
wenzelm
parents:
61890
diff
changeset
|
14 |
val interpret: Expression.expression_i -> term rewrites -> Proof.state -> Proof.state |
646b84666a56
eliminated unused argument (see also 58110c1e02bc);
wenzelm
parents:
61890
diff
changeset
|
15 |
val interpret_cmd: Expression.expression -> string rewrites -> Proof.state -> Proof.state |
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
16 |
|
61890
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
17 |
(*interpretation in local theories*) |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
18 |
val interpretation: Expression.expression_i -> |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
19 |
term rewrites -> local_theory -> Proof.state |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
20 |
val interpretation_cmd: Expression.expression -> |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
21 |
string rewrites -> local_theory -> Proof.state |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
22 |
|
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
23 |
(*interpretation into global theories*) |
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
24 |
val global_interpretation: Expression.expression_i -> |
61890
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
25 |
term defines -> term rewrites -> local_theory -> Proof.state |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
26 |
val global_interpretation_cmd: Expression.expression -> |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
27 |
string defines -> string rewrites -> local_theory -> Proof.state |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
28 |
|
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
29 |
(*interpretation between locales*) |
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
30 |
val sublocale: Expression.expression_i -> |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
31 |
term defines -> term rewrites -> local_theory -> Proof.state |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
32 |
val sublocale_cmd: Expression.expression -> |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
33 |
string defines -> string rewrites -> local_theory -> Proof.state |
61890
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
34 |
val global_sublocale: string -> Expression.expression_i -> |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
35 |
term defines -> term rewrites -> theory -> Proof.state |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
36 |
val global_sublocale_cmd: xstring * Position.T -> Expression.expression -> |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
37 |
string defines -> string rewrites -> theory -> Proof.state |
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
38 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
39 |
(*mixed Isar interface*) |
61890
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
40 |
val isar_interpretation: Expression.expression_i -> |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
41 |
term rewrites -> local_theory -> Proof.state |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
42 |
val isar_interpretation_cmd: Expression.expression -> |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
43 |
string rewrites -> local_theory -> Proof.state |
61669 | 44 |
end; |
45 |
||
46 |
structure Interpretation : INTERPRETATION = |
|
47 |
struct |
|
48 |
||
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
49 |
(** common interpretation machinery **) |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
50 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
51 |
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
|
52 |
type 'a rewrites = (Attrib.binding * 'a) list |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
53 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
54 |
(* reading of locale expressions with rewrite morphisms *) |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
55 |
|
61672
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
56 |
local |
61669 | 57 |
|
61775
ec11275fb263
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents:
61774
diff
changeset
|
58 |
fun augment_with_def prep_term deps ((name, atts), ((b, mx), raw_rhs)) lthy = |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
59 |
let |
61775
ec11275fb263
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents:
61774
diff
changeset
|
60 |
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
|
61 |
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
|
62 |
val ((_, (_, def)), lthy'') = |
ec11275fb263
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents:
61774
diff
changeset
|
63 |
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
|
64 |
in (def, lthy'') end; |
61669 | 65 |
|
61775
ec11275fb263
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents:
61774
diff
changeset
|
66 |
fun augment_with_defs prep_term [] deps ctxt = ([], ctxt) |
61691
91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset
|
67 |
(*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
|
68 |
| 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
|
69 |
let |
61775
ec11275fb263
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents:
61774
diff
changeset
|
70 |
val (_, inner_lthy) = |
ec11275fb263
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents:
61774
diff
changeset
|
71 |
Local_Theory.open_target lthy |
ec11275fb263
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents:
61774
diff
changeset
|
72 |
||> fold Locale.activate_declarations deps; |
ec11275fb263
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents:
61774
diff
changeset
|
73 |
val (inner_defs, inner_lthy') = |
ec11275fb263
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents:
61774
diff
changeset
|
74 |
fold_map (augment_with_def prep_term deps) raw_defs inner_lthy; |
ec11275fb263
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents:
61774
diff
changeset
|
75 |
val lthy' = |
ec11275fb263
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents:
61774
diff
changeset
|
76 |
inner_lthy' |
61708
4de2380ae3ab
explicit nested local theory for definitions, however retaining arcane low-level fiddling with background theory
haftmann
parents:
61698
diff
changeset
|
77 |
|> 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
|
78 |
val def_eqns = |
61775
ec11275fb263
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents:
61774
diff
changeset
|
79 |
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
|
80 |
in (def_eqns, lthy') end; |
ec11275fb263
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents:
61774
diff
changeset
|
81 |
|
ec11275fb263
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents:
61774
diff
changeset
|
82 |
fun prep_eqns prep_props prep_attr [] deps ctxt = ([], []) |
ec11275fb263
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents:
61774
diff
changeset
|
83 |
| prep_eqns prep_props prep_attr raw_eqns deps ctxt = |
ec11275fb263
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents:
61774
diff
changeset
|
84 |
let |
ec11275fb263
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents:
61774
diff
changeset
|
85 |
val ctxt' = fold Locale.activate_declarations deps ctxt; |
ec11275fb263
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents:
61774
diff
changeset
|
86 |
val eqns = |
ec11275fb263
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents:
61774
diff
changeset
|
87 |
(Variable.export_terms ctxt' ctxt o prep_props ctxt' o map snd) raw_eqns; |
ec11275fb263
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents:
61774
diff
changeset
|
88 |
val attrss = map (apsnd (map (prep_attr ctxt)) o fst) raw_eqns; |
ec11275fb263
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents:
61774
diff
changeset
|
89 |
in (eqns, attrss) end; |
61691
91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset
|
90 |
|
61774
029162bc9793
prefer conventional read/check distinction over manual check
haftmann
parents:
61773
diff
changeset
|
91 |
fun prep_interpretation prep_expr prep_term prep_props prep_attr |
61691
91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset
|
92 |
expression raw_defs raw_eqns initial_ctxt = |
91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset
|
93 |
let |
91854ba66adb
clarified contexts by factoring out reading and definition of mixins
haftmann
parents:
61684
diff
changeset
|
94 |
val ((propss, deps, 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
|
95 |
val (def_eqns, def_ctxt) = |
ec11275fb263
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents:
61774
diff
changeset
|
96 |
augment_with_defs prep_term raw_defs deps expr_ctxt; |
ec11275fb263
alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
haftmann
parents:
61774
diff
changeset
|
97 |
val (eqns, attrss) = prep_eqns prep_props prep_attr raw_eqns deps def_ctxt; |
61672
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
98 |
val goal_ctxt = fold Variable.auto_fixes eqns def_ctxt; |
61772
2f33f6cc964d
formally correct context for export, which got screwed up in 87203a0f0041
haftmann
parents:
61771
diff
changeset
|
99 |
val export' = Variable.export_morphism goal_ctxt expr_ctxt; |
61672
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
100 |
in (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end; |
61669 | 101 |
|
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
102 |
in |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
103 |
|
61698 | 104 |
fun cert_interpretation expression = |
61774
029162bc9793
prefer conventional read/check distinction over manual check
haftmann
parents:
61773
diff
changeset
|
105 |
prep_interpretation Expression.cert_goal_expression Syntax.check_term |
029162bc9793
prefer conventional read/check distinction over manual check
haftmann
parents:
61773
diff
changeset
|
106 |
Syntax.check_props (K I) expression; |
61672
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
107 |
|
61698 | 108 |
fun read_interpretation expression = |
61774
029162bc9793
prefer conventional read/check distinction over manual check
haftmann
parents:
61773
diff
changeset
|
109 |
prep_interpretation Expression.read_goal_expression Syntax.read_term |
029162bc9793
prefer conventional read/check distinction over manual check
haftmann
parents:
61773
diff
changeset
|
110 |
Syntax.read_props Attrib.check_src expression; |
61669 | 111 |
|
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
112 |
end; |
61669 | 113 |
|
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
114 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
115 |
(* interpretation machinery *) |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
116 |
|
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
117 |
local |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
118 |
|
63381 | 119 |
fun meta_rewrite eqns ctxt = |
120 |
(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
|
121 |
|
63382
4270da306442
clarified positions, e.g. for reports on literal facts;
wenzelm
parents:
63381
diff
changeset
|
122 |
fun note_eqns_register pos note activate deps witss def_eqns eqns attrss export export' ctxt = |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
123 |
let |
63381 | 124 |
val facts = |
125 |
(Binding.empty_atts, [(map (Morphism.thm (export' $> export)) def_eqns, [])]) :: |
|
126 |
map2 (fn attrs => fn eqn => (attrs, [([Morphism.thm (export' $> export) eqn], [])])) |
|
127 |
attrss eqns; |
|
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
128 |
val (eqns', ctxt') = ctxt |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
129 |
|> note Thm.theoremK facts |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
130 |
|-> meta_rewrite; |
63381 | 131 |
val dep_morphs = |
132 |
map2 (fn (dep, morph) => fn wits => |
|
63382
4270da306442
clarified positions, e.g. for reports on literal facts;
wenzelm
parents:
63381
diff
changeset
|
133 |
let val morph' = morph |
4270da306442
clarified positions, e.g. for reports on literal facts;
wenzelm
parents:
63381
diff
changeset
|
134 |
$> Element.satisfy_morphism (map (Element.transform_witness export') wits) |
4270da306442
clarified positions, e.g. for reports on literal facts;
wenzelm
parents:
63381
diff
changeset
|
135 |
$> Morphism.binding_morphism "position" (Binding.set_pos pos) |
4270da306442
clarified positions, e.g. for reports on literal facts;
wenzelm
parents:
63381
diff
changeset
|
136 |
in (dep, morph') end) deps witss; |
63381 | 137 |
fun activate' dep_morph ctxt = |
138 |
activate dep_morph |
|
139 |
(Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) |
|
140 |
export ctxt; |
|
141 |
in ctxt' |> fold activate' dep_morphs end; |
|
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
142 |
|
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
143 |
in |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
144 |
|
63380 | 145 |
fun generic_interpretation prep_interpretation setup_proof note add_registration |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
146 |
expression raw_defs raw_eqns initial_ctxt = |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
147 |
let |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
148 |
val (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) = |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
149 |
prep_interpretation expression raw_defs raw_eqns initial_ctxt; |
63382
4270da306442
clarified positions, e.g. for reports on literal facts;
wenzelm
parents:
63381
diff
changeset
|
150 |
val pos = Position.thread_data (); |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
151 |
fun after_qed witss eqns = |
63382
4270da306442
clarified positions, e.g. for reports on literal facts;
wenzelm
parents:
63381
diff
changeset
|
152 |
note_eqns_register pos note add_registration deps witss def_eqns eqns attrss export export'; |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
153 |
in setup_proof after_qed propss eqns goal_ctxt end; |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
154 |
|
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
155 |
end; |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
156 |
|
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
157 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
158 |
(** interfaces **) |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
159 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
160 |
(* interpretation in proofs *) |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
161 |
|
61672
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
162 |
local |
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
163 |
|
62680
646b84666a56
eliminated unused argument (see also 58110c1e02bc);
wenzelm
parents:
61890
diff
changeset
|
164 |
fun gen_interpret prep_interpretation expression raw_eqns state = |
61669 | 165 |
let |
166 |
val _ = Proof.assert_forward_or_chain state; |
|
167 |
fun lift_after_qed after_qed witss eqns = |
|
168 |
Proof.map_context (after_qed witss eqns) #> Proof.reset_facts; |
|
169 |
fun setup_proof after_qed propss eqns goal_ctxt = |
|
170 |
Element.witness_local_proof_eqs (lift_after_qed after_qed) "interpret" |
|
62680
646b84666a56
eliminated unused argument (see also 58110c1e02bc);
wenzelm
parents:
61890
diff
changeset
|
171 |
propss eqns goal_ctxt state; |
61669 | 172 |
in |
63379 | 173 |
Proof.context_of state |
174 |
|> generic_interpretation prep_interpretation setup_proof |
|
63380 | 175 |
Attrib.local_notes (Context.proof_map ooo Locale.add_registration) expression [] raw_eqns |
61669 | 176 |
end; |
177 |
||
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
178 |
in |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
179 |
|
63379 | 180 |
val interpret = gen_interpret cert_interpretation; |
181 |
val interpret_cmd = gen_interpret read_interpretation; |
|
61669 | 182 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
183 |
end; |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
184 |
|
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
185 |
|
61890
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
186 |
(* interpretation in local theories *) |
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 |
fun interpretation expression = |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
189 |
generic_interpretation cert_interpretation Element.witness_proof_eqs |
63380 | 190 |
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
|
191 |
|
63380 | 192 |
fun interpretation_cmd expression = |
61890
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
193 |
generic_interpretation read_interpretation Element.witness_proof_eqs |
63380 | 194 |
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
|
195 |
|
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
196 |
|
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
197 |
(* interpretation into global theories *) |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
198 |
|
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
199 |
fun global_interpretation expression = |
63380 | 200 |
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
|
201 |
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
|
202 |
|
63380 | 203 |
fun global_interpretation_cmd expression = |
204 |
generic_interpretation read_interpretation Element.witness_proof_eqs |
|
205 |
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
|
206 |
|
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
207 |
|
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
208 |
(* interpretation between locales *) |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
209 |
|
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
210 |
fun sublocale expression = |
63380 | 211 |
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
|
212 |
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
|
213 |
|
63380 | 214 |
fun sublocale_cmd expression = |
215 |
generic_interpretation read_interpretation Element.witness_proof_eqs |
|
216 |
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
|
217 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
218 |
local |
61669 | 219 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
220 |
fun gen_global_sublocale prep_loc prep_interpretation |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
221 |
raw_locale expression raw_defs raw_eqns thy = |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
222 |
let |
63402 | 223 |
val lthy = Named_Target.init NONE (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
|
224 |
fun setup_proof after_qed = |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
225 |
Element.witness_proof_eqs |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
226 |
(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
|
227 |
in |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
228 |
lthy |> |
63380 | 229 |
generic_interpretation prep_interpretation setup_proof |
61890
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
230 |
Local_Theory.notes_kind Local_Theory.locale_dependency expression raw_defs raw_eqns |
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
231 |
end; |
61669 | 232 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
233 |
in |
61669 | 234 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
235 |
fun global_sublocale expression = |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
236 |
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
|
237 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
238 |
fun global_sublocale_cmd raw_expression = |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
239 |
gen_global_sublocale Locale.check read_interpretation raw_expression; |
61669 | 240 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
241 |
end; |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
242 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
243 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
244 |
(* mixed Isar interface *) |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
245 |
|
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
246 |
local |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
247 |
|
61890
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
248 |
fun register_or_activate lthy = |
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
249 |
if Named_Target.is_theory lthy |
61890
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
250 |
then Local_Theory.theory_registration |
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
251 |
else Locale.activate_fragment; |
61669 | 252 |
|
61890
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
253 |
fun gen_isar_interpretation prep_interpretation expression raw_eqns lthy = |
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
254 |
generic_interpretation prep_interpretation Element.witness_proof_eqs |
63380 | 255 |
Local_Theory.notes_kind (register_or_activate lthy) expression [] raw_eqns lthy; |
61669 | 256 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
257 |
in |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61672
diff
changeset
|
258 |
|
61890
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
259 |
fun isar_interpretation expression = |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
260 |
gen_isar_interpretation cert_interpretation expression; |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
261 |
fun isar_interpretation_cmd raw_expression = |
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
61823
diff
changeset
|
262 |
gen_isar_interpretation read_interpretation raw_expression; |
61669 | 263 |
|
264 |
end; |
|
265 |
||
266 |
end; |