get rid of some junk facts in the MaSh evaluation driver
authorblanchet
Thu Dec 13 23:47:01 2012 +0100 (2012-12-13 ago)
changeset 505230799339fea0f
parent 50522 19dbd7554076
child 50524 bd145273e7c6
get rid of some junk facts in the MaSh evaluation driver
src/HOL/TPTP/mash_export.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
     1.1 --- a/src/HOL/TPTP/mash_export.ML	Thu Dec 13 23:22:10 2012 +0100
     1.2 +++ b/src/HOL/TPTP/mash_export.ML	Thu Dec 13 23:47:01 2012 +0100
     1.3 @@ -132,8 +132,7 @@
     1.4  
     1.5  fun is_bad_query ctxt ho_atp th isar_deps =
     1.6    Thm.legacy_get_kind th = "" orelse null isar_deps orelse
     1.7 -  is_blacklisted_or_something ctxt ho_atp (Thm.get_name_hint th) orelse
     1.8 -  Sledgehammer_Fact.is_bad_for_atps ho_atp th
     1.9 +  is_blacklisted_or_something ctxt ho_atp (Thm.get_name_hint th)
    1.10  
    1.11  fun generate_isar_or_prover_commands ctxt prover params_opt thys file_name =
    1.12    let
    1.13 @@ -179,7 +178,7 @@
    1.14      val facts = all_facts ctxt
    1.15      val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
    1.16      val all_names = build_all_names nickname_of facts
    1.17 -    fun do_fact (fact as (_, th), old_facts) =
    1.18 +    fun do_fact ((_, th), old_facts) =
    1.19        let
    1.20          val name = nickname_of th
    1.21          val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Dec 13 23:22:10 2012 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Dec 13 23:47:01 2012 +0100
     2.3 @@ -24,7 +24,6 @@
     2.4      Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
     2.5      -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
     2.6    val backquote_thm : Proof.context -> thm -> string
     2.7 -  val is_bad_for_atps : bool -> thm -> bool
     2.8    val is_blacklisted_or_something : Proof.context -> bool -> string -> bool
     2.9    val clasimpset_rule_table_of : Proof.context -> status Termtab.table
    2.10    val build_all_names :
    2.11 @@ -175,8 +174,8 @@
    2.12      else
    2.13        term_has_too_many_lambdas max_lambda_nesting t
    2.14  
    2.15 -(* The max apply depth of any "metis" call in "Metis_Examples" (on 2007-10-31)
    2.16 -   was 11. *)
    2.17 +(* The maximum apply depth of any "metis" call in "Metis_Examples" (on
    2.18 +   2007-10-31) was 11. *)
    2.19  val max_apply_depth = 18
    2.20  
    2.21  fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1)
    2.22 @@ -210,7 +209,7 @@
    2.23    andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN
    2.24                             | _ => false) (prop_of th)
    2.25  
    2.26 -fun is_likely_tautology_or_too_meta th =
    2.27 +fun is_likely_tautology_too_meta_or_too_technical th =
    2.28    let
    2.29      fun is_interesting_subterm (Const (s, _)) =
    2.30          not (member (op =) atp_widely_irrelevant_consts s)
    2.31 @@ -229,14 +228,10 @@
    2.32        | is_boring_prop _ (Const (@{const_name "=="}, _) $ t $ u) =
    2.33          is_boring_bool t andalso is_boring_bool u
    2.34        | is_boring_prop _ _ = true
    2.35 +    val t = prop_of th
    2.36    in
    2.37 -    is_boring_prop [] (prop_of th) andalso
    2.38 -    not (Thm.eq_thm_prop (@{thm ext}, th))
    2.39 -  end
    2.40 -
    2.41 -fun is_bad_for_atps ho_atp th =
    2.42 -  let val t = prop_of th in
    2.43 -    is_too_complex ho_atp t orelse
    2.44 +    (is_boring_prop [] (prop_of th) andalso
    2.45 +     not (Thm.eq_thm_prop (@{thm ext}, th))) orelse
    2.46      exists_type type_has_top_sort t orelse exists_technical_const t orelse
    2.47      exists_low_level_class_const t orelse is_that_fact th
    2.48    end
    2.49 @@ -408,7 +403,7 @@
    2.50  fun maybe_filter_no_atps ctxt =
    2.51    not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd)
    2.52  
    2.53 -fun all_facts ctxt really_all ho_atp reserved add_ths chained css =
    2.54 +fun all_facts ctxt generous ho_atp reserved add_ths chained css =
    2.55    let
    2.56      val thy = Proof_Context.theory_of ctxt
    2.57      val global_facts = Global_Theory.facts_of thy
    2.58 @@ -429,7 +424,7 @@
    2.59             forall (not o member Thm.eq_thm_prop add_ths) ths andalso
    2.60             (Facts.is_concealed facts name0 orelse
    2.61              not (can (Proof_Context.get_thms ctxt) name0) orelse
    2.62 -            (not really_all andalso
    2.63 +            (not generous andalso
    2.64               is_blacklisted_or_something ctxt ho_atp name0)) then
    2.65            I
    2.66          else
    2.67 @@ -445,8 +440,9 @@
    2.68              #> fold_rev (fn th => fn (j, (multis, unis)) =>
    2.69                     (j - 1,
    2.70                      if not (member Thm.eq_thm_prop add_ths th) andalso
    2.71 -                       is_likely_tautology_or_too_meta th orelse
    2.72 -                       (not really_all andalso is_bad_for_atps ho_atp th) then
    2.73 +                       (is_likely_tautology_too_meta_or_too_technical th orelse
    2.74 +                        (not generous andalso
    2.75 +                         is_too_complex ho_atp (prop_of th))) then
    2.76                        (multis, unis)
    2.77                      else
    2.78                        let