src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
changeset 43351 b19d95b4d736
parent 43324 2b47822868e4
child 43421 926bfe067a32
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Jun 09 23:30:18 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Fri Jun 10 12:01:15 2011 +0200
     1.3 @@ -39,19 +39,23 @@
     1.4    val new_monomorphizer : bool Config.T
     1.5    val ignore_no_atp : bool Config.T
     1.6    val instantiate_inducts : bool Config.T
     1.7 +  val const_names_in_fact :
     1.8 +    theory -> (string * typ -> term list -> bool * term list) -> term
     1.9 +    -> string list
    1.10    val fact_from_ref :
    1.11      Proof.context -> unit Symtab.table -> thm list
    1.12      -> Facts.ref * Attrib.src list -> ((string * locality) * thm) list
    1.13    val all_facts :
    1.14 -    Proof.context -> 'a Symtab.table -> bool -> (term -> bool) -> thm list
    1.15 -    -> thm list -> (((unit -> string) * locality) * thm) list
    1.16 -  val const_names_in_fact :
    1.17 -    theory -> (string * typ -> term list -> bool * term list) -> term
    1.18 -    -> string list
    1.19 +    Proof.context -> 'a Symtab.table -> bool -> thm list -> thm list
    1.20 +    -> (((unit -> string) * locality) * thm) list
    1.21 +  val nearly_all_facts :
    1.22 +    Proof.context -> relevance_override -> thm list -> term list -> term
    1.23 +    -> (((unit -> string) * locality) * thm) list
    1.24    val relevant_facts :
    1.25 -    Proof.context -> real * real -> int -> (term -> bool)
    1.26 +    Proof.context -> real * real -> int
    1.27      -> (string * typ -> term list -> bool * term list) -> relevance_fudge
    1.28      -> relevance_override -> thm list -> term list -> term
    1.29 +    -> (((unit -> string) * locality) * thm) list
    1.30      -> ((string * locality) * thm) list
    1.31  end;
    1.32  
    1.33 @@ -778,12 +782,11 @@
    1.34  (**** Predicates to detect unwanted facts (prolific or likely to cause
    1.35        unsoundness) ****)
    1.36  
    1.37 -fun is_theorem_bad_for_atps is_appropriate_prop thm =
    1.38 +fun is_theorem_bad_for_atps thm =
    1.39    let val t = prop_of thm in
    1.40 -    not (is_appropriate_prop t) orelse is_formula_too_complex t orelse
    1.41 -    exists_type type_has_top_sort t orelse exists_sledgehammer_const t orelse
    1.42 -    exists_low_level_class_const t orelse is_metastrange_theorem thm orelse
    1.43 -    is_that_fact thm
    1.44 +    is_formula_too_complex t orelse exists_type type_has_top_sort t orelse
    1.45 +    exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
    1.46 +    is_metastrange_theorem thm orelse is_that_fact thm
    1.47    end
    1.48  
    1.49  fun meta_equify (@{const Trueprop}
    1.50 @@ -810,7 +813,7 @@
    1.51                    |> add Simp normalize_simp_prop snd simps
    1.52    end
    1.53  
    1.54 -fun all_facts ctxt reserved really_all is_appropriate_prop add_ths chained_ths =
    1.55 +fun all_facts ctxt reserved really_all add_ths chained_ths =
    1.56    let
    1.57      val thy = Proof_Context.theory_of ctxt
    1.58      val global_facts = Global_Theory.facts_of thy
    1.59 @@ -860,7 +863,7 @@
    1.60              #> fold (fn th => fn (j, (multis, unis)) =>
    1.61                          (j + 1,
    1.62                           if not (member Thm.eq_thm_prop add_ths th) andalso
    1.63 -                            is_theorem_bad_for_atps is_appropriate_prop th then
    1.64 +                            is_theorem_bad_for_atps th then
    1.65                             (multis, unis)
    1.66                           else
    1.67                             let
    1.68 @@ -894,30 +897,36 @@
    1.69  fun external_frees t =
    1.70    [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
    1.71  
    1.72 +fun nearly_all_facts ctxt ({add, only, ...} : relevance_override) chained_ths
    1.73 +                     hyp_ts concl_t =
    1.74 +  let
    1.75 +    val thy = Proof_Context.theory_of ctxt
    1.76 +    val reserved = reserved_isar_keyword_table ()
    1.77 +    val add_ths = Attrib.eval_thms ctxt add
    1.78 +    val ind_stmt =
    1.79 +      Logic.list_implies (hyp_ts |> filter_out (null o external_frees), concl_t)
    1.80 +      |> Object_Logic.atomize_term thy
    1.81 +    val ind_stmt_xs = external_frees ind_stmt
    1.82 +  in
    1.83 +    (if only then
    1.84 +       maps (map (fn ((name, loc), th) => ((K name, loc), th))
    1.85 +             o fact_from_ref ctxt reserved chained_ths) add
    1.86 +     else
    1.87 +       all_facts ctxt reserved false add_ths chained_ths)
    1.88 +    |> Config.get ctxt instantiate_inducts
    1.89 +       ? maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs)
    1.90 +    |> (not (Config.get ctxt ignore_no_atp) andalso not only)
    1.91 +       ? filter_out (No_ATPs.member ctxt o snd)
    1.92 +    |> uniquify
    1.93 +  end
    1.94 +
    1.95  fun relevant_facts ctxt (threshold0, threshold1) max_relevant
    1.96 -        is_appropriate_prop is_built_in_const fudge
    1.97 -        (override as {add, only, ...}) chained_ths hyp_ts concl_t =
    1.98 +                   is_built_in_const fudge (override as {only, ...}) chained_ths
    1.99 +                   hyp_ts concl_t facts =
   1.100    let
   1.101      val thy = Proof_Context.theory_of ctxt
   1.102      val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
   1.103                            1.0 / Real.fromInt (max_relevant + 1))
   1.104 -    val add_ths = Attrib.eval_thms ctxt add
   1.105 -    val reserved = reserved_isar_keyword_table ()
   1.106 -    val ind_stmt =
   1.107 -      Logic.list_implies (hyp_ts |> filter_out (null o external_frees), concl_t)
   1.108 -      |> Object_Logic.atomize_term thy
   1.109 -    val ind_stmt_xs = external_frees ind_stmt
   1.110 -    val facts =
   1.111 -      (if only then
   1.112 -         maps (map (fn ((name, loc), th) => ((K name, loc), th))
   1.113 -               o fact_from_ref ctxt reserved chained_ths) add
   1.114 -       else
   1.115 -         all_facts ctxt reserved false is_appropriate_prop add_ths chained_ths)
   1.116 -      |> Config.get ctxt instantiate_inducts
   1.117 -         ? maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs)
   1.118 -      |> (not (Config.get ctxt ignore_no_atp) andalso not only)
   1.119 -         ? filter_out (No_ATPs.member ctxt o snd)
   1.120 -      |> uniquify
   1.121    in
   1.122      trace_msg ctxt (fn () => "Considering " ^ string_of_int (length facts) ^
   1.123                               " facts");