1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex Wed Aug 25 09:05:22 2010 +0200
1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex Wed Aug 25 09:32:43 2010 +0200
1.3 @@ -469,10 +469,10 @@
1.4 it is taken to be \textit{true} for SPASS and \textit{false} for E and Vampire,
1.5 because empirical results suggest that these are the best settings.
1.6
1.7 -\opfalse{defs\_relevant}{defs\_irrelevant}
1.8 -Specifies whether the definition of constants occurring in the formula to prove
1.9 -should be considered particularly relevant. Enabling this option tends to lead
1.10 -to larger problems and typically slows down the ATPs.
1.11 +%\opfalse{defs\_relevant}{defs\_irrelevant}
1.12 +%Specifies whether the definition of constants occurring in the formula to prove
1.13 +%should be considered particularly relevant. Enabling this option tends to lead
1.14 +%to larger problems and typically slows down the ATPs.
1.15
1.16 \end{enum}
1.17
2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Aug 25 09:05:22 2010 +0200
2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Aug 25 09:32:43 2010 +0200
2.3 @@ -22,7 +22,6 @@
2.4 relevance_decay: real,
2.5 max_relevant_per_iter: int option,
2.6 theory_relevant: bool option,
2.7 - defs_relevant: bool,
2.8 isar_proof: bool,
2.9 isar_shrink_factor: int,
2.10 timeout: Time.time}
2.11 @@ -91,7 +90,6 @@
2.12 relevance_decay: real,
2.13 max_relevant_per_iter: int option,
2.14 theory_relevant: bool option,
2.15 - defs_relevant: bool,
2.16 isar_proof: bool,
2.17 isar_shrink_factor: int,
2.18 timeout: Time.time}
2.19 @@ -216,8 +214,8 @@
2.20 explicit_forall, use_conjecture_for_hypotheses}
2.21 ({debug, verbose, overlord, full_types, explicit_apply,
2.22 relevance_threshold, relevance_decay,
2.23 - max_relevant_per_iter, theory_relevant,
2.24 - defs_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params)
2.25 + max_relevant_per_iter, theory_relevant, isar_proof,
2.26 + isar_shrink_factor, timeout, ...} : params)
2.27 minimize_command
2.28 ({subgoal, goal, relevance_override, axioms} : problem) =
2.29 let
2.30 @@ -234,7 +232,6 @@
2.31 SOME axioms => axioms
2.32 | NONE =>
2.33 (relevant_facts full_types relevance_threshold relevance_decay
2.34 - defs_relevant
2.35 (the_default default_max_relevant_per_iter
2.36 max_relevant_per_iter)
2.37 (the_default default_theory_relevant theory_relevant)
3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Aug 25 09:05:22 2010 +0200
3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Aug 25 09:32:43 2010 +0200
3.3 @@ -15,7 +15,7 @@
3.4 Proof.context -> unit Symtab.table -> thm list -> Facts.ref
3.5 -> (unit -> string * bool) * thm list
3.6 val relevant_facts :
3.7 - bool -> real -> real -> bool -> int -> bool -> relevance_override
3.8 + bool -> real -> real -> int -> bool -> relevance_override
3.9 -> Proof.context * (thm list * 'a) -> term list -> term
3.10 -> ((string * bool) * thm) list
3.11 end;
3.12 @@ -244,9 +244,9 @@
3.13 in if Real.isFinite res then res else 0.0 end
3.14 *)
3.15
3.16 -(*Multiplies out to a list of pairs: 'a * 'b list -> ('a * 'b) list -> ('a * 'b) list*)
3.17 +(* Multiplies out to a list of pairs: 'a * 'b list -> ('a * 'b) list
3.18 + -> ('a * 'b) list. *)
3.19 fun add_expand_pairs (x, ys) xys = List.foldl (fn (y,acc) => (x,y)::acc) xys ys
3.20 -
3.21 fun consts_of_term thy t =
3.22 Symtab.fold add_expand_pairs (get_consts thy (SOME true) [t]) []
3.23
3.24 @@ -254,30 +254,6 @@
3.25 (axiom, axiom |> snd |> theory_const_prop_of theory_relevant
3.26 |> consts_of_term thy)
3.27
3.28 -exception CONST_OR_FREE of unit
3.29 -
3.30 -fun dest_Const_or_Free (Const x) = x
3.31 - | dest_Const_or_Free (Free x) = x
3.32 - | dest_Const_or_Free _ = raise CONST_OR_FREE ()
3.33 -
3.34 -(*Look for definitions of the form f ?x1 ... ?xn = t, but not reversed.*)
3.35 -fun defines thy thm gctypes =
3.36 - let val tm = prop_of thm
3.37 - fun defs lhs rhs =
3.38 - let val (rator,args) = strip_comb lhs
3.39 - val ct = const_with_typ thy (dest_Const_or_Free rator)
3.40 - in
3.41 - forall is_Var args andalso const_mem gctypes ct andalso
3.42 - subset (op =) (Term.add_vars rhs [], Term.add_vars lhs [])
3.43 - end
3.44 - handle CONST_OR_FREE () => false
3.45 - in
3.46 - case tm of
3.47 - @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ lhs $ rhs) =>
3.48 - defs lhs rhs
3.49 - | _ => false
3.50 - end;
3.51 -
3.52 type annotated_thm =
3.53 ((unit -> string * bool) * thm) * (string * const_typ list) list
3.54
3.55 @@ -306,7 +282,7 @@
3.56 val threshold_divisor = 2.0
3.57 val ridiculous_threshold = 0.1
3.58
3.59 -fun relevance_filter ctxt relevance_threshold relevance_decay defs_relevant
3.60 +fun relevance_filter ctxt relevance_threshold relevance_decay
3.61 max_relevant_per_iter theory_relevant
3.62 ({add, del, ...} : relevance_override) axioms goal_ts =
3.63 let
3.64 @@ -366,8 +342,7 @@
3.65 SOME w => w
3.66 | NONE => axiom_weight const_tab rel_const_tab axiom_consts
3.67 in
3.68 - if weight >= threshold orelse
3.69 - (defs_relevant andalso defines thy th rel_const_tab) then
3.70 + if weight >= threshold then
3.71 (trace_msg (fn () =>
3.72 fst (name ()) ^ " passes: " ^ Real.toString weight
3.73 ^ " consts: " ^ commas (map fst axiom_consts));
3.74 @@ -608,7 +583,7 @@
3.75 (* ATP invocation methods setup *)
3.76 (***************************************************************)
3.77
3.78 -fun relevant_facts full_types relevance_threshold relevance_decay defs_relevant
3.79 +fun relevant_facts full_types relevance_threshold relevance_decay
3.80 max_relevant_per_iter theory_relevant
3.81 (relevance_override as {add, del, only})
3.82 (ctxt, (chained_ths, _)) hyp_ts concl_t =
3.83 @@ -631,7 +606,7 @@
3.84 else if relevance_threshold < 0.0 then
3.85 axioms
3.86 else
3.87 - relevance_filter ctxt relevance_threshold relevance_decay defs_relevant
3.88 + relevance_filter ctxt relevance_threshold relevance_decay
3.89 max_relevant_per_iter theory_relevant relevance_override
3.90 axioms (concl_t :: hyp_ts))
3.91 |> map (apfst (fn f => f ()))
4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Wed Aug 25 09:05:22 2010 +0200
4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Wed Aug 25 09:32:43 2010 +0200
4.3 @@ -41,8 +41,8 @@
4.4 end
4.5
4.6 fun test_theorems ({debug, verbose, overlord, atps, full_types,
4.7 - relevance_threshold, relevance_decay, defs_relevant,
4.8 - isar_proof, isar_shrink_factor, ...} : params)
4.9 + relevance_threshold, relevance_decay, isar_proof,
4.10 + isar_shrink_factor, ...} : params)
4.11 (prover : prover) explicit_apply timeout subgoal state
4.12 name_thms_pairs =
4.13 let
4.14 @@ -53,9 +53,8 @@
4.15 full_types = full_types, explicit_apply = explicit_apply,
4.16 relevance_threshold = relevance_threshold,
4.17 relevance_decay = relevance_decay, max_relevant_per_iter = NONE,
4.18 - theory_relevant = NONE, defs_relevant = defs_relevant,
4.19 - isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
4.20 - timeout = timeout}
4.21 + theory_relevant = NONE, isar_proof = isar_proof,
4.22 + isar_shrink_factor = isar_shrink_factor, timeout = timeout}
4.23 val axioms = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
4.24 val {context = ctxt, facts, goal} = Proof.goal state
4.25 val problem =
5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Aug 25 09:05:22 2010 +0200
5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Aug 25 09:32:43 2010 +0200
5.3 @@ -71,7 +71,6 @@
5.4 ("relevance_decay", "31"),
5.5 ("max_relevant_per_iter", "smart"),
5.6 ("theory_relevant", "smart"),
5.7 - ("defs_relevant", "false"),
5.8 ("isar_proof", "false"),
5.9 ("isar_shrink_factor", "1")]
5.10
5.11 @@ -84,7 +83,6 @@
5.12 ("partial_types", "full_types"),
5.13 ("implicit_apply", "explicit_apply"),
5.14 ("theory_irrelevant", "theory_relevant"),
5.15 - ("defs_irrelevant", "defs_relevant"),
5.16 ("no_isar_proof", "isar_proof")]
5.17
5.18 val params_for_minimize =
5.19 @@ -174,7 +172,6 @@
5.20 0.01 * Real.fromInt (lookup_int "relevance_decay")
5.21 val max_relevant_per_iter = lookup_int_option "max_relevant_per_iter"
5.22 val theory_relevant = lookup_bool_option "theory_relevant"
5.23 - val defs_relevant = lookup_bool "defs_relevant"
5.24 val isar_proof = lookup_bool "isar_proof"
5.25 val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
5.26 val timeout = lookup_time "timeout"
5.27 @@ -184,9 +181,8 @@
5.28 relevance_threshold = relevance_threshold,
5.29 relevance_decay = relevance_decay,
5.30 max_relevant_per_iter = max_relevant_per_iter,
5.31 - theory_relevant = theory_relevant, defs_relevant = defs_relevant,
5.32 - isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
5.33 - timeout = timeout}
5.34 + theory_relevant = theory_relevant, isar_proof = isar_proof,
5.35 + isar_shrink_factor = isar_shrink_factor, timeout = timeout}
5.36 end
5.37
5.38 fun get_params thy = extract_params (default_raw_params thy)