1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Jul 18 08:44:03 2012 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Jul 18 08:44:03 2012 +0200
     1.3 @@ -22,6 +22,7 @@
     1.4  val reconstructorK = "reconstructor" (*=NAME: how to reconstruct proofs (ie. using metis/smt)*)
     1.5  val metis_ftK = "metis_ft" (*: apply metis with fully-typed encoding to the theorems found by sledgehammer*)
     1.6  
     1.7 +val max_factsK = "max_facts" (*=NUM: max. relevant clauses to use*)
     1.8  val max_relevantK = "max_relevant" (*=NUM: max. relevant clauses to use*)
     1.9  val max_callsK = "max_calls" (*=NUM: max. no. of calls to sledgehammer*)
    1.10  val preplay_timeoutK = "preplay_timeout" (*=TIME: timeout for finding reconstructed proof*)
    1.11 @@ -53,7 +54,7 @@
    1.12  val uncurried_aliases_default = "smart"
    1.13  val type_enc_default = "smart"
    1.14  val strict_default = "false"
    1.15 -val max_relevant_default = "smart"
    1.16 +val max_facts_default = "smart"
    1.17  val slice_default = "true"
    1.18  val max_calls_default = "10000000"
    1.19  val trivial_default = "false"
    1.20 @@ -398,7 +399,7 @@
    1.21    SH_FAIL of int * int |
    1.22    SH_ERROR
    1.23  
    1.24 -fun run_sh prover_name prover type_enc strict max_relevant slice lam_trans
    1.25 +fun run_sh prover_name prover type_enc strict max_facts slice lam_trans
    1.26          uncurried_aliases e_selection_heuristic term_order force_sos
    1.27          hard_timeout timeout preplay_timeout sh_minimizeLST
    1.28          max_new_mono_instancesLST max_mono_itersLST dir pos st =
    1.29 @@ -423,23 +424,22 @@
    1.30                    term_order |> the_default I)
    1.31              #> (Option.map (Config.put ATP_Systems.force_sos)
    1.32                    force_sos |> the_default I))
    1.33 -    val params as {max_relevant, slice, ...} =
    1.34 +    val params as {max_facts, slice, ...} =
    1.35        Sledgehammer_Isar.default_params ctxt
    1.36           ([("verbose", "true"),
    1.37             ("type_enc", type_enc),
    1.38             ("strict", strict),
    1.39             ("lam_trans", lam_trans |> the_default lam_trans_default),
    1.40             ("uncurried_aliases", uncurried_aliases |> the_default uncurried_aliases_default),
    1.41 -           ("max_relevant", max_relevant),
    1.42 +           ("max_facts", max_facts),
    1.43             ("slice", slice),
    1.44             ("timeout", string_of_int timeout),
    1.45             ("preplay_timeout", preplay_timeout)]
    1.46            |> sh_minimizeLST (*don't confuse the two minimization flags*)
    1.47            |> max_new_mono_instancesLST
    1.48            |> max_mono_itersLST)
    1.49 -    val default_max_relevant =
    1.50 -      Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice
    1.51 -        prover_name
    1.52 +    val default_max_facts =
    1.53 +      Sledgehammer_Provers.default_max_facts_for_prover ctxt slice prover_name
    1.54      val is_appropriate_prop =
    1.55        Sledgehammer_Provers.is_appropriate_prop_for_prover ctxt prover_name
    1.56      val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
    1.57 @@ -464,7 +464,7 @@
    1.58                Sledgehammer_Fact.no_fact_override chained_ths hyp_ts concl_t
    1.59            |> filter (is_appropriate_prop o prop_of o snd)
    1.60            |> Sledgehammer_Filter_MaSh.relevant_facts ctxt params prover_name
    1.61 -                 (the_default default_max_relevant max_relevant)
    1.62 +                 (the_default default_max_facts max_facts)
    1.63                   Sledgehammer_Fact.no_fact_override hyp_ts concl_t
    1.64          val problem =
    1.65            {state = st', goal = goal, subgoal = i,
    1.66 @@ -507,7 +507,12 @@
    1.67      val (prover_name, prover) = get_prover (Proof.context_of st) args
    1.68      val type_enc = AList.lookup (op =) args type_encK |> the_default type_enc_default
    1.69      val strict = AList.lookup (op =) args strictK |> the_default strict_default
    1.70 -    val max_relevant = AList.lookup (op =) args max_relevantK |> the_default max_relevant_default
    1.71 +    val max_facts =
    1.72 +      case AList.lookup (op =) args max_factsK of
    1.73 +        SOME max => max
    1.74 +      | NONE => case AList.lookup (op =) args max_relevantK of
    1.75 +                  SOME max => max
    1.76 +                | NONE => max_facts_default
    1.77      val slice = AList.lookup (op =) args sliceK |> the_default slice_default
    1.78      val lam_trans = AList.lookup (op =) args lam_transK
    1.79      val uncurried_aliases = AList.lookup (op =) args uncurried_aliasesK
    1.80 @@ -527,7 +532,7 @@
    1.81      val max_mono_itersLST = available_parameter args max_mono_itersK max_mono_itersK
    1.82      val hard_timeout = SOME (2 * timeout)
    1.83      val (msg, result) =
    1.84 -      run_sh prover_name prover type_enc strict max_relevant slice lam_trans
    1.85 +      run_sh prover_name prover type_enc strict max_facts slice lam_trans
    1.86          uncurried_aliases e_selection_heuristic term_order force_sos
    1.87          hard_timeout timeout preplay_timeout sh_minimizeLST
    1.88          max_new_mono_instancesLST max_mono_itersLST dir pos st
    1.89 @@ -611,7 +616,7 @@
    1.90  
    1.91  fun override_params prover type_enc timeout =
    1.92    [("provers", prover),
    1.93 -   ("max_relevant", "0"),
    1.94 +   ("max_facts", "0"),
    1.95     ("type_enc", type_enc),
    1.96     ("strict", "true"),
    1.97     ("slice", "false"),

     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Wed Jul 18 08:44:03 2012 +0200
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Wed Jul 18 08:44:03 2012 +0200
     2.3 @@ -113,11 +113,10 @@
     2.4           val {context = ctxt, facts = chained_ths, goal} = Proof.goal pre
     2.5           val prover = AList.lookup (op =) args "prover"
     2.6                        |> the_default default_prover
     2.7 -         val params as {max_relevant, slice, ...} =
     2.8 +         val params as {max_facts, slice, ...} =
     2.9             Sledgehammer_Isar.default_params ctxt args
    2.10 -         val default_max_relevant =
    2.11 -           Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice
    2.12 -                                                                prover
    2.13 +         val default_max_facts =
    2.14 +           Sledgehammer_Provers.default_max_facts_for_prover ctxt slice prover
    2.15           val is_appropriate_prop =
    2.16             Sledgehammer_Provers.is_appropriate_prop_for_prover ctxt
    2.17                 default_prover
    2.18 @@ -132,7 +131,7 @@
    2.19                 Sledgehammer_Fact.no_fact_override chained_ths hyp_ts concl_t
    2.20             |> filter (is_appropriate_prop o prop_of o snd)
    2.21             |> Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
    2.22 -                  default_prover (the_default default_max_relevant max_relevant)
    2.23 +                  default_prover (the_default default_max_facts max_facts)
    2.24                    (SOME relevance_fudge) hyp_ts concl_t
    2.25              |> map ((fn name => name ()) o fst o fst)
    2.26           val (found_facts, lost_facts) =

     3.1 --- a/src/HOL/TPTP/mash_eval.ML	Wed Jul 18 08:44:03 2012 +0200
     3.2 +++ b/src/HOL/TPTP/mash_eval.ML	Wed Jul 18 08:44:03 2012 +0200
     3.3 @@ -36,11 +36,11 @@
     3.4  val mashN = "MaSh"
     3.5  val iter_mashN = "Iter+MaSh"
     3.6  
     3.7 -val max_relevant_slack = 2
     3.8 +val max_facts_slack = 2
     3.9  
    3.10  fun evaluate_mash_suggestions ctxt params thy file_name =
    3.11    let
    3.12 -    val {provers, max_relevant, slice, type_enc, lam_trans, timeout, ...} =
    3.13 +    val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} =
    3.14        Sledgehammer_Isar.default_params ctxt []
    3.15      val prover_name = hd provers
    3.16      val path = file_name |> Path.explode
    3.17 @@ -55,7 +55,7 @@
    3.18        find_first (fn (_, th) => Thm.get_name_hint th = sugg) facts
    3.19      fun sugg_facts hyp_ts concl_t facts =
    3.20        map_filter (find_sugg facts o of_fact_name)
    3.21 -      #> take (max_relevant_slack * the max_relevant)
    3.22 +      #> take (max_facts_slack * the max_facts)
    3.23        #> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t
    3.24      fun hybrid_facts fsp =
    3.25        let
    3.26 @@ -70,7 +70,7 @@
    3.27        in
    3.28          union fact_eq fs1 fs2
    3.29          |> map (`score_of) |> sort (int_ord o pairself fst) |> map snd
    3.30 -        |> take (the max_relevant)
    3.31 +        |> take (the max_facts)
    3.32          |> map (apfst (apfst K))
    3.33        end
    3.34      fun with_index facts s = (find_index (curry (op =) s) facts + 1, s)
    3.35 @@ -84,20 +84,19 @@
    3.36                         |> sort (int_ord o pairself fst)
    3.37                         |> map index_string
    3.38                         |> space_implode " ") ^
    3.39 -           (if length facts < the max_relevant then
    3.40 +           (if length facts < the max_facts then
    3.41                " (of " ^ string_of_int (length facts) ^ ")"
    3.42              else
    3.43                "")
    3.44           else
    3.45             "Failure: " ^
    3.46 -           (facts |> take (the max_relevant)
    3.47 -                  |> tag_list 1
    3.48 +           (facts |> take (the max_facts) |> tag_list 1
    3.49                    |> map index_string
    3.50                    |> space_implode " "))
    3.51        end
    3.52      fun prove ok heading facts goal =
    3.53        let
    3.54 -        val facts = facts |> take (the max_relevant)
    3.55 +        val facts = facts |> take (the max_facts)
    3.56          val res as {outcome, ...} = run_prover ctxt params facts goal
    3.57          val _ = if is_none outcome then ok := !ok + 1 else ()
    3.58        in str_of_res heading facts res end
    3.59 @@ -115,8 +114,8 @@
    3.60          val isa_facts = sugg_facts hyp_ts concl_t facts isa_deps
    3.61          val iter_facts =
    3.62            Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
    3.63 -              prover_name (max_relevant_slack * the max_relevant) NONE hyp_ts
    3.64 -              concl_t facts
    3.65 +              prover_name (max_facts_slack * the max_facts) NONE hyp_ts concl_t
    3.66 +              facts
    3.67          val mash_facts = sugg_facts hyp_ts concl_t facts suggs
    3.68          val iter_mash_facts = hybrid_facts (iter_facts, mash_facts)
    3.69          val iter_s = prove iter_ok iterN iter_facts goal
    3.70 @@ -139,7 +138,7 @@
    3.71                 (100.0 * Real.fromInt (!ok) / Real.fromInt n) ^ "%)"
    3.72      val inst_inducts = Config.get ctxt Sledgehammer_Fact.instantiate_inducts
    3.73      val options =
    3.74 -      [prover_name, string_of_int (the max_relevant) ^ " facts",
    3.75 +      [prover_name, string_of_int (the max_facts) ^ " facts",
    3.76         "slice" |> not slice ? prefix "dont_", the_default "smart" type_enc,
    3.77         the_default "smart" lam_trans, ATP_Util.string_from_time timeout,
    3.78         "instantiate_inducts" |> not inst_inducts ? prefix "dont_"]

     4.1 --- a/src/HOL/TPTP/sledgehammer_tactics.ML	Wed Jul 18 08:44:03 2012 +0200
     4.2 +++ b/src/HOL/TPTP/sledgehammer_tactics.ML	Wed Jul 18 08:44:03 2012 +0200
     4.3 @@ -23,20 +23,20 @@
     4.4  fun run_prover override_params fact_override i n ctxt goal =
     4.5    let
     4.6      val mode = Sledgehammer_Provers.Normal
     4.7 -    val params as {provers, max_relevant, slice, ...} =
     4.8 +    val params as {provers, max_facts, slice, ...} =
     4.9        Sledgehammer_Isar.default_params ctxt override_params
    4.10      val name = hd provers
    4.11      val prover = Sledgehammer_Provers.get_prover ctxt mode name
    4.12 -    val default_max_relevant =
    4.13 -      Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice name
    4.14 +    val default_max_facts =
    4.15 +      Sledgehammer_Provers.default_max_facts_for_prover ctxt slice name
    4.16      val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
    4.17      val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
    4.18      val facts =
    4.19        Sledgehammer_Fact.nearly_all_facts ctxt ho_atp fact_override []
    4.20                                           hyp_ts concl_t
    4.21        |> Sledgehammer_Filter_MaSh.relevant_facts ctxt params name
    4.22 -             (the_default default_max_relevant max_relevant) fact_override
    4.23 -             hyp_ts concl_t
    4.24 +             (the_default default_max_facts max_facts) fact_override hyp_ts
    4.25 +             concl_t
    4.26      val problem =
    4.27        {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
    4.28         facts = facts |> map (apfst (apfst (fn name => name ())))

     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML	Wed Jul 18 08:44:03 2012 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML	Wed Jul 18 08:44:03 2012 +0200
     5.3 @@ -336,14 +336,14 @@
     5.4  type annotated_thm =
     5.5    (((unit -> string) * stature) * thm) * (string * ptype) list
     5.6  
     5.7 -fun take_most_relevant ctxt max_relevant remaining_max
     5.8 +fun take_most_relevant ctxt max_facts remaining_max
     5.9          ({max_imperfect, max_imperfect_exp, ...} : relevance_fudge)
    5.10          (candidates : (annotated_thm * real) list) =
    5.11    let
    5.12      val max_imperfect =
    5.13        Real.ceil (Math.pow (max_imperfect,
    5.14                      Math.pow (Real.fromInt remaining_max
    5.15 -                              / Real.fromInt max_relevant, max_imperfect_exp)))
    5.16 +                              / Real.fromInt max_facts, max_imperfect_exp)))
    5.17      val (perfect, imperfect) =
    5.18        candidates |> sort (Real.compare o swap o pairself snd)
    5.19                   |> take_prefix (fn (_, w) => w > 0.99999)
    5.20 @@ -393,7 +393,7 @@
    5.21     facts are included. *)
    5.22  val special_fact_index = 75
    5.23  
    5.24 -fun relevance_filter ctxt thres0 decay max_relevant is_built_in_const
    5.25 +fun relevance_filter ctxt thres0 decay max_facts is_built_in_const
    5.26          (fudge as {threshold_divisor, ridiculous_threshold, ...}) facts hyp_ts
    5.27          concl_t =
    5.28    let
    5.29 @@ -416,15 +416,14 @@
    5.30              (* Nothing has been added this iteration. *)
    5.31              if j = 0 andalso thres >= ridiculous_threshold then
    5.32                (* First iteration? Try again. *)
    5.33 -              iter 0 max_relevant (thres / threshold_divisor) rel_const_tab
    5.34 +              iter 0 max_facts (thres / threshold_divisor) rel_const_tab
    5.35                     hopeless hopeful
    5.36              else
    5.37                []
    5.38            | relevant candidates rejects [] =
    5.39              let
    5.40                val (accepts, more_rejects) =
    5.41 -                take_most_relevant ctxt max_relevant remaining_max fudge
    5.42 -                                   candidates
    5.43 +                take_most_relevant ctxt max_facts remaining_max fudge candidates
    5.44                val rel_const_tab' =
    5.45                  rel_const_tab
    5.46                  |> fold (add_pconst_to_table false) (maps (snd o fst) accepts)
    5.47 @@ -495,7 +494,7 @@
    5.48            val add = facts |> filter (member Thm.eq_thm_prop ths o snd)
    5.49            val (bef, after) =
    5.50              accepts |> filter_out (member Thm.eq_thm_prop ths o snd)
    5.51 -                    |> take (max_relevant - length add)
    5.52 +                    |> take (max_facts - length add)
    5.53                      |> chop special_fact_index
    5.54          in bef @ add @ after end
    5.55      fun insert_special_facts accepts =
    5.56 @@ -505,15 +504,15 @@
    5.57            |> insert_into_facts accepts
    5.58    in
    5.59      facts |> map_filter (pair_consts_fact thy is_built_in_const fudge)
    5.60 -          |> iter 0 max_relevant thres0 goal_const_tab []
    5.61 +          |> iter 0 max_facts thres0 goal_const_tab []
    5.62            |> insert_special_facts
    5.63            |> tap (fn accepts => trace_msg ctxt (fn () =>
    5.64                        "Total relevant: " ^ string_of_int (length accepts)))
    5.65    end
    5.66  
    5.67  fun iterative_relevant_facts ctxt
    5.68 -        ({relevance_thresholds = (thres0, thres1), ...} : params) prover
    5.69 -        max_relevant fudge hyp_ts concl_t facts =
    5.70 +        ({fact_thresholds = (thres0, thres1), ...} : params) prover
    5.71 +        max_facts fudge hyp_ts concl_t facts =
    5.72    let
    5.73      val thy = Proof_Context.theory_of ctxt
    5.74      val is_built_in_const =
    5.75 @@ -523,7 +522,7 @@
    5.76          SOME fudge => fudge
    5.77        | NONE => Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover
    5.78      val decay = Math.pow ((1.0 - thres1) / (1.0 - thres0),
    5.79 -                          1.0 / Real.fromInt (max_relevant + 1))
    5.80 +                          1.0 / Real.fromInt (max_facts + 1))
    5.81    in
    5.82      trace_msg ctxt (fn () => "Considering " ^ string_of_int (length facts) ^
    5.83                               " facts");
    5.84 @@ -532,8 +531,8 @@
    5.85       else if thres0 > 1.0 orelse thres0 > thres1 then
    5.86         []
    5.87       else
    5.88 -       relevance_filter ctxt thres0 decay max_relevant is_built_in_const
    5.89 -           fudge facts hyp_ts
    5.90 +       relevance_filter ctxt thres0 decay max_facts is_built_in_const fudge
    5.91 +           facts hyp_ts
    5.92             (concl_t |> theory_constify fudge (Context.theory_name thy)))
    5.93    end
    5.94  

     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:03 2012 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:03 2012 +0200
     6.3 @@ -313,7 +313,7 @@
     6.4        in File.append path s end
     6.5    in List.app do_thm ths end
     6.6  
     6.7 -fun generate_atp_dependencies ctxt (params as {provers, max_relevant, ...}) thy
     6.8 +fun generate_atp_dependencies ctxt (params as {provers, max_facts, ...}) thy
     6.9                                include_thy file_name =
    6.10    let
    6.11      val path = file_name |> Path.explode
    6.12 @@ -347,7 +347,7 @@
    6.13                  facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
    6.14                val facts =
    6.15                  facts |> iterative_relevant_facts ctxt params (hd provers)
    6.16 -                             (the max_relevant) NONE hyp_ts concl_t
    6.17 +                             (the max_facts) NONE hyp_ts concl_t
    6.18                        |> fold (add_isa_dep facts) isa_deps
    6.19                        |> map fix_name
    6.20              in
    6.21 @@ -378,11 +378,11 @@
    6.22  fun learn_proof thy t ths =
    6.23    ()
    6.24  
    6.25 -fun relevant_facts ctxt params prover max_relevant
    6.26 -        ({add, only, ...} : fact_override) hyp_ts concl_t facts =
    6.27 +fun relevant_facts ctxt params prover max_facts
    6.28 +                   ({add, only, ...} : fact_override) hyp_ts concl_t facts =
    6.29    if only then
    6.30      facts
    6.31 -  else if max_relevant <= 0 then
    6.32 +  else if max_facts <= 0 then
    6.33      []
    6.34    else
    6.35      let
    6.36 @@ -390,10 +390,11 @@
    6.37        fun prepend_facts ths accepts =
    6.38          ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @
    6.39           (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))
    6.40 -        |> take max_relevant
    6.41 +        |> take max_facts
    6.42      in
    6.43 -      iterative_relevant_facts ctxt params prover max_relevant NONE
    6.44 -                               hyp_ts concl_t facts
    6.45 +      facts
    6.46 +      |> iterative_relevant_facts ctxt params prover max_facts NONE hyp_ts
    6.47 +                                  concl_t
    6.48        |> not (null add_ths) ? prepend_facts add_ths
    6.49      end
    6.50  

     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 18 08:44:03 2012 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 18 08:44:03 2012 +0200
     7.3 @@ -82,8 +82,8 @@
     7.4     ("strict", "false"),
     7.5     ("lam_trans", "smart"),
     7.6     ("uncurried_aliases", "smart"),
     7.7 -   ("relevance_thresholds", "0.45 0.85"),
     7.8 -   ("max_relevant", "smart"),
     7.9 +   ("fact_thresholds", "0.45 0.85"),
    7.10 +   ("max_facts", "smart"),
    7.11     ("max_mono_iters", "smart"),
    7.12     ("max_new_mono_instances", "smart"),
    7.13     ("isar_proof", "false"),
    7.14 @@ -93,7 +93,8 @@
    7.15     ("preplay_timeout", "3")]
    7.16  
    7.17  val alias_params =
    7.18 -  [("prover", ("provers", [])),
    7.19 +  [("prover", ("provers", [])), (* legacy *)
    7.20 +   ("max_relevant", ("max_facts", [])), (* legacy *)
    7.21     ("dont_preplay", ("preplay_timeout", ["0"]))]
    7.22  val negated_alias_params =
    7.23    [("no_debug", "debug"),
    7.24 @@ -288,8 +289,8 @@
    7.25      val strict = mode = Auto_Try orelse lookup_bool "strict"
    7.26      val lam_trans = lookup_option lookup_string "lam_trans"
    7.27      val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases"
    7.28 -    val relevance_thresholds = lookup_real_pair "relevance_thresholds"
    7.29 -    val max_relevant = lookup_option lookup_int "max_relevant"
    7.30 +    val fact_thresholds = lookup_real_pair "fact_thresholds"
    7.31 +    val max_facts = lookup_option lookup_int "max_facts"
    7.32      val max_mono_iters = lookup_option lookup_int "max_mono_iters"
    7.33      val max_new_mono_instances =
    7.34        lookup_option lookup_int "max_new_mono_instances"
    7.35 @@ -308,7 +309,7 @@
    7.36      {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
    7.37       provers = provers, type_enc = type_enc, strict = strict,
    7.38       lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
    7.39 -     relevance_thresholds = relevance_thresholds, max_relevant = max_relevant,
    7.40 +     fact_thresholds = fact_thresholds, max_facts = max_facts,
    7.41       max_mono_iters = max_mono_iters,
    7.42       max_new_mono_instances = max_new_mono_instances,  isar_proof = isar_proof,
    7.43       isar_shrink_factor = isar_shrink_factor, slice = slice,
    7.44 @@ -405,12 +406,12 @@
    7.45  val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) []
    7.46  val parse_fact_refs =
    7.47    Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse_Spec.xthm)
    7.48 -val parse_relevance_chunk =
    7.49 +val parse_fact_override_chunk =
    7.50    (Args.add |-- Args.colon |-- parse_fact_refs >> add_fact_override)
    7.51    || (Args.del |-- Args.colon |-- parse_fact_refs >> del_fact_override)
    7.52    || (parse_fact_refs >> only_fact_override)
    7.53  val parse_fact_override =
    7.54 -  Scan.optional (Args.parens (Scan.repeat parse_relevance_chunk
    7.55 +  Scan.optional (Args.parens (Scan.repeat parse_fact_override_chunk
    7.56                                >> merge_fact_overrides))
    7.57                  no_fact_override
    7.58  

     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Jul 18 08:44:03 2012 +0200
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Jul 18 08:44:03 2012 +0200
     8.3 @@ -68,7 +68,7 @@
     8.4        {debug = debug, verbose = verbose, overlord = overlord, blocking = true,
     8.5         provers = provers, type_enc = type_enc, strict = strict,
     8.6         lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
     8.7 -       relevance_thresholds = (1.01, 1.01), max_relevant = SOME (length facts),
     8.8 +       fact_thresholds = (1.01, 1.01), max_facts = SOME (length facts),
     8.9         max_mono_iters = max_mono_iters,
    8.10         max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
    8.11         isar_shrink_factor = isar_shrink_factor, slice = false,
    8.12 @@ -225,7 +225,7 @@
    8.13  
    8.14  fun adjust_reconstructor_params override_params
    8.15          ({debug, verbose, overlord, blocking, provers, type_enc, strict,
    8.16 -         lam_trans, uncurried_aliases, relevance_thresholds, max_relevant,
    8.17 +         lam_trans, uncurried_aliases, fact_thresholds, max_facts,
    8.18           max_mono_iters, max_new_mono_instances, isar_proof, isar_shrink_factor,
    8.19           slice, minimize, timeout, preplay_timeout, expect} : params) =
    8.20    let
    8.21 @@ -241,7 +241,7 @@
    8.22      {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
    8.23       provers = provers, type_enc = type_enc, strict = strict,
    8.24       lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
    8.25 -     max_relevant = max_relevant, relevance_thresholds = relevance_thresholds,
    8.26 +     max_facts = max_facts, fact_thresholds = fact_thresholds,
    8.27       max_mono_iters = max_mono_iters,
    8.28       max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
    8.29       isar_shrink_factor = isar_shrink_factor, slice = slice,
    8.30 @@ -304,8 +304,8 @@
    8.31        case used_facts of
    8.32          SOME used_facts =>
    8.33          (if debug andalso not (null used_facts) then
    8.34 -           facts ~~ (0 upto length facts - 1)
    8.35 -           |> map (fn (fact, j) => fact |> untranslated_fact |> apsnd (K j))
    8.36 +           tag_list 1 facts
    8.37 +           |> map (fn (j, fact) => fact |> untranslated_fact |> apsnd (K j))
    8.38             |> filter_used_facts used_facts
    8.39             |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
    8.40             |> commas

     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Jul 18 08:44:03 2012 +0200
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Jul 18 08:44:03 2012 +0200
     9.3 @@ -27,8 +27,8 @@
     9.4       strict: bool,
     9.5       lam_trans: string option,
     9.6       uncurried_aliases: bool option,
     9.7 -     relevance_thresholds: real * real,
     9.8 -     max_relevant: int option,
     9.9 +     fact_thresholds: real * real,
    9.10 +     max_facts: int option,
    9.11       max_mono_iters: int option,
    9.12       max_new_mono_instances: int option,
    9.13       isar_proof: bool,
    9.14 @@ -110,7 +110,7 @@
    9.15    val is_unit_equational_atp : Proof.context -> string -> bool
    9.16    val is_prover_supported : Proof.context -> string -> bool
    9.17    val is_prover_installed : Proof.context -> string -> bool
    9.18 -  val default_max_relevant_for_prover : Proof.context -> bool -> string -> int
    9.19 +  val default_max_facts_for_prover : Proof.context -> bool -> string -> int
    9.20    val is_unit_equality : term -> bool
    9.21    val is_appropriate_prop_for_prover : Proof.context -> string -> term -> bool
    9.22    val is_built_in_const_for_prover :
    9.23 @@ -188,12 +188,12 @@
    9.24  fun get_slices slice slices =
    9.25    (0 upto length slices - 1) ~~ slices |> not slice ? (List.last #> single)
    9.26  
    9.27 -val reconstructor_default_max_relevant = 20
    9.28 +val reconstructor_default_max_facts = 20
    9.29  
    9.30 -fun default_max_relevant_for_prover ctxt slice name =
    9.31 +fun default_max_facts_for_prover ctxt slice name =
    9.32    let val thy = Proof_Context.theory_of ctxt in
    9.33      if is_reconstructor name then
    9.34 -      reconstructor_default_max_relevant
    9.35 +      reconstructor_default_max_facts
    9.36      else if is_atp thy name then
    9.37        fold (Integer.max o #1 o fst o snd o snd o snd)
    9.38             (get_slices slice (#best_slices (get_atp thy name ()) ctxt)) 0
    9.39 @@ -314,8 +314,8 @@
    9.40     strict: bool,
    9.41     lam_trans: string option,
    9.42     uncurried_aliases: bool option,
    9.43 -   relevance_thresholds: real * real,
    9.44 -   max_relevant: int option,
    9.45 +   fact_thresholds: real * real,
    9.46 +   max_facts: int option,
    9.47     max_mono_iters: int option,
    9.48     max_new_mono_instances: int option,
    9.49     isar_proof: bool,
    9.50 @@ -629,7 +629,7 @@
    9.51            prem_role, best_slices, best_max_mono_iters,
    9.52            best_max_new_mono_instances, ...} : atp_config)
    9.53          (params as {debug, verbose, overlord, type_enc, strict, lam_trans,
    9.54 -                    uncurried_aliases, max_relevant, max_mono_iters,
    9.55 +                    uncurried_aliases, max_facts, max_mono_iters,
    9.56                      max_new_mono_instances, isar_proof, isar_shrink_factor,
    9.57                      slice, timeout, preplay_timeout, ...})
    9.58          minimize_command
    9.59 @@ -711,13 +711,12 @@
    9.60                end
    9.61              fun run_slice time_left (cache_key, cache_value)
    9.62                      (slice, (time_frac, (complete,
    9.63 -                        (key as (best_max_relevant, format, best_type_enc,
    9.64 +                        (key as (best_max_facts, format, best_type_enc,
    9.65                                   best_lam_trans, best_uncurried_aliases),
    9.66                                   extra)))) =
    9.67                let
    9.68                  val num_facts =
    9.69 -                  length facts |> is_none max_relevant
    9.70 -                                  ? Integer.min best_max_relevant
    9.71 +                  length facts |> is_none max_facts ? Integer.min best_max_facts
    9.72                  val soundness = if strict then Strict else Non_Strict
    9.73                  val type_enc =
    9.74                    type_enc |> choose_type_enc soundness best_type_enc format

    10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Jul 18 08:44:03 2012 +0200
    10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Jul 18 08:44:03 2012 +0200
    10.3 @@ -62,7 +62,7 @@
    10.4     (if blocking then "."
    10.5      else "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))))
    10.6  
    10.7 -fun launch_prover (params as {debug, verbose, blocking, max_relevant, slice,
    10.8 +fun launch_prover (params as {debug, verbose, blocking, max_facts, slice,
    10.9                                timeout, expect, ...})
   10.10          mode minimize_command only {state, goal, subgoal, subgoal_count, facts}
   10.11          name =
   10.12 @@ -71,10 +71,9 @@
   10.13      val hard_timeout = Time.+ (timeout, timeout)
   10.14      val birth_time = Time.now ()
   10.15      val death_time = Time.+ (birth_time, hard_timeout)
   10.16 -    val max_relevant =
   10.17 -      max_relevant
   10.18 -      |> the_default (default_max_relevant_for_prover ctxt slice name)
   10.19 -    val num_facts = length facts |> not only ? Integer.min max_relevant
   10.20 +    val max_facts =
   10.21 +      max_facts |> the_default (default_max_facts_for_prover ctxt slice name)
   10.22 +    val num_facts = length facts |> not only ? Integer.min max_facts
   10.23      fun desc () =
   10.24        prover_description ctxt params name num_facts subgoal subgoal_count goal
   10.25      val problem =
   10.26 @@ -153,10 +152,10 @@
   10.27    ctxt |> select_smt_solver name
   10.28         |> SMT_Config.solver_class_of |> SMT_Utils.string_of_class
   10.29  
   10.30 -val auto_try_max_relevant_divisor = 2 (* FUDGE *)
   10.31 +val auto_try_max_facts_divisor = 2 (* FUDGE *)
   10.32  
   10.33 -fun run_sledgehammer (params as {debug, verbose, blocking, provers,
   10.34 -                                 max_relevant, slice, ...})
   10.35 +fun run_sledgehammer (params as {debug, verbose, blocking, provers, max_facts,
   10.36 +                                 slice, ...})
   10.37          mode i (fact_override as {only, ...}) minimize_command state =
   10.38    if null provers then
   10.39      error "No prover is set."
   10.40 @@ -207,22 +206,20 @@
   10.41          end
   10.42        fun get_facts label is_appropriate_prop provers =
   10.43          let
   10.44 -          val max_max_relevant =
   10.45 -            case max_relevant of
   10.46 +          val max_max_facts =
   10.47 +            case max_facts of
   10.48                SOME n => n
   10.49              | NONE =>
   10.50 -              0 |> fold (Integer.max
   10.51 -                         o default_max_relevant_for_prover ctxt slice)
   10.52 +              0 |> fold (Integer.max o default_max_facts_for_prover ctxt slice)
   10.53                          provers
   10.54 -                |> mode = Auto_Try
   10.55 -                   ? (fn n => n div auto_try_max_relevant_divisor)
   10.56 +                |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor)
   10.57          in
   10.58            facts
   10.59            |> (case is_appropriate_prop of
   10.60                  SOME is_app => filter (is_app o prop_of o snd)
   10.61                | NONE => I)
   10.62 -          |> relevant_facts ctxt params (hd provers) max_max_relevant
   10.63 -                            fact_override hyp_ts concl_t
   10.64 +          |> relevant_facts ctxt params (hd provers) max_max_facts fact_override
   10.65 +                            hyp_ts concl_t
   10.66            |> map (apfst (apfst (fn name => name ())))
   10.67            |> tap (fn facts =>
   10.68                       if debug then