fixed detection of tautologies -- things like "a = b" in a structured proof, where a and b are Frees, shouldn't be discarted as tautologies
authorblanchet
Mon Nov 12 14:46:42 2012 +0100 (2012-11-12 ago)
changeset 50053fea589c8583e
parent 50052 c8d141cce517
child 50054 6da283e4497b
fixed detection of tautologies -- things like "a = b" in a structured proof, where a and b are Frees, shouldn't be discarted as tautologies
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Nov 12 14:11:51 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Nov 12 14:46:42 2012 +0100
     1.3 @@ -207,9 +207,12 @@
     1.4  
     1.5  fun is_likely_tautology_or_too_meta th =
     1.6    let
     1.7 -    val is_boring_const = member (op =) atp_widely_irrelevant_consts
     1.8 +    fun is_interesting_subterm (Const (s, _)) =
     1.9 +        not (member (op =) atp_widely_irrelevant_consts s)
    1.10 +      | is_interesting_subterm (Free _) = true
    1.11 +      | is_interesting_subterm _ = false
    1.12      fun is_boring_bool t =
    1.13 -      not (exists_Const (not o is_boring_const o fst) t) orelse
    1.14 +      not (exists_subterm is_interesting_subterm t) orelse
    1.15        exists_type (exists_subtype (curry (op =) @{typ prop})) t
    1.16      fun is_boring_prop (@{const Trueprop} $ t) = is_boring_bool t
    1.17        | is_boring_prop (@{const "==>"} $ t $ u) =
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Mon Nov 12 14:11:51 2012 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Mon Nov 12 14:46:42 2012 +0100
     2.3 @@ -536,8 +536,7 @@
     2.4    end
     2.5  
     2.6  (* Ad hoc score function roughly based on Blanchette's Ringberg 2011 data. *)
     2.7 -fun weight_of_fact rank =
     2.8 -  Math.pow (1.5, 15.5 - 0.05 * Real.fromInt rank) + 15.0
     2.9 +fun weight_of_fact rank = Math.pow (1.5, 15.5 - 0.05 * Real.fromInt rank) + 15.0
    2.10  
    2.11  fun weight_mepo_facts facts =
    2.12    facts ~~ map weight_of_fact (0 upto length facts - 1)