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