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 @@ -461,12 +461,11 @@
     1.4          val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover_name
     1.5          val facts =
     1.6            Sledgehammer_Fact.nearly_all_facts ctxt ho_atp
     1.7 -              Sledgehammer_Fact.no_relevance_override chained_ths hyp_ts concl_t
     1.8 +              Sledgehammer_Fact.no_fact_override chained_ths hyp_ts concl_t
     1.9            |> filter (is_appropriate_prop o prop_of o snd)
    1.10            |> Sledgehammer_Filter_MaSh.relevant_facts ctxt params prover_name
    1.11                   (the_default default_max_relevant max_relevant)
    1.12 -                 Sledgehammer_Fact.no_relevance_override chained_ths hyp_ts
    1.13 -                 concl_t
    1.14 +                 Sledgehammer_Fact.no_fact_override hyp_ts concl_t
    1.15          val problem =
    1.16            {state = st', goal = goal, subgoal = i,
    1.17             subgoal_count = Sledgehammer_Util.subgoal_count st,
    1.18 @@ -628,13 +627,13 @@
    1.19            #> fst
    1.20          val thms = named_thms |> maps snd
    1.21          val facts = named_thms |> map (ref_of_str o fst o fst)
    1.22 -        val relevance_override = {add = facts, del = [], only = true}
    1.23 +        val fact_override = {add = facts, del = [], only = true}
    1.24          fun my_timeout time_slice =
    1.25            timeout |> Time.toReal |> curry Real.* time_slice |> Time.fromReal
    1.26          fun sledge_tac time_slice prover type_enc =
    1.27            Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
    1.28 -            (override_params prover type_enc (my_timeout time_slice))
    1.29 -            relevance_override
    1.30 +              (override_params prover type_enc (my_timeout time_slice))
    1.31 +              fact_override
    1.32        in
    1.33          if !reconstructor = "sledgehammer_tac" then
    1.34            sledge_tac 0.2 ATP_Systems.z3_tptpN "mono_native"

     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 @@ -129,12 +129,11 @@
     2.4           val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
     2.5           val facts =
     2.6             Sledgehammer_Fact.nearly_all_facts ctxt ho_atp
     2.7 -               Sledgehammer_Fact.no_relevance_override chained_ths hyp_ts concl_t
     2.8 +               Sledgehammer_Fact.no_fact_override chained_ths hyp_ts concl_t
     2.9             |> filter (is_appropriate_prop o prop_of o snd)
    2.10             |> Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
    2.11                    default_prover (the_default default_max_relevant max_relevant)
    2.12 -                  (SOME relevance_fudge) Sledgehammer_Fact.no_relevance_override
    2.13 -                  chained_ths hyp_ts concl_t
    2.14 +                  (SOME relevance_fudge) hyp_ts concl_t
    2.15              |> map ((fn name => name ()) o fst o fst)
    2.16           val (found_facts, lost_facts) =
    2.17             flat proofs |> sort_distinct string_ord

     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 @@ -114,8 +114,9 @@
     3.4          val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
     3.5          val isa_facts = sugg_facts hyp_ts concl_t facts isa_deps
     3.6          val iter_facts =
     3.7 -          iter_facts ctxt params (max_relevant_slack * the max_relevant) goal
     3.8 -                     facts
     3.9 +          Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
    3.10 +              prover_name (max_relevant_slack * the max_relevant) NONE hyp_ts
    3.11 +              concl_t facts
    3.12          val mash_facts = sugg_facts hyp_ts concl_t facts suggs
    3.13          val iter_mash_facts = hybrid_facts (iter_facts, mash_facts)
    3.14          val iter_s = prove iter_ok iterN iter_facts goal

     4.1 --- a/src/HOL/TPTP/mash_export.ML	Wed Jul 18 08:44:03 2012 +0200
     4.2 +++ b/src/HOL/TPTP/mash_export.ML	Wed Jul 18 08:44:03 2012 +0200
     4.3 @@ -46,7 +46,8 @@
     4.4      val parents = parent_thms thy_ths thy
     4.5    in fold do_fact new_facts parents; () end
     4.6  
     4.7 -fun generate_iter_suggestions ctxt params thy max_relevant file_name =
     4.8 +fun generate_iter_suggestions ctxt (params as {provers, ...}) thy max_relevant
     4.9 +                              file_name =
    4.10    let
    4.11      val path = file_name |> Path.explode
    4.12      val _ = File.write path ""
    4.13 @@ -58,14 +59,17 @@
    4.14        let
    4.15          val name = Thm.get_name_hint th
    4.16          val goal = goal_of_thm thy th
    4.17 +        val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
    4.18          val kind = Thm.legacy_get_kind th
    4.19          val _ =
    4.20            if kind <> "" then
    4.21              let
    4.22                val suggs =
    4.23 -                old_facts |> iter_facts ctxt params max_relevant goal
    4.24 -                          |> map (fn ((name, _), _) => fact_name_of (name ()))
    4.25 -                          |> sort string_ord
    4.26 +                old_facts
    4.27 +                |> Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
    4.28 +                                (hd provers) max_relevant NONE hyp_ts concl_t
    4.29 +                |> map (fn ((name, _), _) => fact_name_of (name ()))
    4.30 +                |> sort string_ord
    4.31                val s = fact_name_of name ^ ": " ^ space_implode " " suggs ^ "\n"
    4.32              in File.append path s end
    4.33            else

     5.1 --- a/src/HOL/TPTP/sledgehammer_tactics.ML	Wed Jul 18 08:44:03 2012 +0200
     5.2 +++ b/src/HOL/TPTP/sledgehammer_tactics.ML	Wed Jul 18 08:44:03 2012 +0200
     5.3 @@ -7,14 +7,12 @@
     5.4  
     5.5  signature SLEDGEHAMMER_TACTICS =
     5.6  sig
     5.7 -  type relevance_override = Sledgehammer_Fact.relevance_override
     5.8 +  type fact_override = Sledgehammer_Fact.fact_override
     5.9  
    5.10    val sledgehammer_with_metis_tac :
    5.11 -    Proof.context -> (string * string) list -> relevance_override -> int
    5.12 -    -> tactic
    5.13 +    Proof.context -> (string * string) list -> fact_override -> int -> tactic
    5.14    val sledgehammer_as_oracle_tac :
    5.15 -    Proof.context -> (string * string) list -> relevance_override -> int
    5.16 -    -> tactic
    5.17 +    Proof.context -> (string * string) list -> fact_override -> int -> tactic
    5.18  end;
    5.19  
    5.20  structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
    5.21 @@ -22,10 +20,9 @@
    5.22  
    5.23  open Sledgehammer_Fact
    5.24  
    5.25 -fun run_prover override_params relevance_override i n ctxt goal =
    5.26 +fun run_prover override_params fact_override i n ctxt goal =
    5.27    let
    5.28      val mode = Sledgehammer_Provers.Normal
    5.29 -    val chained_ths = [] (* a tactic has no chained ths *)
    5.30      val params as {provers, max_relevant, slice, ...} =
    5.31        Sledgehammer_Isar.default_params ctxt override_params
    5.32      val name = hd provers
    5.33 @@ -35,11 +32,11 @@
    5.34      val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
    5.35      val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
    5.36      val facts =
    5.37 -      Sledgehammer_Fact.nearly_all_facts ctxt ho_atp relevance_override
    5.38 -                                         chained_ths hyp_ts concl_t
    5.39 +      Sledgehammer_Fact.nearly_all_facts ctxt ho_atp fact_override []
    5.40 +                                         hyp_ts concl_t
    5.41        |> Sledgehammer_Filter_MaSh.relevant_facts ctxt params name
    5.42 -             (the_default default_max_relevant max_relevant) relevance_override
    5.43 -             chained_ths hyp_ts concl_t
    5.44 +             (the_default default_max_relevant max_relevant) fact_override
    5.45 +             hyp_ts concl_t
    5.46      val problem =
    5.47        {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
    5.48         facts = facts |> map (apfst (apfst (fn name => name ())))
    5.49 @@ -64,27 +61,23 @@
    5.50      |> Source.exhaust
    5.51    end
    5.52  
    5.53 -fun sledgehammer_with_metis_tac ctxt override_params relevance_override i th =
    5.54 -  let
    5.55 -    val override_params =
    5.56 -      override_params @
    5.57 -      [("preplay_timeout", "0")]
    5.58 -  in
    5.59 -    case run_prover override_params relevance_override i i ctxt th of
    5.60 +fun sledgehammer_with_metis_tac ctxt override_params fact_override i th =
    5.61 +  let val override_params = override_params @ [("preplay_timeout", "0")] in
    5.62 +    case run_prover override_params fact_override i i ctxt th of
    5.63        SOME facts =>
    5.64        Metis_Tactic.metis_tac [] ATP_Problem_Generate.combs_or_liftingN ctxt
    5.65            (maps (thms_of_name ctxt) facts) i th
    5.66      | NONE => Seq.empty
    5.67    end
    5.68  
    5.69 -fun sledgehammer_as_oracle_tac ctxt override_params relevance_override i th =
    5.70 +fun sledgehammer_as_oracle_tac ctxt override_params fact_override i th =
    5.71    let
    5.72      val thy = Proof_Context.theory_of ctxt
    5.73      val override_params =
    5.74        override_params @
    5.75        [("preplay_timeout", "0"),
    5.76         ("minimize", "false")]
    5.77 -    val xs = run_prover override_params relevance_override i i ctxt th
    5.78 +    val xs = run_prover override_params fact_override i i ctxt th
    5.79    in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
    5.80  
    5.81  end;

     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Jul 18 08:44:03 2012 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Jul 18 08:44:03 2012 +0200
     6.3 @@ -10,14 +10,14 @@
     6.4    type status = ATP_Problem_Generate.status
     6.5    type stature = ATP_Problem_Generate.stature
     6.6  
     6.7 -  type relevance_override =
     6.8 +  type fact_override =
     6.9      {add : (Facts.ref * Attrib.src list) list,
    6.10       del : (Facts.ref * Attrib.src list) list,
    6.11       only : bool}
    6.12  
    6.13    val ignore_no_atp : bool Config.T
    6.14    val instantiate_inducts : bool Config.T
    6.15 -  val no_relevance_override : relevance_override
    6.16 +  val no_fact_override : fact_override
    6.17    val fact_from_ref :
    6.18      Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
    6.19      -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
    6.20 @@ -32,7 +32,7 @@
    6.21      -> (((unit -> string) * stature) * thm) list
    6.22    val all_facts_of : theory -> (((unit -> string) * stature) * thm) list
    6.23    val nearly_all_facts :
    6.24 -    Proof.context -> bool -> relevance_override -> thm list -> term list -> term
    6.25 +    Proof.context -> bool -> fact_override -> thm list -> term list -> term
    6.26      -> (((unit -> string) * stature) * thm) list
    6.27  end;
    6.28  
    6.29 @@ -43,7 +43,7 @@
    6.30  open Metis_Tactic
    6.31  open Sledgehammer_Util
    6.32  
    6.33 -type relevance_override =
    6.34 +type fact_override =
    6.35    {add : (Facts.ref * Attrib.src list) list,
    6.36     del : (Facts.ref * Attrib.src list) list,
    6.37     only : bool}
    6.38 @@ -56,7 +56,7 @@
    6.39  val instantiate_inducts =
    6.40    Attrib.setup_config_bool @{binding sledgehammer_instantiate_inducts} (K false)
    6.41  
    6.42 -val no_relevance_override = {add = [], del = [], only = false}
    6.43 +val no_fact_override = {add = [], del = [], only = false}
    6.44  
    6.45  fun needs_quoting reserved s =
    6.46    Symtab.defined reserved s orelse
    6.47 @@ -424,23 +424,27 @@
    6.48      |> rev (* try to restore the original order of facts, for MaSh *)
    6.49    end
    6.50  
    6.51 -fun nearly_all_facts ctxt ho_atp ({add, only, ...} : relevance_override)
    6.52 -                     chained_ths hyp_ts concl_t =
    6.53 +fun nearly_all_facts ctxt ho_atp {add, del, only} chained_ths hyp_ts concl_t =
    6.54    if only andalso null add then
    6.55      []
    6.56    else
    6.57      let
    6.58 +      val chained_ths =
    6.59 +        chained_ths
    6.60 +        |> maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th])
    6.61        val reserved = reserved_isar_keyword_table ()
    6.62 -      val add_ths = Attrib.eval_thms ctxt add
    6.63        val css_table = clasimpset_rule_table_of ctxt
    6.64      in
    6.65        (if only then
    6.66           maps (map (fn ((name, stature), th) => ((K name, stature), th))
    6.67                 o fact_from_ref ctxt reserved chained_ths css_table) add
    6.68         else
    6.69 -         all_facts ctxt ho_atp reserved false add_ths chained_ths css_table)
    6.70 +         let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in
    6.71 +           all_facts ctxt ho_atp reserved false add chained_ths css_table
    6.72 +           |> filter_out (member Thm.eq_thm_prop del o snd)
    6.73 +           |> maybe_filter_no_atps ctxt
    6.74 +         end)
    6.75        |> maybe_instantiate_inducts ctxt hyp_ts concl_t
    6.76 -      |> not only ? maybe_filter_no_atps ctxt
    6.77        |> uniquify
    6.78      end
    6.79  

     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML	Wed Jul 18 08:44:03 2012 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML	Wed Jul 18 08:44:03 2012 +0200
     7.3 @@ -8,7 +8,6 @@
     7.4  signature SLEDGEHAMMER_FILTER_ITER =
     7.5  sig
     7.6    type stature = ATP_Problem_Generate.stature
     7.7 -  type relevance_override = Sledgehammer_Fact.relevance_override
     7.8    type params = Sledgehammer_Provers.params
     7.9    type relevance_fudge = Sledgehammer_Provers.relevance_fudge
    7.10  
    7.11 @@ -20,8 +19,7 @@
    7.12      -> string list
    7.13    val iterative_relevant_facts :
    7.14      Proof.context -> params -> string -> int -> relevance_fudge option
    7.15 -    -> relevance_override -> thm list -> term list -> term
    7.16 -    -> (((unit -> string) * stature) * thm) list
    7.17 +    -> term list -> term -> (((unit -> string) * stature) * thm) list
    7.18      -> (((unit -> string) * stature) * thm) list
    7.19  end;
    7.20  
    7.21 @@ -29,7 +27,6 @@
    7.22  struct
    7.23  
    7.24  open ATP_Problem_Generate
    7.25 -open Sledgehammer_Fact
    7.26  open Sledgehammer_Provers
    7.27  
    7.28  val trace =
    7.29 @@ -397,12 +394,15 @@
    7.30  val special_fact_index = 75
    7.31  
    7.32  fun relevance_filter ctxt thres0 decay max_relevant is_built_in_const
    7.33 -        (fudge as {threshold_divisor, ridiculous_threshold, ...})
    7.34 -        ({del, ...} : relevance_override) facts chained_ts hyp_ts concl_t =
    7.35 +        (fudge as {threshold_divisor, ridiculous_threshold, ...}) facts hyp_ts
    7.36 +        concl_t =
    7.37    let
    7.38      val thy = Proof_Context.theory_of ctxt
    7.39      val const_tab = fold (count_fact_consts thy fudge) facts Symtab.empty
    7.40      val add_pconsts = add_pconsts_in_term thy is_built_in_const false o SOME
    7.41 +    val chained_ts =
    7.42 +      facts |> map_filter (fn ((_, (Chained, _)), th) => SOME (prop_of th)
    7.43 +                            | _ => NONE)
    7.44      val chained_const_tab = Symtab.empty |> fold (add_pconsts true) chained_ts
    7.45      val goal_const_tab =
    7.46        Symtab.empty |> fold (add_pconsts true) hyp_ts
    7.47 @@ -410,8 +410,6 @@
    7.48        |> (fn tab => if Symtab.is_empty tab then chained_const_tab else tab)
    7.49        |> fold (if_empty_replace_with_scope thy is_built_in_const facts)
    7.50                [Chained, Assum, Local]
    7.51 -    val del_ths = Attrib.eval_thms ctxt del
    7.52 -    val facts = facts |> filter_out (member Thm.eq_thm_prop del_ths o snd)
    7.53      fun iter j remaining_max thres rel_const_tab hopeless hopeful =
    7.54        let
    7.55          fun relevant [] _ [] =
    7.56 @@ -515,7 +513,7 @@
    7.57  
    7.58  fun iterative_relevant_facts ctxt
    7.59          ({relevance_thresholds = (thres0, thres1), ...} : params) prover
    7.60 -        max_relevant fudge override chained_ths hyp_ts concl_t facts =
    7.61 +        max_relevant fudge hyp_ts concl_t facts =
    7.62    let
    7.63      val thy = Proof_Context.theory_of ctxt
    7.64      val is_built_in_const =
    7.65 @@ -535,7 +533,7 @@
    7.66         []
    7.67       else
    7.68         relevance_filter ctxt thres0 decay max_relevant is_built_in_const
    7.69 -           fudge override facts (chained_ths |> map prop_of) hyp_ts
    7.70 +           fudge facts hyp_ts
    7.71             (concl_t |> theory_constify fudge (Context.theory_name thy)))
    7.72    end
    7.73  

     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:03 2012 +0200
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:03 2012 +0200
     8.3 @@ -9,7 +9,7 @@
     8.4    type status = ATP_Problem_Generate.status
     8.5    type stature = ATP_Problem_Generate.stature
     8.6    type params = Sledgehammer_Provers.params
     8.7 -  type relevance_override = Sledgehammer_Fact.relevance_override
     8.8 +  type fact_override = Sledgehammer_Fact.fact_override
     8.9    type relevance_fudge = Sledgehammer_Provers.relevance_fudge
    8.10    type prover_result = Sledgehammer_Provers.prover_result
    8.11  
    8.12 @@ -24,10 +24,6 @@
    8.13    val features_of : theory -> status * thm -> string list
    8.14    val isabelle_dependencies_of : string list -> thm -> string list
    8.15    val goal_of_thm : theory -> thm -> thm
    8.16 -  val iter_facts :
    8.17 -    Proof.context -> params -> int -> thm
    8.18 -    -> (((unit -> string) * stature) * thm) list
    8.19 -    -> (((unit -> string) * stature) * thm) list
    8.20    val run_prover :
    8.21      Proof.context -> params -> (((unit -> string) * stature) * thm) list -> thm
    8.22      -> prover_result
    8.23 @@ -45,8 +41,8 @@
    8.24    val learn_proof : theory -> term -> thm list -> unit
    8.25  
    8.26    val relevant_facts :
    8.27 -    Proof.context -> params -> string -> int -> relevance_override -> thm list
    8.28 -    -> term list -> term -> (((unit -> string) * stature) * thm) list
    8.29 +    Proof.context -> params -> string -> int -> fact_override -> term list
    8.30 +    -> term -> (((unit -> string) * stature) * thm) list
    8.31      -> (((unit -> string) * stature) * thm) list
    8.32  end;
    8.33  
    8.34 @@ -80,8 +76,6 @@
    8.35  
    8.36  (*** Isabelle helpers ***)
    8.37  
    8.38 -val fact_name_of = prefix fact_prefix o ascii_of
    8.39 -
    8.40  fun escape_meta_char c =
    8.41    if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse
    8.42       c = #")" orelse c = #"," then
    8.43 @@ -255,12 +249,6 @@
    8.44  
    8.45  fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init
    8.46  
    8.47 -fun iter_facts ctxt (params as {provers, ...}) max_relevant goal =
    8.48 -  let val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 in
    8.49 -    iterative_relevant_facts ctxt params (hd provers) max_relevant NONE
    8.50 -                             no_relevance_override [] hyp_ts concl_t
    8.51 -  end
    8.52 -
    8.53  fun run_prover ctxt (params as {provers, ...}) facts goal =
    8.54    let
    8.55      val problem =
    8.56 @@ -325,7 +313,7 @@
    8.57        in File.append path s end
    8.58    in List.app do_thm ths end
    8.59  
    8.60 -fun generate_atp_dependencies ctxt (params as {max_relevant, ...}) thy
    8.61 +fun generate_atp_dependencies ctxt (params as {provers, max_relevant, ...}) thy
    8.62                                include_thy file_name =
    8.63    let
    8.64      val path = file_name |> Path.explode
    8.65 @@ -348,6 +336,7 @@
    8.66        let
    8.67          val name = Thm.get_name_hint th
    8.68          val goal = goal_of_thm thy th
    8.69 +        val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
    8.70          val deps =
    8.71            case isabelle_dependencies_of all_names th of
    8.72              [] => []
    8.73 @@ -357,7 +346,8 @@
    8.74                val facts =
    8.75                  facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
    8.76                val facts =
    8.77 -                facts |> iter_facts ctxt params (the max_relevant) goal
    8.78 +                facts |> iterative_relevant_facts ctxt params (hd provers)
    8.79 +                             (the max_relevant) NONE hyp_ts concl_t
    8.80                        |> fold (add_isa_dep facts) isa_deps
    8.81                        |> map fix_name
    8.82              in
    8.83 @@ -385,12 +375,11 @@
    8.84  fun learn_thy thy timeout =
    8.85    ()
    8.86  
    8.87 -fun learn_proof thy t thms =
    8.88 +fun learn_proof thy t ths =
    8.89    ()
    8.90  
    8.91  fun relevant_facts ctxt params prover max_relevant
    8.92 -                   (override as {add, only, ...}) chained_ths hyp_ts concl_t
    8.93 -                   facts =
    8.94 +        ({add, only, ...} : fact_override) hyp_ts concl_t facts =
    8.95    if only then
    8.96      facts
    8.97    else if max_relevant <= 0 then
    8.98 @@ -398,13 +387,13 @@
    8.99    else
   8.100      let
   8.101        val add_ths = Attrib.eval_thms ctxt add
   8.102 -      fun prepend_facts ths facts =
   8.103 +      fun prepend_facts ths accepts =
   8.104          ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @
   8.105 -         (facts |> filter_out (member Thm.eq_thm_prop ths o snd)))
   8.106 +         (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))
   8.107          |> take max_relevant
   8.108      in
   8.109 -      iterative_relevant_facts ctxt params prover max_relevant NONE override
   8.110 -                               chained_ths hyp_ts concl_t facts
   8.111 +      iterative_relevant_facts ctxt params prover max_relevant NONE
   8.112 +                               hyp_ts concl_t facts
   8.113        |> not (null add_ths) ? prepend_facts add_ths
   8.114      end
   8.115  

     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 18 08:44:03 2012 +0200
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 18 08:44:03 2012 +0200
     9.3 @@ -45,18 +45,14 @@
     9.4  
     9.5  (** Sledgehammer commands **)
     9.6  
     9.7 -fun add_relevance_override ns : relevance_override =
     9.8 -  {add = ns, del = [], only = false}
     9.9 -fun del_relevance_override ns : relevance_override =
    9.10 -  {add = [], del = ns, only = false}
    9.11 -fun only_relevance_override ns : relevance_override =
    9.12 -  {add = ns, del = [], only = true}
    9.13 -fun merge_relevance_override_pairwise (r1 : relevance_override)
    9.14 -                                      (r2 : relevance_override) =
    9.15 +fun add_fact_override ns : fact_override = {add = ns, del = [], only = false}
    9.16 +fun del_fact_override ns : fact_override = {add = [], del = ns, only = false}
    9.17 +fun only_fact_override ns : fact_override = {add = ns, del = [], only = true}
    9.18 +fun merge_fact_override_pairwise (r1 : fact_override) (r2 : fact_override) =
    9.19    {add = #add r1 @ #add r2, del = #del r1 @ #del r2,
    9.20     only = #only r1 andalso #only r2}
    9.21 -fun merge_relevance_overrides rs =
    9.22 -  fold merge_relevance_override_pairwise rs (only_relevance_override [])
    9.23 +fun merge_fact_overrides rs =
    9.24 +  fold merge_fact_override_pairwise rs (only_fact_override [])
    9.25  
    9.26  (*** parameters ***)
    9.27  
    9.28 @@ -350,7 +346,7 @@
    9.29      (if i = 1 then "" else " " ^ string_of_int i)
    9.30    end
    9.31  
    9.32 -fun hammer_away override_params subcommand opt_i relevance_override state =
    9.33 +fun hammer_away override_params subcommand opt_i fact_override state =
    9.34    let
    9.35      val ctxt = Proof.context_of state
    9.36      val override_params = override_params |> map (normalize_raw_param ctxt)
    9.37 @@ -358,7 +354,7 @@
    9.38      if subcommand = runN then
    9.39        let val i = the_default 1 opt_i in
    9.40          run_sledgehammer (get_params Normal ctxt override_params) Normal i
    9.41 -                         relevance_override (minimize_command override_params i)
    9.42 +                         fact_override (minimize_command override_params i)
    9.43                           state
    9.44          |> K ()
    9.45        end
    9.46 @@ -366,7 +362,7 @@
    9.47        run_minimize (get_params Minimize ctxt
    9.48                                 (("provers", [default_minimize_prover]) ::
    9.49                                  override_params))
    9.50 -                   (the_default 1 opt_i) (#add relevance_override) state
    9.51 +                   (the_default 1 opt_i) (#add fact_override) state
    9.52      else if subcommand = messagesN then
    9.53        messages opt_i
    9.54      else if subcommand = supported_proversN then
    9.55 @@ -381,8 +377,8 @@
    9.56        error ("Unknown subcommand: " ^ quote subcommand ^ ".")
    9.57    end
    9.58  
    9.59 -fun sledgehammer_trans (((subcommand, params), relevance_override), opt_i) =
    9.60 -  Toplevel.keep (hammer_away params subcommand opt_i relevance_override
    9.61 +fun sledgehammer_trans (((subcommand, params), fact_override), opt_i) =
    9.62 +  Toplevel.keep (hammer_away params subcommand opt_i fact_override
    9.63                   o Toplevel.proof_of)
    9.64  
    9.65  fun string_for_raw_param (name, value) = name ^ " = " ^ implode_param value
    9.66 @@ -410,19 +406,19 @@
    9.67  val parse_fact_refs =
    9.68    Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse_Spec.xthm)
    9.69  val parse_relevance_chunk =
    9.70 -  (Args.add |-- Args.colon |-- parse_fact_refs >> add_relevance_override)
    9.71 -  || (Args.del |-- Args.colon |-- parse_fact_refs >> del_relevance_override)
    9.72 -  || (parse_fact_refs >> only_relevance_override)
    9.73 -val parse_relevance_override =
    9.74 +  (Args.add |-- Args.colon |-- parse_fact_refs >> add_fact_override)
    9.75 +  || (Args.del |-- Args.colon |-- parse_fact_refs >> del_fact_override)
    9.76 +  || (parse_fact_refs >> only_fact_override)
    9.77 +val parse_fact_override =
    9.78    Scan.optional (Args.parens (Scan.repeat parse_relevance_chunk
    9.79 -                              >> merge_relevance_overrides))
    9.80 -                no_relevance_override
    9.81 +                              >> merge_fact_overrides))
    9.82 +                no_fact_override
    9.83  
    9.84  val _ =
    9.85    Outer_Syntax.improper_command @{command_spec "sledgehammer"}
    9.86      "search for first-order proof using automatic theorem provers"
    9.87      ((Scan.optional Parse.short_ident runN -- parse_params
    9.88 -      -- parse_relevance_override -- Scan.option Parse.nat) #>> sledgehammer_trans)
    9.89 +      -- parse_fact_override -- Scan.option Parse.nat) #>> sledgehammer_trans)
    9.90  val _ =
    9.91    Outer_Syntax.command @{command_spec "sledgehammer_params"}
    9.92      "set and display the default parameters for Sledgehammer"
    9.93 @@ -434,7 +430,7 @@
    9.94      val mode = if auto then Auto_Try else Try
    9.95      val i = 1
    9.96    in
    9.97 -    run_sledgehammer (get_params mode ctxt []) mode i no_relevance_override
    9.98 +    run_sledgehammer (get_params mode ctxt []) mode i no_fact_override
    9.99                       (minimize_command [] i) state
   9.100    end
   9.101  

    10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Jul 18 08:44:03 2012 +0200
    10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Jul 18 08:44:03 2012 +0200
    10.3 @@ -327,7 +327,7 @@
    10.4    let
    10.5      val ctxt = Proof.context_of state
    10.6      val reserved = reserved_isar_keyword_table ()
    10.7 -    val chained_ths = normalize_chained_theorems (#facts (Proof.goal state))
    10.8 +    val chained_ths = #facts (Proof.goal state)
    10.9      val css_table = clasimpset_rule_table_of ctxt
   10.10      val facts =
   10.11        refs |> maps (map (apsnd single)

    11.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Jul 18 08:44:03 2012 +0200
    11.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Jul 18 08:44:03 2012 +0200
    11.3 @@ -9,7 +9,7 @@
    11.4  signature SLEDGEHAMMER_RUN =
    11.5  sig
    11.6    type minimize_command = ATP_Proof_Reconstruct.minimize_command
    11.7 -  type relevance_override = Sledgehammer_Fact.relevance_override
    11.8 +  type fact_override = Sledgehammer_Fact.fact_override
    11.9    type mode = Sledgehammer_Provers.mode
   11.10    type params = Sledgehammer_Provers.params
   11.11  
   11.12 @@ -18,7 +18,7 @@
   11.13    val timeoutN : string
   11.14    val unknownN : string
   11.15    val run_sledgehammer :
   11.16 -    params -> mode -> int -> relevance_override
   11.17 +    params -> mode -> int -> fact_override
   11.18      -> ((string * string list) list -> string -> minimize_command)
   11.19      -> Proof.state -> bool * (string * Proof.state)
   11.20  end;
   11.21 @@ -157,7 +157,7 @@
   11.22  
   11.23  fun run_sledgehammer (params as {debug, verbose, blocking, provers,
   11.24                                   max_relevant, slice, ...})
   11.25 -        mode i (relevance_override as {only, ...}) minimize_command state =
   11.26 +        mode i (fact_override as {only, ...}) minimize_command state =
   11.27    if null provers then
   11.28      error "No prover is set."
   11.29    else case subgoal_count state of
   11.30 @@ -170,12 +170,10 @@
   11.31          state |> Proof.map_context (Config.put SMT_Config.verbose debug)
   11.32        val ctxt = Proof.context_of state
   11.33        val {facts = chained_ths, goal, ...} = Proof.goal state
   11.34 -      val chained_ths = chained_ths |> normalize_chained_theorems
   11.35        val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i
   11.36        val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
   11.37        val facts =
   11.38 -        nearly_all_facts ctxt ho_atp relevance_override chained_ths hyp_ts
   11.39 -                         concl_t
   11.40 +        nearly_all_facts ctxt ho_atp fact_override chained_ths hyp_ts concl_t
   11.41        val _ = () |> not blocking ? kill_provers
   11.42        val _ = case find_first (not o is_prover_supported ctxt) provers of
   11.43                  SOME name => error ("No such prover: " ^ name ^ ".")
   11.44 @@ -224,7 +222,7 @@
   11.45                  SOME is_app => filter (is_app o prop_of o snd)
   11.46                | NONE => I)
   11.47            |> relevant_facts ctxt params (hd provers) max_max_relevant
   11.48 -                            relevance_override chained_ths hyp_ts concl_t
   11.49 +                            fact_override hyp_ts concl_t
   11.50            |> map (apfst (apfst (fn name => name ())))
   11.51            |> tap (fn facts =>
   11.52                       if debug then

    12.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Jul 18 08:44:03 2012 +0200
    12.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Jul 18 08:44:03 2012 +0200
    12.3 @@ -12,7 +12,6 @@
    12.4    val parse_bool_option : bool -> string -> string -> bool option
    12.5    val parse_time_option : string -> string -> Time.time option
    12.6    val subgoal_count : Proof.state -> int
    12.7 -  val normalize_chained_theorems : thm list -> thm list
    12.8    val reserved_isar_keyword_table : unit -> unit Symtab.table
    12.9    val thms_in_proof : string list option -> thm -> string list
   12.10  end;
   12.11 @@ -55,11 +54,8 @@
   12.12  
   12.13  val subgoal_count = Try.subgoal_count
   12.14  
   12.15 -val normalize_chained_theorems =
   12.16 -  maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th])
   12.17  fun reserved_isar_keyword_table () =
   12.18 -  Keyword.dest () |-> union (op =)
   12.19 -  |> map (rpair ()) |> Symtab.make
   12.20 +  Keyword.dest () |-> union (op =) |> map (rpair ()) |> Symtab.make
   12.21  
   12.22  (* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few
   12.23     fixes that seem to be missing over there; or maybe the two code portions are