author | wenzelm |
Sun, 30 Apr 2006 22:50:05 +0200 | |
changeset 19511 | b4bd790f9373 |
parent 19503 | 10921826b160 |
child 19522 | a4c790594737 |
permissions | -rw-r--r-- |
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/axclass.ML |
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
3 |
Author: Markus Wenzel, TU Muenchen |
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
4 |
|
19511 | 5 |
Type classes as parameter records and predicates, with explicit |
6 |
definitions and proofs. |
|
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
7 |
*) |
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
8 |
|
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
9 |
signature AX_CLASS = |
3938 | 10 |
sig |
19511 | 11 |
val get_definition: theory -> class -> {def: thm, intro: thm, axioms: thm list} |
19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset
|
12 |
val class_intros: theory -> thm list |
19460 | 13 |
val params_of: theory -> class -> string list |
14 |
val all_params_of: theory -> sort -> string list |
|
19511 | 15 |
val print_axclasses: theory -> unit |
19405 | 16 |
val cert_classrel: theory -> class * class -> class * class |
17 |
val read_classrel: theory -> xstring * xstring -> class * class |
|
18 |
val add_classrel: thm -> theory -> theory |
|
19 |
val add_arity: thm -> theory -> theory |
|
20 |
val prove_classrel: class * class -> tactic -> theory -> theory |
|
19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset
|
21 |
val prove_arity: string * sort list * sort -> tactic -> theory -> theory |
19511 | 22 |
val define_class: bstring * xstring list -> string list -> |
19418
03b01c9314fc
reworded add_axclass(_i): canonical specification format,
wenzelm
parents:
19405
diff
changeset
|
23 |
((bstring * Attrib.src list) * string list) list -> theory -> class * theory |
19511 | 24 |
val define_class_i: bstring * class list -> string list -> |
19418
03b01c9314fc
reworded add_axclass(_i): canonical specification format,
wenzelm
parents:
19405
diff
changeset
|
25 |
((bstring * attribute list) * term list) list -> theory -> class * theory |
19511 | 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 |
|
32 |
val of_sort: theory -> typ * sort -> thm list |
|
3938 | 33 |
end; |
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
34 |
|
15801 | 35 |
structure AxClass: AX_CLASS = |
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
36 |
struct |
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
37 |
|
19405 | 38 |
(** theory data **) |
423 | 39 |
|
19405 | 40 |
(* class parameters (canonical order) *) |
423 | 41 |
|
19405 | 42 |
type param = string * class; |
423 | 43 |
|
19405 | 44 |
fun add_param pp ((x, c): param) params = |
45 |
(case AList.lookup (op =) params x of |
|
46 |
NONE => (x, c) :: params |
|
47 |
| SOME c' => error ("Duplicate class parameter " ^ quote x ^ |
|
48 |
" for " ^ Pretty.string_of_sort pp [c] ^ |
|
49 |
(if c = c' then "" else " and " ^ Pretty.string_of_sort pp [c']))); |
|
423 | 50 |
|
19405 | 51 |
fun merge_params _ ([], qs) = qs |
52 |
| merge_params pp (ps, qs) = |
|
53 |
fold_rev (fn q => if member (op =) ps q then I else add_param pp q) qs ps; |
|
423 | 54 |
|
55 |
||
19511 | 56 |
(* axclasses *) |
6379 | 57 |
|
19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset
|
58 |
val introN = "intro"; |
19511 | 59 |
val superN = "super"; |
19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset
|
60 |
val axiomsN = "axioms"; |
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset
|
61 |
|
19392 | 62 |
datatype axclass = AxClass of |
19460 | 63 |
{def: thm, |
19392 | 64 |
intro: thm, |
65 |
axioms: thm list}; |
|
66 |
||
19460 | 67 |
type axclasses = axclass Symtab.table * param list; |
19392 | 68 |
|
19460 | 69 |
fun make_axclass (def, intro, axioms) = |
70 |
AxClass {def = def, intro = intro, axioms = axioms}; |
|
19405 | 71 |
|
72 |
fun merge_axclasses pp ((tab1, params1), (tab2, params2)) : axclasses = |
|
73 |
(Symtab.merge (K true) (tab1, tab2), merge_params pp (params1, params2)); |
|
74 |
||
19392 | 75 |
|
76 |
(* instances *) |
|
77 |
||
19511 | 78 |
val classrelN = "classrel"; |
79 |
val arityN = "arity"; |
|
80 |
||
19392 | 81 |
datatype instances = Instances of |
19405 | 82 |
{classes: unit Graph.T, (*raw relation -- no closure!*) |
83 |
classrel: ((class * class) * thm) list, |
|
19503 | 84 |
arities: ((class * sort list) * thm) list Symtab.table, |
85 |
types: (class * thm) list Typtab.table}; |
|
19392 | 86 |
|
19503 | 87 |
fun make_instances (classes, classrel, arities, types) = |
88 |
Instances {classes = classes, classrel = classrel, arities = arities, types = types}; |
|
6379 | 89 |
|
19503 | 90 |
fun map_instances f (Instances {classes, classrel, arities, types}) = |
91 |
make_instances (f (classes, classrel, arities, types)); |
|
19392 | 92 |
|
93 |
fun merge_instances |
|
19503 | 94 |
(Instances {classes = classes1, classrel = classrel1, arities = arities1, types = types1}, |
95 |
Instances {classes = classes2, classrel = classrel2, arities = arities2, types = types2}) = |
|
19392 | 96 |
make_instances |
19405 | 97 |
(Graph.merge (K true) (classes1, classes2), |
98 |
merge (eq_fst op =) (classrel1, classrel2), |
|
19503 | 99 |
Symtab.join (K (merge (eq_fst op =))) (arities1, arities2), |
100 |
Typtab.join (K (merge (eq_fst op =))) (types1, types2)); |
|
19392 | 101 |
|
102 |
||
19511 | 103 |
(* setup data *) |
19392 | 104 |
|
105 |
structure AxClassData = TheoryDataFun |
|
16458 | 106 |
(struct |
19392 | 107 |
val name = "Pure/axclass"; |
19503 | 108 |
type T = axclasses * instances ref; |
109 |
val empty : T = |
|
110 |
((Symtab.empty, []), ref (make_instances (Graph.empty, [], Symtab.empty, Typtab.empty))); |
|
111 |
fun copy (axclasses, ref instances) : T = (axclasses, ref instances); |
|
112 |
val extend = copy; |
|
113 |
fun merge pp ((axclasses1, ref instances1), (axclasses2, ref instances2)) = |
|
114 |
(merge_axclasses pp (axclasses1, axclasses2), ref (merge_instances (instances1, instances2))); |
|
19460 | 115 |
fun print _ _ = (); |
16458 | 116 |
end); |
6379 | 117 |
|
19392 | 118 |
val _ = Context.add_setup AxClassData.init; |
6379 | 119 |
|
120 |
||
19511 | 121 |
(* retrieve axclasses *) |
19392 | 122 |
|
19511 | 123 |
val lookup_def = Symtab.lookup o #1 o #1 o AxClassData.get; |
6379 | 124 |
|
19511 | 125 |
fun get_definition thy c = |
126 |
(case lookup_def thy c of |
|
19392 | 127 |
SOME (AxClass info) => info |
19511 | 128 |
| NONE => error ("Undefined type class " ^ quote c)); |
6379 | 129 |
|
19123 | 130 |
fun class_intros thy = |
19392 | 131 |
let |
132 |
fun add_intro c = |
|
19511 | 133 |
(case lookup_def thy c of SOME (AxClass {intro, ...}) => cons intro | _ => I); |
19392 | 134 |
val classes = Sign.classes thy; |
135 |
in map (Thm.class_triv thy) classes @ fold add_intro classes [] end; |
|
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset
|
136 |
|
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset
|
137 |
|
19511 | 138 |
(* retrieve parameters *) |
19460 | 139 |
|
140 |
fun get_params thy pred = |
|
141 |
let val params = #2 (#1 (AxClassData.get thy)) |
|
142 |
in fold (fn (x, c) => if pred c then cons x else I) params [] end; |
|
143 |
||
144 |
fun params_of thy c = get_params thy (fn c' => c' = c); |
|
145 |
fun all_params_of thy S = get_params thy (fn c => Sign.subsort thy (S, [c])); |
|
146 |
||
147 |
||
19511 | 148 |
(* maintain instances *) |
19503 | 149 |
|
150 |
val get_instances = AxClassData.get #> (fn (_, ref (Instances insts)) => insts); |
|
151 |
||
152 |
fun store_instance f thy (x, th) = |
|
153 |
let |
|
154 |
val th' = Drule.standard' th; |
|
155 |
val _ = change (#2 (AxClassData.get thy)) (map_instances (f (x, th'))); |
|
156 |
in th' end; |
|
157 |
||
158 |
val store_classrel = store_instance (fn ((c1, c2), th) => fn (classes, classrel, arities, types) => |
|
159 |
(classes |
|
160 |
|> Graph.default_node (c1, ()) |
|
161 |
|> Graph.default_node (c2, ()) |
|
162 |
|> Graph.add_edge (c1, c2), |
|
163 |
insert (eq_fst op =) ((c1, c2), th) classrel, arities, types)); |
|
164 |
||
165 |
val store_arity = store_instance (fn ((t, Ss, c), th) => fn (classes, classrel, arities, types) => |
|
166 |
(classes, classrel, arities |> Symtab.insert_list (eq_fst op =) (t, ((c, Ss), th)), types)); |
|
167 |
||
168 |
val store_type = store_instance (fn ((T, c), th) => fn (classes, classrel, arities, types) => |
|
169 |
(classes, classrel, arities, types |> Typtab.insert_list (eq_fst op =) (T, (c, th)))); |
|
170 |
||
171 |
||
19511 | 172 |
(* print data *) |
19460 | 173 |
|
174 |
fun print_axclasses thy = |
|
175 |
let |
|
176 |
val axclasses = #1 (#1 (AxClassData.get thy)); |
|
177 |
val ctxt = ProofContext.init thy; |
|
178 |
||
179 |
fun pretty_axclass (class, AxClass {def, intro, axioms}) = |
|
180 |
Pretty.block (Pretty.fbreaks |
|
181 |
[Pretty.block |
|
19511 | 182 |
[Pretty.str "class ", ProofContext.pretty_sort ctxt [class], Pretty.str ":"], |
19460 | 183 |
Pretty.strs ("parameters:" :: params_of thy class), |
184 |
ProofContext.pretty_fact ctxt ("def", [def]), |
|
185 |
ProofContext.pretty_fact ctxt (introN, [intro]), |
|
186 |
ProofContext.pretty_fact ctxt (axiomsN, axioms)]); |
|
187 |
in Pretty.writeln (Pretty.chunks (map pretty_axclass (Symtab.dest axclasses))) end; |
|
188 |
||
189 |
||
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
190 |
|
19511 | 191 |
(** instances **) |
19418
03b01c9314fc
reworded add_axclass(_i): canonical specification format,
wenzelm
parents:
19405
diff
changeset
|
192 |
|
03b01c9314fc
reworded add_axclass(_i): canonical specification format,
wenzelm
parents:
19405
diff
changeset
|
193 |
(* class relations *) |
03b01c9314fc
reworded add_axclass(_i): canonical specification format,
wenzelm
parents:
19405
diff
changeset
|
194 |
|
19405 | 195 |
fun cert_classrel thy raw_rel = |
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset
|
196 |
let |
19405 | 197 |
val (c1, c2) = pairself (Sign.certify_class thy) raw_rel; |
19511 | 198 |
val _ = Type.add_classrel (Sign.pp thy) (c1, c2) (Sign.tsig_of thy); |
19405 | 199 |
val _ = |
19460 | 200 |
(case subtract (op =) (all_params_of thy [c1]) (all_params_of thy [c2]) of |
19405 | 201 |
[] => () |
202 |
| xs => raise TYPE ("Class " ^ Sign.string_of_sort thy [c1] ^ " lacks parameter(s) " ^ |
|
203 |
commas_quote xs ^ " of " ^ Sign.string_of_sort thy [c2], [], [])); |
|
204 |
in (c1, c2) end; |
|
205 |
||
206 |
fun read_classrel thy raw_rel = |
|
207 |
cert_classrel thy (pairself (Sign.read_class thy) raw_rel) |
|
208 |
handle TYPE (msg, _, _) => error msg; |
|
209 |
||
210 |
||
211 |
(* primitive rules *) |
|
212 |
||
213 |
fun add_classrel th thy = |
|
214 |
let |
|
215 |
fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]); |
|
216 |
val prop = Drule.plain_prop_of (Thm.transfer thy th); |
|
217 |
val rel = Logic.dest_classrel prop handle TERM _ => err (); |
|
218 |
val (c1, c2) = cert_classrel thy rel handle TYPE _ => err (); |
|
19511 | 219 |
val thy' = thy |> Sign.primitive_classrel (c1, c2); |
19503 | 220 |
val _ = store_classrel thy' ((c1, c2), Drule.unconstrainTs th); |
221 |
in thy' end; |
|
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset
|
222 |
|
19405 | 223 |
fun add_arity th thy = |
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset
|
224 |
let |
19405 | 225 |
val prop = Drule.plain_prop_of (Thm.transfer thy th); |
226 |
val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => |
|
227 |
raise THM ("add_arity: malformed type arity", 0, [th]); |
|
19511 | 228 |
val thy' = thy |> Sign.primitive_arity (t, Ss, [c]); |
19503 | 229 |
val _ = store_arity thy' ((t, Ss, c), Drule.unconstrainTs th); |
230 |
in thy' end; |
|
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
231 |
|
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
232 |
|
19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset
|
233 |
(* tactical proofs *) |
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset
|
234 |
|
19405 | 235 |
fun prove_classrel raw_rel tac thy = |
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset
|
236 |
let |
19405 | 237 |
val (c1, c2) = cert_classrel thy raw_rel; |
238 |
val th = Goal.prove thy [] [] (Logic.mk_classrel (c1, c2)) (fn _ => tac) handle ERROR msg => |
|
19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset
|
239 |
cat_error msg ("The error(s) above occurred while trying to prove class relation " ^ |
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset
|
240 |
quote (Sign.string_of_classrel thy [c1, c2])); |
19511 | 241 |
in |
242 |
thy |
|
243 |
|> PureThy.add_thms [((classrelN ^ "_" ^ serial_string (), th), [])] |
|
244 |
|-> (fn [th'] => add_classrel th') |
|
245 |
end; |
|
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
246 |
|
19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset
|
247 |
fun prove_arity raw_arity tac thy = |
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset
|
248 |
let |
19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset
|
249 |
val arity = Sign.cert_arity thy raw_arity; |
19405 | 250 |
val props = Logic.mk_arities arity; |
17956 | 251 |
val ths = Goal.prove_multi thy [] [] props |
18678 | 252 |
(fn _ => Tactic.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg => |
19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset
|
253 |
cat_error msg ("The error(s) above occurred while trying to prove type arity " ^ |
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset
|
254 |
quote (Sign.string_of_arity thy arity)); |
19511 | 255 |
in |
256 |
thy |
|
257 |
|> PureThy.add_thms (ths |> map (fn th => ((arityN ^ "_" ^ serial_string (), th), []))) |
|
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); |
|
19392 | 309 |
|
19418
03b01c9314fc
reworded add_axclass(_i): canonical specification format,
wenzelm
parents:
19405
diff
changeset
|
310 |
|
19511 | 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 |
|
19503 | 384 |
|
385 |
fun derive_classrel thy (c1, c2) = |
|
386 |
let |
|
387 |
val {classes, classrel, ...} = get_instances thy; |
|
388 |
val lookup = AList.lookup (op =) classrel; |
|
389 |
fun derive [c, c'] = the (lookup (c, c')) |
|
390 |
| derive (c :: c' :: cs) = derive [c, c'] RS derive (c' :: cs); |
|
391 |
in |
|
392 |
(case lookup (c1, c2) of |
|
393 |
SOME rule => rule |
|
394 |
| NONE => |
|
395 |
(case Graph.find_paths classes (c1, c2) of |
|
396 |
[] => error ("Cannot derive class relation " ^ Sign.string_of_classrel thy [c1, c2]) |
|
397 |
| path :: _ => store_classrel thy ((c1, c2), derive path))) |
|
398 |
end; |
|
399 |
||
400 |
fun weaken_subclass thy (c1, th) c2 = |
|
401 |
if c1 = c2 then th |
|
402 |
else th RS derive_classrel thy (c1, c2); |
|
403 |
||
404 |
fun weaken_subsort thy S1 S2 = S2 |> map (fn c2 => |
|
405 |
(case S1 |> find_first (fn (c1, _) => Sign.subsort thy ([c1], [c2])) of |
|
406 |
SOME c1 => weaken_subclass thy c1 c2 |
|
407 |
| NONE => error ("Cannot derive subsort relation " ^ |
|
408 |
Sign.string_of_sort thy (map #1 S1) ^ " < " ^ Sign.string_of_sort thy S2))); |
|
409 |
||
410 |
fun apply_arity thy t dom c = |
|
411 |
let |
|
412 |
val {arities, ...} = get_instances thy; |
|
413 |
val subsort = Sign.subsort thy; |
|
414 |
val Ss = map (map #1) dom; |
|
415 |
in |
|
416 |
(case Symtab.lookup_list arities t |> find_first (fn ((c', Ss'), _) => |
|
417 |
subsort ([c'], [c]) andalso ListPair.all subsort (Ss, Ss')) of |
|
418 |
SOME ((c', Ss'), rule) => |
|
419 |
weaken_subclass thy (c', rule OF flat (map2 (weaken_subsort thy) dom Ss')) c |
|
420 |
| NONE => error ("Cannot derive type arity " ^ Sign.string_of_arity thy (t, Ss, [c]))) |
|
421 |
end; |
|
422 |
||
423 |
fun derive_type thy hyps = |
|
424 |
let |
|
425 |
fun derive (Type (a, Ts)) S = |
|
426 |
let val Ss = Sign.arity_sorts thy a S |
|
427 |
in map (apply_arity thy a (map2 (fn T => fn S => S ~~ derive T S) Ts Ss)) S end |
|
428 |
| derive (TFree (a, [])) S = |
|
429 |
weaken_subsort thy (the_default [] (AList.lookup (op =) hyps a)) S |
|
430 |
| derive T _ = error ("Illegal occurrence of type variable " ^ |
|
431 |
setmp show_sorts true (Sign.string_of_typ thy) T); |
|
432 |
in derive end; |
|
433 |
||
19511 | 434 |
in |
435 |
||
19503 | 436 |
fun of_sort thy (typ, sort) = |
437 |
let |
|
438 |
fun lookup () = AList.lookup (op =) (Typtab.lookup_list (#types (get_instances thy)) typ); |
|
439 |
val sort' = filter (is_none o lookup ()) sort; |
|
440 |
val _ = conditional (not (null sort')) (fn () => |
|
441 |
let |
|
442 |
val vars = Term.fold_atyps (insert (op =)) typ []; |
|
443 |
val renaming = |
|
444 |
map2 (fn T => fn a => (T, (a, case T of TFree (_, S) => S | TVar (_, S) => S))) |
|
445 |
vars (Term.invent_names [] "'a" (length vars)); |
|
446 |
val typ' = typ |> Term.map_atyps |
|
447 |
(fn T => TFree (#1 (the (AList.lookup (op =) renaming T)), [])); |
|
448 |
||
449 |
val hyps = renaming |> map (fn (_, (a, S)) => (a, S ~~ (S |> map (fn c => |
|
450 |
Thm.assume (Thm.cterm_of thy (Logic.mk_inclass (TFree (a, []), c))))))); |
|
451 |
val inst = renaming |> map (fn (T, (a, S)) => |
|
452 |
pairself (Thm.ctyp_of thy) (TVar ((a, 0), S), T)); |
|
453 |
||
454 |
val ths = |
|
455 |
derive_type thy hyps typ' sort' |
|
456 |
|> map (Thm.instantiate (inst, [])); |
|
457 |
val _ = map (store_type thy) (map (pair typ) sort' ~~ ths); |
|
458 |
in () end); |
|
459 |
in map (the o lookup ()) sort end; |
|
460 |
||
19511 | 461 |
end; |
19418
03b01c9314fc
reworded add_axclass(_i): canonical specification format,
wenzelm
parents:
19405
diff
changeset
|
462 |
|
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset
|
463 |
end; |