merged
authorbulwahn
Thu Mar 31 17:15:13 2011 +0200 (2011-03-31)
changeset 421857101712baae8
parent 42184 1d4fae76ba5e
parent 42183 173b0f488428
child 42186 bb688200b949
child 42188 f6bc441fbf19
merged
     1.1 --- a/NEWS	Thu Mar 31 11:17:52 2011 +0200
     1.2 +++ b/NEWS	Thu Mar 31 17:15:13 2011 +0200
     1.3 @@ -49,6 +49,7 @@
     1.4  * Sledgehammer:
     1.5    - sledgehammer available_provers ~> sledgehammer supported_provers
     1.6      INCOMPATIBILITY.
     1.7 +  - Added "monomorphize" and "monomorphize_limit" options.
     1.8  
     1.9  * "try":
    1.10    - Added "simp:", "intro:", and "elim:" options.
     2.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Thu Mar 31 11:17:52 2011 +0200
     2.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Thu Mar 31 17:15:13 2011 +0200
     2.3 @@ -555,6 +555,19 @@
     2.4  filter. If the option is set to \textit{smart}, it is set to a value that was
     2.5  empirically found to be appropriate for the prover. A typical value would be
     2.6  300.
     2.7 +
     2.8 +\opfalse{monomorphize}{dont\_monomorphize}
     2.9 +Specifies whether the relevant facts should be monomorphized---i.e., whether
    2.10 +their type variables should be instantiated with relevant ground types.
    2.11 +Monomorphization is always performed for SMT solvers, irrespective of this
    2.12 +option. Monomorphization can simplify reasoning but also leads to larger fact
    2.13 +bases, which can slow down the ATPs.
    2.14 +
    2.15 +\opdefault{monomorphize\_limit}{int}{\upshape 4}
    2.16 +Specifies the maximum number of iterations for the monomorphization fixpoint
    2.17 +construction. The higher this limit is, the more monomorphic instances are
    2.18 +potentially generated.
    2.19 +
    2.20  \end{enum}
    2.21  
    2.22  \subsection{Output Format}
     3.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Mar 31 11:17:52 2011 +0200
     3.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Mar 31 17:15:13 2011 +0200
     3.3 @@ -558,7 +558,7 @@
     3.4          Unsynchronized.ref (NONE : ((string * locality) * thm list) list option)
     3.5        val minimize = AList.defined (op =) args minimizeK
     3.6        val metis_ft = AList.defined (op =) args metis_ftK
     3.7 -      val trivial = Try.invoke_try (SOME try_timeout) ([], [], []) pre
     3.8 +      val trivial = Try.invoke_try (SOME try_timeout) ([], [], [], []) pre
     3.9          handle TimeLimit.TimeOut => false
    3.10        fun apply_reconstructor m1 m2 =
    3.11          if metis_ft
     4.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Thu Mar 31 11:17:52 2011 +0200
     4.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Thu Mar 31 17:15:13 2011 +0200
     4.3 @@ -154,7 +154,7 @@
     4.4    let
     4.5      val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (ProofContext.init_global thy)
     4.6    in
     4.7 -    case Try.invoke_try (SOME (seconds 5.0)) ([], [], []) state of
     4.8 +    case Try.invoke_try (SOME (seconds 5.0)) ([], [], [], []) state of
     4.9        true => (Solved, [])
    4.10      | false => (Unsolved, [])
    4.11    end
     5.1 --- a/src/HOL/Tools/SMT/smt_monomorph.ML	Thu Mar 31 11:17:52 2011 +0200
     5.2 +++ b/src/HOL/Tools/SMT/smt_monomorph.ML	Thu Mar 31 17:15:13 2011 +0200
     5.3 @@ -28,8 +28,9 @@
     5.4  
     5.5  signature SMT_MONOMORPH =
     5.6  sig
     5.7 -  val monomorph: (int * thm) list -> Proof.context ->
     5.8 -    (int * thm) list * Proof.context
     5.9 +  val typ_has_tvars: typ -> bool
    5.10 +  val monomorph: bool -> ('a * thm) list -> Proof.context ->
    5.11 +    ('a * thm) list * Proof.context
    5.12  end
    5.13  
    5.14  structure SMT_Monomorph: SMT_MONOMORPH =
    5.15 @@ -159,37 +160,44 @@
    5.16  
    5.17    in most_specific [] end
    5.18  
    5.19 -fun instantiate (i, thm) substs (ithms, ctxt) =
    5.20 +fun instantiate full (i, thm) substs (ithms, ctxt) =
    5.21    let
    5.22 +    val thy = ProofContext.theory_of ctxt
    5.23 +
    5.24      val (vs, Ss) = split_list (Term.add_tvars (Thm.prop_of thm) [])
    5.25      val (Tenv, ctxt') =
    5.26        ctxt
    5.27        |> Variable.invent_types Ss
    5.28        |>> map2 (fn v => fn (n, S) => (v, (S, TFree (n, S)))) vs
    5.29  
    5.30 -    val thy = ProofContext.theory_of ctxt'
    5.31 +    exception PARTIAL_INST of unit
    5.32 +
    5.33 +    fun update_subst vT subst =
    5.34 +      if full then Vartab.update vT subst
    5.35 +      else raise PARTIAL_INST ()
    5.36  
    5.37      fun replace (v, (_, T)) (U as TVar (u, _)) = if u = v then T else U
    5.38        | replace _ T = T
    5.39  
    5.40      fun complete (vT as (v, _)) subst =
    5.41        subst
    5.42 -      |> not (Vartab.defined subst v) ? Vartab.update vT
    5.43 +      |> not (Vartab.defined subst v) ? update_subst vT
    5.44        |> Vartab.map (K (apsnd (Term.map_atyps (replace vT))))
    5.45  
    5.46      fun cert (ix, (S, T)) = pairself (Thm.ctyp_of thy) (TVar (ix, S), T)
    5.47  
    5.48      fun inst subst =
    5.49        let val cTs = Vartab.fold (cons o cert) (fold complete Tenv subst) []
    5.50 -      in (i, Thm.instantiate (cTs, []) thm) end
    5.51 +      in SOME (i, Thm.instantiate (cTs, []) thm) end
    5.52 +      handle PARTIAL_INST () => NONE
    5.53  
    5.54 -  in (map inst substs @ ithms, ctxt') end
    5.55 +  in (map_filter inst substs @ ithms, if full then ctxt' else ctxt) end
    5.56  
    5.57  
    5.58  
    5.59  (* overall procedure *)
    5.60  
    5.61 -fun mono_all ctxt polys monos =
    5.62 +fun mono_all full ctxt polys monos =
    5.63    let
    5.64      val scss = map (single o pair Vartab.empty o tvar_consts_of o snd) polys
    5.65  
    5.66 @@ -208,13 +216,13 @@
    5.67      |> search_substitutions ctxt limit instances Symtab.empty grounds
    5.68      |> map (filter_most_specific (ProofContext.theory_of ctxt))
    5.69      |> rpair (monos, ctxt)
    5.70 -    |-> fold2 instantiate polys
    5.71 +    |-> fold2 (instantiate full) polys
    5.72    end
    5.73  
    5.74 -fun monomorph irules ctxt =
    5.75 +fun monomorph full irules ctxt =
    5.76    irules
    5.77    |> List.partition (Term.exists_type typ_has_tvars o Thm.prop_of o snd)
    5.78    |>> incr_indexes  (* avoid clashes of schematic type variables *)
    5.79 -  |-> (fn [] => rpair ctxt | polys => mono_all ctxt polys)
    5.80 +  |-> (fn [] => rpair ctxt | polys => mono_all full ctxt polys)
    5.81  
    5.82  end
     6.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Thu Mar 31 11:17:52 2011 +0200
     6.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Thu Mar 31 17:15:13 2011 +0200
     6.3 @@ -631,7 +631,7 @@
     6.4    |> gen_normalize ctxt
     6.5    |> unfold1 ctxt
     6.6    |> rpair ctxt
     6.7 -  |-> SMT_Monomorph.monomorph
     6.8 +  |-> SMT_Monomorph.monomorph true
     6.9    |-> unfold2
    6.10    |-> apply_extra_norms
    6.11  
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Thu Mar 31 11:17:52 2011 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Thu Mar 31 17:15:13 2011 +0200
     7.3 @@ -88,6 +88,8 @@
     7.4    #> raw_explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation
     7.5    #> fst
     7.6  
     7.7 +val unprefix_fact_number = space_implode "_" o tl o space_explode "_"
     7.8 +
     7.9  fun repair_conjecture_shape_and_fact_names output conjecture_shape fact_names =
    7.10    if String.isSubstring set_ClauseFormulaRelationN output then
    7.11      let
    7.12 @@ -100,7 +102,8 @@
    7.13          |> map (fn s => find_index (curry (op =) s) seq + 1)
    7.14        fun names_for_number j =
    7.15          j |> AList.lookup (op =) name_map |> these
    7.16 -          |> map_filter (try (unprefix fact_prefix)) |> map unascii_of
    7.17 +          |> map_filter (try (unascii_of o unprefix_fact_number
    7.18 +                              o unprefix fact_prefix))
    7.19            |> map (fn name =>
    7.20                       (name, name |> find_first_in_list_vector fact_names |> the)
    7.21                       handle Option.Option =>
    7.22 @@ -145,16 +148,19 @@
    7.23        "\nTo minimize the number of lemmas, try this: " ^
    7.24        Markup.markup Markup.sendback command ^ "."
    7.25  
    7.26 -val vampire_fact_prefix = "f" (* grrr... *)
    7.27 +val vampire_step_prefix = "f" (* grrr... *)
    7.28  
    7.29  fun resolve_fact fact_names ((_, SOME s)) =
    7.30 -    (case strip_prefix_and_unascii fact_prefix s of
    7.31 -       SOME s' => (case find_first_in_list_vector fact_names s' of
    7.32 -                     SOME x => [(s', x)]
    7.33 -                   | NONE => [])
    7.34 +    (case try (unprefix fact_prefix) s of
    7.35 +       SOME s' =>
    7.36 +       let val s' = s' |> unprefix_fact_number |> unascii_of in
    7.37 +         case find_first_in_list_vector fact_names s' of
    7.38 +           SOME x => [(s', x)]
    7.39 +         | NONE => []
    7.40 +       end
    7.41       | NONE => [])
    7.42    | resolve_fact fact_names (num, NONE) =
    7.43 -    case Int.fromString (perhaps (try (unprefix vampire_fact_prefix)) num) of
    7.44 +    case Int.fromString (perhaps (try (unprefix vampire_step_prefix)) num) of
    7.45        SOME j =>
    7.46        if j > 0 andalso j <= Vector.length fact_names then
    7.47          Vector.sub (fact_names, j - 1)
    7.48 @@ -233,7 +239,7 @@
    7.49  
    7.50  val raw_prefix = "X"
    7.51  val assum_prefix = "A"
    7.52 -val fact_prefix = "F"
    7.53 +val have_prefix = "F"
    7.54  
    7.55  fun resolve_conjecture conjecture_shape (num, s_opt) =
    7.56    let
    7.57 @@ -847,7 +853,7 @@
    7.58                (l, subst, next_fact)
    7.59              else
    7.60                let
    7.61 -                val l' = (prefix_for_depth depth fact_prefix, next_fact)
    7.62 +                val l' = (prefix_for_depth depth have_prefix, next_fact)
    7.63                in (l', (l, l') :: subst, next_fact + 1) end
    7.64            val relabel_facts =
    7.65              apfst (maps (the_list o AList.lookup (op =) subst))
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu Mar 31 11:17:52 2011 +0200
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu Mar 31 17:15:13 2011 +0200
     8.3 @@ -442,9 +442,13 @@
     8.4                  (atp_type_literals_for_types type_sys ctypes_sorts))
     8.5             (formula_for_combformula ctxt type_sys combformula)
     8.6  
     8.7 -fun problem_line_for_fact ctxt prefix type_sys (formula as {name, kind, ...}) =
     8.8 -  Fof (prefix ^ ascii_of name, kind, formula_for_fact ctxt type_sys formula,
     8.9 -       NONE)
    8.10 +(* Each fact is given a unique fact number to avoid name clashes (e.g., because
    8.11 +   of monomorphization). The TPTP explicitly forbids name clashes, and some of
    8.12 +   the remote provers might care. *)
    8.13 +fun problem_line_for_fact ctxt prefix type_sys
    8.14 +                          (j, formula as {name, kind, ...}) =
    8.15 +  Fof (prefix ^ string_of_int j ^ "_" ^ ascii_of name, kind,
    8.16 +       formula_for_fact ctxt type_sys formula, NONE)
    8.17  
    8.18  fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
    8.19                                                         superclass, ...}) =
    8.20 @@ -626,7 +630,8 @@
    8.21      (* Reordering these might or might not confuse the proof reconstruction
    8.22         code or the SPASS Flotter hack. *)
    8.23      val problem =
    8.24 -      [(factsN, map (problem_line_for_fact ctxt fact_prefix type_sys) facts),
    8.25 +      [(factsN, map (problem_line_for_fact ctxt fact_prefix type_sys)
    8.26 +                    (0 upto length facts - 1 ~~ facts)),
    8.27         (class_relsN, map problem_line_for_class_rel_clause class_rel_clauses),
    8.28         (aritiesN, map problem_line_for_arity_clause arity_clauses),
    8.29         (helpersN, []),
    8.30 @@ -638,7 +643,8 @@
    8.31      val helper_lines =
    8.32        get_helper_facts ctxt explicit_forall type_sys
    8.33                         (maps (map (#3 o dest_Fof) o snd) problem)
    8.34 -      |>> map (problem_line_for_fact ctxt helper_prefix type_sys
    8.35 +      |>> map (pair 0
    8.36 +               #> problem_line_for_fact ctxt helper_prefix type_sys
    8.37                 #> repair_problem_line thy explicit_forall type_sys const_tab)
    8.38        |> op @
    8.39      val (problem, pool) =
     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Mar 31 11:17:52 2011 +0200
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Mar 31 17:15:13 2011 +0200
     9.3 @@ -79,10 +79,12 @@
     9.4     ("verbose", "false"),
     9.5     ("overlord", "false"),
     9.6     ("blocking", "false"),
     9.7 +   ("relevance_thresholds", "0.45 0.85"),
     9.8 +   ("max_relevant", "smart"),
     9.9 +   ("monomorphize", "false"),
    9.10 +   ("monomorphize_limit", "4"),
    9.11     ("type_sys", "smart"),
    9.12     ("explicit_apply", "false"),
    9.13 -   ("relevance_thresholds", "0.45 0.85"),
    9.14 -   ("max_relevant", "smart"),
    9.15     ("isar_proof", "false"),
    9.16     ("isar_shrink_factor", "1")]
    9.17  
    9.18 @@ -95,6 +97,7 @@
    9.19     ("quiet", "verbose"),
    9.20     ("no_overlord", "overlord"),
    9.21     ("non_blocking", "blocking"),
    9.22 +   ("dont_monomorphize", "monomorphize"),
    9.23     ("partial_types", "full_types"),
    9.24     ("implicit_apply", "explicit_apply"),
    9.25     ("no_isar_proof", "isar_proof")]
    9.26 @@ -233,6 +236,10 @@
    9.27      val blocking = auto orelse debug orelse lookup_bool "blocking"
    9.28      val provers = lookup_string "provers" |> space_explode " "
    9.29                    |> auto ? single o hd
    9.30 +    val relevance_thresholds = lookup_real_pair "relevance_thresholds"
    9.31 +    val max_relevant = lookup_int_option "max_relevant"
    9.32 +    val monomorphize = lookup_bool "monomorphize"
    9.33 +    val monomorphize_limit = lookup_int "monomorphize_limit"
    9.34      val type_sys =
    9.35        case (lookup_string "type_sys", lookup_bool "full_types") of
    9.36          ("tags", full_types) => Tags full_types
    9.37 @@ -245,18 +252,18 @@
    9.38          else
    9.39            error ("Unknown type system: " ^ quote type_sys ^ ".")
    9.40      val explicit_apply = lookup_bool "explicit_apply"
    9.41 -    val relevance_thresholds = lookup_real_pair "relevance_thresholds"
    9.42 -    val max_relevant = lookup_int_option "max_relevant"
    9.43      val isar_proof = lookup_bool "isar_proof"
    9.44      val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
    9.45      val timeout = (if auto then NONE else lookup_time "timeout") |> the_timeout
    9.46      val expect = lookup_string "expect"
    9.47    in
    9.48      {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
    9.49 -     provers = provers, type_sys = type_sys, explicit_apply = explicit_apply,
    9.50 -     relevance_thresholds = relevance_thresholds, max_relevant = max_relevant,
    9.51 -     isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
    9.52 -     timeout = timeout, expect = expect}
    9.53 +     provers = provers, relevance_thresholds = relevance_thresholds,
    9.54 +     max_relevant = max_relevant, monomorphize = monomorphize,
    9.55 +     monomorphize_limit = monomorphize_limit, type_sys = type_sys,
    9.56 +     explicit_apply = explicit_apply, isar_proof = isar_proof,
    9.57 +     isar_shrink_factor = isar_shrink_factor, timeout = timeout,
    9.58 +     expect = expect}
    9.59    end
    9.60  
    9.61  fun get_params auto ctxt = extract_params auto (default_raw_params ctxt)
    10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Mar 31 11:17:52 2011 +0200
    10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Mar 31 17:15:13 2011 +0200
    10.3 @@ -42,8 +42,8 @@
    10.4  
    10.5  fun print silent f = if silent then () else Output.urgent_message (f ())
    10.6  
    10.7 -fun test_facts ({debug, verbose, overlord, provers, type_sys, isar_proof,
    10.8 -                 isar_shrink_factor, ...} : params)
    10.9 +fun test_facts ({debug, verbose, overlord, provers, monomorphize_limit,
   10.10 +                 type_sys, isar_proof, isar_shrink_factor, ...} : params)
   10.11          explicit_apply_opt silent (prover : prover) timeout i n state facts =
   10.12    let
   10.13      val thy = Proof.theory_of state
   10.14 @@ -65,6 +65,7 @@
   10.15        {debug = debug, verbose = verbose, overlord = overlord, blocking = true,
   10.16         provers = provers, type_sys = type_sys, explicit_apply = explicit_apply,
   10.17         relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
   10.18 +       monomorphize = false, monomorphize_limit = monomorphize_limit,
   10.19         isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
   10.20         timeout = timeout, expect = ""}
   10.21      val facts =
    11.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Mar 31 11:17:52 2011 +0200
    11.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Mar 31 17:15:13 2011 +0200
    11.3 @@ -21,10 +21,12 @@
    11.4       overlord: bool,
    11.5       blocking: bool,
    11.6       provers: string list,
    11.7 +     relevance_thresholds: real * real,
    11.8 +     max_relevant: int option,
    11.9 +     monomorphize: bool,
   11.10 +     monomorphize_limit: int,
   11.11       type_sys: type_system,
   11.12       explicit_apply: bool,
   11.13 -     relevance_thresholds: real * real,
   11.14 -     max_relevant: int option,
   11.15       isar_proof: bool,
   11.16       isar_shrink_factor: int,
   11.17       timeout: Time.time,
   11.18 @@ -66,7 +68,6 @@
   11.19    val smt_iter_fact_frac : real Unsynchronized.ref
   11.20    val smt_iter_time_frac : real Unsynchronized.ref
   11.21    val smt_iter_min_msecs : int Unsynchronized.ref
   11.22 -  val smt_monomorphize_limit : int Unsynchronized.ref
   11.23  
   11.24    val das_Tool : string
   11.25    val select_smt_solver : string -> Proof.context -> Proof.context
   11.26 @@ -229,10 +230,12 @@
   11.27     overlord: bool,
   11.28     blocking: bool,
   11.29     provers: string list,
   11.30 +   relevance_thresholds: real * real,
   11.31 +   max_relevant: int option,
   11.32 +   monomorphize: bool,
   11.33 +   monomorphize_limit: int,
   11.34     type_sys: type_system,
   11.35     explicit_apply: bool,
   11.36 -   relevance_thresholds: real * real,
   11.37 -   max_relevant: int option,
   11.38     isar_proof: bool,
   11.39     isar_shrink_factor: int,
   11.40     timeout: Time.time,
   11.41 @@ -333,13 +336,40 @@
   11.42          ({exec, required_execs, arguments, has_incomplete_mode, proof_delims,
   11.43            known_failures, explicit_forall, use_conjecture_for_hypotheses, ...}
   11.44            : atp_config)
   11.45 -        ({debug, verbose, overlord, type_sys, explicit_apply, isar_proof,
   11.46 -          isar_shrink_factor, timeout, ...} : params)
   11.47 +        ({debug, verbose, overlord, monomorphize, monomorphize_limit, type_sys,
   11.48 +          explicit_apply, isar_proof, isar_shrink_factor, timeout, ...}
   11.49 +         : params)
   11.50          minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) =
   11.51    let
   11.52 +    val thy = Proof.theory_of state
   11.53      val ctxt = Proof.context_of state
   11.54      val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
   11.55 -    val facts = facts |> map (atp_translated_fact ctxt)
   11.56 +    fun monomorphize_facts facts =
   11.57 +      let
   11.58 +        val facts = facts |> map untranslated_fact
   11.59 +        (* pseudo-theorem involving the same constants as the subgoal *)
   11.60 +        val subgoal_th =
   11.61 +          Logic.list_implies (hyp_ts, concl_t) |> Skip_Proof.make_thm thy
   11.62 +        val indexed_facts =
   11.63 +          (~1, subgoal_th) :: (0 upto length facts - 1 ~~ map snd facts)
   11.64 +        val (mono_facts, ctxt') =
   11.65 +          ctxt |> Config.put SMT_Config.verbose debug
   11.66 +               |> Config.put SMT_Config.monomorph_limit monomorphize_limit
   11.67 +               |> SMT_Monomorph.monomorph true indexed_facts
   11.68 +      in
   11.69 +        mono_facts
   11.70 +        |> sort (int_ord o pairself fst)
   11.71 +        |> filter_out (curry (op =) ~1 o fst)
   11.72 +        (* The next step shouldn't be necessary but currently the monomorphizer
   11.73 +           generates unexpected instances with fresh TFrees, which typically
   11.74 +           become TVars once exported. *)
   11.75 +        |> filter_out (Term.exists_type SMT_Monomorph.typ_has_tvars
   11.76 +                       o singleton (Variable.export_terms ctxt' ctxt)
   11.77 +                       o prop_of o snd)
   11.78 +        |> map (Untranslated_Fact o apfst (fst o nth facts))
   11.79 +      end
   11.80 +    val facts = facts |> monomorphize ? monomorphize_facts
   11.81 +                      |> map (atp_translated_fact ctxt)
   11.82      val (dest_dir, problem_prefix) =
   11.83        if overlord then overlord_file_location_for_prover name
   11.84        else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix)
   11.85 @@ -513,9 +543,9 @@
   11.86  val smt_iter_fact_frac = Unsynchronized.ref 0.5
   11.87  val smt_iter_time_frac = Unsynchronized.ref 0.5
   11.88  val smt_iter_min_msecs = Unsynchronized.ref 5000
   11.89 -val smt_monomorphize_limit = Unsynchronized.ref 4
   11.90  
   11.91 -fun smt_filter_loop name ({debug, verbose, overlord, timeout, ...} : params)
   11.92 +fun smt_filter_loop name ({debug, verbose, overlord, monomorphize_limit,
   11.93 +                           timeout, ...} : params)
   11.94                      state i smt_filter =
   11.95    let
   11.96      val ctxt = Proof.context_of state
   11.97 @@ -529,7 +559,7 @@
   11.98            else
   11.99              I)
  11.100        #> Config.put SMT_Config.infer_triggers (!smt_triggers)
  11.101 -      #> Config.put SMT_Config.monomorph_limit (!smt_monomorphize_limit)
  11.102 +      #> Config.put SMT_Config.monomorph_limit monomorphize_limit
  11.103      val state = state |> Proof.map_context repair_context
  11.104  
  11.105      fun iter timeout iter_num outcome0 time_so_far facts =
    12.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Mar 31 11:17:52 2011 +0200
    12.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Mar 31 17:15:13 2011 +0200
    12.3 @@ -164,9 +164,9 @@
    12.4  (* FUDGE *)
    12.5  val auto_max_relevant_divisor = 2
    12.6  
    12.7 -fun run_sledgehammer (params as {debug, blocking, provers, type_sys,
    12.8 -                                 relevance_thresholds, max_relevant, timeout,
    12.9 -                                 ...})
   12.10 +fun run_sledgehammer (params as {debug, blocking, provers, monomorphize,
   12.11 +                                 type_sys, relevance_thresholds, max_relevant,
   12.12 +                                 timeout, ...})
   12.13                       auto i (relevance_override as {only, ...}) minimize_command
   12.14                       state =
   12.15    if null provers then
   12.16 @@ -246,7 +246,10 @@
   12.17          else
   12.18            launch_provers state
   12.19                (get_facts "ATP" no_dangerous_types atp_relevance_fudge o K atps)
   12.20 -              (ATP_Translated_Fact oo K (translate_atp_fact ctxt false o fst))
   12.21 +              (if monomorphize then
   12.22 +                 K (Untranslated_Fact o fst)
   12.23 +               else
   12.24 +                 ATP_Translated_Fact oo K (translate_atp_fact ctxt false o fst))
   12.25                (K (K NONE)) atps
   12.26        fun launch_smts accum =
   12.27          if null smts then
    13.1 --- a/src/HOL/Tools/try.ML	Thu Mar 31 11:17:52 2011 +0200
    13.2 +++ b/src/HOL/Tools/try.ML	Thu Mar 31 17:15:13 2011 +0200
    13.3 @@ -8,8 +8,8 @@
    13.4  sig
    13.5    val auto : bool Unsynchronized.ref
    13.6    val invoke_try :
    13.7 -    Time.time option -> string list * string list * string list -> Proof.state
    13.8 -    -> bool
    13.9 +    Time.time option -> string list * string list * string list * string list
   13.10 +    -> Proof.state -> bool
   13.11    val setup : theory -> theory
   13.12  end;
   13.13  
   13.14 @@ -61,13 +61,13 @@
   13.15    | add_attr_text (_, []) s = s
   13.16    | add_attr_text (SOME x, fs) s =
   13.17      s ^ " " ^ (if x = "" then "" else x ^ ": ") ^ space_implode " " fs
   13.18 -fun attrs_text (sx, ix, ex) (ss, is, es) =
   13.19 -  "" |> fold add_attr_text [(sx, ss), (ix, is), (ex, es)]
   13.20 +fun attrs_text (sx, ix, ex, dx) (ss, is, es, ds) =
   13.21 +  "" |> fold add_attr_text [(sx, ss), (ix, is), (ex, es), (dx, ds)]
   13.22  
   13.23  fun do_named_method (name, ((all_goals, run_if_auto), attrs)) auto timeout_opt
   13.24 -                    triple st =
   13.25 +                    quad st =
   13.26    if not auto orelse run_if_auto then
   13.27 -    let val attrs = attrs_text attrs triple in
   13.28 +    let val attrs = attrs_text attrs quad in
   13.29        do_generic timeout_opt
   13.30                   (name ^ (if all_goals andalso
   13.31                               nprems_of (#goal (Proof.goal st)) > 1 then
   13.32 @@ -81,13 +81,13 @@
   13.33    else
   13.34      NONE
   13.35  
   13.36 -val full_attrs = (SOME "simp", SOME "intro", SOME "elim")
   13.37 -val clas_attrs = (NONE, SOME "intro", SOME "elim")
   13.38 -val simp_attrs = (SOME "add", NONE, NONE)
   13.39 -val metis_attrs = (SOME "", SOME "", SOME "")
   13.40 -val no_attrs = (NONE, NONE, NONE)
   13.41 +val full_attrs = (SOME "simp", SOME "intro", SOME "elim", SOME "dest")
   13.42 +val clas_attrs = (NONE, SOME "intro", SOME "elim", SOME "dest")
   13.43 +val simp_attrs = (SOME "add", NONE, NONE, NONE)
   13.44 +val metis_attrs = (SOME "", SOME "", SOME "", SOME "")
   13.45 +val no_attrs = (NONE, NONE, NONE, NONE)
   13.46  
   13.47 -(* name * ((all_goals, run_if_auto), (simp, intro, elim) *)
   13.48 +(* name * ((all_goals, run_if_auto), (simp, intro, elim, dest) *)
   13.49  val named_methods =
   13.50    [("simp", ((false, true), simp_attrs)),
   13.51     ("auto", ((true, true), full_attrs)),
   13.52 @@ -102,11 +102,11 @@
   13.53  
   13.54  fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"
   13.55  
   13.56 -fun do_try auto timeout_opt triple st =
   13.57 +fun do_try auto timeout_opt quad st =
   13.58    let
   13.59      val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose false)
   13.60    in
   13.61 -    case do_methods |> Par_List.map (fn f => f auto timeout_opt triple st)
   13.62 +    case do_methods |> Par_List.map (fn f => f auto timeout_opt quad st)
   13.63                      |> map_filter I |> sort (int_ord o pairself snd) of
   13.64        [] => (if auto then () else writeln "No proof found."; (false, st))
   13.65      | xs as (s, _) :: _ =>
   13.66 @@ -137,11 +137,12 @@
   13.67  
   13.68  val tryN = "try"
   13.69  
   13.70 -fun try_trans triple =
   13.71 -  Toplevel.keep (K () o do_try false (SOME default_timeout) triple
   13.72 +fun try_trans quad =
   13.73 +  Toplevel.keep (K () o do_try false (SOME default_timeout) quad
   13.74                   o Toplevel.proof_of)
   13.75  
   13.76 -fun merge_attrs (s1, i1, e1) (s2, i2, e2) = (s1 @ s2, i1 @ i2, e1 @ e2)
   13.77 +fun merge_attrs (s1, i1, e1, d1) (s2, i2, e2, d2) =
   13.78 +  (s1 @ s2, i1 @ i2, e1 @ e2, d1 @ d2)
   13.79  
   13.80  fun string_of_xthm (xref, args) =
   13.81    Facts.string_of_ref xref ^
   13.82 @@ -153,23 +154,25 @@
   13.83                              (Parse_Spec.xthm >> string_of_xthm))
   13.84  val parse_attr =
   13.85       Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs
   13.86 -     >> (fn ss => (ss, [], []))
   13.87 +     >> (fn ss => (ss, [], [], []))
   13.88    || Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs
   13.89 -     >> (fn is => ([], is, []))
   13.90 +     >> (fn is => ([], is, [], []))
   13.91    || Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs
   13.92 -     >> (fn es => ([], [], es))
   13.93 +     >> (fn es => ([], [], es, []))
   13.94 +  || Args.$$$ "dest" |-- Args.colon |-- parse_fact_refs
   13.95 +     >> (fn ds => ([], [], [], ds))
   13.96  fun parse_attrs x =
   13.97      (Args.parens parse_attrs
   13.98    || Scan.repeat parse_attr
   13.99 -     >> (fn triple => fold merge_attrs triple ([], [], []))) x
  13.100 +     >> (fn quad => fold merge_attrs quad ([], [], [], []))) x
  13.101  
  13.102 -val parse_try_command = Scan.optional parse_attrs ([], [], []) #>> try_trans
  13.103 +val parse_try_command = Scan.optional parse_attrs ([], [], [], []) #>> try_trans
  13.104  
  13.105  val _ =
  13.106    Outer_Syntax.improper_command tryN
  13.107        "try a combination of proof methods" Keyword.diag parse_try_command
  13.108  
  13.109 -val auto_try = do_try true NONE ([], [], [])
  13.110 +val auto_try = do_try true NONE ([], [], [], [])
  13.111  
  13.112  val setup = Auto_Tools.register_tool (auto, auto_try)
  13.113