1 (* Title: Pure/axclass.ML |
1 (* Title: Pure/axclass.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Markus Wenzel, TU Muenchen |
3 Author: Markus Wenzel, TU Muenchen |
4 |
4 |
5 Axiomatic type classes: managing predicates and parameter collections. |
5 Type classes as parameter records and predicates, with explicit |
|
6 definitions and proofs. |
6 *) |
7 *) |
7 |
8 |
8 signature AX_CLASS = |
9 signature AX_CLASS = |
9 sig |
10 sig |
10 val print_axclasses: theory -> unit |
11 val get_definition: theory -> class -> {def: thm, intro: thm, axioms: thm list} |
11 val get_info: theory -> class -> {def: thm, intro: thm, axioms: thm list} |
|
12 val class_intros: theory -> thm list |
12 val class_intros: theory -> thm list |
13 val params_of: theory -> class -> string list |
13 val params_of: theory -> class -> string list |
14 val all_params_of: theory -> sort -> string list |
14 val all_params_of: theory -> sort -> string list |
|
15 val print_axclasses: theory -> unit |
15 val cert_classrel: theory -> class * class -> class * class |
16 val cert_classrel: theory -> class * class -> class * class |
16 val read_classrel: theory -> xstring * xstring -> class * class |
17 val read_classrel: theory -> xstring * xstring -> class * class |
17 val add_classrel: thm -> theory -> theory |
18 val add_classrel: thm -> theory -> theory |
18 val add_arity: thm -> theory -> theory |
19 val add_arity: thm -> theory -> theory |
19 val prove_classrel: class * class -> tactic -> theory -> theory |
20 val prove_classrel: class * class -> tactic -> theory -> theory |
20 val prove_arity: string * sort list * sort -> tactic -> theory -> theory |
21 val prove_arity: string * sort list * sort -> tactic -> theory -> theory |
|
22 val define_class: bstring * xstring list -> string list -> |
|
23 ((bstring * Attrib.src list) * string list) list -> theory -> class * theory |
|
24 val define_class_i: bstring * class list -> string list -> |
|
25 ((bstring * attribute list) * term list) list -> theory -> class * theory |
|
26 val axiomatize_class: bstring * xstring list -> theory -> theory |
|
27 val axiomatize_class_i: bstring * class list -> theory -> theory |
|
28 val axiomatize_classrel: (xstring * xstring) list -> theory -> theory |
|
29 val axiomatize_classrel_i: (class * class) list -> theory -> theory |
|
30 val axiomatize_arity: xstring * string list * string -> theory -> theory |
|
31 val axiomatize_arity_i: arity -> theory -> theory |
21 val of_sort: theory -> typ * sort -> thm list |
32 val of_sort: theory -> typ * sort -> thm list |
22 val add_axclass: bstring * xstring list -> string list -> |
|
23 ((bstring * Attrib.src list) * string list) list -> theory -> class * theory |
|
24 val add_axclass_i: bstring * class list -> string list -> |
|
25 ((bstring * attribute list) * term list) list -> theory -> class * theory |
|
26 end; |
33 end; |
27 |
34 |
28 structure AxClass: AX_CLASS = |
35 structure AxClass: AX_CLASS = |
29 struct |
36 struct |
30 |
37 |
105 end); |
116 end); |
106 |
117 |
107 val _ = Context.add_setup AxClassData.init; |
118 val _ = Context.add_setup AxClassData.init; |
108 |
119 |
109 |
120 |
110 (* classes *) |
121 (* retrieve axclasses *) |
111 |
122 |
112 val lookup_info = Symtab.lookup o #1 o #1 o AxClassData.get; |
123 val lookup_def = Symtab.lookup o #1 o #1 o AxClassData.get; |
113 |
124 |
114 fun get_info thy c = |
125 fun get_definition thy c = |
115 (case lookup_info thy c of |
126 (case lookup_def thy c of |
116 SOME (AxClass info) => info |
127 SOME (AxClass info) => info |
117 | NONE => error ("Unknown axclass " ^ quote c)); |
128 | NONE => error ("Undefined type class " ^ quote c)); |
118 |
129 |
119 fun class_intros thy = |
130 fun class_intros thy = |
120 let |
131 let |
121 fun add_intro c = |
132 fun add_intro c = |
122 (case lookup_info thy c of SOME (AxClass {intro, ...}) => cons intro | _ => I); |
133 (case lookup_def thy c of SOME (AxClass {intro, ...}) => cons intro | _ => I); |
123 val classes = Sign.classes thy; |
134 val classes = Sign.classes thy; |
124 in map (Thm.class_triv thy) classes @ fold add_intro classes [] end; |
135 in map (Thm.class_triv thy) classes @ fold add_intro classes [] end; |
125 |
136 |
126 |
137 |
127 (* parameters *) |
138 (* retrieve parameters *) |
128 |
139 |
129 fun get_params thy pred = |
140 fun get_params thy pred = |
130 let val params = #2 (#1 (AxClassData.get thy)) |
141 let val params = #2 (#1 (AxClassData.get thy)) |
131 in fold (fn (x, c) => if pred c then cons x else I) params [] end; |
142 in fold (fn (x, c) => if pred c then cons x else I) params [] end; |
132 |
143 |
133 fun params_of thy c = get_params thy (fn c' => c' = c); |
144 fun params_of thy c = get_params thy (fn c' => c' = c); |
134 fun all_params_of thy S = get_params thy (fn c => Sign.subsort thy (S, [c])); |
145 fun all_params_of thy S = get_params thy (fn c => Sign.subsort thy (S, [c])); |
135 |
146 |
136 |
147 |
137 (* instances *) |
148 (* maintain instances *) |
138 |
149 |
139 val get_instances = AxClassData.get #> (fn (_, ref (Instances insts)) => insts); |
150 val get_instances = AxClassData.get #> (fn (_, ref (Instances insts)) => insts); |
140 |
151 |
141 fun store_instance f thy (x, th) = |
152 fun store_instance f thy (x, th) = |
142 let |
153 let |
156 |
167 |
157 val store_type = store_instance (fn ((T, c), th) => fn (classes, classrel, arities, types) => |
168 val store_type = store_instance (fn ((T, c), th) => fn (classes, classrel, arities, types) => |
158 (classes, classrel, arities, types |> Typtab.insert_list (eq_fst op =) (T, (c, th)))); |
169 (classes, classrel, arities, types |> Typtab.insert_list (eq_fst op =) (T, (c, th)))); |
159 |
170 |
160 |
171 |
161 (* print_axclasses *) |
172 (* print data *) |
162 |
173 |
163 fun print_axclasses thy = |
174 fun print_axclasses thy = |
164 let |
175 let |
165 val axclasses = #1 (#1 (AxClassData.get thy)); |
176 val axclasses = #1 (#1 (AxClassData.get thy)); |
166 val ctxt = ProofContext.init thy; |
177 val ctxt = ProofContext.init thy; |
167 |
178 |
168 fun pretty_axclass (class, AxClass {def, intro, axioms}) = |
179 fun pretty_axclass (class, AxClass {def, intro, axioms}) = |
169 Pretty.block (Pretty.fbreaks |
180 Pretty.block (Pretty.fbreaks |
170 [Pretty.block |
181 [Pretty.block |
171 [Pretty.str "axclass ", ProofContext.pretty_sort ctxt [class], Pretty.str ":"], |
182 [Pretty.str "class ", ProofContext.pretty_sort ctxt [class], Pretty.str ":"], |
172 Pretty.strs ("parameters:" :: params_of thy class), |
183 Pretty.strs ("parameters:" :: params_of thy class), |
173 ProofContext.pretty_fact ctxt ("def", [def]), |
184 ProofContext.pretty_fact ctxt ("def", [def]), |
174 ProofContext.pretty_fact ctxt (introN, [intro]), |
185 ProofContext.pretty_fact ctxt (introN, [intro]), |
175 ProofContext.pretty_fact ctxt (axiomsN, axioms)]); |
186 ProofContext.pretty_fact ctxt (axiomsN, axioms)]); |
176 in Pretty.writeln (Pretty.chunks (map pretty_axclass (Symtab.dest axclasses))) end; |
187 in Pretty.writeln (Pretty.chunks (map pretty_axclass (Symtab.dest axclasses))) end; |
177 |
188 |
178 |
189 |
179 |
190 |
180 (** instance proofs **) |
191 (** instances **) |
181 |
192 |
182 (* class relations *) |
193 (* class relations *) |
183 |
194 |
184 fun cert_classrel thy raw_rel = |
195 fun cert_classrel thy raw_rel = |
185 let |
196 let |
186 val (c1, c2) = pairself (Sign.certify_class thy) raw_rel; |
197 val (c1, c2) = pairself (Sign.certify_class thy) raw_rel; |
187 val _ = Type.add_classrel (Sign.pp thy) [(c1, c2)] (Sign.tsig_of thy); |
198 val _ = Type.add_classrel (Sign.pp thy) (c1, c2) (Sign.tsig_of thy); |
188 val _ = |
199 val _ = |
189 (case subtract (op =) (all_params_of thy [c1]) (all_params_of thy [c2]) of |
200 (case subtract (op =) (all_params_of thy [c1]) (all_params_of thy [c2]) of |
190 [] => () |
201 [] => () |
191 | xs => raise TYPE ("Class " ^ Sign.string_of_sort thy [c1] ^ " lacks parameter(s) " ^ |
202 | xs => raise TYPE ("Class " ^ Sign.string_of_sort thy [c1] ^ " lacks parameter(s) " ^ |
192 commas_quote xs ^ " of " ^ Sign.string_of_sort thy [c2], [], [])); |
203 commas_quote xs ^ " of " ^ Sign.string_of_sort thy [c2], [], [])); |
203 let |
214 let |
204 fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]); |
215 fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]); |
205 val prop = Drule.plain_prop_of (Thm.transfer thy th); |
216 val prop = Drule.plain_prop_of (Thm.transfer thy th); |
206 val rel = Logic.dest_classrel prop handle TERM _ => err (); |
217 val rel = Logic.dest_classrel prop handle TERM _ => err (); |
207 val (c1, c2) = cert_classrel thy rel handle TYPE _ => err (); |
218 val (c1, c2) = cert_classrel thy rel handle TYPE _ => err (); |
208 val thy' = thy |> Theory.add_classrel_i [(c1, c2)]; |
219 val thy' = thy |> Sign.primitive_classrel (c1, c2); |
209 val _ = store_classrel thy' ((c1, c2), Drule.unconstrainTs th); |
220 val _ = store_classrel thy' ((c1, c2), Drule.unconstrainTs th); |
210 in thy' end; |
221 in thy' end; |
211 |
222 |
212 fun add_arity th thy = |
223 fun add_arity th thy = |
213 let |
224 let |
214 val prop = Drule.plain_prop_of (Thm.transfer thy th); |
225 val prop = Drule.plain_prop_of (Thm.transfer thy th); |
215 val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => |
226 val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => |
216 raise THM ("add_arity: malformed type arity", 0, [th]); |
227 raise THM ("add_arity: malformed type arity", 0, [th]); |
217 val thy' = thy |> Theory.add_arities_i [(t, Ss, [c])]; |
228 val thy' = thy |> Sign.primitive_arity (t, Ss, [c]); |
218 val _ = store_arity thy' ((t, Ss, c), Drule.unconstrainTs th); |
229 val _ = store_arity thy' ((t, Ss, c), Drule.unconstrainTs th); |
219 in thy' end; |
230 in thy' end; |
220 |
231 |
221 |
232 |
222 (* tactical proofs *) |
233 (* tactical proofs *) |
225 let |
236 let |
226 val (c1, c2) = cert_classrel thy raw_rel; |
237 val (c1, c2) = cert_classrel thy raw_rel; |
227 val th = Goal.prove thy [] [] (Logic.mk_classrel (c1, c2)) (fn _ => tac) handle ERROR msg => |
238 val th = Goal.prove thy [] [] (Logic.mk_classrel (c1, c2)) (fn _ => tac) handle ERROR msg => |
228 cat_error msg ("The error(s) above occurred while trying to prove class relation " ^ |
239 cat_error msg ("The error(s) above occurred while trying to prove class relation " ^ |
229 quote (Sign.string_of_classrel thy [c1, c2])); |
240 quote (Sign.string_of_classrel thy [c1, c2])); |
230 in add_classrel th thy end; |
241 in |
|
242 thy |
|
243 |> PureThy.add_thms [((classrelN ^ "_" ^ serial_string (), th), [])] |
|
244 |-> (fn [th'] => add_classrel th') |
|
245 end; |
231 |
246 |
232 fun prove_arity raw_arity tac thy = |
247 fun prove_arity raw_arity tac thy = |
233 let |
248 let |
234 val arity = Sign.cert_arity thy raw_arity; |
249 val arity = Sign.cert_arity thy raw_arity; |
235 val props = Logic.mk_arities arity; |
250 val props = Logic.mk_arities arity; |
236 val ths = Goal.prove_multi thy [] [] props |
251 val ths = Goal.prove_multi thy [] [] props |
237 (fn _ => Tactic.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg => |
252 (fn _ => Tactic.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg => |
238 cat_error msg ("The error(s) above occurred while trying to prove type arity " ^ |
253 cat_error msg ("The error(s) above occurred while trying to prove type arity " ^ |
239 quote (Sign.string_of_arity thy arity)); |
254 quote (Sign.string_of_arity thy arity)); |
240 in fold add_arity ths thy end; |
255 in |
241 |
256 thy |
242 |
257 |> PureThy.add_thms (ths |> map (fn th => ((arityN ^ "_" ^ serial_string (), th), []))) |
243 (* derived instances -- cached *) |
258 |-> fold add_arity |
|
259 end; |
|
260 |
|
261 |
|
262 |
|
263 (** class definitions **) |
|
264 |
|
265 local |
|
266 |
|
267 fun def_class prep_class prep_att prep_propp |
|
268 (bclass, raw_super) params raw_specs thy = |
|
269 let |
|
270 val ctxt = ProofContext.init thy; |
|
271 val pp = ProofContext.pp ctxt; |
|
272 |
|
273 |
|
274 (* prepare specification *) |
|
275 |
|
276 val bconst = Logic.const_of_class bclass; |
|
277 val class = Sign.full_name thy bclass; |
|
278 val super = map (prep_class thy) raw_super |> Sign.certify_sort thy; |
|
279 |
|
280 fun prep_axiom t = |
|
281 (case Term.add_tfrees t [] of |
|
282 [(a, S)] => |
|
283 if Sign.subsort thy (super, S) then t |
|
284 else error ("Sort constraint of type variable " ^ |
|
285 setmp show_sorts true (Pretty.string_of_typ pp) (TFree (a, S)) ^ |
|
286 " needs to be weaker than " ^ Pretty.string_of_sort pp super) |
|
287 | [] => t |
|
288 | _ => error ("Multiple type variables in class axiom:\n" ^ Pretty.string_of_term pp t)) |
|
289 |> map_term_types (Term.map_atyps (fn TFree _ => Term.aT [] | U => U)) |
|
290 |> Logic.close_form; |
|
291 |
|
292 val axiomss = prep_propp (ctxt, map (map (rpair ([], [])) o snd) raw_specs) |
|
293 |> snd |> map (map (prep_axiom o fst)); |
|
294 val name_atts = Attrib.map_specs (prep_att thy) raw_specs |> map fst; |
|
295 |
|
296 |
|
297 (* definition *) |
|
298 |
|
299 val conjs = map (curry Logic.mk_inclass (Term.aT [])) super @ flat axiomss; |
|
300 val class_eq = |
|
301 Logic.mk_equals (Logic.mk_inclass (Term.aT [], class), Logic.mk_conjunction_list conjs); |
|
302 |
|
303 val ([def], def_thy) = |
|
304 thy |
|
305 |> Sign.primitive_class (bclass, super) |
|
306 |> PureThy.add_defs_i false [((Thm.def_name bconst, class_eq), [])]; |
|
307 val (raw_intro, (raw_classrel, raw_axioms)) = |
|
308 (Conjunction.split_defined (length conjs) def) ||> chop (length super); |
|
309 |
|
310 |
|
311 (* facts *) |
|
312 |
|
313 val class_triv = Thm.class_triv def_thy class; |
|
314 val ([(_, [intro]), (_, classrel), (_, axioms)], facts_thy) = |
|
315 def_thy |
|
316 |> PureThy.note_thmss_qualified "" bconst |
|
317 [((introN, []), [([Drule.standard raw_intro], [])]), |
|
318 ((superN, []), [(map Drule.standard raw_classrel, [])]), |
|
319 ((axiomsN, []), [(map (fn th => Drule.standard (class_triv RS th)) raw_axioms, [])])]; |
|
320 val _ = map (store_classrel facts_thy) (map (pair class) super ~~ classrel); |
|
321 |
|
322 |
|
323 (* result *) |
|
324 |
|
325 val result_thy = |
|
326 facts_thy |
|
327 |> Sign.add_path bconst |
|
328 |> PureThy.note_thmss_i "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> snd |
|
329 |> Sign.restore_naming facts_thy |
|
330 |> AxClassData.map (apfst (fn (axclasses, parameters) => |
|
331 (Symtab.update (class, make_axclass (def, intro, axioms)) axclasses, |
|
332 fold (fn x => add_param pp (x, class)) params parameters))); |
|
333 |
|
334 in (class, result_thy) end; |
|
335 |
|
336 in |
|
337 |
|
338 val define_class = def_class Sign.read_class Attrib.attribute ProofContext.read_propp; |
|
339 val define_class_i = def_class Sign.certify_class (K I) ProofContext.cert_propp; |
|
340 |
|
341 end; |
|
342 |
|
343 |
|
344 (** axiomatizations **) |
|
345 |
|
346 local |
|
347 |
|
348 fun axiomatize kind add prep arg thy = |
|
349 let val specs = arg |> prep thy |> map (fn prop => ((kind ^ "_" ^ serial_string (), prop), [])) |
|
350 in thy |> PureThy.add_axioms_i specs |-> fold add end; |
|
351 |
|
352 fun ax_classrel prep = |
|
353 axiomatize classrelN add_classrel (fn thy => map (prep thy #> Logic.mk_classrel)); |
|
354 |
|
355 fun ax_arity prep = |
|
356 axiomatize arityN add_arity (fn thy => prep thy #> Logic.mk_arities); |
|
357 |
|
358 fun ax_class prep_class prep_classrel (bclass, raw_super) thy = |
|
359 let |
|
360 val class = Sign.full_name thy bclass; |
|
361 val super = map (prep_class thy) raw_super |> Sign.certify_sort thy; |
|
362 in |
|
363 thy |
|
364 |> Sign.primitive_class (bclass, super) |
|
365 |> ax_classrel prep_classrel (map (fn c => (class, c)) super) |
|
366 end; |
|
367 |
|
368 in |
|
369 |
|
370 val axiomatize_class = ax_class Sign.read_class read_classrel; |
|
371 val axiomatize_class_i = ax_class Sign.certify_class cert_classrel; |
|
372 val axiomatize_classrel = ax_classrel read_classrel; |
|
373 val axiomatize_classrel_i = ax_classrel cert_classrel; |
|
374 val axiomatize_arity = ax_arity Sign.read_arity; |
|
375 val axiomatize_arity_i = ax_arity Sign.cert_arity; |
|
376 |
|
377 end; |
|
378 |
|
379 |
|
380 |
|
381 (** explicit derivations -- cached **) |
|
382 |
|
383 local |
244 |
384 |
245 fun derive_classrel thy (c1, c2) = |
385 fun derive_classrel thy (c1, c2) = |
246 let |
386 let |
247 val {classes, classrel, ...} = get_instances thy; |
387 val {classes, classrel, ...} = get_instances thy; |
248 val lookup = AList.lookup (op =) classrel; |
388 val lookup = AList.lookup (op =) classrel; |
314 |> map (Thm.instantiate (inst, [])); |
456 |> map (Thm.instantiate (inst, [])); |
315 val _ = map (store_type thy) (map (pair typ) sort' ~~ ths); |
457 val _ = map (store_type thy) (map (pair typ) sort' ~~ ths); |
316 in () end); |
458 in () end); |
317 in map (the o lookup ()) sort end; |
459 in map (the o lookup ()) sort end; |
318 |
460 |
319 |
|
320 |
|
321 (** axclass definitions **) |
|
322 |
|
323 (* add_axclass(_i) *) |
|
324 |
|
325 fun gen_axclass prep_class prep_att prep_propp |
|
326 (bclass, raw_super) params raw_specs thy = |
|
327 let |
|
328 val ctxt = ProofContext.init thy; |
|
329 val pp = ProofContext.pp ctxt; |
|
330 |
|
331 |
|
332 (* prepare specification *) |
|
333 |
|
334 val bconst = Logic.const_of_class bclass; |
|
335 val class = Sign.full_name thy bclass; |
|
336 val super = map (prep_class thy) raw_super |> Sign.certify_sort thy; |
|
337 |
|
338 fun prep_axiom t = |
|
339 (case Term.add_tfrees t [] of |
|
340 [(a, S)] => |
|
341 if Sign.subsort thy (super, S) then t |
|
342 else error ("Sort constraint of type variable " ^ |
|
343 setmp show_sorts true (Pretty.string_of_typ pp) (TFree (a, S)) ^ |
|
344 " needs to be weaker than " ^ Pretty.string_of_sort pp super) |
|
345 | [] => t |
|
346 | _ => error ("Multiple type variables in class axiom:\n" ^ Pretty.string_of_term pp t)) |
|
347 |> map_term_types (Term.map_atyps (fn TFree _ => Term.aT [] | U => U)) |
|
348 |> Logic.close_form; |
|
349 |
|
350 val axiomss = prep_propp (ctxt, map (map (rpair ([], [])) o snd) raw_specs) |
|
351 |> snd |> map (map (prep_axiom o fst)); |
|
352 val name_atts = Attrib.map_specs (prep_att thy) raw_specs |> map fst; |
|
353 |
|
354 |
|
355 (* definition *) |
|
356 |
|
357 val conjs = map (curry Logic.mk_inclass (Term.aT [])) super @ flat axiomss; |
|
358 val class_eq = |
|
359 Logic.mk_equals (Logic.mk_inclass (Term.aT [], class), Logic.mk_conjunction_list conjs); |
|
360 |
|
361 val ([def], def_thy) = |
|
362 thy |
|
363 |> Theory.add_classes_i [(bclass, super)] |
|
364 |> PureThy.add_defs_i false [((Thm.def_name bconst, class_eq), [])]; |
|
365 val (raw_intro, (raw_classrel, raw_axioms)) = |
|
366 (Conjunction.split_defined (length conjs) def) ||> chop (length super); |
|
367 |
|
368 |
|
369 (* facts *) |
|
370 |
|
371 val class_triv = Thm.class_triv def_thy class; |
|
372 val ([(_, [intro]), (_, axioms)], facts_thy) = |
|
373 def_thy |
|
374 |> PureThy.note_thmss_qualified "" bconst |
|
375 [((introN, []), [([Drule.standard raw_intro], [])]), |
|
376 ((axiomsN, []), [(map (fn th => Drule.standard (class_triv RS th)) raw_axioms, [])])]; |
|
377 val _ = map (store_classrel facts_thy) |
|
378 (map (pair class) super ~~ map Drule.standard raw_classrel); |
|
379 |
|
380 |
|
381 (* result *) |
|
382 |
|
383 val result_thy = |
|
384 facts_thy |
|
385 |> Sign.add_path bconst |
|
386 |> PureThy.note_thmss_i "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> snd |
|
387 |> Sign.restore_naming facts_thy |
|
388 |> AxClassData.map (apfst (fn (axclasses, parameters) => |
|
389 (Symtab.update (class, make_axclass (def, intro, axioms)) axclasses, |
|
390 fold (fn x => add_param pp (x, class)) params parameters))); |
|
391 |
|
392 in (class, result_thy) end; |
|
393 |
|
394 val add_axclass = gen_axclass Sign.read_class Attrib.attribute ProofContext.read_propp; |
|
395 val add_axclass_i = gen_axclass Sign.certify_class (K I) ProofContext.cert_propp; |
|
396 |
|
397 end; |
461 end; |
|
462 |
|
463 end; |