author | wenzelm |
Tue, 23 Oct 2001 19:13:44 +0200 | |
changeset 11902 | db207d68392c |
parent 11828 | ef3e51b1b4ec |
child 11969 | c850db2e2e98 |
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 |
11539 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
5 |
|
6379 | 6 |
Axiomatic type class package. |
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 |
5685 | 11 |
val quiet_mode: bool ref |
6379 | 12 |
val print_axclasses: theory -> unit |
1498 | 13 |
val add_classrel_thms: thm list -> theory -> theory |
14 |
val add_arity_thms: thm list -> theory -> theory |
|
6379 | 15 |
val add_axclass: bclass * xclass list -> ((bstring * string) * Args.src list) list |
16 |
-> theory -> theory * {intro: thm, axioms: thm list} |
|
17 |
val add_axclass_i: bclass * class list -> ((bstring * term) * theory attribute list) list |
|
18 |
-> theory -> theory * {intro: thm, axioms: thm list} |
|
11828 | 19 |
val add_inst_subclass_x: xclass * xclass -> string list -> thm list |
3788 | 20 |
-> tactic option -> theory -> theory |
11828 | 21 |
val add_inst_subclass: xclass * xclass -> tactic -> theory -> theory |
22 |
val add_inst_subclass_i: class * class -> tactic -> theory -> theory |
|
23 |
val add_inst_arity_x: xstring * string list * string -> string list |
|
3938 | 24 |
-> thm list -> tactic option -> theory -> theory |
11828 | 25 |
val add_inst_arity: xstring * string list * string -> tactic -> theory -> theory |
26 |
val add_inst_arity_i: string * sort list * sort -> tactic -> theory -> theory |
|
10309 | 27 |
val default_intro_classes_tac: thm list -> int -> tactic |
6379 | 28 |
val axclass_tac: thm list -> tactic |
1498 | 29 |
val prove_subclass: theory -> class * class -> thm list |
30 |
-> tactic option -> thm |
|
31 |
val prove_arity: theory -> string * sort list * class -> thm list |
|
32 |
-> tactic option -> thm |
|
3949 | 33 |
val goal_subclass: theory -> xclass * xclass -> thm list |
8897 | 34 |
val goal_arity: theory -> xstring * string list * xclass -> thm list |
6729 | 35 |
val instance_subclass_proof: (xclass * xclass) * Comment.text -> bool -> theory -> ProofHistory.T |
36 |
val instance_subclass_proof_i: (class * class) * Comment.text -> bool -> theory -> ProofHistory.T |
|
8897 | 37 |
val instance_arity_proof: (xstring * string list * xclass) * Comment.text |
6729 | 38 |
-> bool -> theory -> ProofHistory.T |
39 |
val instance_arity_proof_i: (string * sort list * class) * Comment.text |
|
40 |
-> bool -> theory -> ProofHistory.T |
|
6379 | 41 |
val setup: (theory -> theory) list |
3938 | 42 |
end; |
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
43 |
|
1498 | 44 |
structure AxClass : AX_CLASS = |
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
45 |
struct |
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
46 |
|
4015 | 47 |
|
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
48 |
(** utilities **) |
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
49 |
|
5685 | 50 |
(* messages *) |
51 |
||
52 |
val quiet_mode = ref false; |
|
53 |
fun message s = if ! quiet_mode then () else writeln s; |
|
54 |
||
55 |
||
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
56 |
(* type vars *) |
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
57 |
|
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
58 |
fun map_typ_frees f (Type (t, tys)) = Type (t, map (map_typ_frees f) tys) |
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
59 |
| map_typ_frees f (TFree a) = f a |
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
60 |
| map_typ_frees _ a = a; |
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
61 |
|
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
62 |
val map_term_tfrees = map_term_types o map_typ_frees; |
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
63 |
|
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
64 |
fun aT S = TFree ("'a", S); |
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
65 |
|
3395 | 66 |
fun dest_varT (TFree (x, S)) = ((x, ~1), S) |
67 |
| dest_varT (TVar xi_S) = xi_S |
|
3788 | 68 |
| dest_varT T = raise TYPE ("dest_varT", [T], []); |
3395 | 69 |
|
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
70 |
|
886
9af08725600b
instance: now automatically includes defs of current thy node as witnesses;
wenzelm
parents:
638
diff
changeset
|
71 |
(* get axioms and theorems *) |
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
72 |
|
1498 | 73 |
val is_def = Logic.is_equals o #prop o rep_thm; |
886
9af08725600b
instance: now automatically includes defs of current thy node as witnesses;
wenzelm
parents:
638
diff
changeset
|
74 |
|
4934 | 75 |
fun witnesses thy names thms = |
6379 | 76 |
PureThy.get_thmss thy names @ thms @ filter is_def (map snd (axioms_of thy)); |
886
9af08725600b
instance: now automatically includes defs of current thy node as witnesses;
wenzelm
parents:
638
diff
changeset
|
77 |
|
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
78 |
|
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
79 |
|
560 | 80 |
(** abstract syntax operations **) |
423 | 81 |
|
6379 | 82 |
(* names *) |
83 |
||
84 |
fun intro_name c = c ^ "I"; |
|
85 |
val introN = "intro"; |
|
86 |
val axiomsN = "axioms"; |
|
87 |
||
88 |
||
423 | 89 |
(* subclass relations as terms *) |
90 |
||
1498 | 91 |
fun mk_classrel (c1, c2) = Logic.mk_inclass (aT [c1], c2); |
423 | 92 |
|
93 |
fun dest_classrel tm = |
|
94 |
let |
|
3788 | 95 |
fun err () = raise TERM ("dest_classrel", [tm]); |
423 | 96 |
|
3395 | 97 |
val (ty, c2) = Logic.dest_inclass tm handle TERM _ => err (); |
98 |
val c1 = (case dest_varT ty of (_, [c]) => c | _ => err ()) |
|
99 |
handle TYPE _ => err (); |
|
6379 | 100 |
in (c1, c2) end; |
423 | 101 |
|
102 |
||
103 |
(* arities as terms *) |
|
104 |
||
105 |
fun mk_arity (t, ss, c) = |
|
106 |
let |
|
11541 | 107 |
val tfrees = ListPair.map TFree (Term.invent_names (length ss) "'", ss); |
6379 | 108 |
in Logic.mk_inclass (Type (t, tfrees), c) end; |
423 | 109 |
|
110 |
fun dest_arity tm = |
|
111 |
let |
|
3788 | 112 |
fun err () = raise TERM ("dest_arity", [tm]); |
423 | 113 |
|
3395 | 114 |
val (ty, c) = Logic.dest_inclass tm handle TERM _ => err (); |
115 |
val (t, tvars) = |
|
423 | 116 |
(case ty of |
3395 | 117 |
Type (t, tys) => (t, map dest_varT tys handle TYPE _ => err ()) |
423 | 118 |
| _ => err ()); |
119 |
val ss = |
|
3395 | 120 |
if null (gen_duplicates eq_fst tvars) |
121 |
then map snd tvars else err (); |
|
6379 | 122 |
in (t, ss, c) end; |
423 | 123 |
|
124 |
||
125 |
||
560 | 126 |
(** add theorems as axioms **) |
423 | 127 |
|
128 |
fun prep_thm_axm thy thm = |
|
129 |
let |
|
130 |
fun err msg = raise THM ("prep_thm_axm: " ^ msg, 0, [thm]); |
|
131 |
||
1237 | 132 |
val {sign, hyps, prop, ...} = rep_thm thm; |
423 | 133 |
in |
6390 | 134 |
if not (Sign.subsig (sign, Theory.sign_of thy)) then |
423 | 135 |
err "theorem not of same theory" |
1237 | 136 |
else if not (null (extra_shyps thm)) orelse not (null hyps) then |
423 | 137 |
err "theorem may not contain hypotheses" |
138 |
else prop |
|
139 |
end; |
|
140 |
||
141 |
(*theorems expressing class relations*) |
|
142 |
fun add_classrel_thms thms thy = |
|
143 |
let |
|
144 |
fun prep_thm thm = |
|
145 |
let |
|
146 |
val prop = prep_thm_axm thy thm; |
|
147 |
val (c1, c2) = dest_classrel prop handle TERM _ => |
|
148 |
raise THM ("add_classrel_thms: theorem is not a class relation", 0, [thm]); |
|
149 |
in (c1, c2) end; |
|
8897 | 150 |
in Theory.add_classrel_i (map prep_thm thms) thy end; |
423 | 151 |
|
152 |
(*theorems expressing arities*) |
|
153 |
fun add_arity_thms thms thy = |
|
154 |
let |
|
155 |
fun prep_thm thm = |
|
156 |
let |
|
157 |
val prop = prep_thm_axm thy thm; |
|
158 |
val (t, ss, c) = dest_arity prop handle TERM _ => |
|
159 |
raise THM ("add_arity_thms: theorem is not an arity", 0, [thm]); |
|
160 |
in (t, ss, [c]) end; |
|
8897 | 161 |
in Theory.add_arities_i (map prep_thm thms) thy end; |
6379 | 162 |
|
163 |
||
164 |
||
165 |
(** axclass info **) |
|
166 |
||
167 |
(* data kind 'Pure/axclasses' *) |
|
168 |
||
169 |
type axclass_info = |
|
170 |
{super_classes: class list, |
|
171 |
intro: thm, |
|
172 |
axioms: thm list}; |
|
173 |
||
174 |
structure AxclassesArgs = |
|
175 |
struct |
|
176 |
val name = "Pure/axclasses"; |
|
177 |
type T = axclass_info Symtab.table; |
|
178 |
||
179 |
val empty = Symtab.empty; |
|
6546 | 180 |
val copy = I; |
6379 | 181 |
val prep_ext = I; |
182 |
fun merge (tab1, tab2) = Symtab.merge (K true) (tab1, tab2); |
|
183 |
||
184 |
fun print sg tab = |
|
185 |
let |
|
186 |
val ext_class = Sign.cond_extern sg Sign.classK; |
|
187 |
val ext_thm = PureThy.cond_extern_thm_sg sg; |
|
188 |
||
189 |
fun pretty_class c cs = Pretty.block |
|
190 |
(Pretty.str (ext_class c) :: Pretty.str " <" :: Pretty.brk 1 :: |
|
191 |
Pretty.breaks (map (Pretty.str o ext_class) cs)); |
|
192 |
||
10008 | 193 |
fun pretty_thms name thms = Pretty.big_list (name ^ ":") |
194 |
(map (Display.pretty_thm_sg sg) thms); |
|
6379 | 195 |
|
196 |
fun pretty_axclass (name, {super_classes, intro, axioms}) = Pretty.block (Pretty.fbreaks |
|
197 |
[pretty_class name super_classes, pretty_thms introN [intro], pretty_thms axiomsN axioms]); |
|
8720 | 198 |
in Pretty.writeln (Pretty.chunks (map pretty_axclass (Symtab.dest tab))) end; |
6379 | 199 |
end; |
200 |
||
201 |
structure AxclassesData = TheoryDataFun(AxclassesArgs); |
|
202 |
val print_axclasses = AxclassesData.print; |
|
203 |
||
204 |
||
205 |
(* get and put data *) |
|
206 |
||
207 |
fun lookup_axclass_info_sg sg c = Symtab.lookup (AxclassesData.get_sg sg, c); |
|
208 |
||
209 |
fun get_axclass_info thy c = |
|
210 |
(case lookup_axclass_info_sg (Theory.sign_of thy) c of |
|
211 |
None => error ("Unknown axclass " ^ quote c) |
|
212 |
| Some info => info); |
|
213 |
||
214 |
fun put_axclass_info c info thy = |
|
215 |
thy |> AxclassesData.put (Symtab.update ((c, info), AxclassesData.get thy)); |
|
423 | 216 |
|
217 |
||
218 |
||
219 |
(** add axiomatic type classes **) |
|
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
220 |
|
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
221 |
(* errors *) |
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
222 |
|
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
223 |
fun err_not_logic c = |
4917 | 224 |
error ("Axiomatic class " ^ quote c ^ " not subclass of " ^ quote logicC); |
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
225 |
|
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
226 |
fun err_bad_axsort ax c = |
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
227 |
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
|
228 |
|
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
229 |
fun err_bad_tfrees ax = |
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
230 |
error ("More than one type variable in axiom " ^ quote ax); |
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 |
|
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
233 |
(* ext_axclass *) |
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
234 |
|
6379 | 235 |
fun ext_axclass prep_class prep_axm prep_att (bclass, raw_super_classes) raw_axioms_atts thy = |
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
236 |
let |
6379 | 237 |
val sign = Theory.sign_of thy; |
3938 | 238 |
|
6379 | 239 |
val class = Sign.full_name sign bclass; |
240 |
val super_classes = map (prep_class sign) raw_super_classes; |
|
241 |
val axms = map (prep_axm sign o fst) raw_axioms_atts; |
|
242 |
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
|
243 |
|
6379 | 244 |
(*declare class*) |
245 |
val class_thy = |
|
246 |
thy |> Theory.add_classes_i [(bclass, super_classes)]; |
|
247 |
val class_sign = Theory.sign_of class_thy; |
|
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
248 |
|
6379 | 249 |
(*prepare abstract axioms*) |
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
250 |
fun abs_axm ax = |
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
251 |
if null (term_tfrees ax) then |
1498 | 252 |
Logic.mk_implies (Logic.mk_inclass (aT logicS, class), ax) |
3788 | 253 |
else map_term_tfrees (K (aT [class])) ax; |
6379 | 254 |
val abs_axms = map (abs_axm o #2) axms; |
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
255 |
|
6379 | 256 |
(*prepare introduction rule*) |
257 |
val _ = if Sign.subsort class_sign ([class], logicS) then () else err_not_logic class; |
|
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
258 |
|
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
259 |
fun axm_sort (name, ax) = |
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
260 |
(case term_tfrees ax of |
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
261 |
[] => [] |
6379 | 262 |
| [(_, S)] => if Sign.subsort class_sign ([class], S) then S else err_bad_axsort name class |
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
263 |
| _ => err_bad_tfrees name); |
6379 | 264 |
val axS = Sign.norm_sort class_sign (logicC :: flat (map axm_sort axms)); |
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
265 |
|
1498 | 266 |
val int_axm = Logic.close_form o map_term_tfrees (K (aT axS)); |
267 |
fun inclass c = Logic.mk_inclass (aT axS, c); |
|
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
268 |
|
1498 | 269 |
val intro_axm = Logic.list_implies |
6379 | 270 |
(map inclass super_classes @ map (int_axm o #2) axms, inclass class); |
271 |
||
272 |
(*declare axioms and rule*) |
|
8420 | 273 |
val (axms_thy, ([intro], [axioms])) = |
6379 | 274 |
class_thy |
275 |
|> Theory.add_path bclass |
|
276 |
|> PureThy.add_axioms_i [Thm.no_attributes (introN, intro_axm)] |
|
8420 | 277 |
|>>> PureThy.add_axiomss_i [Thm.no_attributes (axiomsN, abs_axms)]; |
6379 | 278 |
val info = {super_classes = super_classes, intro = intro, axioms = axioms}; |
279 |
||
280 |
(*store info*) |
|
281 |
val final_thy = |
|
282 |
axms_thy |
|
8420 | 283 |
|> (#1 o PureThy.add_thms ((map #1 axms ~~ axioms) ~~ atts)) |
6379 | 284 |
|> Theory.parent_path |
8420 | 285 |
|> (#1 o PureThy.add_thms [Thm.no_attributes (intro_name bclass, intro)]) |
6379 | 286 |
|> put_axclass_info class info; |
287 |
in (final_thy, {intro = intro, axioms = axioms}) end; |
|
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
288 |
|
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
289 |
|
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
290 |
(* external interfaces *) |
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
291 |
|
6390 | 292 |
val add_axclass = ext_axclass Sign.intern_class Theory.read_axm Attrib.global_attribute; |
293 |
val add_axclass_i = ext_axclass (K I) Theory.cert_axm (K I); |
|
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
294 |
|
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
295 |
|
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
296 |
|
423 | 297 |
(** prove class relations and type arities **) |
298 |
||
299 |
(* class_axms *) |
|
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
300 |
|
6379 | 301 |
fun class_axms sign = |
302 |
let val classes = Sign.classes sign in |
|
303 |
map (Thm.class_triv sign) classes @ |
|
304 |
mapfilter (apsome #intro o lookup_axclass_info_sg sign) classes |
|
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
305 |
end; |
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
306 |
|
423 | 307 |
|
7351 | 308 |
(* intro_classes *) |
6379 | 309 |
|
10309 | 310 |
fun intro_classes_tac facts i st = |
10507
ea5de7c64c23
Tactic.distinct_subgoals_tac moved to internal intro_classes_tac;
wenzelm
parents:
10493
diff
changeset
|
311 |
((Method.insert_tac facts THEN' |
ea5de7c64c23
Tactic.distinct_subgoals_tac moved to internal intro_classes_tac;
wenzelm
parents:
10493
diff
changeset
|
312 |
REPEAT_ALL_NEW (resolve_tac (class_axms (Thm.sign_of_thm st)))) i |
ea5de7c64c23
Tactic.distinct_subgoals_tac moved to internal intro_classes_tac;
wenzelm
parents:
10493
diff
changeset
|
313 |
THEN Tactic.distinct_subgoals_tac) st; (*affects all subgoals!?*) |
6379 | 314 |
|
7351 | 315 |
val intro_classes_method = |
10309 | 316 |
("intro_classes", Method.no_args (Method.METHOD (HEADGOAL o intro_classes_tac)), |
7351 | 317 |
"back-chain introduction rules of axiomatic type classes"); |
6379 | 318 |
|
319 |
||
10309 | 320 |
(* default method *) |
321 |
||
10507
ea5de7c64c23
Tactic.distinct_subgoals_tac moved to internal intro_classes_tac;
wenzelm
parents:
10493
diff
changeset
|
322 |
fun default_intro_classes_tac [] i = intro_classes_tac [] i |
10493
76e05ec87b57
default_intro_classes_tac: Tactic.distinct_subgoals_tac;
wenzelm
parents:
10463
diff
changeset
|
323 |
| default_intro_classes_tac _ _ = Tactical.no_tac; (*no error message!*) |
10309 | 324 |
|
325 |
fun default_tac rules ctxt facts = |
|
326 |
HEADGOAL (Method.some_rule_tac rules ctxt facts ORELSE' default_intro_classes_tac facts); |
|
327 |
||
328 |
val default_method = |
|
329 |
("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some rule") |
|
330 |
||
331 |
||
423 | 332 |
(* axclass_tac *) |
333 |
||
487
af83700cb771
added experimental add_defns (actually should be moved somewhere else);
wenzelm
parents:
474
diff
changeset
|
334 |
(*(1) repeatedly resolve goals of form "OFCLASS(ty, c_class)", |
1217 | 335 |
try class_trivs first, then "cI" axioms |
423 | 336 |
(2) rewrite goals using user supplied definitions |
337 |
(3) repeatedly resolve goals with user supplied non-definitions*) |
|
338 |
||
6379 | 339 |
fun axclass_tac thms = |
1217 | 340 |
let |
341 |
val defs = filter is_def thms; |
|
342 |
val non_defs = filter_out is_def thms; |
|
343 |
in |
|
10309 | 344 |
HEADGOAL (intro_classes_tac []) THEN |
1217 | 345 |
TRY (rewrite_goals_tac defs) THEN |
346 |
TRY (REPEAT_FIRST (fn i => assume_tac i ORELSE resolve_tac non_defs i)) |
|
347 |
end; |
|
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
348 |
|
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
349 |
|
423 | 350 |
(* provers *) |
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
351 |
|
6379 | 352 |
fun prove mk_prop str_of thy sig_prop thms usr_tac = |
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
353 |
let |
6390 | 354 |
val sign = Theory.sign_of thy; |
6679 | 355 |
val goal = Thm.cterm_of sign (mk_prop sig_prop) |
356 |
handle TERM (msg, _) => error msg |
|
357 |
| TYPE (msg, _, _) => error msg; |
|
6379 | 358 |
val tac = axclass_tac thms THEN (if_none usr_tac all_tac); |
423 | 359 |
in |
360 |
prove_goalw_cterm [] goal (K [tac]) |
|
361 |
end |
|
362 |
handle ERROR => error ("The error(s) above occurred while trying to prove " |
|
6390 | 363 |
^ quote (str_of (Theory.sign_of thy, sig_prop))); |
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
364 |
|
638 | 365 |
val prove_subclass = |
3854
762606a888fe
uses Sign.str_of_classrel, Sign.str_of_arity, Sign.str_of_arity;
wenzelm
parents:
3809
diff
changeset
|
366 |
prove mk_classrel (fn (sg, c1_c2) => Sign.str_of_classrel sg c1_c2); |
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
367 |
|
423 | 368 |
val prove_arity = |
3854
762606a888fe
uses Sign.str_of_classrel, Sign.str_of_arity, Sign.str_of_arity;
wenzelm
parents:
3809
diff
changeset
|
369 |
prove mk_arity (fn (sg, (t, Ss, c)) => Sign.str_of_arity sg (t, Ss, [c])); |
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
370 |
|
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
371 |
|
423 | 372 |
|
449 | 373 |
(** add proved subclass relations and arities **) |
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
374 |
|
8897 | 375 |
(* prepare classes and arities *) |
376 |
||
377 |
fun read_class sg c = Sign.certify_class sg (Sign.intern_class sg c); |
|
378 |
||
379 |
fun cert_classrel sg cc = Library.pairself (Sign.certify_class sg) cc; |
|
380 |
fun read_classrel sg cc = Library.pairself (read_class sg) cc; |
|
3949 | 381 |
|
8897 | 382 |
fun check_tycon sg t = |
383 |
let val {tycons, abbrs, ...} = Type.rep_tsig (Sign.tsig_of sg) in |
|
384 |
if is_some (Symtab.lookup (abbrs, t)) then |
|
385 |
error ("Illegal type abbreviation: " ^ quote t) |
|
386 |
else if is_none (Symtab.lookup (tycons, t)) then |
|
387 |
error ("Undeclared type constructor: " ^ quote t) |
|
388 |
else t |
|
8716 | 389 |
end; |
6379 | 390 |
|
8897 | 391 |
fun prep_arity prep_tycon prep_sort prep_x sg (t, Ss, x) = |
392 |
(check_tycon sg (prep_tycon sg t), map (prep_sort sg) Ss, prep_x sg x); |
|
393 |
||
394 |
val read_arity = prep_arity Sign.intern_tycon Sign.read_sort Sign.read_sort; |
|
395 |
val cert_arity = prep_arity (K I) Sign.certify_sort Sign.certify_sort; |
|
396 |
val read_simple_arity = prep_arity Sign.intern_tycon Sign.read_sort Sign.intern_class; |
|
8927 | 397 |
fun cert_simple_arity arg = prep_arity (K I) Sign.certify_sort (K I) arg; |
8897 | 398 |
|
399 |
||
400 |
(* old-style instance declarations *) |
|
6379 | 401 |
|
402 |
fun ext_inst_subclass prep_classrel raw_c1_c2 names thms usr_tac thy = |
|
403 |
let val c1_c2 = prep_classrel (Theory.sign_of thy) raw_c1_c2 in |
|
5685 | 404 |
message ("Proving class inclusion " ^ |
6390 | 405 |
quote (Sign.str_of_classrel (Theory.sign_of thy) c1_c2) ^ " ..."); |
6379 | 406 |
thy |> add_classrel_thms [prove_subclass thy c1_c2 (witnesses thy names thms) usr_tac] |
3788 | 407 |
end; |
423 | 408 |
|
6379 | 409 |
fun ext_inst_arity prep_arity (raw_t, raw_Ss, raw_cs) names thms usr_tac thy = |
423 | 410 |
let |
6379 | 411 |
val sign = Theory.sign_of thy; |
412 |
val (t, Ss, cs) = prep_arity sign (raw_t, raw_Ss, raw_cs); |
|
4934 | 413 |
val wthms = witnesses thy names thms; |
423 | 414 |
fun prove c = |
5685 | 415 |
(message ("Proving type arity " ^ |
3854
762606a888fe
uses Sign.str_of_classrel, Sign.str_of_arity, Sign.str_of_arity;
wenzelm
parents:
3809
diff
changeset
|
416 |
quote (Sign.str_of_arity sign (t, Ss, [c])) ^ " ..."); |
762606a888fe
uses Sign.str_of_classrel, Sign.str_of_arity, Sign.str_of_arity;
wenzelm
parents:
3809
diff
changeset
|
417 |
prove_arity thy (t, Ss, c) wthms usr_tac); |
6379 | 418 |
in add_arity_thms (map prove cs) thy end; |
419 |
||
11828 | 420 |
fun sane_inst_subclass prep sub tac = ext_inst_subclass prep sub [] [] (Some tac); |
421 |
fun sane_inst_arity prep arity tac = ext_inst_arity prep arity [] [] (Some tac); |
|
6379 | 422 |
|
11828 | 423 |
val add_inst_subclass_x = ext_inst_subclass read_classrel; |
424 |
val add_inst_subclass = sane_inst_subclass read_classrel; |
|
425 |
val add_inst_subclass_i = sane_inst_subclass cert_classrel; |
|
426 |
val add_inst_arity_x = ext_inst_arity read_arity; |
|
427 |
val add_inst_arity = sane_inst_arity read_arity; |
|
428 |
val add_inst_arity_i = sane_inst_arity cert_arity; |
|
6379 | 429 |
|
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
430 |
|
6379 | 431 |
(* make old-style interactive goals *) |
432 |
||
433 |
fun mk_goal mk_prop thy sig_prop = |
|
434 |
Goals.goalw_cterm [] (Thm.cterm_of (Theory.sign_of thy) (mk_prop (Theory.sign_of thy) sig_prop)); |
|
435 |
||
8897 | 436 |
val goal_subclass = mk_goal (mk_classrel oo read_classrel); |
437 |
val goal_arity = mk_goal (mk_arity oo read_simple_arity); |
|
6379 | 438 |
|
3788 | 439 |
|
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
440 |
|
6379 | 441 |
(** instance proof interfaces **) |
442 |
||
443 |
fun inst_attribute add_thms (thy, thm) = (add_thms [thm] thy, thm); |
|
444 |
||
6729 | 445 |
fun inst_proof mk_prop add_thms (sig_prop, comment) int thy = |
6379 | 446 |
thy |
11740 | 447 |
|> IsarThy.theorem_i Drule.internalK ((("", [inst_attribute add_thms]), |
6935 | 448 |
(mk_prop (Theory.sign_of thy) sig_prop, ([], []))), comment) int; |
3949 | 449 |
|
8897 | 450 |
val instance_subclass_proof = inst_proof (mk_classrel oo read_classrel) add_classrel_thms; |
451 |
val instance_subclass_proof_i = inst_proof (mk_classrel oo cert_classrel) add_classrel_thms; |
|
452 |
val instance_arity_proof = inst_proof (mk_arity oo read_simple_arity) add_arity_thms; |
|
453 |
val instance_arity_proof_i = inst_proof (mk_arity oo cert_simple_arity) add_arity_thms; |
|
6379 | 454 |
|
455 |
||
456 |
||
457 |
(** package setup **) |
|
458 |
||
459 |
(* setup theory *) |
|
3949 | 460 |
|
6379 | 461 |
val setup = |
462 |
[AxclassesData.init, |
|
10309 | 463 |
Method.add_methods [intro_classes_method, default_method]]; |
6379 | 464 |
|
465 |
||
466 |
(* outer syntax *) |
|
467 |
||
6719 | 468 |
local structure P = OuterParse and K = OuterSyntax.Keyword in |
3949 | 469 |
|
6379 | 470 |
val axclassP = |
6719 | 471 |
OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl |
11101
014e7b5c77ba
support \<subseteq> syntax in classes/classrel/axclass/instance;
wenzelm
parents:
10507
diff
changeset
|
472 |
(((P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- |
014e7b5c77ba
support \<subseteq> syntax in classes/classrel/axclass/instance;
wenzelm
parents:
10507
diff
changeset
|
473 |
P.!!! (P.list1 P.xname)) []) --| P.marg_comment) |
6729 | 474 |
-- Scan.repeat (P.spec_name --| P.marg_comment) |
6379 | 475 |
>> (fn (cls, axs) => Toplevel.theory (#1 o add_axclass cls axs))); |
476 |
||
477 |
val instanceP = |
|
6719 | 478 |
OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal |
11101
014e7b5c77ba
support \<subseteq> syntax in classes/classrel/axclass/instance;
wenzelm
parents:
10507
diff
changeset
|
479 |
((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.xname) |
014e7b5c77ba
support \<subseteq> syntax in classes/classrel/axclass/instance;
wenzelm
parents:
10507
diff
changeset
|
480 |
-- P.marg_comment >> instance_subclass_proof || |
6729 | 481 |
(P.xname -- (P.$$$ "::" |-- P.simple_arity) >> P.triple2) -- P.marg_comment |
482 |
>> instance_arity_proof) |
|
6379 | 483 |
>> (Toplevel.print oo Toplevel.theory_to_proof)); |
484 |
||
485 |
val _ = OuterSyntax.add_parsers [axclassP, instanceP]; |
|
486 |
||
487 |
end; |
|
3949 | 488 |
|
489 |
||
404
dd3d3d6467db
axiomatic type class 'package' for Pure (alpha version);
wenzelm
parents:
diff
changeset
|
490 |
end; |