author blanchet Thu, 16 Dec 2010 15:12:17 +0100 changeset 41200 6cc9b6fd7f6f parent 41199 4698d12dd860 child 41201 208bd47b6f29
add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
```--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Dec 16 15:12:17 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Dec 16 15:12:17 2010 +0100
@@ -155,7 +155,7 @@

(** Structural induction rules **)

-fun induct_rule_on th =
+fun struct_induct_rule_on th =
case Logic.strip_horn (prop_of th) of
(prems, @{const Trueprop}
\$ ((p as Var ((p_name, 0), _)) \$ (a as Var (_, ind_T)))) =>
@@ -187,7 +187,7 @@
handle Type.TYPE_MATCH => false

fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, (_, th))) =
-  case induct_rule_on th of
+  case struct_induct_rule_on th of
SOME (p_name, ind_T) =>
let val thy = ProofContext.theory_of ctxt in
stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T))
@@ -335,17 +335,16 @@

(*Inserts a dummy "constant" referring to the theory name, so that relevance
takes the given theory into account.*)
-fun theory_const_prop_of ({theory_const_rel_weight,
-                           theory_const_irrel_weight, ...} : relevance_fudge)
-                         th =
+fun theory_constify ({theory_const_rel_weight, theory_const_irrel_weight, ...}
+                     : relevance_fudge) thy_name t =
if exists (curry (op <) 0.0) [theory_const_rel_weight,
theory_const_irrel_weight] then
-    let
-      val name = Context.theory_name (theory_of_thm th)
-      val t = Const (name ^ theory_const_suffix, @{typ bool})
-    in t \$ prop_of th end
+    Const (thy_name ^ theory_const_suffix, @{typ bool}) \$ t
else
-    prop_of th
+    t
+
+fun theory_const_prop_of fudge th =
+  theory_constify fudge (Context.theory_name (theory_of_thm th)) (prop_of th)

(**** Constant / Type Frequencies ****)

@@ -875,6 +874,7 @@
max_relevant is_built_in_const fudge
(override as {add, only, ...}) chained_ths hyp_ts concl_t =
let
+    val thy = ProofContext.theory_of ctxt
val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
1.0 / Real.fromInt (max_relevant + 1))