1.1 --- a/NEWS	Fri Mar 18 17:27:28 2011 +0100
     1.2 +++ b/NEWS	Fri Mar 18 22:55:28 2011 +0100
     1.3 @@ -50,6 +50,9 @@
     1.4    - sledgehammer available_provers ~> sledgehammer supported_provers
     1.5      INCOMPATIBILITY.
     1.6  
     1.7 +* "try":
     1.8 +  - Added "simp:", "intro:", and "elim:" options.
     1.9 +
    1.10  * Function package: discontinued option "tailrec".
    1.11  INCOMPATIBILITY. Use partial_function instead.
    1.12  

     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Mar 18 17:27:28 2011 +0100
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Mar 18 22:55:28 2011 +0100
     2.3 @@ -558,7 +558,7 @@
     2.4          Unsynchronized.ref (NONE : ((string * locality) * thm list) list option)
     2.5        val minimize = AList.defined (op =) args minimizeK
     2.6        val metis_ft = AList.defined (op =) args metis_ftK
     2.7 -      val trivial = Try.invoke_try (SOME try_timeout) pre
     2.8 +      val trivial = Try.invoke_try (SOME try_timeout) ([], [], []) pre
     2.9          handle TimeLimit.TimeOut => false
    2.10        fun apply_reconstructor m1 m2 =
    2.11          if metis_ft

     3.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Mar 18 17:27:28 2011 +0100
     3.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Mar 18 22:55:28 2011 +0100
     3.3 @@ -150,7 +150,7 @@
     3.4    let
     3.5      val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (ProofContext.init_global thy)
     3.6    in
     3.7 -    case Try.invoke_try (SOME (seconds 5.0)) state of
     3.8 +    case Try.invoke_try (SOME (seconds 5.0)) ([], [], []) state of
     3.9        true => (Solved, ([], NONE))
    3.10      | false => (Unsolved, ([], NONE))
    3.11    end

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Fri Mar 18 17:27:28 2011 +0100
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Fri Mar 18 22:55:28 2011 +0100
     4.3 @@ -115,8 +115,8 @@
     4.4    let
     4.5      val ths = Attrib.eval_thms ctxt [xthm]
     4.6      val bracket =
     4.7 -      implode (map (fn arg => "[" ^ Pretty.str_of (Args.pretty_src ctxt arg)
     4.8 -                               ^ "]") args)
     4.9 +      map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args
    4.10 +      |> implode
    4.11      fun nth_name j =
    4.12        case xref of
    4.13          Facts.Fact s => backquote s ^ bracket

     5.1 --- a/src/HOL/Tools/try.ML	Fri Mar 18 17:27:28 2011 +0100
     5.2 +++ b/src/HOL/Tools/try.ML	Fri Mar 18 22:55:28 2011 +0100
     5.3 @@ -7,7 +7,9 @@
     5.4  signature TRY =
     5.5  sig
     5.6    val auto : bool Unsynchronized.ref
     5.7 -  val invoke_try : Time.time option -> Proof.state -> bool
     5.8 +  val invoke_try :
     5.9 +    Time.time option -> string list * string list * string list -> Proof.state
    5.10 +    -> bool
    5.11    val setup : theory -> theory
    5.12  end;
    5.13  
    5.14 @@ -40,59 +42,85 @@
    5.15        NONE
    5.16    end
    5.17  
    5.18 -fun named_method thy name =
    5.19 -  Method.method thy (Args.src ((name, []), Position.none))
    5.20 +val parse_method =
    5.21 +  enclose "(" ")"
    5.22 +  #> Outer_Syntax.scan Position.start
    5.23 +  #> filter Token.is_proper
    5.24 +  #> Scan.read Token.stopper Method.parse
    5.25 +  #> (fn SOME (Method.Source src) => src | _ => raise Fail "expected Source")
    5.26  
    5.27 -fun apply_named_method_on_first_goal name ctxt =
    5.28 -  let val thy = ProofContext.theory_of ctxt in
    5.29 -    Proof.refine (Method.SelectGoals (1, Method.Basic (named_method thy name)))
    5.30 -  end
    5.31 +fun apply_named_method_on_first_goal method thy =
    5.32 +  method |> parse_method
    5.33 +         |> Method.method thy
    5.34 +         |> Method.Basic
    5.35 +         |> curry Method.SelectGoals 1
    5.36 +         |> Proof.refine
    5.37    handle ERROR _ => K Seq.empty (* e.g., the method isn't available yet *)
    5.38  
    5.39 -fun do_named_method (name, (all_goals, run_if_auto)) auto timeout_opt st =
    5.40 +fun add_attr_text (NONE, _) s = s
    5.41 +  | add_attr_text (_, []) s = s
    5.42 +  | add_attr_text (SOME x, fs) s =
    5.43 +    s ^ " " ^ (if x = "" then "" else x ^ ": ") ^ space_implode " " fs
    5.44 +fun attrs_text (sx, ix, ex) (ss, is, es) =
    5.45 +  "" |> fold add_attr_text [(sx, ss), (ix, is), (ex, es)]
    5.46 +
    5.47 +fun do_named_method (name, ((all_goals, run_if_auto), attrs)) auto timeout_opt
    5.48 +                    triple st =
    5.49    if not auto orelse run_if_auto then
    5.50 -    do_generic timeout_opt
    5.51 -               (name ^ (if all_goals andalso
    5.52 -                           nprems_of (#goal (Proof.goal st)) > 1 then
    5.53 -                          "[1]"
    5.54 -                        else
    5.55 -                          "")) I (#goal o Proof.goal)
    5.56 -               (apply_named_method_on_first_goal name (Proof.context_of st)) st
    5.57 +    let val attrs = attrs_text attrs triple in
    5.58 +      do_generic timeout_opt
    5.59 +                 (name ^ (if all_goals andalso
    5.60 +                             nprems_of (#goal (Proof.goal st)) > 1 then
    5.61 +                            "[1]"
    5.62 +                          else
    5.63 +                            "") ^
    5.64 +                  attrs) I (#goal o Proof.goal)
    5.65 +                 (apply_named_method_on_first_goal (name ^ attrs)
    5.66 +                                                   (Proof.theory_of st)) st
    5.67 +    end
    5.68    else
    5.69      NONE
    5.70  
    5.71 -(* name * (all_goals, run_if_auto) *)
    5.72 +val full_attrs = (SOME "simp", SOME "intro", SOME "elim")
    5.73 +val clas_attrs = (NONE, SOME "intro", SOME "elim")
    5.74 +val simp_attrs = (SOME "add", NONE, NONE)
    5.75 +val metis_attrs = (SOME "", SOME "", SOME "")
    5.76 +val no_attrs = (NONE, NONE, NONE)
    5.77 +
    5.78 +(* name * ((all_goals, run_if_auto), (simp, intro, elim) *)
    5.79  val named_methods =
    5.80 -  [("simp", (false, true)),
    5.81 -   ("auto", (true, true)),
    5.82 -   ("fast", (false, false)),
    5.83 -   ("fastsimp", (false, false)),
    5.84 -   ("force", (false, false)),
    5.85 -   ("blast", (false, true)),
    5.86 -   ("metis", (false, true)),
    5.87 -   ("linarith", (false, true)),
    5.88 -   ("presburger", (false, true))]
    5.89 +  [("simp", ((false, true), simp_attrs)),
    5.90 +   ("auto", ((true, true), full_attrs)),
    5.91 +   ("fast", ((false, false), clas_attrs)),
    5.92 +   ("fastsimp", ((false, false), full_attrs)),
    5.93 +   ("force", ((false, false), full_attrs)),
    5.94 +   ("blast", ((false, true), clas_attrs)),
    5.95 +   ("metis", ((false, true), metis_attrs)),
    5.96 +   ("linarith", ((false, true), no_attrs)),
    5.97 +   ("presburger", ((false, true), no_attrs))]
    5.98  val do_methods = map do_named_method named_methods
    5.99  
   5.100  fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"
   5.101  
   5.102 -fun do_try auto timeout_opt st =
   5.103 +fun do_try auto timeout_opt triple st =
   5.104    let
   5.105      val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose false)
   5.106    in
   5.107 -    case do_methods |> Par_List.map (fn f => f auto timeout_opt st)
   5.108 +    case do_methods |> Par_List.map (fn f => f auto timeout_opt triple st)
   5.109                      |> map_filter I |> sort (int_ord o pairself snd) of
   5.110        [] => (if auto then () else writeln "No proof found."; (false, st))
   5.111      | xs as (s, _) :: _ =>
   5.112        let
   5.113 -        val xs = xs |> map swap |> AList.coalesce (op =)
   5.114 +        val xs = xs |> map (fn (s, n) => (n, hd (space_explode " " s)))
   5.115 +                    |> AList.coalesce (op =)
   5.116                      |> map (swap o apsnd commas)
   5.117 +        val need_parens = exists_string (curry (op =) " ") s
   5.118          val message =
   5.119            (if auto then "Auto Try found a proof" else "Try this command") ^
   5.120            ": " ^
   5.121            Markup.markup Markup.sendback
   5.122                ((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
   5.123 -                else "apply") ^ " " ^ s) ^
   5.124 +                else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^
   5.125            "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"
   5.126        in
   5.127          (true, st |> (if auto then
   5.128 @@ -105,17 +133,43 @@
   5.129        end
   5.130    end
   5.131  
   5.132 -val invoke_try = fst oo do_try false
   5.133 +fun invoke_try timeout_opt = fst oo do_try false timeout_opt
   5.134  
   5.135  val tryN = "try"
   5.136  
   5.137 +fun try_trans triple =
   5.138 +  Toplevel.keep (K () o do_try false (SOME default_timeout) triple
   5.139 +                 o Toplevel.proof_of)
   5.140 +
   5.141 +fun merge_attrs (s1, i1, e1) (s2, i2, e2) = (s1 @ s2, i1 @ i2, e1 @ e2)
   5.142 +
   5.143 +fun string_of_xthm (xref, args) =
   5.144 +  Facts.string_of_ref xref ^
   5.145 +  implode (map (enclose "[" "]" o Pretty.str_of
   5.146 +                o Args.pretty_src @{context}) args)
   5.147 +
   5.148 +val parse_fact_refs =
   5.149 +  Scan.repeat1 (Scan.unless (Parse.name -- Args.colon)
   5.150 +                            (Parse_Spec.xthm >> string_of_xthm))
   5.151 +val parse_attr =
   5.152 +     Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs
   5.153 +     >> (fn ss => (ss, [], []))
   5.154 +  || Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs
   5.155 +     >> (fn is => ([], is, []))
   5.156 +  || Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs
   5.157 +     >> (fn es => ([], [], es))
   5.158 +fun parse_attrs x =
   5.159 +    (Args.parens parse_attrs
   5.160 +  || Scan.repeat parse_attr
   5.161 +     >> (fn triple => fold merge_attrs triple ([], [], []))) x
   5.162 +
   5.163 +val parse_try_command = Scan.optional parse_attrs ([], [], []) #>> try_trans
   5.164 +
   5.165  val _ =
   5.166    Outer_Syntax.improper_command tryN
   5.167 -      "try a combination of proof methods" Keyword.diag
   5.168 -      (Scan.succeed (Toplevel.keep (K () o do_try false (SOME default_timeout)
   5.169 -                                    o Toplevel.proof_of)))
   5.170 +      "try a combination of proof methods" Keyword.diag parse_try_command
   5.171  
   5.172 -val auto_try = do_try true NONE
   5.173 +val auto_try = do_try true NONE ([], [], [])
   5.174  
   5.175  val setup = Auto_Tools.register_tool (auto, auto_try)
   5.176