6 *) |
6 *) |
7 |
7 |
8 signature INTERPRETATION = |
8 signature INTERPRETATION = |
9 sig |
9 sig |
10 type 'a defines = (Attrib.binding * ((binding * mixfix) * 'a)) list |
10 type 'a defines = (Attrib.binding * ((binding * mixfix) * 'a)) list |
11 type 'a rewrites = (Attrib.binding * 'a) list |
|
12 |
11 |
13 (*interpretation in proofs*) |
12 (*interpretation in proofs*) |
14 val interpret: Expression.expression_i -> term rewrites -> Proof.state -> Proof.state |
13 val interpret: Expression.expression_i -> Proof.state -> Proof.state |
15 val interpret_cmd: Expression.expression -> string rewrites -> Proof.state -> Proof.state |
14 val interpret_cmd: Expression.expression -> Proof.state -> Proof.state |
16 |
15 |
17 (*interpretation in local theories*) |
16 (*interpretation in local theories*) |
18 val interpretation: Expression.expression_i -> |
17 val interpretation: Expression.expression_i -> local_theory -> Proof.state |
19 term rewrites -> local_theory -> Proof.state |
18 val interpretation_cmd: Expression.expression -> local_theory -> Proof.state |
20 val interpretation_cmd: Expression.expression -> |
|
21 string rewrites -> local_theory -> Proof.state |
|
22 |
19 |
23 (*interpretation into global theories*) |
20 (*interpretation into global theories*) |
24 val global_interpretation: Expression.expression_i -> |
21 val global_interpretation: Expression.expression_i -> |
25 term defines -> term rewrites -> local_theory -> Proof.state |
22 term defines -> local_theory -> Proof.state |
26 val global_interpretation_cmd: Expression.expression -> |
23 val global_interpretation_cmd: Expression.expression -> |
27 string defines -> string rewrites -> local_theory -> Proof.state |
24 string defines -> local_theory -> Proof.state |
28 |
25 |
29 (*interpretation between locales*) |
26 (*interpretation between locales*) |
30 val sublocale: Expression.expression_i -> |
27 val sublocale: Expression.expression_i -> |
31 term defines -> term rewrites -> local_theory -> Proof.state |
28 term defines -> local_theory -> Proof.state |
32 val sublocale_cmd: Expression.expression -> |
29 val sublocale_cmd: Expression.expression -> |
33 string defines -> string rewrites -> local_theory -> Proof.state |
30 string defines -> local_theory -> Proof.state |
34 val global_sublocale: string -> Expression.expression_i -> |
31 val global_sublocale: string -> Expression.expression_i -> |
35 term defines -> term rewrites -> theory -> Proof.state |
32 term defines -> theory -> Proof.state |
36 val global_sublocale_cmd: xstring * Position.T -> Expression.expression -> |
33 val global_sublocale_cmd: xstring * Position.T -> Expression.expression -> |
37 string defines -> string rewrites -> theory -> Proof.state |
34 string defines -> theory -> Proof.state |
38 |
35 |
39 (*mixed Isar interface*) |
36 (*mixed Isar interface*) |
40 val isar_interpretation: Expression.expression_i -> |
37 val isar_interpretation: Expression.expression_i -> local_theory -> Proof.state |
41 term rewrites -> local_theory -> Proof.state |
38 val isar_interpretation_cmd: Expression.expression -> local_theory -> Proof.state |
42 val isar_interpretation_cmd: Expression.expression -> |
|
43 string rewrites -> local_theory -> Proof.state |
|
44 end; |
39 end; |
45 |
40 |
46 structure Interpretation : INTERPRETATION = |
41 structure Interpretation : INTERPRETATION = |
47 struct |
42 struct |
48 |
43 |
49 (** common interpretation machinery **) |
44 (** common interpretation machinery **) |
50 |
45 |
51 type 'a defines = (Attrib.binding * ((binding * mixfix) * 'a)) list |
46 type 'a defines = (Attrib.binding * ((binding * mixfix) * 'a)) list |
52 type 'a rewrites = 'a Expression.rewrites |
|
53 |
47 |
54 (* reading of locale expressions with rewrite morphisms *) |
48 (* reading of locale expressions with rewrite morphisms *) |
55 |
49 |
56 local |
50 local |
57 |
51 |
77 |> Local_Theory.close_target; |
71 |> Local_Theory.close_target; |
78 val def_eqns = |
72 val def_eqns = |
79 map (singleton (Proof_Context.export inner_lthy' lthy') o Thm.symmetric) inner_defs |
73 map (singleton (Proof_Context.export inner_lthy' lthy') o Thm.symmetric) inner_defs |
80 in (def_eqns, lthy') end; |
74 in (def_eqns, lthy') end; |
81 |
75 |
82 fun prep_eqns _ _ [] _ _ = ([], []) |
76 fun prep_interpretation prep_expr prep_term |
83 | prep_eqns prep_props prep_attr raw_eqns deps ctxt = |
77 expression raw_defs initial_ctxt = |
84 let |
|
85 (* FIXME incompatibility, creating context for parsing rewrites equation may fail in |
|
86 presence of rewrites clause in expression *) |
|
87 val ctxt' = fold Locale.activate_declarations deps ctxt; |
|
88 val eqns = |
|
89 (Variable.export_terms ctxt' ctxt o prep_props ctxt' o map snd) raw_eqns; |
|
90 val attrss = map (apsnd (map (prep_attr ctxt)) o fst) raw_eqns; |
|
91 in (eqns, attrss) end; |
|
92 |
|
93 fun prep_interpretation prep_expr prep_term prep_props prep_attr |
|
94 expression raw_defs raw_eqns initial_ctxt = |
|
95 let |
78 let |
96 val ((propss, eq_propss, deps, eqnss, export), expr_ctxt) = prep_expr expression initial_ctxt; |
79 val ((propss, eq_propss, deps, eqnss, export), expr_ctxt) = prep_expr expression initial_ctxt; |
97 val (def_eqns, def_ctxt) = |
80 val (def_eqns, def_ctxt) = |
98 augment_with_defs prep_term raw_defs deps expr_ctxt; |
81 augment_with_defs prep_term raw_defs deps expr_ctxt; |
99 val (eqns, attrss) = prep_eqns prep_props prep_attr raw_eqns deps def_ctxt; |
82 val export' = Variable.export_morphism def_ctxt expr_ctxt; |
100 val goal_ctxt = fold Variable.auto_fixes eqns def_ctxt; |
83 in (((propss, eq_propss, deps, eqnss, export, export'), def_eqns), def_ctxt) end; |
101 val export' = Variable.export_morphism goal_ctxt expr_ctxt; |
|
102 in (((propss, eq_propss, deps, eqnss, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end; |
|
103 |
84 |
104 in |
85 in |
105 |
86 |
106 fun cert_interpretation expression = |
87 fun cert_interpretation expression = |
107 prep_interpretation Expression.cert_goal_expression Syntax.check_term |
88 prep_interpretation Expression.cert_goal_expression Syntax.check_term expression; |
108 Syntax.check_props (K I) expression; |
|
109 |
89 |
110 fun read_interpretation expression = |
90 fun read_interpretation expression = |
111 prep_interpretation Expression.read_goal_expression Syntax.read_term |
91 prep_interpretation Expression.read_goal_expression Syntax.read_term expression; |
112 Syntax.read_props Attrib.check_src expression; |
|
113 |
92 |
114 end; |
93 end; |
115 |
94 |
116 |
95 |
117 (* interpretation machinery *) |
96 (* interpretation machinery *) |
119 local |
98 local |
120 |
99 |
121 fun meta_rewrite eqns ctxt = |
100 fun meta_rewrite eqns ctxt = |
122 (map (Local_Defs.abs_def_rule ctxt) (maps snd eqns), ctxt); |
101 (map (Local_Defs.abs_def_rule ctxt) (maps snd eqns), ctxt); |
123 |
102 |
124 fun note_eqns_register pos note activate deps eqnss witss def_eqns thms attrss export export' ctxt = |
103 fun note_eqns_register pos note activate deps eqnss witss def_eqns thms export export' ctxt = |
125 let |
104 let |
126 val (thmss, thms') = split_last (unflat ((map o map) fst eqnss @ [attrss]) thms); |
105 val thmss = unflat ((map o map) fst eqnss) thms; |
127 val factss = |
106 val factss = |
128 map2 (map2 (fn b => fn eq => (b, [([Morphism.thm export eq], [])]))) ((map o map) fst eqnss) thmss; |
107 map2 (map2 (fn b => fn eq => (b, [([Morphism.thm export eq], [])]))) ((map o map) fst eqnss) thmss; |
129 val (eqnss', ctxt') = fold_map (fn facts => note Thm.theoremK facts #-> meta_rewrite) factss ctxt; |
108 val (eqnss', ctxt') = fold_map (fn facts => note Thm.theoremK facts #-> meta_rewrite) factss ctxt; |
130 val facts = |
109 val defs = (Binding.empty_atts, [(map (Morphism.thm (export' $> export)) def_eqns, [])]); |
131 (Binding.empty_atts, [(map (Morphism.thm (export' $> export)) def_eqns, [])]) :: |
|
132 map2 (fn attrs => fn eqn => (attrs, [([Morphism.thm (export' $> export) eqn], [])])) |
|
133 attrss thms'; |
|
134 val (eqns', ctxt'') = ctxt' |
110 val (eqns', ctxt'') = ctxt' |
135 |> note Thm.theoremK facts |
111 |> note Thm.theoremK [defs] |
136 |-> meta_rewrite; |
112 |-> meta_rewrite; |
137 val dep_morphs = |
113 val dep_morphs = |
138 map2 (fn (dep, morph) => fn wits => |
114 map2 (fn (dep, morph) => fn wits => |
139 let val morph' = morph |
115 let val morph' = morph |
140 $> Element.satisfy_morphism (map (Element.transform_witness export') wits) |
116 $> Element.satisfy_morphism (map (Element.transform_witness export') wits) |
147 in ctxt'' |> fold activate' (dep_morphs ~~ eqnss') end; |
123 in ctxt'' |> fold activate' (dep_morphs ~~ eqnss') end; |
148 |
124 |
149 in |
125 in |
150 |
126 |
151 fun generic_interpretation prep_interpretation setup_proof note add_registration |
127 fun generic_interpretation prep_interpretation setup_proof note add_registration |
152 expression raw_defs raw_eqns initial_ctxt = |
128 expression raw_defs initial_ctxt = |
153 let |
129 let |
154 val (((propss, eq_propss, deps, eqnss, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) = |
130 val (((propss, eq_propss, deps, eqnss, export, export'), def_eqns), goal_ctxt) = |
155 prep_interpretation expression raw_defs raw_eqns initial_ctxt; |
131 prep_interpretation expression raw_defs initial_ctxt; |
156 val pos = Position.thread_data (); |
132 val pos = Position.thread_data (); |
157 fun after_qed witss eqns = |
133 fun after_qed witss eqns = |
158 note_eqns_register pos note add_registration deps eqnss witss def_eqns eqns attrss export export'; |
134 note_eqns_register pos note add_registration deps eqnss witss def_eqns eqns export export'; |
159 in setup_proof after_qed propss (flat (eq_propss @ [eqns])) goal_ctxt end; |
135 in setup_proof after_qed propss (flat eq_propss) goal_ctxt end; |
160 |
136 |
161 end; |
137 end; |
162 |
138 |
163 |
139 |
164 (** interfaces **) |
140 (** interfaces **) |
165 |
141 |
166 (* interpretation in proofs *) |
142 (* interpretation in proofs *) |
167 |
143 |
168 local |
144 local |
169 |
145 |
170 fun gen_interpret prep_interpretation expression raw_eqns state = |
146 fun gen_interpret prep_interpretation expression state = |
171 let |
147 let |
172 val _ = Proof.assert_forward_or_chain state; |
148 val _ = Proof.assert_forward_or_chain state; |
173 fun lift_after_qed after_qed witss eqns = |
149 fun lift_after_qed after_qed witss eqns = |
174 Proof.map_context (after_qed witss eqns) #> Proof.reset_facts; |
150 Proof.map_context (after_qed witss eqns) #> Proof.reset_facts; |
175 fun setup_proof after_qed propss eqns goal_ctxt = |
151 fun setup_proof after_qed propss eqns goal_ctxt = |
226 Local_Theory.notes_kind Local_Theory.locale_dependency expression; |
202 Local_Theory.notes_kind Local_Theory.locale_dependency expression; |
227 |
203 |
228 local |
204 local |
229 |
205 |
230 fun gen_global_sublocale prep_loc prep_interpretation |
206 fun gen_global_sublocale prep_loc prep_interpretation |
231 raw_locale expression raw_defs raw_eqns thy = |
207 raw_locale expression raw_defs thy = |
232 let |
208 let |
233 val lthy = Named_Target.init (prep_loc thy raw_locale) thy; |
209 val lthy = Named_Target.init (prep_loc thy raw_locale) thy; |
234 fun setup_proof after_qed = |
210 fun setup_proof after_qed = |
235 Element.witness_proof_eqs |
211 Element.witness_proof_eqs |
236 (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit); |
212 (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit); |
237 in |
213 in |
238 lthy |> |
214 lthy |> |
239 generic_interpretation prep_interpretation setup_proof |
215 generic_interpretation prep_interpretation setup_proof |
240 Local_Theory.notes_kind Local_Theory.locale_dependency expression raw_defs raw_eqns |
216 Local_Theory.notes_kind Local_Theory.locale_dependency expression raw_defs |
241 end; |
217 end; |
242 |
218 |
243 in |
219 in |
244 |
220 |
245 fun global_sublocale expression = |
221 fun global_sublocale expression = |
258 fun register_or_activate lthy = |
234 fun register_or_activate lthy = |
259 if Named_Target.is_theory lthy |
235 if Named_Target.is_theory lthy |
260 then Local_Theory.theory_registration |
236 then Local_Theory.theory_registration |
261 else Locale.activate_fragment; |
237 else Locale.activate_fragment; |
262 |
238 |
263 fun gen_isar_interpretation prep_interpretation expression raw_eqns lthy = |
239 fun gen_isar_interpretation prep_interpretation expression lthy = |
264 generic_interpretation prep_interpretation Element.witness_proof_eqs |
240 generic_interpretation prep_interpretation Element.witness_proof_eqs |
265 Local_Theory.notes_kind (register_or_activate lthy) expression [] raw_eqns lthy; |
241 Local_Theory.notes_kind (register_or_activate lthy) expression [] lthy; |
266 |
242 |
267 in |
243 in |
268 |
244 |
269 fun isar_interpretation expression = |
245 fun isar_interpretation expression = |
270 gen_isar_interpretation cert_interpretation expression; |
246 gen_isar_interpretation cert_interpretation expression; |