drop only real duplicates, not subsumed facts -- this confuses MaSh
authorblanchet
Tue Oct 15 15:26:58 2013 +0200 (2013-10-15 ago)
changeset 541129c0f464d1854
parent 54111 fb6ef69b8c85
child 54113 df080dfefddc
drop only real duplicates, not subsumed facts -- this confuses MaSh
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Oct 15 11:49:39 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Oct 15 15:26:58 2013 +0200
     1.3 @@ -39,6 +39,7 @@
     1.4    val nearly_all_facts :
     1.5      Proof.context -> bool -> fact_override -> unit Symtab.table
     1.6      -> status Termtab.table -> thm list -> term list -> term -> raw_fact list
     1.7 +  val drop_duplicate_facts: theory -> raw_fact list -> raw_fact list
     1.8  end;
     1.9  
    1.10  structure Sledgehammer_Fact : SLEDGEHAMMER_FACT =
    1.11 @@ -545,14 +546,17 @@
    1.12             val facts =
    1.13               all_facts ctxt false ho_atp reserved add chained css
    1.14               |> filter_out ((member Thm.eq_thm_prop del orf No_ATPs.member ctxt) o snd)
    1.15 -            val num_facts = length facts
    1.16           in
    1.17             facts
    1.18 -           |> num_facts <= max_facts_for_duplicates
    1.19 -              ? fact_distinct (if num_facts > max_facts_for_duplicate_matching then op aconv
    1.20 -                  else Pattern.matches thy o swap)
    1.21           end)
    1.22        |> maybe_instantiate_inducts ctxt hyp_ts concl_t
    1.23      end
    1.24  
    1.25 +fun drop_duplicate_facts thy facts =
    1.26 +  let val num_facts = length facts in
    1.27 +    facts |> num_facts <= max_facts_for_duplicates
    1.28 +      ? fact_distinct (if num_facts > max_facts_for_duplicate_matching then op aconv
    1.29 +          else Pattern.matches thy o swap)
    1.30 +  end
    1.31 +
    1.32  end;
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Tue Oct 15 11:49:39 2013 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Tue Oct 15 15:26:58 2013 +0200
     2.3 @@ -439,6 +439,7 @@
     2.4          (fudge as {threshold_divisor, ridiculous_threshold, ...}) facts hyp_ts concl_t =
     2.5    let
     2.6      val thy = Proof_Context.theory_of ctxt
     2.7 +    val facts = drop_duplicate_facts thy facts
     2.8      val const_tab = fold (count_fact_consts thy fudge) facts Symtab.empty
     2.9      val add_pconsts = add_pconsts_in_term thy
    2.10      val chained_ts =