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