better tautology check -- don't reject "prod_cases3" for example
authorblanchet
Wed Dec 12 15:25:17 2012 +0100 (2012-12-12 ago)
changeset 50495bd9a0028b063
parent 50494 06b199a042ff
child 50496 8665ec681e47
better tautology check -- don't reject "prod_cases3" for example
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Dec 12 13:42:14 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Dec 12 15:25:17 2012 +0100
     1.3 @@ -42,6 +42,7 @@
     1.4  structure Sledgehammer_Fact : SLEDGEHAMMER_FACT =
     1.5  struct
     1.6  
     1.7 +open ATP_Util
     1.8  open ATP_Problem_Generate
     1.9  open Metis_Tactic
    1.10  open Sledgehammer_Util
    1.11 @@ -216,16 +217,19 @@
    1.12      fun is_boring_bool t =
    1.13        not (exists_subterm is_interesting_subterm t) orelse
    1.14        exists_type (exists_subtype (curry (op =) @{typ prop})) t
    1.15 -    fun is_boring_prop (@{const Trueprop} $ t) = is_boring_bool t
    1.16 -      | is_boring_prop (@{const "==>"} $ t $ u) =
    1.17 -        is_boring_prop t andalso is_boring_prop u
    1.18 -      | is_boring_prop (Const (@{const_name all}, _) $ (Abs (_, _, t)) $ u) =
    1.19 -        is_boring_prop t andalso is_boring_prop u
    1.20 -      | is_boring_prop (Const (@{const_name "=="}, _) $ t $ u) =
    1.21 +    fun is_boring_prop _ (@{const Trueprop} $ t) = is_boring_bool t
    1.22 +      | is_boring_prop Ts (@{const "==>"} $ t $ u) =
    1.23 +        is_boring_prop Ts t andalso is_boring_prop Ts u
    1.24 +      | is_boring_prop Ts (Const (@{const_name all}, _) $ (Abs (_, T, t)) $ u) =
    1.25 +        is_boring_prop (T :: Ts) t andalso is_boring_prop (T :: Ts) u
    1.26 +      | is_boring_prop Ts ((t as Const (@{const_name all}, _)) $ u) =
    1.27 +        is_boring_prop Ts (t $ eta_expand Ts u 1)
    1.28 +      | is_boring_prop _ (Const (@{const_name "=="}, _) $ t $ u) =
    1.29          is_boring_bool t andalso is_boring_bool u
    1.30 -      | is_boring_prop _ = true
    1.31 +      | is_boring_prop _ _ = true
    1.32    in
    1.33 -    is_boring_prop (prop_of th) andalso not (Thm.eq_thm_prop (@{thm ext}, th))
    1.34 +    is_boring_prop [] (prop_of th) andalso
    1.35 +    not (Thm.eq_thm_prop (@{thm ext}, th))
    1.36    end
    1.37  
    1.38  fun is_theorem_bad_for_atps ho_atp th =