src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
changeset 50510 7e4f2f8d9b50
parent 50496 8665ec681e47
child 50511 8825c36cb1ce
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Dec 12 19:03:49 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Dec 12 21:48:29 2012 +0100
     1.3 @@ -24,6 +24,9 @@
     1.4      Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
     1.5      -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
     1.6    val backquote_thm : Proof.context -> thm -> string
     1.7 +  val is_bad_for_atps : bool -> thm -> bool
     1.8 +  val is_concealed_or_backlisted_or_something :
     1.9 +    Proof.context -> bool -> Facts.T -> string -> bool
    1.10    val clasimpset_rule_table_of : Proof.context -> status Termtab.table
    1.11    val build_all_names :
    1.12      (thm -> string) -> ('a * thm) list -> string Symtab.table
    1.13 @@ -232,13 +235,19 @@
    1.14      not (Thm.eq_thm_prop (@{thm ext}, th))
    1.15    end
    1.16  
    1.17 -fun is_theorem_bad_for_atps ho_atp th =
    1.18 +fun is_bad_for_atps ho_atp th =
    1.19    let val t = prop_of th in
    1.20      is_formula_too_complex ho_atp t orelse
    1.21      exists_type type_has_top_sort t orelse exists_technical_const t orelse
    1.22      exists_low_level_class_const t orelse is_that_fact th
    1.23    end
    1.24  
    1.25 +fun is_concealed_or_backlisted_or_something ctxt ho_atp facts name =
    1.26 +  Facts.is_concealed facts name orelse
    1.27 +  not (can (Proof_Context.get_thms ctxt) name) orelse
    1.28 +  (not (Config.get ctxt ignore_no_atp) andalso is_package_def name) orelse
    1.29 +  exists (fn s => String.isSuffix s name) (multi_base_blacklist ctxt ho_atp)
    1.30 +
    1.31  fun hackish_string_for_term ctxt =
    1.32    with_vanilla_print_mode (Syntax.string_of_term ctxt) #> simplify_spaces
    1.33  
    1.34 @@ -422,12 +431,7 @@
    1.35          if not really_all andalso
    1.36             name0 <> "" andalso
    1.37             forall (not o member Thm.eq_thm_prop add_ths) ths andalso
    1.38 -           (Facts.is_concealed facts name0 orelse
    1.39 -            not (can (Proof_Context.get_thms ctxt) name0) orelse
    1.40 -            (not (Config.get ctxt ignore_no_atp) andalso
    1.41 -             is_package_def name0) orelse
    1.42 -            exists (fn s => String.isSuffix s name0)
    1.43 -                   (multi_base_blacklist ctxt ho_atp)) then
    1.44 +           is_concealed_or_backlisted_or_something ctxt ho_atp facts name0 then
    1.45            I
    1.46          else
    1.47            let
    1.48 @@ -444,7 +448,7 @@
    1.49                      if not (member Thm.eq_thm_prop add_ths th) andalso
    1.50                         is_likely_tautology_or_too_meta th orelse
    1.51                         (not really_all andalso
    1.52 -                        is_theorem_bad_for_atps ho_atp th) then
    1.53 +                        is_bad_for_atps ho_atp th) then
    1.54                        (multis, unis)
    1.55                      else
    1.56                        let