--- a/src/HOL/Tools/ATP/reduce_axiomsN.ML Fri Sep 01 08:36:55 2006 +0200
+++ b/src/HOL/Tools/ATP/reduce_axiomsN.ML Fri Sep 01 08:51:53 2006 +0200
@@ -2,9 +2,16 @@
ID: $Id$
Filtering strategies *)
+(*A surprising number of theorems contain only a few significant constants.
+ These include all induction rules, and other general theorems. Filtering
+ theorems in clause form reveals these complexities in the form of Skolem
+ functions. If we were instead to filter theorems in their natural form,
+ some other method of measuring theorem complexity would become necessary.*)
+
structure ReduceAxiomsN =
struct
+val run_relevance_filter = ref true;
val pass_mark = ref 0.6;
val convergence = ref 2.4; (*Higher numbers allow longer inference chains*)
val follow_defs = ref false; (*Follow definitions. Makes problems bigger.*)
@@ -19,8 +26,8 @@
(*Including equality in this list might be expected to stop rules like subset_antisym from
being chosen, but for some reason filtering works better with them listed.*)
val standard_consts =
- ["Trueprop","==>","all","Ex","op &","op |","Not","All","op -->",
- "op =","==","True","False"];
+ ["Trueprop","==>","all","==","All","Ex","Ball","Bex","op &","op |","Not","op -->",
+ "op =","True","False"];
(*** constants with types ***)
@@ -74,7 +81,7 @@
val null_const_tab : const_typ list list Symtab.table =
foldl add_standard_const Symtab.empty standard_consts;
-fun get_goal_consts_typs thy cs = foldl (add_term_consts_typs_rm thy) null_const_tab cs;
+fun get_goal_consts_typs thy = foldl (add_term_consts_typs_rm thy) null_const_tab;
(**** Constant / Type Frequencies ****)
@@ -201,8 +208,8 @@
end;
fun relevance_filter thy axioms goals =
- if !pass_mark < 0.1 then axioms
- else map #1 (relevance_filter_aux thy axioms goals);
-
+ if !run_relevance_filter andalso !pass_mark >= 0.1
+ then map #1 (relevance_filter_aux thy axioms goals)
+ else axioms
end;
--- a/src/HOL/Tools/res_atp.ML Fri Sep 01 08:36:55 2006 +0200
+++ b/src/HOL/Tools/res_atp.ML Fri Sep 01 08:51:53 2006 +0200
@@ -5,6 +5,7 @@
ATPs with TPTP format input.
*)
+(*FIXME: Do we need this signature?*)
signature RES_ATP =
sig
val prover: string ref
@@ -52,7 +53,7 @@
val rm_clasimp : unit -> unit
end;
-structure ResAtp : RES_ATP =
+structure ResAtp =
struct
(********************************************************************)
@@ -159,7 +160,7 @@
(**** relevance filter ****)
-val run_relevance_filter = ref true;
+val run_relevance_filter = ReduceAxiomsN.run_relevance_filter;
val run_blacklist_filter = ref true;
(******************************************************************)
@@ -173,11 +174,9 @@
| string_of_logic HOLC = "HOLC"
| string_of_logic HOLCS = "HOLCS";
-
fun is_fol_logic FOL = true
| is_fol_logic _ = false
-
(*HOLCS will not occur here*)
fun upgrade_lg HOLC _ = HOLC
| upgrade_lg HOL HOLC = HOLC
@@ -216,51 +215,47 @@
fun term_lg [] (lg,seen) = (lg,seen)
| term_lg (tm::tms) (FOL,seen) =
- let val (f,args) = strip_comb tm
- val (lg',seen') = if f mem seen then (FOL,seen)
- else fn_lg f (FOL,seen)
- val _ =
- if is_fol_logic lg' then ()
- else Output.debug ("Found a HOL term: " ^ Display.raw_string_of_term f)
- in
- term_lg (args@tms) (lg',seen')
- end
+ let val (f,args) = strip_comb tm
+ val (lg',seen') = if f mem seen then (FOL,seen)
+ else fn_lg f (FOL,seen)
+ in
+ if is_fol_logic lg' then ()
+ else Output.debug ("Found a HOL term: " ^ Display.raw_string_of_term f);
+ term_lg (args@tms) (lg',seen')
+ end
| term_lg _ (lg,seen) = (lg,seen)
exception PRED_LG of term;
fun pred_lg (t as Const(P,tp)) (lg,seen)=
- if is_hol_pred tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen)
+ if is_hol_pred tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen)
| pred_lg (t as Free(P,tp)) (lg,seen) =
- if is_hol_pred tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen)
+ if is_hol_pred tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen)
| pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, t ins seen)
| pred_lg P _ = raise PRED_LG(P);
fun lit_lg (Const("Not",_) $ P) (lg,seen) = lit_lg P (lg,seen)
| lit_lg P (lg,seen) =
- let val (pred,args) = strip_comb P
- val (lg',seen') = if pred mem seen then (lg,seen)
- else pred_lg pred (lg,seen)
- val _ =
- if is_fol_logic lg' then ()
- else Output.debug ("Found a HOL predicate: " ^ Display.raw_string_of_term pred)
- in
+ let val (pred,args) = strip_comb P
+ val (lg',seen') = if pred mem seen then (lg,seen)
+ else pred_lg pred (lg,seen)
+ in
+ if is_fol_logic lg' then ()
+ else Output.debug ("Found a HOL predicate: " ^ Display.raw_string_of_term pred);
term_lg args (lg',seen')
- end;
+ end;
fun lits_lg [] (lg,seen) = (lg,seen)
| lits_lg (lit::lits) (FOL,seen) =
- let val (lg,seen') = lit_lg lit (FOL,seen)
- val _ =
- if is_fol_logic lg then ()
- else Output.debug ("Found a HOL literal: " ^ Display.raw_string_of_term lit)
- in
+ let val (lg,seen') = lit_lg lit (FOL,seen)
+ in
+ if is_fol_logic lg then ()
+ else Output.debug ("Found a HOL literal: " ^ Display.raw_string_of_term lit);
lits_lg lits (lg,seen')
- end
+ end
| lits_lg lits (lg,seen) = (lg,seen);
-
fun dest_disj_aux (Const ("op |", _) $ t $ t') disjs =
dest_disj_aux t (dest_disj_aux t' disjs)
| dest_disj_aux t disjs = t::disjs;
@@ -314,11 +309,10 @@
"Datatype.unit.inducts",
"Datatype.unit.split",
"Datatype.unit.splits",
- "Product_Type.unit_abs_eta_conv",
- "Product_Type.unit_induct",
+ "Datatype.prod.size",
- "Datatype.prod.size",
"Divides.dvd_0_left_iff",
+
"Finite_Set.card_0_eq",
"Finite_Set.card_infinite",
"Finite_Set.Max_ge",
@@ -335,15 +329,22 @@
"Finite_Set.min_max.below_inf_sup_Inf_Sup.sup_Inf_absorb",
"Finite_Set.min.f_below_strict_below.below_f_conv", (*duplicates in Orderings.*)
"Finite_Set.min.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*)
+
+ "HOL.split_if", (*splitting theorem*)
+ "HOL.split_if_asm", (*splitting theorem*)
+
"IntDef.Integ.Abs_Integ_inject",
"IntDef.Integ.Abs_Integ_inverse",
+ "IntDef.abs_split",
"IntDiv.zdvd_0_left",
+
"List.append_eq_append_conv",
"List.hd_Cons_tl", (*Says everything is [] or Cons. Probably prolific.*)
"List.in_listsD",
"List.in_listsI",
"List.lists.Cons",
"List.listsE",
+
"Nat.less_one", (*not directional? obscure*)
"Nat.not_gr0",
"Nat.one_eq_mult_iff", (*duplicate by symmetry*)
@@ -368,6 +369,7 @@
"NatSimprocs.mult_less_cancel_right_number_of", (*excessive case analysis*)
"NatSimprocs.zero_le_divide_iff_number_of", (*excessive case analysis*)
"NatSimprocs.zero_less_divide_iff_number_of",
+
"OrderedGroup.abs_0_eq", (*duplicate by symmetry*)
"OrderedGroup.diff_eq_0_iff_eq", (*prolific?*)
"OrderedGroup.join_0_eq_0",
@@ -375,6 +377,9 @@
"OrderedGroup.pprt_eq_0", (*obscure*)
"OrderedGroup.pprt_eq_id", (*obscure*)
"OrderedGroup.pprt_mono", (*obscure*)
+ "Orderings.split_min", (*splitting theorem*)
+ "Orderings.split_max", (*splitting theorem*)
+
"Parity.even_nat_power", (*obscure, somewhat prolilfic*)
"Parity.power_eq_0_iff_number_of",
"Parity.power_le_zero_eq_number_of", (*obscure and prolific*)
@@ -382,6 +387,14 @@
"Parity.zero_le_power_eq_number_of", (*obscure and prolific*)
"Parity.zero_less_power_eq_number_of", (*obscure and prolific*)
"Power.zero_less_power_abs_iff",
+ "Product_Type.unit_abs_eta_conv",
+ "Product_Type.unit_induct",
+
+ "Product_Type.split_paired_Ball_Sigma", (*splitting theorem*)
+ "Product_Type.split_paired_Bex_Sigma", (*splitting theorem*)
+ "Product_Type.split_split", (*splitting theorem*)
+ "Product_Type.split_split_asm", (*splitting theorem*)
+
"Relation.diagI",
"Relation.ImageI",
"Ring_and_Field.divide_cancel_left", (*fields are seldom used & often prolific*)
@@ -446,18 +459,8 @@
(*** retrieve lemmas from clasimpset and atpset, may filter them ***)
-(*The "name" of a theorem is its statement, if nothing else is available.*)
-val plain_string_of_thm =
- setmp show_question_marks false
- (setmp print_mode []
- (Pretty.setmp_margin 999 string_of_thm));
-
-(*Returns the first substring enclosed in quotation marks, typically omitting
- the [.] of meta-level assumptions.*)
-val firstquoted = hd o (String.tokens (fn c => c = #"\""))
-
fun fake_thm_name th =
- Context.theory_name (theory_of_thm th) ^ "." ^ firstquoted (plain_string_of_thm th);
+ Context.theory_name (theory_of_thm th) ^ "." ^ gensym"";
fun put_name_pair ("",th) = (fake_thm_name th, th)
| put_name_pair (a,th) = (a,th);
@@ -484,11 +487,14 @@
else [s]
| [] => [s];
+fun banned_thmlist s =
+ (Sign.base_name s) mem_string ["induct","inducts","split","splits","split_asm"];
+
fun make_banned_test xs =
let val ht = Polyhash.mkTable (Polyhash.hash_string, op =)
(6000, HASH_STRING)
- fun banned s = exists (fn s' => isSome (Polyhash.peek ht s'))
- (delete_numeric_suffix s)
+ fun banned_aux s = isSome (Polyhash.peek ht s) orelse banned_thmlist s
+ fun banned s = exists banned_aux (delete_numeric_suffix s)
in app (fn x => Polyhash.insert ht (x,())) (!blacklist);
app (insert_suffixed_names ht) (!blacklist @ xs);
banned
@@ -519,28 +525,41 @@
| get_literals lit lits = (lit::lits);
-fun hash_term term = Word.toIntX (xor_words (map hash_literal (get_literals term [])));
-
-fun hash_thm thm = hash_term (prop_of thm);
+fun hash_term t = Word.toIntX (xor_words (map hash_literal (get_literals t [])));
fun equal_thm (thm1,thm2) = Term.aconv(prop_of thm1, prop_of thm2);
+
(*Create a hash table for clauses, of the given size*)
fun mk_clause_table n =
- Polyhash.mkTable (hash_thm, equal_thm)
+ Polyhash.mkTable (hash_term o prop_of, equal_thm)
(n, HASH_CLAUSE);
-(*Use a hash table to eliminate duplicates from xs*)
-fun make_unique ht xs =
- (app (ignore o Polyhash.peekInsert ht) xs; Polyhash.listItems ht);
+(*Use a hash table to eliminate duplicates from xs. Argument is a list of
+ (name, theorem) pairs, but the theorems are hashed into the table. *)
+fun make_unique xs =
+ let val ht = mk_clause_table 2200
+ in
+ (app (ignore o Polyhash.peekInsert ht) (map swap xs);
+ map swap (Polyhash.listItems ht))
+ end;
+(*FIXME: SLOW!!!*)
fun mem_thm th [] = false
| mem_thm th ((th',_)::thms_names) = equal_thm (th,th') orelse mem_thm th thms_names;
+(*FIXME: SLOW!!! These two functions are called only by get_relevant_clauses.
+ It would be faster to compare names, rather than theorems, and to use
+ a symbol table or hash table.*)
fun insert_thms [] thms_names = thms_names
| insert_thms ((thm,name)::thms_names) thms_names' =
if mem_thm thm thms_names' then insert_thms thms_names thms_names'
else insert_thms thms_names ((thm,name)::thms_names');
+(* filter axiom clauses, but keep supplied clauses and clauses in whitelist *)
+fun get_relevant_clauses thy cls_thms white_cls goals =
+ insert_thms white_cls (ReduceAxiomsN.relevance_filter thy cls_thms goals);
+
+
fun display_thms [] = ()
| display_thms ((name,thm)::nthms) =
let val nthm = name ^ ": " ^ (string_of_thm thm)
@@ -555,8 +574,8 @@
fun get_clasimp_atp_lemmas ctxt user_thms =
let val included_thms =
if !include_all
- then (tap (fn ths => Output.debug ("Including all " ^ Int.toString (length ths) ^
- " theorems"))
+ then (tap (fn ths => Output.debug
+ ("Including all " ^ Int.toString (length ths) ^ " theorems"))
(all_facts_of ctxt @ PureThy.all_thms_of (ProofContext.theory_of ctxt)))
else
let val claset_thms =
@@ -578,7 +597,7 @@
(map put_name_pair included_thms, user_rules)
end;
-(* remove lemmas that are banned from the backlist *)
+(*Remove lemmas that are banned from the backlist. Also remove duplicates. *)
fun blacklist_filter thms =
if !run_blacklist_filter then
let val banned = make_banned_test (map #1 thms)
@@ -586,22 +605,10 @@
in filter ok thms end
else thms;
-(* filter axiom clauses, but keep supplied clauses and clauses in whitelist *)
-fun get_relevant_clauses ctxt cls_thms white_cls goals =
- let val cls_thms_list = make_unique (mk_clause_table 2200) (List.concat (white_cls@cls_thms))
- val relevant_cls_thms_list =
- if !run_relevance_filter
- then ReduceAxiomsN.relevance_filter (ProofContext.theory_of ctxt) cls_thms_list goals
- else cls_thms_list
- in
- insert_thms (List.concat white_cls) relevant_cls_thms_list
- end;
-
(***************************************************************)
(* ATP invocation methods setup *)
(***************************************************************)
-
(**** prover-specific format: TPTP ****)
@@ -634,12 +641,12 @@
val goal_cls = conj_cls@hyp_cls
val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
val user_lemmas_names = map #1 user_rules
- val rm_black_cls = blacklist_filter included_thms
- val cla_simp_atp_clauses = ResAxioms.cnf_rules_pairs rm_black_cls
+ val cla_simp_atp_clauses = included_thms |> blacklist_filter
+ |> make_unique |> ResAxioms.cnf_rules_pairs
val user_cls = ResAxioms.cnf_rules_pairs user_rules
- val axclauses = get_relevant_clauses ctxt cla_simp_atp_clauses
+ val thy = ProofContext.theory_of ctxt
+ val axclauses = get_relevant_clauses thy cla_simp_atp_clauses
user_cls (map prop_of goal_cls)
- val thy = ProofContext.theory_of ctxt
val prob_logic = case mode of
Auto => problem_logic_goals [map prop_of goal_cls]
| Fol => FOL
@@ -730,6 +737,13 @@
let val path = File.tmp_path (Path.basic fname)
in Array.app (File.append path o (fn s => s ^ "\n")) end;
+(*Converting a subgoal into negated conjecture clauses*)
+fun neg_clauses th n =
+ let val tacs = [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac]
+ val st = Seq.hd (EVERY' tacs n th)
+ val negs = Option.valOf (metahyps_thms n st)
+ in make_clauses negs |> ResAxioms.assume_abstract_list |> Meson.finish_cnf end;
+
(*We write out problem files for each subgoal. Argument probfile generates filenames,
and allows the suppression of the suffix "_1" in problem-generation mode.
FIXME: does not cope with &&, and it isn't easy because one could have multiple
@@ -738,38 +752,39 @@
let val goals = Thm.prems_of th
val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals))
val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt []
- val rm_blacklist_cls = blacklist_filter included_thms
- val cla_simp_atp_clauses = ResAxioms.cnf_rules_pairs rm_blacklist_cls
- val axclauses = get_relevant_clauses ctxt cla_simp_atp_clauses (ResAxioms.cnf_rules_pairs white_thms) goals
- val _ = Output.debug ("total clauses from thms = " ^ Int.toString (length axclauses))
+ val cla_simp_atp_clauses = included_thms |> blacklist_filter
+ |> make_unique |> ResAxioms.cnf_rules_pairs
+ val white_cls = ResAxioms.cnf_rules_pairs white_thms
+ val _ = Output.debug ("clauses = " ^ Int.toString(length cla_simp_atp_clauses))
val thy = ProofContext.theory_of ctxt
- fun get_neg_subgoals n =
- if n=0 then []
- else
- let val st = Seq.hd (EVERY' [rtac ccontr, ObjectLogic.atomize_tac,
- skolemize_tac] n th)
- val negs = Option.valOf (metahyps_thms n st)
- val negs_clauses = make_clauses negs |> ResAxioms.assume_abstract_list
- |> Meson.finish_cnf
+ fun get_neg_subgoals [] _ = []
+ | get_neg_subgoals (gl::gls) n =
+ let val axclauses = get_relevant_clauses thy cla_simp_atp_clauses
+ white_cls [gl] (*relevant to goal*)
in
- negs_clauses :: get_neg_subgoals (n-1)
+ (neg_clauses th n, axclauses) :: get_neg_subgoals gls (n+1)
end
- val neg_subgoals = get_neg_subgoals (length goals)
- val goals_logic = case !linkup_logic_mode of
- Auto => problem_logic_goals (map (map prop_of) neg_subgoals)
- | Fol => FOL
- | Hol => HOL
- val keep_types = if is_fol_logic goals_logic then !ResClause.keep_types else is_typed_hol ()
- val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else []
- val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))
- val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else []
+ val goal_pairs = get_neg_subgoals goals 1
+ val logic = case !linkup_logic_mode of
+ Auto => problem_logic_goals (map ((map prop_of) o #1) goal_pairs)
+ | Fol => FOL
+ | Hol => HOL
+ val keep_types = if is_fol_logic logic then !ResClause.keep_types
+ else is_typed_hol ()
+ val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy
+ else []
+ val _ = Output.debug ("classrel clauses = " ^
+ Int.toString (length classrel_clauses))
+ val arity_clauses = if keep_types then ResClause.arity_clause_thy thy
+ else []
val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
val writer = if !prover = "spass" then dfg_writer else tptp_writer
fun write_all [] _ = []
- | write_all (sub::subgoals) k =
- (writer goals_logic sub (probfile k) (axclauses,classrel_clauses,arity_clauses) [],
- probfile k) :: write_all subgoals (k-1)
- val (clnames::_, filenames) = ListPair.unzip (write_all neg_subgoals (length goals))
+ | write_all ((ccls,axcls)::subgoals) k =
+ (writer logic ccls (probfile k) (axcls,classrel_clauses,arity_clauses) [],
+ probfile k)
+ :: write_all subgoals (k+1)
+ val (clnames::_, filenames) = ListPair.unzip (write_all goal_pairs 1)
val thm_names = Array.fromList clnames
val _ = if !Output.show_debug_msgs
then trace_array "thm_names" thm_names else ()
--- a/src/HOL/Tools/res_axioms.ML Fri Sep 01 08:36:55 2006 +0200
+++ b/src/HOL/Tools/res_axioms.ML Fri Sep 01 08:51:53 2006 +0200
@@ -229,15 +229,13 @@
fun crhs_of th =
case Drule.strip_comb (cprop_of th) of
(f, [_, rhs]) =>
- (case term_of f of
- Const ("==", _) => rhs
+ (case term_of f of Const ("==", _) => rhs
| _ => raise THM ("crhs_of", 0, [th]))
| _ => raise THM ("crhs_of", 1, [th]);
fun rhs_of th =
- case #prop (rep_thm th) of
- (Const("==",_) $ _ $ rhs) => rhs
- | _ => raise THM ("rhs_of", 1, [th]);
+ case prop_of th of (Const("==",_) $ _ $ rhs) => rhs
+ | _ => raise THM ("rhs_of", 1, [th]);
(*Apply a function definition to an argument, beta-reducing the result.*)
fun beta_comb cf x =
@@ -265,9 +263,7 @@
fun lambda_free (Abs _) = false
| lambda_free (t $ u) = lambda_free t andalso lambda_free u
| lambda_free _ = true;
-
-fun lambda_free_thm th = lambda_free (#prop (rep_thm th));
-
+
(*Traverse a theorem, declaring abstraction function definitions. String s is the suggested
prefix for the constants. Resulting theory is returned in the first theorem. *)
fun declare_absfuns th =
@@ -424,10 +420,12 @@
fun skolem_of_nnf th =
map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns th);
+fun assert_lambda_free ths = assert (forall (lambda_free o prop_of) ths);
+
fun assume_abstract th =
- if lambda_free_thm th then [th]
+ if lambda_free (prop_of th) then [th]
else th |> eta_conversion_rule |> assume_absfuns
- |> tap (fn ths => assert ((forall lambda_free_thm) ths) "assume_abstract: lambdas")
+ |> tap (fn ths => assert_lambda_free ths "assume_abstract: lambdas")
(*Replace lambdas by assumed function definitions in the theorems*)
fun assume_abstract_list ths =
@@ -438,11 +436,11 @@
fun declare_abstract' (thy, []) = (thy, [])
| declare_abstract' (thy, th::ths) =
let val (thy', th_defs) =
- if lambda_free_thm th then (thy, [th])
+ if lambda_free (prop_of th) then (thy, [th])
else
th |> zero_var_indexes |> Drule.freeze_thaw |> #1
|> eta_conversion_rule |> transfer thy |> declare_absfuns
- val _ = assert ((forall lambda_free_thm) th_defs) "declare_abstract: lambdas"
+ val _ = assert_lambda_free th_defs "declare_abstract: lambdas"
val (thy'', ths') = declare_abstract' (thy', ths)
in (thy'', th_defs @ ths') end;
@@ -494,9 +492,6 @@
Output.debug (string_of_thm th');
([th],thy));
-fun skolem_cache ((name,th), thy) = #2 (skolem_cache_thm ((name,th), thy));
-
-
(*Exported function to convert Isabelle theorems into axiom clauses*)
fun cnf_axiom (name,th) =
case name of
@@ -565,7 +560,7 @@
fun cnf_rules_pairs_aux pairs [] = pairs
| cnf_rules_pairs_aux pairs ((name,th)::ths) =
- let val pairs' = (pair_name_cls 0 (name, cnf_axiom(name,th))) :: pairs
+ let val pairs' = (pair_name_cls 0 (name, cnf_axiom(name,th))) @ pairs
handle THM _ => pairs | ResClause.CLAUSE _ => pairs
| ResHolClause.LAM2COMB _ => pairs
in cnf_rules_pairs_aux pairs' ths end;
@@ -576,6 +571,15 @@
(**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****)
(*Setup function: takes a theory and installs ALL known theorems into the clause cache*)
+
+fun skolem_cache ((name,th), thy) =
+ let val prop = prop_of th
+ in
+ if lambda_free prop orelse null (term_tvars prop)
+ then thy (*monomorphic theorems can be Skolemized on demand*)
+ else #2 (skolem_cache_thm ((name,th), thy))
+ end;
+
fun clause_cache_setup thy = List.foldl skolem_cache thy (PureThy.all_thms_of thy);
@@ -598,8 +602,8 @@
fun conj2_rule (th1,th2) = conjI OF [th1,th2];
-(*Conjoin a list of theorems to recreate a single theorem*)
-fun conj_rule [] = raise THM ("conj_rule", 0, [])
+(*Conjoin a list of theorems to form a single theorem*)
+fun conj_rule [] = TrueI
| conj_rule ths = foldr1 conj2_rule ths;
fun skolem_attr (Context.Theory thy, th) =