12 val trace_msg: (unit -> string) -> unit |
12 val trace_msg: (unit -> string) -> unit |
13 val skolem_prefix: string |
13 val skolem_prefix: string |
14 val skolem_infix: string |
14 val skolem_infix: string |
15 val cnf_axiom: theory -> thm -> thm list |
15 val cnf_axiom: theory -> thm -> thm list |
16 val multi_base_blacklist: string list |
16 val multi_base_blacklist: string list |
17 val bad_for_atp: thm -> bool |
17 val is_bad_for_atp: thm -> bool |
18 val type_has_topsort: typ -> bool |
18 val type_has_topsort: typ -> bool |
19 val cnf_rules_pairs: theory -> (string * thm) list -> (thm * (string * int)) list |
19 val cnf_rules_pairs: theory -> (string * thm) list -> (thm * (string * int)) list |
20 val suppress_endtheory: bool Unsynchronized.ref |
20 val suppress_endtheory: bool Unsynchronized.ref |
21 (*for emergency use where endtheory causes problems*) |
21 (*for emergency use where endtheory causes problems*) |
22 val strip_subgoal : thm -> int -> (string * typ) list * term list * term |
22 val strip_subgoal : thm -> int -> (string * typ) list * term list * term |
338 case head_of (concl_of th) of |
338 case head_of (concl_of th) of |
339 Const (a, _) => (a <> @{const_name Trueprop} andalso |
339 Const (a, _) => (a <> @{const_name Trueprop} andalso |
340 a <> @{const_name "=="}) |
340 a <> @{const_name "=="}) |
341 | _ => false; |
341 | _ => false; |
342 |
342 |
343 fun bad_for_atp th = |
343 fun is_bad_for_atp th = |
344 too_complex (prop_of th) |
344 too_complex (prop_of th) orelse |
345 orelse exists_type type_has_topsort (prop_of th) |
345 exists_type type_has_topsort (prop_of th) orelse is_strange_thm th |
346 orelse is_strange_thm th; |
|
347 |
346 |
348 (* FIXME: put other record thms here, or declare as "no_atp" *) |
347 (* FIXME: put other record thms here, or declare as "no_atp" *) |
349 val multi_base_blacklist = |
348 val multi_base_blacklist = |
350 ["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits", |
349 ["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits", |
351 "split_asm", "cases", "ext_cases"]; |
350 "split_asm", "cases", "ext_cases"]; |
355 else gensym "unknown_thm_"; |
354 else gensym "unknown_thm_"; |
356 |
355 |
357 (*Skolemize a named theorem, with Skolem functions as additional premises.*) |
356 (*Skolemize a named theorem, with Skolem functions as additional premises.*) |
358 fun skolem_thm (s, th) = |
357 fun skolem_thm (s, th) = |
359 if member (op =) multi_base_blacklist (Long_Name.base_name s) orelse |
358 if member (op =) multi_base_blacklist (Long_Name.base_name s) orelse |
360 bad_for_atp th then |
359 is_bad_for_atp th then |
361 [] |
360 [] |
362 else |
361 else |
363 let |
362 let |
364 val ctxt0 = Variable.global_thm_context th |
363 val ctxt0 = Variable.global_thm_context th |
365 val (nnfth, ctxt1) = to_nnf th ctxt0 |
364 val (nnfth, ctxt1) = to_nnf th ctxt0 |
441 if Facts.is_concealed facts name orelse already_seen thy name then I |
440 if Facts.is_concealed facts name orelse already_seen thy name then I |
442 else cons (name, ths)); |
441 else cons (name, ths)); |
443 val new_thms = (new_facts, []) |-> fold (fn (name, ths) => |
442 val new_thms = (new_facts, []) |-> fold (fn (name, ths) => |
444 if member (op =) multi_base_blacklist (Long_Name.base_name name) then I |
443 if member (op =) multi_base_blacklist (Long_Name.base_name name) then I |
445 else fold_index (fn (i, th) => |
444 else fold_index (fn (i, th) => |
446 if bad_for_atp th orelse is_some (lookup_cache thy th) then I |
445 if is_bad_for_atp th orelse is_some (lookup_cache thy th) then I |
447 else cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths); |
446 else cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths); |
448 in |
447 in |
449 if null new_facts then NONE |
448 if null new_facts then NONE |
450 else |
449 else |
451 let |
450 let |