got rid of old, needless logic
authorblanchet
Tue Sep 10 15:56:51 2013 +0200 (2013-09-10 ago)
changeset 53506f99ee3adb81d
parent 53505 412f8c590c6c
child 53507 a6ed27399ba9
got rid of old, needless logic
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Sep 10 15:56:51 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Sep 10 15:56:51 2013 +0200
     1.3 @@ -195,36 +195,6 @@
     1.4          append ["induct", "inducts"]
     1.5    |> map (prefix Long_Name.separator)
     1.6  
     1.7 -val max_lambda_nesting = 5 (*only applies if not ho_atp*)
     1.8 -
     1.9 -fun term_has_too_many_lambdas max (t1 $ t2) =
    1.10 -    exists (term_has_too_many_lambdas max) [t1, t2]
    1.11 -  | term_has_too_many_lambdas max (Abs (_, _, t)) =
    1.12 -    max = 0 orelse term_has_too_many_lambdas (max - 1) t
    1.13 -  | term_has_too_many_lambdas _ _ = false
    1.14 -
    1.15 -(* Don't count nested lambdas at the level of formulas, since they are
    1.16 -   quantifiers. *)
    1.17 -fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) =
    1.18 -    formula_has_too_many_lambdas (T :: Ts) t
    1.19 -  | formula_has_too_many_lambdas Ts t =
    1.20 -    if member (op =) [HOLogic.boolT, propT] (fastype_of1 (Ts, t)) then
    1.21 -      exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t))
    1.22 -    else
    1.23 -      term_has_too_many_lambdas max_lambda_nesting t
    1.24 -
    1.25 -(* The maximum apply depth of any "metis" call in "Metis_Examples" (on
    1.26 -   2007-10-31) was 11. *)
    1.27 -val max_apply_depth = 18
    1.28 -
    1.29 -fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1)
    1.30 -  | apply_depth (Abs (_, _, t)) = apply_depth t
    1.31 -  | apply_depth _ = 0
    1.32 -
    1.33 -fun is_too_complex ho_atp t =
    1.34 -  apply_depth t > max_apply_depth orelse
    1.35 -  (not ho_atp andalso formula_has_too_many_lambdas [] t)
    1.36 -
    1.37  (* FIXME: Ad hoc list *)
    1.38  val technical_prefixes =
    1.39    ["ATP", "Code_Evaluation", "Datatype", "Enum", "Lazy_Sequence",
    1.40 @@ -496,9 +466,7 @@
    1.41              #> fold_rev (fn th => fn (j, accum) =>
    1.42                     (j - 1,
    1.43                      if not (member Thm.eq_thm_prop add_ths th) andalso
    1.44 -                       (is_likely_tautology_too_meta_or_too_technical th orelse
    1.45 -                        (not generous andalso
    1.46 -                         is_too_complex ho_atp (prop_of th))) then
    1.47 +                       (is_likely_tautology_too_meta_or_too_technical th) then
    1.48                        accum
    1.49                      else
    1.50                        let