--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Sat Jun 05 16:39:23 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Sat Jun 05 21:30:40 2010 +0200
@@ -376,7 +376,7 @@
val name1 = Facts.extern facts name;
val name2 = Name_Space.extern full_space name;
- val ths = filter_out is_bad_for_atp ths0;
+ val ths = filter_out is_theorem_bad_for_atps ths0;
in
if Facts.is_concealed facts name orelse
(respect_no_atp andalso is_package_def name) then
@@ -483,20 +483,22 @@
when X does not occur properly in the other operand. This rules out clearly
inconsistent clauses such as V=a|V=b, though it by no means guarantees soundness. **)
-fun occurs ix =
- let fun occ(Var (jx,_)) = (ix=jx)
- | occ(t1$t2) = occ t1 orelse occ t2
- | occ(Abs(_,_,t)) = occ t
- | occ _ = false
- in occ end;
+fun var_occurs_in_term ix =
+ let
+ fun aux (Var (jx, _)) = (ix = jx)
+ | aux (t1 $ t2) = aux t1 orelse aux t2
+ | aux (Abs (_, _, t)) = aux t
+ | aux _ = false
+ in aux end
-fun is_recordtype T = not (null (Record.dest_recTs T));
+fun is_record_type T = not (null (Record.dest_recTs T))
(*Unwanted equalities include
(1) those between a variable that does not properly occur in the second operand,
(2) those between a variable and a record, since these seem to be prolific "cases" thms
*)
-fun too_general_eqterms (Var (ix,T), t) = not (occurs ix t) orelse is_recordtype T
+fun too_general_eqterms (Var (ix,T), t) =
+ not (var_occurs_in_term ix t) orelse is_record_type T
| too_general_eqterms _ = false;
fun too_general_equality (Const (@{const_name "op ="}, _) $ x $ y) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Sat Jun 05 16:39:23 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Sat Jun 05 21:30:40 2010 +0200
@@ -14,11 +14,12 @@
val skolem_infix: string
val cnf_axiom: theory -> thm -> thm list
val multi_base_blacklist: string list
- val is_bad_for_atp: thm -> bool
+ val is_theorem_bad_for_atps: thm -> bool
val type_has_topsort: typ -> bool
- val cnf_rules_pairs: theory -> (string * thm) list -> (thm * (string * int)) list
- val suppress_endtheory: bool Unsynchronized.ref
- (*for emergency use where endtheory causes problems*)
+ val cnf_rules_pairs:
+ theory -> (string * thm) list -> (thm * (string * int)) list
+ val use_skolem_cache: bool Unsynchronized.ref
+ (* for emergency use where the Skolem cache causes problems *)
val strip_subgoal : thm -> int -> (string * typ) list * term list * term
val neg_clausify: thm -> thm list
val neg_conjecture_clauses:
@@ -86,9 +87,9 @@
val rhs_consts = fold_aterms (fn Const c => insert (op =) c | _ => I) rhs []
in fold (#2 #> Term.fold_atyps add_new_TFrees) rhs_consts [] end;
-(*Traverse a theorem, declaring Skolem function definitions. String s is the suggested
- prefix for the Skolem constant.*)
-fun declare_skofuns s th =
+(* Traverse a theorem, declaring Skolem function definitions. String "s" is the
+ suggested prefix for the Skolem constants. *)
+fun declare_skolem_funs s th =
let
val nref = Unsynchronized.ref 0 (* FIXME ??? *)
fun dec_sko (Const (@{const_name Ex}, _) $ (xtp as Abs (s', T, p))) (axs, thy) =
@@ -121,7 +122,7 @@
in fn thy => dec_sko (Thm.prop_of th) ([], thy) end;
(*Traverse a theorem, accumulating Skolem function definitions.*)
-fun assume_skofuns s th =
+fun assume_skolem_funs s th =
let val sko_count = Unsynchronized.ref 0 (* FIXME ??? *)
fun dec_sko (Const (@{const_name Ex}, _) $ (xtp as Abs (s', T, p))) defs =
(*Existential: declare a Skolem function, then insert into body and continue*)
@@ -302,37 +303,43 @@
(*Generate Skolem functions for a theorem supplied in nnf*)
fun assume_skolem_of_def s th =
- map (skolem_of_def o Thm.assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th);
+ map (skolem_of_def o Thm.assume o (cterm_of (theory_of_thm th)))
+ (assume_skolem_funs s th)
(*** Blacklisting (FIXME: duplicated in "Sledgehammer_Fact_Filter"?) ***)
-val max_lambda_nesting = 3;
+val max_lambda_nesting = 3
-fun excessive_lambdas (f$t, k) = excessive_lambdas (f,k) orelse excessive_lambdas (t,k)
- | excessive_lambdas (Abs(_,_,t), k) = k=0 orelse excessive_lambdas (t,k-1)
- | excessive_lambdas _ = false;
+fun term_has_too_many_lambdas max (t1 $ t2) =
+ exists (term_has_too_many_lambdas max) [t1, t2]
+ | term_has_too_many_lambdas max (Abs (_, _, t)) =
+ max = 0 orelse term_has_too_many_lambdas (max - 1) t
+ | term_has_too_many_lambdas _ _ = false
-fun is_formula_type T = (T = HOLogic.boolT orelse T = propT);
+fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
-(*Don't count nested lambdas at the level of formulas, as they are quantifiers*)
-fun excessive_lambdas_fm Ts (Abs(_,T,t)) = excessive_lambdas_fm (T::Ts) t
- | excessive_lambdas_fm Ts t =
- if is_formula_type (fastype_of1 (Ts, t))
- then exists (excessive_lambdas_fm Ts) (#2 (strip_comb t))
- else excessive_lambdas (t, max_lambda_nesting);
+(* Don't count nested lambdas at the level of formulas, since they are
+ quantifiers. *)
+fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) =
+ formula_has_too_many_lambdas (T :: Ts) t
+ | formula_has_too_many_lambdas Ts t =
+ if is_formula_type (fastype_of1 (Ts, t)) then
+ exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t))
+ else
+ term_has_too_many_lambdas max_lambda_nesting t
-(*The max apply_depth of any metis call in Metis_Examples (on 31-10-2007) was 11.*)
-val max_apply_depth = 15;
+(* The max apply depth of any "metis" call in "Metis_Examples" (on 31-10-2007)
+ was 11. *)
+val max_apply_depth = 15
-fun apply_depth (f$t) = Int.max (apply_depth f, apply_depth t + 1)
- | apply_depth (Abs(_,_,t)) = apply_depth t
- | apply_depth _ = 0;
+fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1)
+ | apply_depth (Abs (_, _, t)) = apply_depth t
+ | apply_depth _ = 0
-fun too_complex t =
- apply_depth t > max_apply_depth orelse
- Meson.too_many_clauses NONE t orelse
- excessive_lambdas_fm [] t;
+fun is_formula_too_complex t =
+ apply_depth t > max_apply_depth orelse Meson.too_many_clauses NONE t orelse
+ formula_has_too_many_lambdas [] t
fun is_strange_thm th =
case head_of (concl_of th) of
@@ -340,9 +347,11 @@
a <> @{const_name "=="})
| _ => false;
-fun is_bad_for_atp th =
- too_complex (prop_of th) orelse
- exists_type type_has_topsort (prop_of th) orelse is_strange_thm th
+fun is_theorem_bad_for_atps thm =
+ let val t = prop_of thm in
+ is_formula_too_complex t orelse exists_type type_has_topsort t orelse
+ is_strange_thm thm
+ end
(* FIXME: put other record thms here, or declare as "no_atp" *)
val multi_base_blacklist =
@@ -356,7 +365,7 @@
(*Skolemize a named theorem, with Skolem functions as additional premises.*)
fun skolem_thm (s, th) =
if member (op =) multi_base_blacklist (Long_Name.base_name s) orelse
- is_bad_for_atp th then
+ is_theorem_bad_for_atps th then
[]
else
let
@@ -414,11 +423,11 @@
fun skolem_def (name, th) thy =
let val ctxt0 = Variable.global_thm_context th in
- (case try (to_nnf th) ctxt0 of
+ case try (to_nnf th) ctxt0 of
NONE => (NONE, thy)
| SOME (nnfth, ctxt1) =>
- let val (defs, thy') = declare_skofuns (flatten_name name) nnfth thy
- in (SOME (th, ctxt0, ctxt1, nnfth, defs), thy') end)
+ let val (defs, thy') = declare_skolem_funs (flatten_name name) nnfth thy
+ in (SOME (th, ctxt0, ctxt1, nnfth, defs), thy') end
end;
fun skolem_cnfs (th, ctxt0, ctxt1, nnfth, defs) =
@@ -442,8 +451,10 @@
val new_thms = (new_facts, []) |-> fold (fn (name, ths) =>
if member (op =) multi_base_blacklist (Long_Name.base_name name) then I
else fold_index (fn (i, th) =>
- if is_bad_for_atp th orelse is_some (lookup_cache thy th) then I
- else cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths);
+ if is_theorem_bad_for_atps th orelse is_some (lookup_cache thy th) then
+ I
+ else
+ cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths)
in
if null new_facts then NONE
else
@@ -458,11 +469,10 @@
end;
-val suppress_endtheory = Unsynchronized.ref false
+val use_skolem_cache = Unsynchronized.ref true
fun clause_cache_endtheory thy =
- if ! suppress_endtheory then NONE
- else saturate_skolem_cache thy;
+ if !use_skolem_cache then saturate_skolem_cache thy else NONE
(*The cache can be kept smaller by inspecting the prop of each thm. Can ignore all that are
@@ -510,7 +520,7 @@
(** setup **)
val setup =
- perhaps saturate_skolem_cache #>
- Theory.at_end clause_cache_endtheory;
+ perhaps saturate_skolem_cache
+ #> Theory.at_end clause_cache_endtheory
end;