author | blanchet |
Thu, 16 Dec 2010 15:12:17 +0100 | |
changeset 41448 | 6cc9b6fd7f6f |
parent 41447 | 4698d12dd860 |
child 41449 | 208bd47b6f29 |
1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Dec 16 15:12:17 2010 +0100 1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Dec 16 15:12:17 2010 +0100 1.3 @@ -155,7 +155,7 @@ 1.4 1.5 (** Structural induction rules **) 1.6 1.7 -fun induct_rule_on th = 1.8 +fun struct_induct_rule_on th = 1.9 case Logic.strip_horn (prop_of th) of 1.10 (prems, @{const Trueprop} 1.11 $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) => 1.12 @@ -187,7 +187,7 @@ 1.13 handle Type.TYPE_MATCH => false 1.14 1.15 fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, (_, th))) = 1.16 - case induct_rule_on th of 1.17 + case struct_induct_rule_on th of 1.18 SOME (p_name, ind_T) => 1.19 let val thy = ProofContext.theory_of ctxt in 1.20 stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T)) 1.21 @@ -335,17 +335,16 @@ 1.22 1.23 (*Inserts a dummy "constant" referring to the theory name, so that relevance 1.24 takes the given theory into account.*) 1.25 -fun theory_const_prop_of ({theory_const_rel_weight, 1.26 - theory_const_irrel_weight, ...} : relevance_fudge) 1.27 - th = 1.28 +fun theory_constify ({theory_const_rel_weight, theory_const_irrel_weight, ...} 1.29 + : relevance_fudge) thy_name t = 1.30 if exists (curry (op <) 0.0) [theory_const_rel_weight, 1.31 theory_const_irrel_weight] then 1.32 - let 1.33 - val name = Context.theory_name (theory_of_thm th) 1.34 - val t = Const (name ^ theory_const_suffix, @{typ bool}) 1.35 - in t $ prop_of th end 1.36 + Const (thy_name ^ theory_const_suffix, @{typ bool}) $ t 1.37 else 1.38 - prop_of th 1.39 + t 1.40 + 1.41 +fun theory_const_prop_of fudge th = 1.42 + theory_constify fudge (Context.theory_name (theory_of_thm th)) (prop_of th) 1.43 1.44 (**** Constant / Type Frequencies ****) 1.45 1.46 @@ -875,6 +874,7 @@ 1.47 max_relevant is_built_in_const fudge 1.48 (override as {add, only, ...}) chained_ths hyp_ts concl_t = 1.49 let 1.50 + val thy = ProofContext.theory_of ctxt 1.51 val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0), 1.52 1.0 / Real.fromInt (max_relevant + 1)) 1.53 val add_ths = Attrib.eval_thms ctxt add 1.54 @@ -901,8 +901,9 @@ 1.55 max_relevant = 0 then 1.56 [] 1.57 else 1.58 - relevance_filter ctxt threshold0 decay max_relevant is_built_in_const 1.59 - fudge override facts (concl_t :: hyp_ts)) 1.60 + ((concl_t |> theory_constify fudge (Context.theory_name thy)) :: hyp_ts) 1.61 + |> relevance_filter ctxt threshold0 decay max_relevant is_built_in_const 1.62 + fudge override facts) 1.63 |> map (apfst (apfst (fn f => f ()))) 1.64 end 1.65