author | wenzelm |
Tue, 11 Apr 2006 16:00:02 +0200 | |
changeset 19406 | 410b9d9bf9a1 |
parent 19405 | a551256aba15 |
child 19418 | 03b01c9314fc |
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 |
|
19405 | 5 |
Axiomatic type classes. |
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
6 |
*) |
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 |
signature AX_CLASS = |
3938 | 9 |
sig |
6379 | 10 |
val print_axclasses: theory -> unit |
19392 | 11 |
val get_info: theory -> class -> {super_classes: class list, intro: thm, axioms: thm list} |
12 |
val get_instances: theory -> |
|
19405 | 13 |
{classes: unit Graph.T, |
14 |
classrel: ((class * class) * thm) list, |
|
15 |
arities: ((string * sort list * class) * thm) list} |
|
19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset
|
16 |
val class_intros: theory -> thm list |
19405 | 17 |
val add_axclass: bstring * xstring list -> string list -> |
18 |
((bstring * string) * Attrib.src list) list -> theory -> class * theory |
|
19 |
val add_axclass_i: bstring * class list -> string list -> |
|
20 |
((bstring * term) * attribute list) list -> theory -> class * theory |
|
21 |
val params_of_sort: theory -> sort -> string list |
|
22 |
val cert_classrel: theory -> class * class -> class * class |
|
23 |
val read_classrel: theory -> xstring * xstring -> class * class |
|
24 |
val add_classrel: thm -> theory -> theory |
|
25 |
val add_arity: thm -> theory -> theory |
|
26 |
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
|
27 |
val prove_arity: string * sort list * sort -> tactic -> theory -> theory |
3938 | 28 |
end; |
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
29 |
|
15801 | 30 |
structure AxClass: AX_CLASS = |
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
31 |
struct |
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
32 |
|
19405 | 33 |
(** theory data **) |
423 | 34 |
|
19405 | 35 |
(* class parameters (canonical order) *) |
423 | 36 |
|
19405 | 37 |
type param = string * class; |
423 | 38 |
|
19405 | 39 |
fun add_param pp ((x, c): param) params = |
40 |
(case AList.lookup (op =) params x of |
|
41 |
NONE => (x, c) :: params |
|
42 |
| SOME c' => error ("Duplicate class parameter " ^ quote x ^ |
|
43 |
" for " ^ Pretty.string_of_sort pp [c] ^ |
|
44 |
(if c = c' then "" else " and " ^ Pretty.string_of_sort pp [c']))); |
|
423 | 45 |
|
19405 | 46 |
fun merge_params _ ([], qs) = qs |
47 |
| merge_params pp (ps, qs) = |
|
48 |
fold_rev (fn q => if member (op =) ps q then I else add_param pp q) qs ps; |
|
423 | 49 |
|
50 |
||
19392 | 51 |
(* axclass *) |
6379 | 52 |
|
19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset
|
53 |
val introN = "intro"; |
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset
|
54 |
val axiomsN = "axioms"; |
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset
|
55 |
|
19392 | 56 |
datatype axclass = AxClass of |
57 |
{super_classes: class list, |
|
58 |
intro: thm, |
|
59 |
axioms: thm list}; |
|
60 |
||
61 |
fun make_axclass (super_classes, intro, axioms) = |
|
62 |
AxClass {super_classes = super_classes, intro = intro, axioms = axioms}; |
|
63 |
||
19405 | 64 |
type axclasses = axclass Symtab.table * param list; |
65 |
||
66 |
fun merge_axclasses pp ((tab1, params1), (tab2, params2)) : axclasses = |
|
67 |
(Symtab.merge (K true) (tab1, tab2), merge_params pp (params1, params2)); |
|
68 |
||
19392 | 69 |
|
70 |
(* instances *) |
|
71 |
||
72 |
datatype instances = Instances of |
|
19405 | 73 |
{classes: unit Graph.T, (*raw relation -- no closure!*) |
74 |
classrel: ((class * class) * thm) list, |
|
75 |
arities: ((string * sort list * class) * thm) list}; |
|
19392 | 76 |
|
19405 | 77 |
fun make_instances (classes, classrel, arities) = |
78 |
Instances {classes = classes, classrel = classrel, arities = arities}; |
|
6379 | 79 |
|
19405 | 80 |
fun map_instances f (Instances {classes, classrel, arities}) = |
81 |
make_instances (f (classes, classrel, arities)); |
|
19392 | 82 |
|
83 |
fun merge_instances |
|
19405 | 84 |
(Instances {classes = classes1, classrel = classrel1, arities = arities1}, |
85 |
Instances {classes = classes2, classrel = classrel2, arities = arities2}) = |
|
19392 | 86 |
make_instances |
19405 | 87 |
(Graph.merge (K true) (classes1, classes2), |
88 |
merge (eq_fst op =) (classrel1, classrel2), |
|
19392 | 89 |
merge (eq_fst op =) (arities1, arities2)); |
90 |
||
91 |
||
19405 | 92 |
(* data *) |
19392 | 93 |
|
94 |
structure AxClassData = TheoryDataFun |
|
16458 | 95 |
(struct |
19392 | 96 |
val name = "Pure/axclass"; |
19405 | 97 |
type T = axclasses * instances; |
98 |
val empty : T = ((Symtab.empty, []), make_instances (Graph.empty, [], [])); |
|
6546 | 99 |
val copy = I; |
16458 | 100 |
val extend = I; |
6379 | 101 |
|
19405 | 102 |
fun merge pp ((axclasses1, instances1), (axclasses2, instances2)) = |
103 |
(merge_axclasses pp (axclasses1, axclasses2), merge_instances (instances1, instances2)); |
|
19392 | 104 |
|
19405 | 105 |
fun print thy ((axclasses, params), _) = |
6379 | 106 |
let |
19405 | 107 |
val ctxt = ProofContext.init thy; |
108 |
val prt_cls = ProofContext.pretty_sort ctxt o single; |
|
109 |
||
110 |
fun pretty_class c [] = prt_cls c |
|
111 |
| pretty_class c cs = Pretty.block |
|
112 |
(prt_cls c :: Pretty.str " <" :: Pretty.brk 1 :: Pretty.commas (map prt_cls cs)); |
|
6379 | 113 |
|
19405 | 114 |
fun pretty_axclass (class, AxClass {super_classes, intro, axioms}) = |
19392 | 115 |
Pretty.block (Pretty.fbreaks |
19405 | 116 |
[pretty_class class super_classes, |
117 |
Pretty.strs ("parameters:" :: |
|
118 |
fold (fn (x, c) => if c = class then cons x else I) params []), |
|
119 |
ProofContext.pretty_fact ctxt (introN, [intro]), |
|
120 |
ProofContext.pretty_fact ctxt (axiomsN, axioms)]); |
|
121 |
in |
|
122 |
Pretty.writeln (Pretty.chunks (map pretty_axclass (Symtab.dest axclasses))) |
|
123 |
end; |
|
16458 | 124 |
end); |
6379 | 125 |
|
19392 | 126 |
val _ = Context.add_setup AxClassData.init; |
127 |
val print_axclasses = AxClassData.print; |
|
128 |
||
129 |
val get_instances = AxClassData.get #> (fn (_, Instances insts) => insts); |
|
6379 | 130 |
|
131 |
||
19392 | 132 |
|
133 |
(** axclass definitions **) |
|
134 |
||
135 |
(* lookup *) |
|
136 |
||
19405 | 137 |
val lookup_info = Symtab.lookup o #1 o #1 o AxClassData.get; |
6379 | 138 |
|
17281
3b9ff0131ed1
name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17221
diff
changeset
|
139 |
fun get_info thy c = |
3b9ff0131ed1
name space prefix is now "c_class" instead of just "c";
wenzelm
parents:
17221
diff
changeset
|
140 |
(case lookup_info thy c of |
19392 | 141 |
SOME (AxClass info) => info |
142 |
| NONE => error ("Unknown axclass " ^ quote c)); |
|
6379 | 143 |
|
19123 | 144 |
fun class_intros thy = |
19392 | 145 |
let |
146 |
fun add_intro c = |
|
147 |
(case lookup_info thy c of SOME (AxClass {intro, ...}) => cons intro | _ => I); |
|
148 |
val classes = Sign.classes thy; |
|
149 |
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
|
150 |
|
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset
|
151 |
|
19392 | 152 |
(* add_axclass(_i) *) |
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
153 |
|
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset
|
154 |
local |
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
155 |
|
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
156 |
fun err_bad_axsort ax c = |
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
157 |
error ("Sort constraint in axiom " ^ quote ax ^ " not supersort of " ^ quote c); |
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
158 |
|
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
159 |
fun err_bad_tfrees ax = |
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
160 |
error ("More than one type variable in axiom " ^ quote ax); |
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
161 |
|
19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset
|
162 |
fun replace_tfree T = map_term_types (Term.map_atyps (fn TFree _ => T | U => U)); |
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset
|
163 |
|
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset
|
164 |
fun gen_axclass prep_class prep_axm prep_att |
19405 | 165 |
(bclass, raw_super_classes) params raw_axioms_atts thy = |
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
166 |
let |
19405 | 167 |
val pp = Sign.pp thy; |
168 |
||
16458 | 169 |
val class = Sign.full_name thy bclass; |
170 |
val super_classes = map (prep_class thy) raw_super_classes; |
|
19405 | 171 |
|
16458 | 172 |
val axms = map (prep_axm thy o fst) raw_axioms_atts; |
6379 | 173 |
val atts = map (map (prep_att thy) o snd) raw_axioms_atts; |
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
174 |
|
6379 | 175 |
(*declare class*) |
176 |
val class_thy = |
|
177 |
thy |> Theory.add_classes_i [(bclass, super_classes)]; |
|
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
178 |
|
6379 | 179 |
(*prepare abstract axioms*) |
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
180 |
fun abs_axm ax = |
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
181 |
if null (term_tfrees ax) then |
19392 | 182 |
Logic.mk_implies (Logic.mk_inclass (Term.aT [], class), ax) |
183 |
else replace_tfree (Term.aT [class]) ax; |
|
17756 | 184 |
val abs_axms = map (abs_axm o snd) axms; |
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
185 |
|
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
186 |
fun axm_sort (name, ax) = |
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
187 |
(case term_tfrees ax of |
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
188 |
[] => [] |
16458 | 189 |
| [(_, S)] => if Sign.subsort class_thy ([class], S) then S else err_bad_axsort name class |
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
190 |
| _ => err_bad_tfrees name); |
16458 | 191 |
val axS = Sign.certify_sort class_thy (List.concat (map axm_sort axms)); |
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
192 |
|
19392 | 193 |
val int_axm = Logic.close_form o replace_tfree (Term.aT axS); |
194 |
fun inclass c = Logic.mk_inclass (Term.aT axS, c); |
|
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
195 |
|
1498 | 196 |
val intro_axm = Logic.list_implies |
6379 | 197 |
(map inclass super_classes @ map (int_axm o #2) axms, inclass class); |
198 |
||
199 |
(*declare axioms and rule*) |
|
18377 | 200 |
val (([intro], [axioms]), axms_thy) = |
6379 | 201 |
class_thy |
18932 | 202 |
|> Theory.add_path (Logic.const_of_class bclass) |
6379 | 203 |
|> PureThy.add_axioms_i [Thm.no_attributes (introN, intro_axm)] |
18377 | 204 |
||>> PureThy.add_axiomss_i [Thm.no_attributes (axiomsN, abs_axms)]; |
19392 | 205 |
val info = make_axclass (super_classes, intro, axioms); |
6379 | 206 |
|
207 |
(*store info*) |
|
18377 | 208 |
val (_, final_thy) = |
6379 | 209 |
axms_thy |
19392 | 210 |
|> Theory.add_finals_i false [Const (Logic.const_of_class class, Term.a_itselfT --> propT)] |
18377 | 211 |
|> PureThy.add_thms ((map #1 axms ~~ axioms) ~~ atts) |
212 |
||> Theory.restore_naming class_thy |
|
19405 | 213 |
||> AxClassData.map (apfst (fn (is, ps) => |
214 |
(Symtab.update (class, info) is, fold (fn x => add_param pp (x, class)) params ps))); |
|
19392 | 215 |
in (class, final_thy) end; |
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
216 |
|
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset
|
217 |
in |
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
218 |
|
19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset
|
219 |
val add_axclass = gen_axclass Sign.intern_class Theory.read_axm Attrib.attribute; |
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset
|
220 |
val add_axclass_i = gen_axclass (K I) Theory.cert_axm (K I); |
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
221 |
|
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 |
end; |
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset
|
223 |
|
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset
|
224 |
|
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset
|
225 |
|
19392 | 226 |
(** instantiation 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
|
227 |
|
19405 | 228 |
(* parameters *) |
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset
|
229 |
|
19405 | 230 |
fun params_of_sort thy S = |
231 |
let |
|
232 |
val range = Graph.all_succs (Sign.classes_of thy) (Sign.certify_sort thy S); |
|
233 |
val params = #2 (#1 (AxClassData.get thy)); |
|
234 |
in fold (fn (x, c) => if member (op =) range c then cons x else I) params [] end; |
|
235 |
||
236 |
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
|
237 |
let |
19405 | 238 |
val (c1, c2) = pairself (Sign.certify_class thy) raw_rel; |
239 |
val _ = Type.add_classrel (Sign.pp thy) [(c1, c2)] (Sign.tsig_of thy); |
|
240 |
val _ = |
|
241 |
(case subtract (op =) (params_of_sort thy [c1]) (params_of_sort thy [c2]) of |
|
242 |
[] => () |
|
243 |
| xs => raise TYPE ("Class " ^ Sign.string_of_sort thy [c1] ^ " lacks parameter(s) " ^ |
|
244 |
commas_quote xs ^ " of " ^ Sign.string_of_sort thy [c2], [], [])); |
|
245 |
in (c1, c2) end; |
|
246 |
||
247 |
fun read_classrel thy raw_rel = |
|
248 |
cert_classrel thy (pairself (Sign.read_class thy) raw_rel) |
|
249 |
handle TYPE (msg, _, _) => error msg; |
|
250 |
||
251 |
||
252 |
(* primitive rules *) |
|
253 |
||
254 |
fun add_classrel th thy = |
|
255 |
let |
|
256 |
fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]); |
|
257 |
val prop = Drule.plain_prop_of (Thm.transfer thy th); |
|
258 |
val rel = Logic.dest_classrel prop handle TERM _ => err (); |
|
259 |
val (c1, c2) = cert_classrel thy rel handle TYPE _ => err (); |
|
19392 | 260 |
in |
261 |
thy |
|
19405 | 262 |
|> Theory.add_classrel_i [(c1, c2)] |
263 |
|> AxClassData.map (apsnd (map_instances (fn (classes, classrel, arities) => |
|
264 |
(classes |
|
265 |
|> Graph.default_node (c1, ()) |
|
266 |
|> Graph.default_node (c2, ()) |
|
267 |
|> Graph.add_edge (c1, c2), |
|
268 |
((c1, c2), th) :: classrel, arities)))) |
|
19392 | 269 |
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
|
270 |
|
19405 | 271 |
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
|
272 |
let |
19405 | 273 |
val prop = Drule.plain_prop_of (Thm.transfer thy th); |
274 |
val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => |
|
275 |
raise THM ("add_arity: malformed type arity", 0, [th]); |
|
19392 | 276 |
in |
277 |
thy |
|
19405 | 278 |
|> Theory.add_arities_i [(t, Ss, [c])] |
279 |
|> AxClassData.map (apsnd (map_instances (fn (classes, classrel, arities) => |
|
280 |
(classes, classrel, ((t, Ss, c), th) :: arities)))) |
|
19392 | 281 |
end; |
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
282 |
|
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
283 |
|
19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset
|
284 |
(* 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
|
285 |
|
19405 | 286 |
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
|
287 |
let |
19405 | 288 |
val (c1, c2) = cert_classrel thy raw_rel; |
289 |
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
|
290 |
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
|
291 |
quote (Sign.string_of_classrel thy [c1, c2])); |
19405 | 292 |
in add_classrel th thy end; |
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
293 |
|
19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset
|
294 |
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
|
295 |
let |
19243
5dcb899a8486
moved read_class, read/cert_classrel/arity to sign.ML;
wenzelm
parents:
19134
diff
changeset
|
296 |
val arity = Sign.cert_arity thy raw_arity; |
19405 | 297 |
val props = Logic.mk_arities arity; |
17956 | 298 |
val ths = Goal.prove_multi thy [] [] props |
18678 | 299 |
(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
|
300 |
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
|
301 |
quote (Sign.string_of_arity thy arity)); |
19405 | 302 |
in fold add_arity ths thy end; |
19392 | 303 |
|
15876
a67343c6ab2a
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
wenzelm
parents:
15853
diff
changeset
|
304 |
end; |