further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
authorblanchet
Wed Jul 11 21:43:19 2012 +0200 (2012-07-11)
changeset 482501065c307fafe
parent 48249 2bd242c56c90
child 48251 6cdcfbddc077
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
src/HOL/IsaMakefile
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
src/HOL/Sledgehammer.thy
src/HOL/TPTP/MaSh_Export.thy
src/HOL/TPTP/MaSh_Import.thy
src/HOL/TPTP/ROOT.ML
src/HOL/TPTP/atp_theory_export.ML
src/HOL/TPTP/mash_export.ML
src/HOL/TPTP/mash_import.ML
src/HOL/TPTP/sledgehammer_tactics.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
     1.1 --- a/src/HOL/IsaMakefile	Wed Jul 11 21:43:19 2012 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Wed Jul 11 21:43:19 2012 +0200
     1.3 @@ -371,7 +371,10 @@
     1.4    Tools/record.ML \
     1.5    Tools/semiring_normalizer.ML \
     1.6    Tools/Sledgehammer/async_manager.ML \
     1.7 +  Tools/Sledgehammer/sledgehammer_fact.ML \
     1.8    Tools/Sledgehammer/sledgehammer_filter.ML \
     1.9 +  Tools/Sledgehammer/sledgehammer_filter_iter.ML \
    1.10 +  Tools/Sledgehammer/sledgehammer_filter_mash.ML \
    1.11    Tools/Sledgehammer/sledgehammer_minimize.ML \
    1.12    Tools/Sledgehammer/sledgehammer_isar.ML \
    1.13    Tools/Sledgehammer/sledgehammer_provers.ML \
     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Jul 11 21:43:19 2012 +0200
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Jul 11 21:43:19 2012 +0200
     2.3 @@ -365,7 +365,7 @@
     2.4        hd (#provers (Sledgehammer_Isar.default_params ctxt []))
     2.5        handle List.Empty => error "No ATP available."
     2.6      fun get_prover name =
     2.7 -      (name, Sledgehammer_Run.get_minimizing_prover ctxt
     2.8 +      (name, Sledgehammer_Minimize.get_minimizing_prover ctxt
     2.9                  Sledgehammer_Provers.Normal name)
    2.10    in
    2.11      (case AList.lookup (op =) args proverK of
    2.12 @@ -465,7 +465,7 @@
    2.13                  else raise Fail "inappropriate"
    2.14          val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover_name
    2.15          val facts =
    2.16 -          Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override
    2.17 +          Sledgehammer_Fact.nearly_all_facts ctxt ho_atp relevance_override
    2.18              chained_ths hyp_ts concl_t
    2.19            |> filter (is_appropriate_prop o prop_of o snd)
    2.20            |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
     3.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Wed Jul 11 21:43:19 2012 +0200
     3.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Wed Jul 11 21:43:19 2012 +0200
     3.3 @@ -131,8 +131,8 @@
     3.4           val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal subgoal
     3.5           val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
     3.6           val facts =
     3.7 -          Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override
     3.8 -                                               chained_ths hyp_ts concl_t
     3.9 +          Sledgehammer_Fact.nearly_all_facts ctxt ho_atp relevance_override
    3.10 +                                             chained_ths hyp_ts concl_t
    3.11            |> filter (is_appropriate_prop o prop_of o snd)
    3.12            |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
    3.13                   (the_default default_max_relevant max_relevant)
     4.1 --- a/src/HOL/Sledgehammer.thy	Wed Jul 11 21:43:19 2012 +0200
     4.2 +++ b/src/HOL/Sledgehammer.thy	Wed Jul 11 21:43:19 2012 +0200
     4.3 @@ -11,8 +11,11 @@
     4.4  keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl
     4.5  uses "Tools/Sledgehammer/async_manager.ML"
     4.6       "Tools/Sledgehammer/sledgehammer_util.ML"
     4.7 +     "Tools/Sledgehammer/sledgehammer_fact.ML"
     4.8 +     "Tools/Sledgehammer/sledgehammer_filter_iter.ML"
     4.9 +     "Tools/Sledgehammer/sledgehammer_provers.ML"
    4.10 +     "Tools/Sledgehammer/sledgehammer_filter_mash.ML"
    4.11       "Tools/Sledgehammer/sledgehammer_filter.ML"
    4.12 -     "Tools/Sledgehammer/sledgehammer_provers.ML"
    4.13       "Tools/Sledgehammer/sledgehammer_minimize.ML"
    4.14       "Tools/Sledgehammer/sledgehammer_run.ML"
    4.15       "Tools/Sledgehammer/sledgehammer_isar.ML"
     5.1 --- a/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 11 21:43:19 2012 +0200
     5.2 +++ b/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 11 21:43:19 2012 +0200
     5.3 @@ -18,7 +18,7 @@
     5.4  *}
     5.5  
     5.6  ML {*
     5.7 -val do_it = true (* switch to "true" to generate the files *);
     5.8 +val do_it = false (* switch to "true" to generate the files *);
     5.9  val thy = @{theory Nat}
    5.10  *}
    5.11  
     6.1 --- a/src/HOL/TPTP/MaSh_Import.thy	Wed Jul 11 21:43:19 2012 +0200
     6.2 +++ b/src/HOL/TPTP/MaSh_Import.thy	Wed Jul 11 21:43:19 2012 +0200
     6.3 @@ -9,10 +9,6 @@
     6.4  uses "mash_import.ML"
     6.5  begin
     6.6  
     6.7 -sledgehammer_params
     6.8 -  [max_relevant = 40, strict, dont_slice, type_enc = poly_guards??,
     6.9 -   lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize]
    6.10 -
    6.11  declare [[sledgehammer_instantiate_inducts]]
    6.12  
    6.13  ML {*
    6.14 @@ -20,13 +16,15 @@
    6.15  *}
    6.16  
    6.17  ML {*
    6.18 -val do_it = false (* switch to "true" to generate the files *);
    6.19 +val do_it = true (* switch to "true" to generate the files *);
    6.20  val thy = @{theory List}
    6.21  *}
    6.22  
    6.23  ML {*
    6.24 -if do_it then import_and_evaluate_mash_suggestions @{context} thy "/tmp/mash_suggestions_list"
    6.25 -else ()
    6.26 +if do_it then
    6.27 +  import_and_evaluate_mash_suggestions @{context} thy "/tmp/mash_suggestions_list"
    6.28 +else
    6.29 +  ()
    6.30  *}
    6.31  
    6.32  end
     7.1 --- a/src/HOL/TPTP/ROOT.ML	Wed Jul 11 21:43:19 2012 +0200
     7.2 +++ b/src/HOL/TPTP/ROOT.ML	Wed Jul 11 21:43:19 2012 +0200
     7.3 @@ -7,7 +7,6 @@
     7.4  *)
     7.5  
     7.6  use_thys [
     7.7 -  "ATP_Theory_Export",
     7.8    "MaSh_Import",
     7.9    "TPTP_Interpret",
    7.10    "THF_Arith"
     8.1 --- a/src/HOL/TPTP/atp_theory_export.ML	Wed Jul 11 21:43:19 2012 +0200
     8.2 +++ b/src/HOL/TPTP/atp_theory_export.ML	Wed Jul 11 21:43:19 2012 +0200
     8.3 @@ -61,8 +61,8 @@
     8.4  
     8.5  fun all_facts_of_theory thy =
     8.6    let val ctxt = Proof_Context.init_global thy in
     8.7 -    Sledgehammer_Filter.all_facts ctxt false Symtab.empty true [] []
     8.8 -        (Sledgehammer_Filter.clasimpset_rule_table_of ctxt)
     8.9 +    Sledgehammer_Fact.all_facts ctxt false Symtab.empty true [] []
    8.10 +        (Sledgehammer_Fact.clasimpset_rule_table_of ctxt)
    8.11      |> rev (* try to restore the original order of facts, for MaSh *)
    8.12    end
    8.13  
     9.1 --- a/src/HOL/TPTP/mash_export.ML	Wed Jul 11 21:43:19 2012 +0200
     9.2 +++ b/src/HOL/TPTP/mash_export.ML	Wed Jul 11 21:43:19 2012 +0200
     9.3 @@ -15,7 +15,7 @@
     9.4    val theory_ord : theory * theory -> order
     9.5    val thm_ord : thm * thm -> order
     9.6    val dependencies_of : string list -> thm -> string list
     9.7 -  val goal_of_thm : thm -> thm
     9.8 +  val goal_of_thm : theory -> thm -> thm
     9.9    val meng_paulson_facts :
    9.10      Proof.context -> int -> thm -> (((unit -> string) * stature) * thm) list
    9.11      -> ((string * stature) * thm) list
    9.12 @@ -34,8 +34,9 @@
    9.13  structure MaSh_Export : MASH_EXPORT =
    9.14  struct
    9.15  
    9.16 +open ATP_Util
    9.17  open ATP_Problem_Generate
    9.18 -open ATP_Util
    9.19 +open ATP_Theory_Export
    9.20  
    9.21  type prover_result = Sledgehammer_Provers.prover_result
    9.22  
    9.23 @@ -215,7 +216,7 @@
    9.24    | freeze (Free (s, T)) = Free (s, freezeT T)
    9.25    | freeze t = t
    9.26  
    9.27 -val goal_of_thm = prop_of #> freeze #> cterm_of thy #> Goal.init
    9.28 +fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init
    9.29  
    9.30  fun meng_paulson_facts ctxt max_relevant goal =
    9.31    let
    9.32 @@ -241,7 +242,7 @@
    9.33        {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
    9.34         facts = facts |> map Sledgehammer_Provers.Untranslated_Fact}
    9.35      val prover =
    9.36 -      Sledgehammer_Run.get_minimizing_prover ctxt
    9.37 +      Sledgehammer_Minimize.get_minimizing_prover ctxt
    9.38            Sledgehammer_Provers.Normal (hd provers)
    9.39    in prover params (K (K (K ""))) problem end
    9.40  
    9.41 @@ -320,18 +321,25 @@
    9.42      fun do_thm th =
    9.43        let
    9.44          val name = Thm.get_name_hint th
    9.45 -        val goal = goal_of_thm th
    9.46 -        val isa_deps = dependencies_of all_names th
    9.47 -        val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
    9.48 -        val facts =
    9.49 -          facts |> meng_paulson_facts ctxt (the max_relevant) goal
    9.50 -                |> fold (add_isa_dep facts) isa_deps
    9.51 -                |> map fix_name
    9.52 +        val goal = goal_of_thm thy th
    9.53          val deps =
    9.54 -          case run_sledgehammer ctxt facts goal of
    9.55 -            {outcome = NONE, used_facts, ...} =>
    9.56 -            used_facts |> map fst |> sort string_ord
    9.57 -          | _ => isa_deps
    9.58 +          case dependencies_of all_names th of
    9.59 +            [] => []
    9.60 +          | isa_dep as [_] => isa_dep (* can hardly beat that *)
    9.61 +          | isa_deps =>
    9.62 +            let
    9.63 +              val facts =
    9.64 +                facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
    9.65 +              val facts =
    9.66 +                facts |> meng_paulson_facts ctxt (the max_relevant) goal
    9.67 +                      |> fold (add_isa_dep facts) isa_deps
    9.68 +                      |> map fix_name
    9.69 +            in
    9.70 +              case run_sledgehammer ctxt facts goal of
    9.71 +                {outcome = NONE, used_facts, ...} =>
    9.72 +                used_facts |> map fst |> sort string_ord
    9.73 +              | _ => isa_deps
    9.74 +            end
    9.75          val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n"
    9.76        in File.append path s end
    9.77    in List.app do_thm ths end
    9.78 @@ -374,7 +382,7 @@
    9.79      fun do_fact (fact as (_, th)) old_facts =
    9.80        let
    9.81          val name = Thm.get_name_hint th
    9.82 -        val goal = goal_of_thm th
    9.83 +        val goal = goal_of_thm thy th
    9.84          val kind = Thm.legacy_get_kind th
    9.85          val _ =
    9.86            if kind <> "" then
    10.1 --- a/src/HOL/TPTP/mash_import.ML	Wed Jul 11 21:43:19 2012 +0200
    10.2 +++ b/src/HOL/TPTP/mash_import.ML	Wed Jul 11 21:43:19 2012 +0200
    10.3 @@ -55,7 +55,7 @@
    10.4      fun sugg_facts hyp_ts concl_t facts =
    10.5        map_filter (find_sugg facts o of_fact_name)
    10.6        #> take (max_relevant_slack * the max_relevant)
    10.7 -      #> Sledgehammer_Filter.maybe_instantiate_inducts ctxt hyp_ts concl_t
    10.8 +      #> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t
    10.9        #> map (apfst (apfst (fn name => name ())))
   10.10      fun meng_mash_facts fs1 fs2 =
   10.11        let
   10.12 @@ -106,7 +106,7 @@
   10.13              SOME (_, th) => th
   10.14            | NONE => error ("No fact called \"" ^ name ^ "\"")
   10.15          val deps = dependencies_of all_names th
   10.16 -        val goal = goal_of_thm th
   10.17 +        val goal = goal_of_thm thy th
   10.18          val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
   10.19          val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
   10.20          val deps_facts = sugg_facts hyp_ts concl_t facts deps
   10.21 @@ -133,7 +133,7 @@
   10.22        " " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^
   10.23        Real.fmt (StringCvt.FIX (SOME 1))
   10.24                 (100.0 * Real.fromInt (!ok) / Real.fromInt n) ^ "%)"
   10.25 -    val inst_inducts = Config.get ctxt Sledgehammer_Filter.instantiate_inducts
   10.26 +    val inst_inducts = Config.get ctxt Sledgehammer_Fact.instantiate_inducts
   10.27      val options =
   10.28        [prover_name, string_of_int (the max_relevant) ^ " facts",
   10.29         "slice" |> not slice ? prefix "dont_", the_default "smart" type_enc,
    11.1 --- a/src/HOL/TPTP/sledgehammer_tactics.ML	Wed Jul 11 21:43:19 2012 +0200
    11.2 +++ b/src/HOL/TPTP/sledgehammer_tactics.ML	Wed Jul 11 21:43:19 2012 +0200
    11.3 @@ -39,8 +39,8 @@
    11.4      val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
    11.5      val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
    11.6      val facts =
    11.7 -      Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override
    11.8 -                                           chained_ths hyp_ts concl_t
    11.9 +      Sledgehammer_Fact.nearly_all_facts ctxt ho_atp relevance_override
   11.10 +                                         chained_ths hyp_ts concl_t
   11.11        |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
   11.12               (the_default default_max_relevant max_relevant) is_built_in_const
   11.13               relevance_fudge relevance_override chained_ths hyp_ts concl_t
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Jul 11 21:43:19 2012 +0200
    12.3 @@ -0,0 +1,439 @@
    12.4 +(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_fact.ML
    12.5 +    Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
    12.6 +    Author:     Jasmin Blanchette, TU Muenchen
    12.7 +
    12.8 +Sledgehammer fact handling.
    12.9 +*)
   12.10 +
   12.11 +signature SLEDGEHAMMER_FACT =
   12.12 +sig
   12.13 +  type status = ATP_Problem_Generate.status
   12.14 +  type stature = ATP_Problem_Generate.stature
   12.15 +
   12.16 +  type relevance_override =
   12.17 +    {add : (Facts.ref * Attrib.src list) list,
   12.18 +     del : (Facts.ref * Attrib.src list) list,
   12.19 +     only : bool}
   12.20 +
   12.21 +  val ignore_no_atp : bool Config.T
   12.22 +  val instantiate_inducts : bool Config.T
   12.23 +  val no_relevance_override : relevance_override
   12.24 +  val fact_from_ref :
   12.25 +    Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
   12.26 +    -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
   12.27 +  val all_facts :
   12.28 +    Proof.context -> bool -> 'a Symtab.table -> bool -> thm list
   12.29 +    -> thm list -> status Termtab.table
   12.30 +    -> (((unit -> string) * stature) * thm) list
   12.31 +  val clasimpset_rule_table_of : Proof.context -> status Termtab.table
   12.32 +  val maybe_instantiate_inducts :
   12.33 +    Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
   12.34 +    -> (((unit -> string) * 'a) * thm) list
   12.35 +  val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list
   12.36 +  val nearly_all_facts :
   12.37 +    Proof.context -> bool -> relevance_override -> thm list -> term list -> term
   12.38 +    -> (((unit -> string) * stature) * thm) list
   12.39 +end;
   12.40 +
   12.41 +structure Sledgehammer_Fact : SLEDGEHAMMER_FACT =
   12.42 +struct
   12.43 +
   12.44 +open ATP_Problem_Generate
   12.45 +open Metis_Tactic
   12.46 +open Sledgehammer_Util
   12.47 +
   12.48 +type relevance_override =
   12.49 +  {add : (Facts.ref * Attrib.src list) list,
   12.50 +   del : (Facts.ref * Attrib.src list) list,
   12.51 +   only : bool}
   12.52 +
   12.53 +val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
   12.54 +
   12.55 +(* experimental features *)
   12.56 +val ignore_no_atp =
   12.57 +  Attrib.setup_config_bool @{binding sledgehammer_ignore_no_atp} (K false)
   12.58 +val instantiate_inducts =
   12.59 +  Attrib.setup_config_bool @{binding sledgehammer_instantiate_inducts} (K false)
   12.60 +
   12.61 +val no_relevance_override = {add = [], del = [], only = false}
   12.62 +
   12.63 +fun needs_quoting reserved s =
   12.64 +  Symtab.defined reserved s orelse
   12.65 +  exists (not o Lexicon.is_identifier) (Long_Name.explode s)
   12.66 +
   12.67 +fun make_name reserved multi j name =
   12.68 +  (name |> needs_quoting reserved name ? quote) ^
   12.69 +  (if multi then "(" ^ string_of_int j ^ ")" else "")
   12.70 +
   12.71 +fun explode_interval _ (Facts.FromTo (i, j)) = i upto j
   12.72 +  | explode_interval max (Facts.From i) = i upto i + max - 1
   12.73 +  | explode_interval _ (Facts.Single i) = [i]
   12.74 +
   12.75 +val backquote =
   12.76 +  raw_explode #> map (fn "`" => "\\`" | s => s) #> implode #> enclose "`" "`"
   12.77 +
   12.78 +(* unfolding these can yield really huge terms *)
   12.79 +val risky_defs = @{thms Bit0_def Bit1_def}
   12.80 +
   12.81 +fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs))
   12.82 +fun is_rec_def (@{const Trueprop} $ t) = is_rec_def t
   12.83 +  | is_rec_def (@{const ==>} $ _ $ t2) = is_rec_def t2
   12.84 +  | is_rec_def (Const (@{const_name "=="}, _) $ t1 $ t2) = is_rec_eq t1 t2
   12.85 +  | is_rec_def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2
   12.86 +  | is_rec_def _ = false
   12.87 +
   12.88 +fun is_assum assms th = exists (fn ct => prop_of th aconv term_of ct) assms
   12.89 +fun is_chained chained_ths = member Thm.eq_thm_prop chained_ths
   12.90 +
   12.91 +fun scope_of_thm global assms chained_ths th =
   12.92 +  if is_chained chained_ths th then Chained
   12.93 +  else if global then Global
   12.94 +  else if is_assum assms th then Assum
   12.95 +  else Local
   12.96 +
   12.97 +val may_be_induction =
   12.98 +  exists_subterm (fn Var (_, Type (@{type_name fun}, [_, T])) =>
   12.99 +                     body_type T = @{typ bool}
  12.100 +                   | _ => false)
  12.101 +
  12.102 +fun status_of_thm css_table name th =
  12.103 +  (* FIXME: use structured name *)
  12.104 +  if (String.isSubstring ".induct" name orelse
  12.105 +      String.isSubstring ".inducts" name) andalso
  12.106 +     may_be_induction (prop_of th) then
  12.107 +    Induction
  12.108 +  else case Termtab.lookup css_table (prop_of th) of
  12.109 +    SOME status => status
  12.110 +  | NONE => General
  12.111 +
  12.112 +fun stature_of_thm global assms chained_ths css_table name th =
  12.113 +  (scope_of_thm global assms chained_ths th, status_of_thm css_table name th)
  12.114 +
  12.115 +fun fact_from_ref ctxt reserved chained_ths css_table (xthm as (xref, args)) =
  12.116 +  let
  12.117 +    val ths = Attrib.eval_thms ctxt [xthm]
  12.118 +    val bracket =
  12.119 +      map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args
  12.120 +      |> implode
  12.121 +    fun nth_name j =
  12.122 +      case xref of
  12.123 +        Facts.Fact s => backquote s ^ bracket
  12.124 +      | Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
  12.125 +      | Facts.Named ((name, _), NONE) =>
  12.126 +        make_name reserved (length ths > 1) (j + 1) name ^ bracket
  12.127 +      | Facts.Named ((name, _), SOME intervals) =>
  12.128 +        make_name reserved true
  12.129 +                 (nth (maps (explode_interval (length ths)) intervals) j) name ^
  12.130 +        bracket
  12.131 +  in
  12.132 +    (ths, (0, []))
  12.133 +    |-> fold (fn th => fn (j, rest) =>
  12.134 +                 let val name = nth_name j in
  12.135 +                   (j + 1, ((name, stature_of_thm false [] chained_ths
  12.136 +                                             css_table name th), th) :: rest)
  12.137 +                 end)
  12.138 +    |> snd
  12.139 +  end
  12.140 +
  12.141 +(* Reject theorems with names like "List.filter.filter_list_def" or
  12.142 +  "Accessible_Part.acc.defs", as these are definitions arising from packages. *)
  12.143 +fun is_package_def a =
  12.144 +  let val names = Long_Name.explode a in
  12.145 +    (length names > 2 andalso not (hd names = "local") andalso
  12.146 +     String.isSuffix "_def" a) orelse String.isSuffix "_defs" a
  12.147 +  end
  12.148 +
  12.149 +(* FIXME: put other record thms here, or declare as "no_atp" *)
  12.150 +fun multi_base_blacklist ctxt ho_atp =
  12.151 +  ["defs", "select_defs", "update_defs", "split", "splits", "split_asm",
  12.152 +   "cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong",
  12.153 +   "weak_case_cong"]
  12.154 +  |> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ?
  12.155 +        append ["induct", "inducts"]
  12.156 +  |> map (prefix ".")
  12.157 +
  12.158 +val max_lambda_nesting = 3 (*only applies if not ho_atp*)
  12.159 +
  12.160 +fun term_has_too_many_lambdas max (t1 $ t2) =
  12.161 +    exists (term_has_too_many_lambdas max) [t1, t2]
  12.162 +  | term_has_too_many_lambdas max (Abs (_, _, t)) =
  12.163 +    max = 0 orelse term_has_too_many_lambdas (max - 1) t
  12.164 +  | term_has_too_many_lambdas _ _ = false
  12.165 +
  12.166 +(* Don't count nested lambdas at the level of formulas, since they are
  12.167 +   quantifiers. *)
  12.168 +fun formula_has_too_many_lambdas true _ _ = false (*i.e. ho_atp*)
  12.169 +  | formula_has_too_many_lambdas _ Ts (Abs (_, T, t)) =
  12.170 +      formula_has_too_many_lambdas false (T :: Ts) t
  12.171 +  | formula_has_too_many_lambdas _ Ts t =
  12.172 +    if member (op =) [HOLogic.boolT, propT] (fastype_of1 (Ts, t)) then
  12.173 +      exists (formula_has_too_many_lambdas false Ts) (#2 (strip_comb t))
  12.174 +    else
  12.175 +      term_has_too_many_lambdas max_lambda_nesting t
  12.176 +
  12.177 +(* The max apply depth of any "metis" call in "Metis_Examples" (on 2007-10-31)
  12.178 +   was 11. *)
  12.179 +val max_apply_depth = 15
  12.180 +
  12.181 +fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1)
  12.182 +  | apply_depth (Abs (_, _, t)) = apply_depth t
  12.183 +  | apply_depth _ = 0
  12.184 +
  12.185 +fun is_formula_too_complex ho_atp t =
  12.186 +  apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas ho_atp [] t
  12.187 +
  12.188 +(* FIXME: Extend to "Meson" and "Metis" *)
  12.189 +val exists_sledgehammer_const =
  12.190 +  exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)
  12.191 +
  12.192 +(* FIXME: make more reliable *)
  12.193 +val exists_low_level_class_const =
  12.194 +  exists_Const (fn (s, _) =>
  12.195 +     s = @{const_name equal_class.equal} orelse
  12.196 +     String.isSubstring (Long_Name.separator ^ "class" ^ Long_Name.separator) s)
  12.197 +
  12.198 +fun is_metastrange_theorem th =
  12.199 +  case head_of (concl_of th) of
  12.200 +    Const (s, _) => (s <> @{const_name Trueprop} andalso
  12.201 +                     s <> @{const_name "=="})
  12.202 +  | _ => false
  12.203 +
  12.204 +fun is_that_fact th =
  12.205 +  String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th)
  12.206 +  andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN
  12.207 +                           | _ => false) (prop_of th)
  12.208 +
  12.209 +fun is_theorem_bad_for_atps ho_atp exporter thm =
  12.210 +  is_metastrange_theorem thm orelse
  12.211 +  (not exporter andalso
  12.212 +   let val t = prop_of thm in
  12.213 +     is_formula_too_complex ho_atp t orelse exists_type type_has_top_sort t orelse
  12.214 +     exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
  12.215 +     is_that_fact thm
  12.216 +   end)
  12.217 +
  12.218 +fun hackish_string_for_term ctxt t =
  12.219 +  Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
  12.220 +                   (print_mode_value ())) (Syntax.string_of_term ctxt) t
  12.221 +  |> String.translate (fn c => if Char.isPrint c then str c else "")
  12.222 +  |> simplify_spaces
  12.223 +
  12.224 +(* This is a terrible hack. Free variables are sometimes coded as "M__" when
  12.225 +   they are displayed as "M" and we want to avoid clashes with these. But
  12.226 +   sometimes it's even worse: "Ma__" encodes "M". So we simply reserve all
  12.227 +   prefixes of all free variables. In the worse case scenario, where the fact
  12.228 +   won't be resolved correctly, the user can fix it manually, e.g., by naming
  12.229 +   the fact in question. Ideally we would need nothing of it, but backticks
  12.230 +   simply don't work with schematic variables. *)
  12.231 +fun all_prefixes_of s =
  12.232 +  map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1)
  12.233 +
  12.234 +fun close_form t =
  12.235 +  (t, [] |> Term.add_free_names t |> maps all_prefixes_of)
  12.236 +  |> fold (fn ((s, i), T) => fn (t', taken) =>
  12.237 +              let val s' = singleton (Name.variant_list taken) s in
  12.238 +                ((if fastype_of t' = HOLogic.boolT then HOLogic.all_const
  12.239 +                  else Logic.all_const) T
  12.240 +                 $ Abs (s', T, abstract_over (Var ((s, i), T), t')),
  12.241 +                 s' :: taken)
  12.242 +              end)
  12.243 +          (Term.add_vars t [] |> sort_wrt (fst o fst))
  12.244 +  |> fst
  12.245 +
  12.246 +fun all_facts ctxt ho_atp reserved exporter add_ths chained_ths css_table =
  12.247 +  let
  12.248 +    val thy = Proof_Context.theory_of ctxt
  12.249 +    val global_facts = Global_Theory.facts_of thy
  12.250 +    val local_facts = Proof_Context.facts_of ctxt
  12.251 +    val named_locals = local_facts |> Facts.dest_static []
  12.252 +    val assms = Assumption.all_assms_of ctxt
  12.253 +    fun is_good_unnamed_local th =
  12.254 +      not (Thm.has_name_hint th) andalso
  12.255 +      forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
  12.256 +    val unnamed_locals =
  12.257 +      union Thm.eq_thm_prop (Facts.props local_facts) chained_ths
  12.258 +      |> filter is_good_unnamed_local |> map (pair "" o single)
  12.259 +    val full_space =
  12.260 +      Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
  12.261 +    fun add_facts global foldx facts =
  12.262 +      foldx (fn (name0, ths) =>
  12.263 +        if not exporter andalso name0 <> "" andalso
  12.264 +           forall (not o member Thm.eq_thm_prop add_ths) ths andalso
  12.265 +           (Facts.is_concealed facts name0 orelse
  12.266 +            (not (Config.get ctxt ignore_no_atp) andalso
  12.267 +             is_package_def name0) orelse
  12.268 +            exists (fn s => String.isSuffix s name0)
  12.269 +                   (multi_base_blacklist ctxt ho_atp)) then
  12.270 +          I
  12.271 +        else
  12.272 +          let
  12.273 +            val multi = length ths > 1
  12.274 +            val backquote_thm =
  12.275 +              backquote o hackish_string_for_term ctxt o close_form o prop_of
  12.276 +            fun check_thms a =
  12.277 +              case try (Proof_Context.get_thms ctxt) a of
  12.278 +                NONE => false
  12.279 +              | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')
  12.280 +          in
  12.281 +            pair 1
  12.282 +            #> fold (fn th => fn (j, (multis, unis)) =>
  12.283 +                        (j + 1,
  12.284 +                         if not (member Thm.eq_thm_prop add_ths th) andalso
  12.285 +                            is_theorem_bad_for_atps ho_atp exporter th then
  12.286 +                           (multis, unis)
  12.287 +                         else
  12.288 +                           let
  12.289 +                             val new =
  12.290 +                               (((fn () =>
  12.291 +                                 if name0 = "" then
  12.292 +                                   th |> backquote_thm
  12.293 +                                 else
  12.294 +                                   [Facts.extern ctxt facts name0,
  12.295 +                                    Name_Space.extern ctxt full_space name0,
  12.296 +                                    name0]
  12.297 +                                   |> find_first check_thms
  12.298 +                                   |> (fn SOME name =>
  12.299 +                                          make_name reserved multi j name
  12.300 +                                        | NONE => "")),
  12.301 +                                stature_of_thm global assms chained_ths
  12.302 +                                               css_table name0 th), th)
  12.303 +                           in
  12.304 +                             if multi then (new :: multis, unis)
  12.305 +                             else (multis, new :: unis)
  12.306 +                           end)) ths
  12.307 +            #> snd
  12.308 +          end)
  12.309 +  in
  12.310 +    (* The single-name theorems go after the multiple-name ones, so that single
  12.311 +       names are preferred when both are available. *)
  12.312 +    ([], []) |> add_facts false fold local_facts (unnamed_locals @ named_locals)
  12.313 +             |> add_facts true Facts.fold_static global_facts global_facts
  12.314 +             |> op @
  12.315 +  end
  12.316 +
  12.317 +fun clasimpset_rule_table_of ctxt =
  12.318 +  let
  12.319 +    val thy = Proof_Context.theory_of ctxt
  12.320 +    val atomize = HOLogic.mk_Trueprop o Object_Logic.atomize_term thy
  12.321 +    fun add stature normalizers get_th =
  12.322 +      fold (fn rule =>
  12.323 +               let
  12.324 +                 val th = rule |> get_th
  12.325 +                 val t =
  12.326 +                   th |> Thm.maxidx_of th > 0 ? zero_var_indexes |> prop_of
  12.327 +               in
  12.328 +                 fold (fn normalize => Termtab.update (normalize t, stature))
  12.329 +                      (I :: normalizers)
  12.330 +               end)
  12.331 +    val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} =
  12.332 +      ctxt |> claset_of |> Classical.rep_cs
  12.333 +    val intros = Item_Net.content safeIs @ Item_Net.content hazIs
  12.334 +(* Add once it is used:
  12.335 +    val elims =
  12.336 +      Item_Net.content safeEs @ Item_Net.content hazEs
  12.337 +      |> map Classical.classical_rule
  12.338 +*)
  12.339 +    val simps = ctxt |> simpset_of |> dest_ss |> #simps
  12.340 +    val specs = ctxt |> Spec_Rules.get
  12.341 +    val (rec_defs, nonrec_defs) =
  12.342 +      specs |> filter (curry (op =) Spec_Rules.Equational o fst)
  12.343 +            |> maps (snd o snd)
  12.344 +            |> filter_out (member Thm.eq_thm_prop risky_defs)
  12.345 +            |> List.partition (is_rec_def o prop_of)
  12.346 +    val spec_intros =
  12.347 +      specs |> filter (member (op =) [Spec_Rules.Inductive,
  12.348 +                                      Spec_Rules.Co_Inductive] o fst)
  12.349 +            |> maps (snd o snd)
  12.350 +  in
  12.351 +    Termtab.empty |> add Simp [atomize] snd simps
  12.352 +                  |> add Simp [] I rec_defs
  12.353 +                  |> add Def [] I nonrec_defs
  12.354 +(* Add once it is used:
  12.355 +                  |> add Elim [] I elims
  12.356 +*)
  12.357 +                  |> add Intro [] I intros
  12.358 +                  |> add Inductive [] I spec_intros
  12.359 +  end
  12.360 +
  12.361 +fun uniquify xs =
  12.362 +  Termtab.fold (cons o snd)
  12.363 +               (fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty) []
  12.364 +
  12.365 +fun struct_induct_rule_on th =
  12.366 +  case Logic.strip_horn (prop_of th) of
  12.367 +    (prems, @{const Trueprop}
  12.368 +            $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) =>
  12.369 +    if not (is_TVar ind_T) andalso length prems > 1 andalso
  12.370 +       exists (exists_subterm (curry (op aconv) p)) prems andalso
  12.371 +       not (exists (exists_subterm (curry (op aconv) a)) prems) then
  12.372 +      SOME (p_name, ind_T)
  12.373 +    else
  12.374 +      NONE
  12.375 +  | _ => NONE
  12.376 +
  12.377 +fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x =
  12.378 +  let
  12.379 +    fun varify_noninducts (t as Free (s, T)) =
  12.380 +        if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T)
  12.381 +      | varify_noninducts t = t
  12.382 +    val p_inst =
  12.383 +      concl_prop |> map_aterms varify_noninducts |> close_form
  12.384 +                 |> lambda (Free ind_x)
  12.385 +                 |> hackish_string_for_term ctxt
  12.386 +  in
  12.387 +    ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]",
  12.388 +      stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)])
  12.389 +  end
  12.390 +
  12.391 +fun type_match thy (T1, T2) =
  12.392 +  (Sign.typ_match thy (T2, T1) Vartab.empty; true)
  12.393 +  handle Type.TYPE_MATCH => false
  12.394 +
  12.395 +fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, th)) =
  12.396 +  case struct_induct_rule_on th of
  12.397 +    SOME (p_name, ind_T) =>
  12.398 +    let val thy = Proof_Context.theory_of ctxt in
  12.399 +      stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T))
  12.400 +              |> map_filter (try (instantiate_induct_rule ctxt stmt p_name ax))
  12.401 +    end
  12.402 +  | NONE => [ax]
  12.403 +
  12.404 +fun external_frees t =
  12.405 +  [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
  12.406 +
  12.407 +fun maybe_instantiate_inducts ctxt hyp_ts concl_t =
  12.408 +  if Config.get ctxt instantiate_inducts then
  12.409 +    let
  12.410 +      val thy = Proof_Context.theory_of ctxt
  12.411 +      val ind_stmt =
  12.412 +        (hyp_ts |> filter_out (null o external_frees), concl_t)
  12.413 +        |> Logic.list_implies |> Object_Logic.atomize_term thy
  12.414 +      val ind_stmt_xs = external_frees ind_stmt
  12.415 +    in maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) end
  12.416 +  else
  12.417 +    I
  12.418 +
  12.419 +fun maybe_filter_no_atps ctxt =
  12.420 +  not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd)
  12.421 +
  12.422 +fun nearly_all_facts ctxt ho_atp ({add, only, ...} : relevance_override)
  12.423 +                     chained_ths hyp_ts concl_t =
  12.424 +  if only andalso null add then
  12.425 +    []
  12.426 +  else
  12.427 +    let
  12.428 +      val reserved = reserved_isar_keyword_table ()
  12.429 +      val add_ths = Attrib.eval_thms ctxt add
  12.430 +      val css_table = clasimpset_rule_table_of ctxt
  12.431 +    in
  12.432 +      (if only then
  12.433 +         maps (map (fn ((name, stature), th) => ((K name, stature), th))
  12.434 +               o fact_from_ref ctxt reserved chained_ths css_table) add
  12.435 +       else
  12.436 +         all_facts ctxt ho_atp reserved false add_ths chained_ths css_table)
  12.437 +      |> maybe_instantiate_inducts ctxt hyp_ts concl_t
  12.438 +      |> not only ? maybe_filter_no_atps ctxt
  12.439 +      |> uniquify
  12.440 +    end
  12.441 +
  12.442 +end;
    13.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Jul 11 21:43:19 2012 +0200
    13.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Jul 11 21:43:19 2012 +0200
    13.3 @@ -7,27 +7,10 @@
    13.4  
    13.5  signature SLEDGEHAMMER_FILTER =
    13.6  sig
    13.7 -  type status = ATP_Problem_Generate.status
    13.8    type stature = ATP_Problem_Generate.stature
    13.9    type relevance_fudge = Sledgehammer_Filter_Iter.relevance_fudge
   13.10    type relevance_override = Sledgehammer_Filter_Iter.relevance_override
   13.11  
   13.12 -  val no_relevance_override : relevance_override
   13.13 -  val fact_from_ref :
   13.14 -    Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
   13.15 -    -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
   13.16 -  val all_facts :
   13.17 -    Proof.context -> bool -> 'a Symtab.table -> bool -> thm list
   13.18 -    -> thm list -> status Termtab.table
   13.19 -    -> (((unit -> string) * stature) * thm) list
   13.20 -  val clasimpset_rule_table_of : Proof.context -> status Termtab.table
   13.21 -  val maybe_instantiate_inducts :
   13.22 -    Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
   13.23 -    -> (((unit -> string) * 'a) * thm) list
   13.24 -  val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list
   13.25 -  val nearly_all_facts :
   13.26 -    Proof.context -> bool -> relevance_override -> thm list -> term list -> term
   13.27 -    -> (((unit -> string) * stature) * thm) list
   13.28    val relevant_facts :
   13.29      Proof.context -> real * real -> int
   13.30      -> (string * typ -> term list -> bool * term list) -> relevance_fudge
   13.31 @@ -39,394 +22,8 @@
   13.32  structure Sledgehammer_Filter : SLEDGEHAMMER_FILTER =
   13.33  struct
   13.34  
   13.35 -open ATP_Problem_Generate
   13.36 -open Metis_Tactic
   13.37 -open Sledgehammer_Util
   13.38  open Sledgehammer_Filter_Iter
   13.39  
   13.40 -val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
   13.41 -
   13.42 -val no_relevance_override = {add = [], del = [], only = false}
   13.43 -
   13.44 -fun needs_quoting reserved s =
   13.45 -  Symtab.defined reserved s orelse
   13.46 -  exists (not o Lexicon.is_identifier) (Long_Name.explode s)
   13.47 -
   13.48 -fun make_name reserved multi j name =
   13.49 -  (name |> needs_quoting reserved name ? quote) ^
   13.50 -  (if multi then "(" ^ string_of_int j ^ ")" else "")
   13.51 -
   13.52 -fun explode_interval _ (Facts.FromTo (i, j)) = i upto j
   13.53 -  | explode_interval max (Facts.From i) = i upto i + max - 1
   13.54 -  | explode_interval _ (Facts.Single i) = [i]
   13.55 -
   13.56 -val backquote =
   13.57 -  raw_explode #> map (fn "`" => "\\`" | s => s) #> implode #> enclose "`" "`"
   13.58 -
   13.59 -(* unfolding these can yield really huge terms *)
   13.60 -val risky_defs = @{thms Bit0_def Bit1_def}
   13.61 -
   13.62 -fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs))
   13.63 -fun is_rec_def (@{const Trueprop} $ t) = is_rec_def t
   13.64 -  | is_rec_def (@{const ==>} $ _ $ t2) = is_rec_def t2
   13.65 -  | is_rec_def (Const (@{const_name "=="}, _) $ t1 $ t2) = is_rec_eq t1 t2
   13.66 -  | is_rec_def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2
   13.67 -  | is_rec_def _ = false
   13.68 -
   13.69 -fun is_assum assms th = exists (fn ct => prop_of th aconv term_of ct) assms
   13.70 -fun is_chained chained_ths = member Thm.eq_thm_prop chained_ths
   13.71 -
   13.72 -fun scope_of_thm global assms chained_ths th =
   13.73 -  if is_chained chained_ths th then Chained
   13.74 -  else if global then Global
   13.75 -  else if is_assum assms th then Assum
   13.76 -  else Local
   13.77 -
   13.78 -val may_be_induction =
   13.79 -  exists_subterm (fn Var (_, Type (@{type_name fun}, [_, T])) =>
   13.80 -                     body_type T = @{typ bool}
   13.81 -                   | _ => false)
   13.82 -
   13.83 -fun status_of_thm css_table name th =
   13.84 -  (* FIXME: use structured name *)
   13.85 -  if (String.isSubstring ".induct" name orelse
   13.86 -      String.isSubstring ".inducts" name) andalso
   13.87 -     may_be_induction (prop_of th) then
   13.88 -    Induction
   13.89 -  else case Termtab.lookup css_table (prop_of th) of
   13.90 -    SOME status => status
   13.91 -  | NONE => General
   13.92 -
   13.93 -fun stature_of_thm global assms chained_ths css_table name th =
   13.94 -  (scope_of_thm global assms chained_ths th, status_of_thm css_table name th)
   13.95 -
   13.96 -fun fact_from_ref ctxt reserved chained_ths css_table (xthm as (xref, args)) =
   13.97 -  let
   13.98 -    val ths = Attrib.eval_thms ctxt [xthm]
   13.99 -    val bracket =
  13.100 -      map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args
  13.101 -      |> implode
  13.102 -    fun nth_name j =
  13.103 -      case xref of
  13.104 -        Facts.Fact s => backquote s ^ bracket
  13.105 -      | Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
  13.106 -      | Facts.Named ((name, _), NONE) =>
  13.107 -        make_name reserved (length ths > 1) (j + 1) name ^ bracket
  13.108 -      | Facts.Named ((name, _), SOME intervals) =>
  13.109 -        make_name reserved true
  13.110 -                 (nth (maps (explode_interval (length ths)) intervals) j) name ^
  13.111 -        bracket
  13.112 -  in
  13.113 -    (ths, (0, []))
  13.114 -    |-> fold (fn th => fn (j, rest) =>
  13.115 -                 let val name = nth_name j in
  13.116 -                   (j + 1, ((name, stature_of_thm false [] chained_ths
  13.117 -                                             css_table name th), th) :: rest)
  13.118 -                 end)
  13.119 -    |> snd
  13.120 -  end
  13.121 -
  13.122 -(*Reject theorems with names like "List.filter.filter_list_def" or
  13.123 -  "Accessible_Part.acc.defs", as these are definitions arising from packages.*)
  13.124 -fun is_package_def a =
  13.125 -  let val names = Long_Name.explode a in
  13.126 -    (length names > 2 andalso not (hd names = "local") andalso
  13.127 -     String.isSuffix "_def" a) orelse String.isSuffix "_defs" a
  13.128 -  end
  13.129 -
  13.130 -(* FIXME: put other record thms here, or declare as "no_atp" *)
  13.131 -fun multi_base_blacklist ctxt ho_atp =
  13.132 -  ["defs", "select_defs", "update_defs", "split", "splits", "split_asm",
  13.133 -   "cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong",
  13.134 -   "weak_case_cong"]
  13.135 -  |> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ?
  13.136 -        append ["induct", "inducts"]
  13.137 -  |> map (prefix ".")
  13.138 -
  13.139 -val max_lambda_nesting = 3 (*only applies if not ho_atp*)
  13.140 -
  13.141 -fun term_has_too_many_lambdas max (t1 $ t2) =
  13.142 -    exists (term_has_too_many_lambdas max) [t1, t2]
  13.143 -  | term_has_too_many_lambdas max (Abs (_, _, t)) =
  13.144 -    max = 0 orelse term_has_too_many_lambdas (max - 1) t
  13.145 -  | term_has_too_many_lambdas _ _ = false
  13.146 -
  13.147 -(* Don't count nested lambdas at the level of formulas, since they are
  13.148 -   quantifiers. *)
  13.149 -fun formula_has_too_many_lambdas true _ _ = false (*i.e. ho_atp*)
  13.150 -  | formula_has_too_many_lambdas _ Ts (Abs (_, T, t)) =
  13.151 -      formula_has_too_many_lambdas false (T :: Ts) t
  13.152 -  | formula_has_too_many_lambdas _ Ts t =
  13.153 -    if member (op =) [HOLogic.boolT, propT] (fastype_of1 (Ts, t)) then
  13.154 -      exists (formula_has_too_many_lambdas false Ts) (#2 (strip_comb t))
  13.155 -    else
  13.156 -      term_has_too_many_lambdas max_lambda_nesting t
  13.157 -
  13.158 -(* The max apply depth of any "metis" call in "Metis_Examples" (on 2007-10-31)
  13.159 -   was 11. *)
  13.160 -val max_apply_depth = 15
  13.161 -
  13.162 -fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1)
  13.163 -  | apply_depth (Abs (_, _, t)) = apply_depth t
  13.164 -  | apply_depth _ = 0
  13.165 -
  13.166 -fun is_formula_too_complex ho_atp t =
  13.167 -  apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas ho_atp [] t
  13.168 -
  13.169 -(* FIXME: Extend to "Meson" and "Metis" *)
  13.170 -val exists_sledgehammer_const =
  13.171 -  exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)
  13.172 -
  13.173 -(* FIXME: make more reliable *)
  13.174 -val exists_low_level_class_const =
  13.175 -  exists_Const (fn (s, _) =>
  13.176 -     s = @{const_name equal_class.equal} orelse
  13.177 -     String.isSubstring (Long_Name.separator ^ "class" ^ Long_Name.separator) s)
  13.178 -
  13.179 -fun is_metastrange_theorem th =
  13.180 -  case head_of (concl_of th) of
  13.181 -    Const (s, _) => (s <> @{const_name Trueprop} andalso
  13.182 -                     s <> @{const_name "=="})
  13.183 -  | _ => false
  13.184 -
  13.185 -fun is_that_fact th =
  13.186 -  String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th)
  13.187 -  andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN
  13.188 -                           | _ => false) (prop_of th)
  13.189 -
  13.190 -fun is_theorem_bad_for_atps ho_atp exporter thm =
  13.191 -  is_metastrange_theorem thm orelse
  13.192 -  (not exporter andalso
  13.193 -   let val t = prop_of thm in
  13.194 -     is_formula_too_complex ho_atp t orelse exists_type type_has_top_sort t orelse
  13.195 -     exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
  13.196 -     is_that_fact thm
  13.197 -   end)
  13.198 -
  13.199 -fun string_for_term ctxt t =
  13.200 -  Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
  13.201 -                   (print_mode_value ())) (Syntax.string_of_term ctxt) t
  13.202 -  |> String.translate (fn c => if Char.isPrint c then str c else "")
  13.203 -  |> simplify_spaces
  13.204 -
  13.205 -(* This is a terrible hack. Free variables are sometimes coded as "M__" when
  13.206 -   they are displayed as "M" and we want to avoid clashes with these. But
  13.207 -   sometimes it's even worse: "Ma__" encodes "M". So we simply reserve all
  13.208 -   prefixes of all free variables. In the worse case scenario, where the fact
  13.209 -   won't be resolved correctly, the user can fix it manually, e.g., by naming
  13.210 -   the fact in question. Ideally we would need nothing of it, but backticks
  13.211 -   simply don't work with schematic variables. *)
  13.212 -fun all_prefixes_of s =
  13.213 -  map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1)
  13.214 -
  13.215 -fun close_form t =
  13.216 -  (t, [] |> Term.add_free_names t |> maps all_prefixes_of)
  13.217 -  |> fold (fn ((s, i), T) => fn (t', taken) =>
  13.218 -              let val s' = singleton (Name.variant_list taken) s in
  13.219 -                ((if fastype_of t' = HOLogic.boolT then HOLogic.all_const
  13.220 -                  else Logic.all_const) T
  13.221 -                 $ Abs (s', T, abstract_over (Var ((s, i), T), t')),
  13.222 -                 s' :: taken)
  13.223 -              end)
  13.224 -          (Term.add_vars t [] |> sort_wrt (fst o fst))
  13.225 -  |> fst
  13.226 -
  13.227 -fun all_facts ctxt ho_atp reserved exporter add_ths chained_ths css_table =
  13.228 -  let
  13.229 -    val thy = Proof_Context.theory_of ctxt
  13.230 -    val global_facts = Global_Theory.facts_of thy
  13.231 -    val local_facts = Proof_Context.facts_of ctxt
  13.232 -    val named_locals = local_facts |> Facts.dest_static []
  13.233 -    val assms = Assumption.all_assms_of ctxt
  13.234 -    fun is_good_unnamed_local th =
  13.235 -      not (Thm.has_name_hint th) andalso
  13.236 -      forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
  13.237 -    val unnamed_locals =
  13.238 -      union Thm.eq_thm_prop (Facts.props local_facts) chained_ths
  13.239 -      |> filter is_good_unnamed_local |> map (pair "" o single)
  13.240 -    val full_space =
  13.241 -      Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
  13.242 -    fun add_facts global foldx facts =
  13.243 -      foldx (fn (name0, ths) =>
  13.244 -        if not exporter andalso name0 <> "" andalso
  13.245 -           forall (not o member Thm.eq_thm_prop add_ths) ths andalso
  13.246 -           (Facts.is_concealed facts name0 orelse
  13.247 -            (not (Config.get ctxt ignore_no_atp) andalso
  13.248 -             is_package_def name0) orelse
  13.249 -            exists (fn s => String.isSuffix s name0)
  13.250 -                   (multi_base_blacklist ctxt ho_atp)) then
  13.251 -          I
  13.252 -        else
  13.253 -          let
  13.254 -            val multi = length ths > 1
  13.255 -            val backquote_thm =
  13.256 -              backquote o string_for_term ctxt o close_form o prop_of
  13.257 -            fun check_thms a =
  13.258 -              case try (Proof_Context.get_thms ctxt) a of
  13.259 -                NONE => false
  13.260 -              | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')
  13.261 -          in
  13.262 -            pair 1
  13.263 -            #> fold (fn th => fn (j, (multis, unis)) =>
  13.264 -                        (j + 1,
  13.265 -                         if not (member Thm.eq_thm_prop add_ths th) andalso
  13.266 -                            is_theorem_bad_for_atps ho_atp exporter th then
  13.267 -                           (multis, unis)
  13.268 -                         else
  13.269 -                           let
  13.270 -                             val new =
  13.271 -                               (((fn () =>
  13.272 -                                 if name0 = "" then
  13.273 -                                   th |> backquote_thm
  13.274 -                                 else
  13.275 -                                   [Facts.extern ctxt facts name0,
  13.276 -                                    Name_Space.extern ctxt full_space name0,
  13.277 -                                    name0]
  13.278 -                                   |> find_first check_thms
  13.279 -                                   |> (fn SOME name =>
  13.280 -                                          make_name reserved multi j name
  13.281 -                                        | NONE => "")),
  13.282 -                                stature_of_thm global assms chained_ths
  13.283 -                                               css_table name0 th), th)
  13.284 -                           in
  13.285 -                             if multi then (new :: multis, unis)
  13.286 -                             else (multis, new :: unis)
  13.287 -                           end)) ths
  13.288 -            #> snd
  13.289 -          end)
  13.290 -  in
  13.291 -    (* The single-name theorems go after the multiple-name ones, so that single
  13.292 -       names are preferred when both are available. *)
  13.293 -    ([], []) |> add_facts false fold local_facts (unnamed_locals @ named_locals)
  13.294 -             |> add_facts true Facts.fold_static global_facts global_facts
  13.295 -             |> op @
  13.296 -  end
  13.297 -
  13.298 -fun clasimpset_rule_table_of ctxt =
  13.299 -  let
  13.300 -    val thy = Proof_Context.theory_of ctxt
  13.301 -    val atomize = HOLogic.mk_Trueprop o Object_Logic.atomize_term thy
  13.302 -    fun add stature normalizers get_th =
  13.303 -      fold (fn rule =>
  13.304 -               let
  13.305 -                 val th = rule |> get_th
  13.306 -                 val t =
  13.307 -                   th |> Thm.maxidx_of th > 0 ? zero_var_indexes |> prop_of
  13.308 -               in
  13.309 -                 fold (fn normalize => Termtab.update (normalize t, stature))
  13.310 -                      (I :: normalizers)
  13.311 -               end)
  13.312 -    val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} =
  13.313 -      ctxt |> claset_of |> Classical.rep_cs
  13.314 -    val intros = Item_Net.content safeIs @ Item_Net.content hazIs
  13.315 -(* Add once it is used:
  13.316 -    val elims =
  13.317 -      Item_Net.content safeEs @ Item_Net.content hazEs
  13.318 -      |> map Classical.classical_rule
  13.319 -*)
  13.320 -    val simps = ctxt |> simpset_of |> dest_ss |> #simps
  13.321 -    val specs = ctxt |> Spec_Rules.get
  13.322 -    val (rec_defs, nonrec_defs) =
  13.323 -      specs |> filter (curry (op =) Spec_Rules.Equational o fst)
  13.324 -            |> maps (snd o snd)
  13.325 -            |> filter_out (member Thm.eq_thm_prop risky_defs)
  13.326 -            |> List.partition (is_rec_def o prop_of)
  13.327 -    val spec_intros =
  13.328 -      specs |> filter (member (op =) [Spec_Rules.Inductive,
  13.329 -                                      Spec_Rules.Co_Inductive] o fst)
  13.330 -            |> maps (snd o snd)
  13.331 -  in
  13.332 -    Termtab.empty |> add Simp [atomize] snd simps
  13.333 -                  |> add Simp [] I rec_defs
  13.334 -                  |> add Def [] I nonrec_defs
  13.335 -(* Add once it is used:
  13.336 -                  |> add Elim [] I elims
  13.337 -*)
  13.338 -                  |> add Intro [] I intros
  13.339 -                  |> add Inductive [] I spec_intros
  13.340 -  end
  13.341 -
  13.342 -fun uniquify xs =
  13.343 -  Termtab.fold (cons o snd)
  13.344 -               (fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty) []
  13.345 -
  13.346 -fun struct_induct_rule_on th =
  13.347 -  case Logic.strip_horn (prop_of th) of
  13.348 -    (prems, @{const Trueprop}
  13.349 -            $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) =>
  13.350 -    if not (is_TVar ind_T) andalso length prems > 1 andalso
  13.351 -       exists (exists_subterm (curry (op aconv) p)) prems andalso
  13.352 -       not (exists (exists_subterm (curry (op aconv) a)) prems) then
  13.353 -      SOME (p_name, ind_T)
  13.354 -    else
  13.355 -      NONE
  13.356 -  | _ => NONE
  13.357 -
  13.358 -fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x =
  13.359 -  let
  13.360 -    fun varify_noninducts (t as Free (s, T)) =
  13.361 -        if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T)
  13.362 -      | varify_noninducts t = t
  13.363 -    val p_inst =
  13.364 -      concl_prop |> map_aterms varify_noninducts |> close_form
  13.365 -                 |> lambda (Free ind_x)
  13.366 -                 |> string_for_term ctxt
  13.367 -  in
  13.368 -    ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]",
  13.369 -      stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)])
  13.370 -  end
  13.371 -
  13.372 -fun type_match thy (T1, T2) =
  13.373 -  (Sign.typ_match thy (T2, T1) Vartab.empty; true)
  13.374 -  handle Type.TYPE_MATCH => false
  13.375 -
  13.376 -fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, th)) =
  13.377 -  case struct_induct_rule_on th of
  13.378 -    SOME (p_name, ind_T) =>
  13.379 -    let val thy = Proof_Context.theory_of ctxt in
  13.380 -      stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T))
  13.381 -              |> map_filter (try (instantiate_induct_rule ctxt stmt p_name ax))
  13.382 -    end
  13.383 -  | NONE => [ax]
  13.384 -
  13.385 -fun external_frees t =
  13.386 -  [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
  13.387 -
  13.388 -fun maybe_instantiate_inducts ctxt hyp_ts concl_t =
  13.389 -  if Config.get ctxt instantiate_inducts then
  13.390 -    let
  13.391 -      val thy = Proof_Context.theory_of ctxt
  13.392 -      val ind_stmt =
  13.393 -        (hyp_ts |> filter_out (null o external_frees), concl_t)
  13.394 -        |> Logic.list_implies |> Object_Logic.atomize_term thy
  13.395 -      val ind_stmt_xs = external_frees ind_stmt
  13.396 -    in maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) end
  13.397 -  else
  13.398 -    I
  13.399 -
  13.400 -fun maybe_filter_no_atps ctxt =
  13.401 -  not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd)
  13.402 -
  13.403 -fun nearly_all_facts ctxt ho_atp ({add, only, ...} : relevance_override)
  13.404 -                     chained_ths hyp_ts concl_t =
  13.405 -  if only andalso null add then
  13.406 -    []
  13.407 -  else
  13.408 -    let
  13.409 -      val reserved = reserved_isar_keyword_table ()
  13.410 -      val add_ths = Attrib.eval_thms ctxt add
  13.411 -      val css_table = clasimpset_rule_table_of ctxt
  13.412 -    in
  13.413 -      (if only then
  13.414 -         maps (map (fn ((name, stature), th) => ((K name, stature), th))
  13.415 -               o fact_from_ref ctxt reserved chained_ths css_table) add
  13.416 -       else
  13.417 -         all_facts ctxt ho_atp reserved false add_ths chained_ths css_table)
  13.418 -      |> maybe_instantiate_inducts ctxt hyp_ts concl_t
  13.419 -      |> not only ? maybe_filter_no_atps ctxt
  13.420 -      |> uniquify
  13.421 -    end
  13.422 -
  13.423  val relevant_facts = iterative_relevant_facts
  13.424  
  13.425  end;
    14.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML	Wed Jul 11 21:43:19 2012 +0200
    14.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML	Wed Jul 11 21:43:19 2012 +0200
    14.3 @@ -8,6 +8,7 @@
    14.4  signature SLEDGEHAMMER_FILTER_ITER =
    14.5  sig
    14.6    type stature = ATP_Problem_Generate.stature
    14.7 +  type relevance_override = Sledgehammer_Fact.relevance_override
    14.8  
    14.9    type relevance_fudge =
   14.10      {local_const_multiplier : real,
   14.11 @@ -30,14 +31,7 @@
   14.12       threshold_divisor : real,
   14.13       ridiculous_threshold : real}
   14.14  
   14.15 -  type relevance_override =
   14.16 -    {add : (Facts.ref * Attrib.src list) list,
   14.17 -     del : (Facts.ref * Attrib.src list) list,
   14.18 -     only : bool}
   14.19 -
   14.20    val trace : bool Config.T
   14.21 -  val ignore_no_atp : bool Config.T
   14.22 -  val instantiate_inducts : bool Config.T
   14.23    val pseudo_abs_name : string
   14.24    val pseudo_skolem_prefix : string
   14.25    val const_names_in_fact :
   14.26 @@ -55,17 +49,12 @@
   14.27  struct
   14.28  
   14.29  open ATP_Problem_Generate
   14.30 +open Sledgehammer_Fact
   14.31  
   14.32  val trace =
   14.33    Attrib.setup_config_bool @{binding sledgehammer_filter_trace} (K false)
   14.34  fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
   14.35  
   14.36 -(* experimental features *)
   14.37 -val ignore_no_atp =
   14.38 -  Attrib.setup_config_bool @{binding sledgehammer_ignore_no_atp} (K false)
   14.39 -val instantiate_inducts =
   14.40 -  Attrib.setup_config_bool @{binding sledgehammer_instantiate_inducts} (K false)
   14.41 -
   14.42  type relevance_fudge =
   14.43    {local_const_multiplier : real,
   14.44     worse_irrel_freq : real,
   14.45 @@ -87,11 +76,6 @@
   14.46     threshold_divisor : real,
   14.47     ridiculous_threshold : real}
   14.48  
   14.49 -type relevance_override =
   14.50 -  {add : (Facts.ref * Attrib.src list) list,
   14.51 -   del : (Facts.ref * Attrib.src list) list,
   14.52 -   only : bool}
   14.53 -
   14.54  val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
   14.55  val pseudo_abs_name = sledgehammer_prefix ^ "abs"
   14.56  val pseudo_skolem_prefix = sledgehammer_prefix ^ "sko"
    15.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 11 21:43:19 2012 +0200
    15.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 11 21:43:19 2012 +0200
    15.3 @@ -23,7 +23,7 @@
    15.4  open ATP_Problem_Generate
    15.5  open ATP_Proof_Reconstruct
    15.6  open Sledgehammer_Util
    15.7 -open Sledgehammer_Filter
    15.8 +open Sledgehammer_Fact
    15.9  open Sledgehammer_Provers
   15.10  open Sledgehammer_Minimize
   15.11  open Sledgehammer_Run
    16.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Jul 11 21:43:19 2012 +0200
    16.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Jul 11 21:43:19 2012 +0200
    16.3 @@ -9,14 +9,19 @@
    16.4  sig
    16.5    type stature = ATP_Problem_Generate.stature
    16.6    type play = ATP_Proof_Reconstruct.play
    16.7 +  type mode = Sledgehammer_Provers.mode
    16.8    type params = Sledgehammer_Provers.params
    16.9 +  type prover = Sledgehammer_Provers.prover
   16.10  
   16.11    val binary_min_facts : int Config.T
   16.12 +  val auto_minimize_min_facts : int Config.T
   16.13 +  val auto_minimize_max_time : real Config.T
   16.14    val minimize_facts :
   16.15      string -> params -> bool -> int -> int -> Proof.state
   16.16      -> ((string * stature) * thm list) list
   16.17      -> ((string * stature) * thm list) list option
   16.18         * ((unit -> play) * (play -> string) * string)
   16.19 +  val get_minimizing_prover : Proof.context -> mode -> string -> prover
   16.20    val run_minimize :
   16.21      params -> int -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit
   16.22  end;
   16.23 @@ -29,7 +34,7 @@
   16.24  open ATP_Problem_Generate
   16.25  open ATP_Proof_Reconstruct
   16.26  open Sledgehammer_Util
   16.27 -open Sledgehammer_Filter
   16.28 +open Sledgehammer_Fact
   16.29  open Sledgehammer_Provers
   16.30  
   16.31  (* wrapper for calling external prover *)
   16.32 @@ -107,6 +112,12 @@
   16.33  val binary_min_facts =
   16.34    Attrib.setup_config_int @{binding sledgehammer_minimize_binary_min_facts}
   16.35                            (K 20)
   16.36 +val auto_minimize_min_facts =
   16.37 +  Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}
   16.38 +      (fn generic => Config.get_generic generic binary_min_facts)
   16.39 +val auto_minimize_max_time =
   16.40 +  Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_time}
   16.41 +                           (K 5.0)
   16.42  
   16.43  fun linear_minimize test timeout result xs =
   16.44    let
   16.45 @@ -212,6 +223,106 @@
   16.46             (NONE, (K (Failed_to_Play plain_metis), fn _ => "Error: " ^ msg, ""))
   16.47    end
   16.48  
   16.49 +fun adjust_reconstructor_params override_params
   16.50 +        ({debug, verbose, overlord, blocking, provers, type_enc, strict,
   16.51 +         lam_trans, uncurried_aliases, relevance_thresholds, max_relevant,
   16.52 +         max_mono_iters, max_new_mono_instances, isar_proof, isar_shrink_factor,
   16.53 +         slice, minimize, timeout, preplay_timeout, expect} : params) =
   16.54 +  let
   16.55 +    fun lookup_override name default_value =
   16.56 +      case AList.lookup (op =) override_params name of
   16.57 +        SOME [s] => SOME s
   16.58 +      | _ => default_value
   16.59 +    (* Only those options that reconstructors are interested in are considered
   16.60 +       here. *)
   16.61 +    val type_enc = lookup_override "type_enc" type_enc
   16.62 +    val lam_trans = lookup_override "lam_trans" lam_trans
   16.63 +  in
   16.64 +    {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
   16.65 +     provers = provers, type_enc = type_enc, strict = strict,
   16.66 +     lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
   16.67 +     max_relevant = max_relevant, relevance_thresholds = relevance_thresholds,
   16.68 +     max_mono_iters = max_mono_iters,
   16.69 +     max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
   16.70 +     isar_shrink_factor = isar_shrink_factor, slice = slice,
   16.71 +     minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
   16.72 +     expect = expect}
   16.73 +  end
   16.74 +
   16.75 +fun minimize ctxt mode name
   16.76 +             (params as {debug, verbose, isar_proof, minimize, ...})
   16.77 +             ({state, subgoal, subgoal_count, facts, ...} : prover_problem)
   16.78 +             (result as {outcome, used_facts, run_time, preplay, message,
   16.79 +                         message_tail} : prover_result) =
   16.80 +  if is_some outcome orelse null used_facts then
   16.81 +    result
   16.82 +  else
   16.83 +    let
   16.84 +      val num_facts = length used_facts
   16.85 +      val ((perhaps_minimize, (minimize_name, params)), preplay) =
   16.86 +        if mode = Normal then
   16.87 +          if num_facts >= Config.get ctxt auto_minimize_min_facts then
   16.88 +            ((true, (name, params)), preplay)
   16.89 +          else
   16.90 +            let
   16.91 +              fun can_min_fast_enough time =
   16.92 +                0.001
   16.93 +                * Real.fromInt ((num_facts + 1) * Time.toMilliseconds time)
   16.94 +                <= Config.get ctxt auto_minimize_max_time
   16.95 +              fun prover_fast_enough () = can_min_fast_enough run_time
   16.96 +            in
   16.97 +              if isar_proof then
   16.98 +                ((prover_fast_enough (), (name, params)), preplay)
   16.99 +              else
  16.100 +                let val preplay = preplay () in
  16.101 +                  (case preplay of
  16.102 +                     Played (reconstr, timeout) =>
  16.103 +                     if can_min_fast_enough timeout then
  16.104 +                       (true, extract_reconstructor params reconstr
  16.105 +                              ||> (fn override_params =>
  16.106 +                                      adjust_reconstructor_params
  16.107 +                                          override_params params))
  16.108 +                     else
  16.109 +                       (prover_fast_enough (), (name, params))
  16.110 +                   | _ => (prover_fast_enough (), (name, params)),
  16.111 +                   K preplay)
  16.112 +                end
  16.113 +            end
  16.114 +        else
  16.115 +          ((false, (name, params)), preplay)
  16.116 +      val minimize = minimize |> the_default perhaps_minimize
  16.117 +      val (used_facts, (preplay, message, _)) =
  16.118 +        if minimize then
  16.119 +          minimize_facts minimize_name params (not verbose) subgoal
  16.120 +                         subgoal_count state
  16.121 +                         (filter_used_facts used_facts
  16.122 +                              (map (apsnd single o untranslated_fact) facts))
  16.123 +          |>> Option.map (map fst)
  16.124 +        else
  16.125 +          (SOME used_facts, (preplay, message, ""))
  16.126 +    in
  16.127 +      case used_facts of
  16.128 +        SOME used_facts =>
  16.129 +        (if debug andalso not (null used_facts) then
  16.130 +           facts ~~ (0 upto length facts - 1)
  16.131 +           |> map (fn (fact, j) => fact |> untranslated_fact |> apsnd (K j))
  16.132 +           |> filter_used_facts used_facts
  16.133 +           |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
  16.134 +           |> commas
  16.135 +           |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^
  16.136 +                       " proof (of " ^ string_of_int (length facts) ^ "): ") "."
  16.137 +           |> Output.urgent_message
  16.138 +         else
  16.139 +           ();
  16.140 +         {outcome = NONE, used_facts = used_facts, run_time = run_time,
  16.141 +          preplay = preplay, message = message, message_tail = message_tail})
  16.142 +      | NONE => result
  16.143 +    end
  16.144 +
  16.145 +fun get_minimizing_prover ctxt mode name params minimize_command problem =
  16.146 +  get_prover ctxt mode name params minimize_command problem
  16.147 +  |> minimize ctxt mode name params problem
  16.148 +
  16.149  fun run_minimize (params as {provers, ...}) i refs state =
  16.150    let
  16.151      val ctxt = Proof.context_of state
    17.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Jul 11 21:43:19 2012 +0200
    17.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Jul 11 21:43:19 2012 +0200
    17.3 @@ -14,7 +14,7 @@
    17.4    type reconstructor = ATP_Proof_Reconstruct.reconstructor
    17.5    type play = ATP_Proof_Reconstruct.play
    17.6    type minimize_command = ATP_Proof_Reconstruct.minimize_command
    17.7 -  type relevance_fudge = Sledgehammer_Filter.relevance_fudge
    17.8 +  type relevance_fudge = Sledgehammer_Filter_Iter.relevance_fudge
    17.9  
   17.10    datatype mode = Auto_Try | Try | Normal | Auto_Minimize | Minimize
   17.11  
   17.12 @@ -124,7 +124,7 @@
   17.13  open ATP_Proof_Reconstruct
   17.14  open Metis_Tactic
   17.15  open Sledgehammer_Util
   17.16 -open Sledgehammer_Filter
   17.17 +open Sledgehammer_Filter_Iter
   17.18  
   17.19  (** The Sledgehammer **)
   17.20  
    18.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Jul 11 21:43:19 2012 +0200
    18.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Jul 11 21:43:19 2012 +0200
    18.3 @@ -12,15 +12,11 @@
    18.4    type relevance_override = Sledgehammer_Filter.relevance_override
    18.5    type mode = Sledgehammer_Provers.mode
    18.6    type params = Sledgehammer_Provers.params
    18.7 -  type prover = Sledgehammer_Provers.prover
    18.8  
    18.9    val someN : string
   18.10    val noneN : string
   18.11    val timeoutN : string
   18.12    val unknownN : string
   18.13 -  val auto_minimize_min_facts : int Config.T
   18.14 -  val auto_minimize_max_time : real Config.T
   18.15 -  val get_minimizing_prover : Proof.context -> mode -> string -> prover
   18.16    val run_sledgehammer :
   18.17      params -> mode -> int -> relevance_override
   18.18      -> ((string * string list) list -> string -> minimize_command)
   18.19 @@ -34,9 +30,10 @@
   18.20  open ATP_Problem_Generate
   18.21  open ATP_Proof_Reconstruct
   18.22  open Sledgehammer_Util
   18.23 -open Sledgehammer_Filter
   18.24 +open Sledgehammer_Fact
   18.25  open Sledgehammer_Provers
   18.26  open Sledgehammer_Minimize
   18.27 +open Sledgehammer_Filter
   18.28  
   18.29  val someN = "some"
   18.30  val noneN = "none"
   18.31 @@ -65,113 +62,6 @@
   18.32     (if blocking then "."
   18.33      else "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))))
   18.34  
   18.35 -val auto_minimize_min_facts =
   18.36 -  Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}
   18.37 -      (fn generic => Config.get_generic generic binary_min_facts)
   18.38 -val auto_minimize_max_time =
   18.39 -  Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_time}
   18.40 -                           (K 5.0)
   18.41 -
   18.42 -fun adjust_reconstructor_params override_params
   18.43 -        ({debug, verbose, overlord, blocking, provers, type_enc, strict,
   18.44 -         lam_trans, uncurried_aliases, relevance_thresholds, max_relevant,
   18.45 -         max_mono_iters, max_new_mono_instances, isar_proof, isar_shrink_factor,
   18.46 -         slice, minimize, timeout, preplay_timeout, expect} : params) =
   18.47 -  let
   18.48 -    fun lookup_override name default_value =
   18.49 -      case AList.lookup (op =) override_params name of
   18.50 -        SOME [s] => SOME s
   18.51 -      | _ => default_value
   18.52 -    (* Only those options that reconstructors are interested in are considered
   18.53 -       here. *)
   18.54 -    val type_enc = lookup_override "type_enc" type_enc
   18.55 -    val lam_trans = lookup_override "lam_trans" lam_trans
   18.56 -  in
   18.57 -    {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
   18.58 -     provers = provers, type_enc = type_enc, strict = strict,
   18.59 -     lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
   18.60 -     max_relevant = max_relevant, relevance_thresholds = relevance_thresholds,
   18.61 -     max_mono_iters = max_mono_iters,
   18.62 -     max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
   18.63 -     isar_shrink_factor = isar_shrink_factor, slice = slice,
   18.64 -     minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
   18.65 -     expect = expect}
   18.66 -  end
   18.67 -
   18.68 -fun minimize ctxt mode name
   18.69 -             (params as {debug, verbose, isar_proof, minimize, ...})
   18.70 -             ({state, subgoal, subgoal_count, facts, ...} : prover_problem)
   18.71 -             (result as {outcome, used_facts, run_time, preplay, message,
   18.72 -                         message_tail} : prover_result) =
   18.73 -  if is_some outcome orelse null used_facts then
   18.74 -    result
   18.75 -  else
   18.76 -    let
   18.77 -      val num_facts = length used_facts
   18.78 -      val ((perhaps_minimize, (minimize_name, params)), preplay) =
   18.79 -        if mode = Normal then
   18.80 -          if num_facts >= Config.get ctxt auto_minimize_min_facts then
   18.81 -            ((true, (name, params)), preplay)
   18.82 -          else
   18.83 -            let
   18.84 -              fun can_min_fast_enough time =
   18.85 -                0.001
   18.86 -                * Real.fromInt ((num_facts + 1) * Time.toMilliseconds time)
   18.87 -                <= Config.get ctxt auto_minimize_max_time
   18.88 -              fun prover_fast_enough () = can_min_fast_enough run_time
   18.89 -            in
   18.90 -              if isar_proof then
   18.91 -                ((prover_fast_enough (), (name, params)), preplay)
   18.92 -              else
   18.93 -                let val preplay = preplay () in
   18.94 -                  (case preplay of
   18.95 -                     Played (reconstr, timeout) =>
   18.96 -                     if can_min_fast_enough timeout then
   18.97 -                       (true, extract_reconstructor params reconstr
   18.98 -                              ||> (fn override_params =>
   18.99 -                                      adjust_reconstructor_params
  18.100 -                                          override_params params))
  18.101 -                     else
  18.102 -                       (prover_fast_enough (), (name, params))
  18.103 -                   | _ => (prover_fast_enough (), (name, params)),
  18.104 -                   K preplay)
  18.105 -                end
  18.106 -            end
  18.107 -        else
  18.108 -          ((false, (name, params)), preplay)
  18.109 -      val minimize = minimize |> the_default perhaps_minimize
  18.110 -      val (used_facts, (preplay, message, _)) =
  18.111 -        if minimize then
  18.112 -          minimize_facts minimize_name params (not verbose) subgoal
  18.113 -                         subgoal_count state
  18.114 -                         (filter_used_facts used_facts
  18.115 -                              (map (apsnd single o untranslated_fact) facts))
  18.116 -          |>> Option.map (map fst)
  18.117 -        else
  18.118 -          (SOME used_facts, (preplay, message, ""))
  18.119 -    in
  18.120 -      case used_facts of
  18.121 -        SOME used_facts =>
  18.122 -        (if debug andalso not (null used_facts) then
  18.123 -           facts ~~ (0 upto length facts - 1)
  18.124 -           |> map (fn (fact, j) => fact |> untranslated_fact |> apsnd (K j))
  18.125 -           |> filter_used_facts used_facts
  18.126 -           |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
  18.127 -           |> commas
  18.128 -           |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^
  18.129 -                       " proof (of " ^ string_of_int (length facts) ^ "): ") "."
  18.130 -           |> Output.urgent_message
  18.131 -         else
  18.132 -           ();
  18.133 -         {outcome = NONE, used_facts = used_facts, run_time = run_time,
  18.134 -          preplay = preplay, message = message, message_tail = message_tail})
  18.135 -      | NONE => result
  18.136 -    end
  18.137 -
  18.138 -fun get_minimizing_prover ctxt mode name params minimize_command problem =
  18.139 -  get_prover ctxt mode name params minimize_command problem
  18.140 -  |> minimize ctxt mode name params problem
  18.141 -
  18.142  fun launch_prover (params as {debug, verbose, blocking, max_relevant, slice,
  18.143                                timeout, expect, ...})
  18.144          mode minimize_command only {state, goal, subgoal, subgoal_count, facts}