src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
changeset 54080 540835cf11ed
parent 54078 1d371c3f2703
child 54081 c7e9f1df30bb
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Oct 08 20:53:37 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Oct 08 20:56:35 2013 +0200
     1.3 @@ -57,6 +57,12 @@
     1.4     del : (Facts.ref * Attrib.src list) list,
     1.5     only : bool}
     1.6  
     1.7 +(* gracefully handle huge background theories *)
     1.8 +val max_facts_for_duplicates = 50000
     1.9 +val max_facts_for_duplicate_matching = 25000
    1.10 +val max_facts_for_complex_check = 25000
    1.11 +val max_simps_for_clasimpset = 5000
    1.12 +
    1.13  (* experimental feature *)
    1.14  val instantiate_inducts =
    1.15    Attrib.setup_config_bool @{binding sledgehammer_instantiate_inducts} (K false)
    1.16 @@ -301,9 +307,6 @@
    1.17  fun backquote_term ctxt = close_form #> hackish_string_of_term ctxt #> backquote
    1.18  fun backquote_thm ctxt = backquote_term ctxt o prop_of
    1.19  
    1.20 -(* gracefully handle huge background theories *)
    1.21 -val max_simps_for_clasimpset = 10000
    1.22 -
    1.23  fun clasimpset_rule_table_of ctxt =
    1.24    let val simps = ctxt |> simpset_of |> dest_ss |> #simps in
    1.25      if length simps >= max_simps_for_clasimpset then
    1.26 @@ -378,12 +381,9 @@
    1.27      val inclass_name_tab = Symtab.fold add_inclass plain_name_tab Symtab.empty
    1.28    in (plain_name_tab, inclass_name_tab) end
    1.29  
    1.30 -(* The function would have slightly cleaner semantics if it called "Pattern.equiv" instead of
    1.31 -   "Pattern.matches", but it would also be slower. "Pattern.matches" throws out theorems that are
    1.32 -   strict instances of other theorems, but only if the instance is met after the general version. *)
    1.33 -fun fact_distinct thy facts =
    1.34 +fun fact_distinct eq facts =
    1.35    fold (fn fact as (_, th) =>
    1.36 -      Net.insert_term_safe (Pattern.matches thy o swap o pairself (normalize_eq o prop_of o snd))
    1.37 +      Net.insert_term_safe (eq o pairself (normalize_eq o prop_of o snd))
    1.38          (normalize_eq (prop_of th), fact))
    1.39      facts Net.empty
    1.40    |> Net.entries
    1.41 @@ -449,9 +449,6 @@
    1.42  
    1.43  fun fact_count facts = Facts.fold_static (K (Integer.add 1)) facts 0
    1.44  
    1.45 -(* gracefully handle huge background theories *)
    1.46 -val max_facts_for_complex_check = 25000
    1.47 -
    1.48  fun all_facts ctxt generous ho_atp reserved add_ths chained css =
    1.49    let
    1.50      val thy = Proof_Context.theory_of ctxt
    1.51 @@ -541,10 +538,21 @@
    1.52           maps (map (fn ((name, stature), th) => ((K name, stature), th))
    1.53                 o fact_of_ref ctxt reserved chained css) add
    1.54         else
    1.55 -         let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in
    1.56 -           all_facts ctxt false ho_atp reserved add chained css
    1.57 -           |> filter_out ((member Thm.eq_thm_prop del orf No_ATPs.member ctxt) o snd)
    1.58 -           |> fact_distinct thy
    1.59 +        (* The "fact_distinct" call would have cleaner semantics if it called "Pattern.equiv"
    1.60 +           instead of "Pattern.matches", but it would also be slower and less precise.
    1.61 +           "Pattern.matches" throws out theorems that are strict instances of other theorems, but
    1.62 +           only if the instance is met after the general version. *)
    1.63 +         let
    1.64 +           val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del)
    1.65 +           val facts =
    1.66 +             all_facts ctxt false ho_atp reserved add chained css
    1.67 +             |> filter_out ((member Thm.eq_thm_prop del orf No_ATPs.member ctxt) o snd)
    1.68 +            val num_facts = length facts
    1.69 +         in
    1.70 +           facts
    1.71 +           |> num_facts <= max_facts_for_duplicates
    1.72 +              ? fact_distinct (if num_facts > max_facts_for_duplicate_matching then op aconv
    1.73 +                  else Pattern.matches thy o swap)
    1.74           end)
    1.75        |> maybe_instantiate_inducts ctxt hyp_ts concl_t
    1.76      end