equal
deleted
inserted
replaced
19 val add_inst_subclass: class * class -> string list -> thm list |
19 val add_inst_subclass: class * class -> string list -> thm list |
20 -> tactic option -> theory -> theory |
20 -> tactic option -> theory -> theory |
21 val add_inst_arity: string * sort list * class list -> string list |
21 val add_inst_arity: string * sort list * class list -> string list |
22 -> thm list -> tactic option -> theory -> theory |
22 -> thm list -> tactic option -> theory -> theory |
23 val axclass_tac: theory -> thm list -> tactic |
23 val axclass_tac: theory -> thm list -> tactic |
|
24 val prove_subclass: theory -> class * class -> thm list |
|
25 -> tactic option -> thm |
|
26 val prove_arity: theory -> string * sort list * class -> thm list |
|
27 -> tactic option -> thm |
24 val goal_subclass: theory -> class * class -> thm list |
28 val goal_subclass: theory -> class * class -> thm list |
25 val goal_arity: theory -> string * sort list * class -> thm list |
29 val goal_arity: theory -> string * sort list * class -> thm list |
26 end |
30 end |
27 end; |
31 end; |
28 |
32 |
56 |
60 |
57 fun get_ax thy name = |
61 fun get_ax thy name = |
58 Some (get_axiom thy name) handle THEORY _ => None; |
62 Some (get_axiom thy name) handle THEORY _ => None; |
59 |
63 |
60 val get_axioms = mapfilter o get_ax; |
64 val get_axioms = mapfilter o get_ax; |
61 |
|
62 |
|
63 (* is_defn *) |
|
64 |
|
65 fun is_defn thm = |
|
66 (case #prop (rep_thm thm) of |
|
67 Const ("==", _) $ _ $ _ => true |
|
68 | _ => false); |
|
69 |
65 |
70 |
66 |
71 |
67 |
72 (** abstract syntax operations **) |
68 (** abstract syntax operations **) |
73 |
69 |
247 (*(1) repeatedly resolve goals of form "OFCLASS(ty, c_class)", |
243 (*(1) repeatedly resolve goals of form "OFCLASS(ty, c_class)", |
248 try "cI" axioms first and use class_triv as last resort |
244 try "cI" axioms first and use class_triv as last resort |
249 (2) rewrite goals using user supplied definitions |
245 (2) rewrite goals using user supplied definitions |
250 (3) repeatedly resolve goals with user supplied non-definitions*) |
246 (3) repeatedly resolve goals with user supplied non-definitions*) |
251 |
247 |
|
248 val is_def = is_equals o #prop o rep_thm; |
|
249 |
252 fun axclass_tac thy thms = |
250 fun axclass_tac thy thms = |
253 TRY (REPEAT_FIRST (resolve_tac (class_axms thy))) THEN |
251 TRY (REPEAT_FIRST (resolve_tac (class_axms thy))) THEN |
254 TRY (rewrite_goals_tac (filter is_defn thms)) THEN |
252 TRY (rewrite_goals_tac (filter is_def thms)) THEN |
255 TRY (REPEAT_FIRST (resolve_tac (filter_out is_defn thms))); |
253 TRY (REPEAT_FIRST (resolve_tac (filter_out is_def thms))); |
256 |
254 |
257 |
255 |
258 (* provers *) |
256 (* provers *) |
259 |
257 |
260 fun prove term_of str_of thy sig_prop thms usr_tac = |
258 fun prove term_of str_of thy sig_prop thms usr_tac = |
266 prove_goalw_cterm [] goal (K [tac]) |
264 prove_goalw_cterm [] goal (K [tac]) |
267 end |
265 end |
268 handle ERROR => error ("The error(s) above occurred while trying to prove " |
266 handle ERROR => error ("The error(s) above occurred while trying to prove " |
269 ^ quote (str_of sig_prop)); |
267 ^ quote (str_of sig_prop)); |
270 |
268 |
271 val prove_classrel = |
269 val prove_subclass = |
272 prove mk_classrel (fn (c1, c2) => c1 ^ " < " ^ c2); |
270 prove mk_classrel (fn (c1, c2) => c1 ^ " < " ^ c2); |
273 |
271 |
274 val prove_arity = |
272 val prove_arity = |
275 prove mk_arity (fn (t, ss, c) => Type.str_of_arity (t, ss, [c])); |
273 prove mk_arity (fn (t, ss, c) => Type.str_of_arity (t, ss, [c])); |
276 |
274 |
287 |
285 |
288 (** add proved subclass relations and arities **) |
286 (** add proved subclass relations and arities **) |
289 |
287 |
290 fun add_inst_subclass (c1, c2) axms thms usr_tac thy = |
288 fun add_inst_subclass (c1, c2) axms thms usr_tac thy = |
291 add_classrel_thms |
289 add_classrel_thms |
292 [prove_classrel thy (c1, c2) (get_axioms thy axms @ thms) usr_tac] thy; |
290 [prove_subclass thy (c1, c2) (get_axioms thy axms @ thms) usr_tac] thy; |
293 |
291 |
294 fun add_inst_arity (t, ss, cs) axms thms usr_tac thy = |
292 fun add_inst_arity (t, ss, cs) axms thms usr_tac thy = |
295 let |
293 let |
296 val usr_thms = get_axioms thy axms @ thms; |
294 val usr_thms = get_axioms thy axms @ thms; |
297 fun prove c = |
295 fun prove c = |