src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
changeset 37626 1146291fe718
parent 37616 c8d2d84d6011
child 37995 06f02b15ef8a
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Jun 29 09:26:56 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Jun 29 10:25:53 2010 +0200
     1.3 @@ -393,8 +393,60 @@
     1.4  fun make_unique xs =
     1.5    Termtab.fold (cons o snd) (make_clause_table xs) []
     1.6  
     1.7 +(* FIXME: put other record thms here, or declare as "no_atp" *)
     1.8 +val multi_base_blacklist =
     1.9 +  ["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits",
    1.10 +   "split_asm", "cases", "ext_cases"]
    1.11 +
    1.12 +val max_lambda_nesting = 3
    1.13 +
    1.14 +fun term_has_too_many_lambdas max (t1 $ t2) =
    1.15 +    exists (term_has_too_many_lambdas max) [t1, t2]
    1.16 +  | term_has_too_many_lambdas max (Abs (_, _, t)) =
    1.17 +    max = 0 orelse term_has_too_many_lambdas (max - 1) t
    1.18 +  | term_has_too_many_lambdas _ _ = false
    1.19 +
    1.20 +fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
    1.21 +
    1.22 +(* Don't count nested lambdas at the level of formulas, since they are
    1.23 +   quantifiers. *)
    1.24 +fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) =
    1.25 +    formula_has_too_many_lambdas (T :: Ts) t
    1.26 +  | formula_has_too_many_lambdas Ts t =
    1.27 +    if is_formula_type (fastype_of1 (Ts, t)) then
    1.28 +      exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t))
    1.29 +    else
    1.30 +      term_has_too_many_lambdas max_lambda_nesting t
    1.31 +
    1.32 +(* The max apply depth of any "metis" call in "Metis_Examples" (on 31-10-2007)
    1.33 +   was 11. *)
    1.34 +val max_apply_depth = 15
    1.35 +
    1.36 +fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1)
    1.37 +  | apply_depth (Abs (_, _, t)) = apply_depth t
    1.38 +  | apply_depth _ = 0
    1.39 +
    1.40 +fun is_formula_too_complex t =
    1.41 +  apply_depth t > max_apply_depth orelse Meson.too_many_clauses NONE t orelse
    1.42 +  formula_has_too_many_lambdas [] t
    1.43 +
    1.44  val exists_sledgehammer_const =
    1.45 -  exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s) o prop_of
    1.46 +  exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)
    1.47 +
    1.48 +fun is_strange_thm th =
    1.49 +  case head_of (concl_of th) of
    1.50 +      Const (a, _) => (a <> @{const_name Trueprop} andalso
    1.51 +                       a <> @{const_name "=="})
    1.52 +    | _ => false
    1.53 +
    1.54 +val type_has_top_sort =
    1.55 +  exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
    1.56 +
    1.57 +fun is_theorem_bad_for_atps thm =
    1.58 +  let val t = prop_of thm in
    1.59 +    is_formula_too_complex t orelse exists_type type_has_top_sort t orelse
    1.60 +    exists_sledgehammer_const t orelse is_strange_thm thm
    1.61 +  end
    1.62  
    1.63  fun all_name_thms_pairs ctxt chained_ths =
    1.64    let
    1.65 @@ -407,8 +459,7 @@
    1.66        (facts, []) |-> Facts.fold_static (fn (name, ths0) =>
    1.67          if Facts.is_concealed facts name orelse
    1.68             (respect_no_atp andalso is_package_def name) orelse
    1.69 -           member (op =) Clausifier.multi_base_blacklist
    1.70 -                  (Long_Name.base_name name) then
    1.71 +           member (op =) multi_base_blacklist (Long_Name.base_name name) then
    1.72            I
    1.73          else
    1.74            let
    1.75 @@ -419,8 +470,7 @@
    1.76  
    1.77              val name1 = Facts.extern facts name;
    1.78              val name2 = Name_Space.extern full_space name;
    1.79 -            val ths = filter_out (Clausifier.is_theorem_bad_for_atps orf
    1.80 -                                  exists_sledgehammer_const) ths0
    1.81 +            val ths = filter_out is_theorem_bad_for_atps ths0
    1.82            in
    1.83              case find_first check_thms [name1, name2, name] of
    1.84                NONE => I