renamed 'try_methods' to 'try0'
authorblanchet
Fri Feb 24 11:23:34 2012 +0100 (2012-02-24)
changeset 466418801a24f9e9a
parent 46640 622691cec7c3
child 46642 37a055f37224
renamed 'try_methods' to 'try0'
NEWS
doc-src/IsarRef/Thy/HOL_Specific.thy
doc-src/IsarRef/Thy/document/HOL_Specific.tex
etc/isar-keywords.el
src/HOL/IsaMakefile
src/HOL/Metis.thy
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Mutabelle/mutabelle_extra.ML
src/HOL/Tools/try0.ML
src/HOL/Tools/try_methods.ML
     1.1 --- a/NEWS	Fri Feb 24 11:23:33 2012 +0100
     1.2 +++ b/NEWS	Fri Feb 24 11:23:34 2012 +0100
     1.3 @@ -336,6 +336,9 @@
     1.4    - Added possibility to specify lambda translations scheme as a
     1.5      parenthesized argument (e.g., "by (metis (lifting) ...)").
     1.6  
     1.7 +* Command 'try0':
     1.8 +  - Renamed from 'try_methods'. INCOMPATIBILITY.
     1.9 +
    1.10  
    1.11  *** FOL ***
    1.12  
     2.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Feb 24 11:23:33 2012 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Feb 24 11:23:34 2012 +0100
     2.3 @@ -1571,7 +1571,7 @@
     2.4    \begin{matharray}{rcl}
     2.5      @{command_def (HOL) "solve_direct"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
     2.6      @{command_def (HOL) "try"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
     2.7 -    @{command_def (HOL) "try_methods"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
     2.8 +    @{command_def (HOL) "try0"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
     2.9      @{command_def (HOL) "sledgehammer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
    2.10      @{command_def (HOL) "sledgehammer_params"} & : & @{text "theory \<rightarrow> theory"}
    2.11    \end{matharray}
    2.12 @@ -1580,7 +1580,7 @@
    2.13      @@{command (HOL) try}
    2.14      ;
    2.15  
    2.16 -    @@{command (HOL) try_methods} ( ( ( 'simp' | 'intro' | 'elim' | 'dest' ) ':' @{syntax thmrefs} ) + ) ?
    2.17 +    @@{command (HOL) try0} ( ( ( 'simp' | 'intro' | 'elim' | 'dest' ) ':' @{syntax thmrefs} ) + ) ?
    2.18        @{syntax nat}?
    2.19      ;
    2.20  
    2.21 @@ -1603,7 +1603,7 @@
    2.22    subgoals can be solved directly by an existing theorem. Duplicate
    2.23    lemmas can be detected in this way.
    2.24  
    2.25 -  \item @{command (HOL) "try_methods"} attempts to prove a subgoal
    2.26 +  \item @{command (HOL) "try0"} attempts to prove a subgoal
    2.27    using a combination of standard proof methods (@{method auto},
    2.28    @{method simp}, @{method blast}, etc.).  Additional facts supplied
    2.29    via @{text "simp:"}, @{text "intro:"}, @{text "elim:"}, and @{text
    2.30 @@ -1612,7 +1612,7 @@
    2.31    \item @{command (HOL) "try"} attempts to prove or disprove a subgoal
    2.32    using a combination of provers and disprovers (@{command (HOL)
    2.33    "solve_direct"}, @{command (HOL) "quickcheck"}, @{command (HOL)
    2.34 -  "try_methods"}, @{command (HOL) "sledgehammer"}, @{command (HOL)
    2.35 +  "try0"}, @{command (HOL) "sledgehammer"}, @{command (HOL)
    2.36    "nitpick"}).
    2.37  
    2.38    \item @{command (HOL) "sledgehammer"} attempts to prove a subgoal
     3.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Feb 24 11:23:33 2012 +0100
     3.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Feb 24 11:23:34 2012 +0100
     3.3 @@ -2207,7 +2207,7 @@
     3.4    \begin{matharray}{rcl}
     3.5      \indexdef{HOL}{command}{solve\_direct}\hypertarget{command.HOL.solve-direct}{\hyperlink{command.HOL.solve-direct}{\mbox{\isa{\isacommand{solve{\isaliteral{5F}{\isacharunderscore}}direct}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
     3.6      \indexdef{HOL}{command}{try}\hypertarget{command.HOL.try}{\hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
     3.7 -    \indexdef{HOL}{command}{try\_methods}\hypertarget{command.HOL.try-methods}{\hyperlink{command.HOL.try-methods}{\mbox{\isa{\isacommand{try{\isaliteral{5F}{\isacharunderscore}}methods}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
     3.8 +    \indexdef{HOL}{command}{try0}\hypertarget{command.HOL.try0}{\hyperlink{command.HOL.try0}{\mbox{\isa{\isacommand{try0}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
     3.9      \indexdef{HOL}{command}{sledgehammer}\hypertarget{command.HOL.sledgehammer}{\hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
    3.10      \indexdef{HOL}{command}{sledgehammer\_params}\hypertarget{command.HOL.sledgehammer-params}{\hyperlink{command.HOL.sledgehammer-params}{\mbox{\isa{\isacommand{sledgehammer{\isaliteral{5F}{\isacharunderscore}}params}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}}
    3.11    \end{matharray}
    3.12 @@ -2217,7 +2217,7 @@
    3.13  \rail@term{\hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}}}[]
    3.14  \rail@end
    3.15  \rail@begin{6}{}
    3.16 -\rail@term{\hyperlink{command.HOL.try-methods}{\mbox{\isa{\isacommand{try{\isaliteral{5F}{\isacharunderscore}}methods}}}}}[]
    3.17 +\rail@term{\hyperlink{command.HOL.try0}{\mbox{\isa{\isacommand{try0}}}}}[]
    3.18  \rail@bar
    3.19  \rail@nextbar{1}
    3.20  \rail@plus
    3.21 @@ -2304,13 +2304,13 @@
    3.22    subgoals can be solved directly by an existing theorem. Duplicate
    3.23    lemmas can be detected in this way.
    3.24  
    3.25 -  \item \hyperlink{command.HOL.try-methods}{\mbox{\isa{\isacommand{try{\isaliteral{5F}{\isacharunderscore}}methods}}}} attempts to prove a subgoal
    3.26 +  \item \hyperlink{command.HOL.try0}{\mbox{\isa{\isacommand{try0}}}} attempts to prove a subgoal
    3.27    using a combination of standard proof methods (\hyperlink{method.auto}{\mbox{\isa{auto}}},
    3.28    \hyperlink{method.simp}{\mbox{\isa{simp}}}, \hyperlink{method.blast}{\mbox{\isa{blast}}}, etc.).  Additional facts supplied
    3.29    via \isa{{\isaliteral{22}{\isachardoublequote}}simp{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}intro{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}elim{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}}, and \isa{{\isaliteral{22}{\isachardoublequote}}dest{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} are passed to the appropriate proof methods.
    3.30  
    3.31    \item \hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}} attempts to prove or disprove a subgoal
    3.32 -  using a combination of provers and disprovers (\hyperlink{command.HOL.solve-direct}{\mbox{\isa{\isacommand{solve{\isaliteral{5F}{\isacharunderscore}}direct}}}}, \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}, \hyperlink{command.HOL.try-methods}{\mbox{\isa{\isacommand{try{\isaliteral{5F}{\isacharunderscore}}methods}}}}, \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}, \hyperlink{command.HOL.nitpick}{\mbox{\isa{\isacommand{nitpick}}}}).
    3.33 +  using a combination of provers and disprovers (\hyperlink{command.HOL.solve-direct}{\mbox{\isa{\isacommand{solve{\isaliteral{5F}{\isacharunderscore}}direct}}}}, \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}, \hyperlink{command.HOL.try0}{\mbox{\isa{\isacommand{try0}}}}, \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}, \hyperlink{command.HOL.nitpick}{\mbox{\isa{\isacommand{nitpick}}}}).
    3.34  
    3.35    \item \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} attempts to prove a subgoal
    3.36    using external automatic provers (resolution provers and SMT
     4.1 --- a/etc/isar-keywords.el	Fri Feb 24 11:23:33 2012 +0100
     4.2 +++ b/etc/isar-keywords.el	Fri Feb 24 11:23:34 2012 +0100
     4.3 @@ -254,7 +254,7 @@
     4.4      "thy_deps"
     4.5      "translations"
     4.6      "try"
     4.7 -    "try_methods"
     4.8 +    "try0"
     4.9      "txt"
    4.10      "txt_raw"
    4.11      "typ"
    4.12 @@ -413,7 +413,7 @@
    4.13      "thm_deps"
    4.14      "thy_deps"
    4.15      "try"
    4.16 -    "try_methods"
    4.17 +    "try0"
    4.18      "typ"
    4.19      "unused_thms"
    4.20      "value"
     5.1 --- a/src/HOL/IsaMakefile	Fri Feb 24 11:23:33 2012 +0100
     5.2 +++ b/src/HOL/IsaMakefile	Fri Feb 24 11:23:34 2012 +0100
     5.3 @@ -263,7 +263,7 @@
     5.4    Tools/sat_funcs.ML \
     5.5    Tools/sat_solver.ML \
     5.6    Tools/split_rule.ML \
     5.7 -  Tools/try_methods.ML \
     5.8 +  Tools/try0.ML \
     5.9    Tools/typedef.ML \
    5.10    Transitive_Closure.thy \
    5.11    Typedef.thy \
     6.1 --- a/src/HOL/Metis.thy	Fri Feb 24 11:23:33 2012 +0100
     6.2 +++ b/src/HOL/Metis.thy	Fri Feb 24 11:23:34 2012 +0100
     6.3 @@ -12,7 +12,7 @@
     6.4       ("Tools/Metis/metis_generate.ML")
     6.5       ("Tools/Metis/metis_reconstruct.ML")
     6.6       ("Tools/Metis/metis_tactic.ML")
     6.7 -     ("Tools/try_methods.ML")
     6.8 +     ("Tools/try0.ML")
     6.9  begin
    6.10  
    6.11  subsection {* Literal selection and lambda-lifting helpers *}
    6.12 @@ -52,10 +52,10 @@
    6.13      select_FalseI lambda_def eq_lambdaI
    6.14  
    6.15  
    6.16 -subsection {* Try Methods *}
    6.17 +subsection {* Try0 *}
    6.18  
    6.19 -use "Tools/try_methods.ML"
    6.20 +use "Tools/try0.ML"
    6.21  
    6.22 -setup {* Try_Methods.setup *}
    6.23 +setup {* Try0.setup *}
    6.24  
    6.25  end
     7.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Feb 24 11:23:33 2012 +0100
     7.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Feb 24 11:23:34 2012 +0100
     7.3 @@ -662,7 +662,7 @@
     7.4            val minimize = AList.defined (op =) args minimizeK
     7.5            val metis_ft = AList.defined (op =) args metis_ftK
     7.6            val trivial =
     7.7 -            Try_Methods.try_methods (SOME try_timeout) ([], [], [], []) pre
     7.8 +            Try0.try0 (SOME try_timeout) ([], [], [], []) pre
     7.9              handle TimeLimit.TimeOut => false
    7.10            fun apply_reconstructor m1 m2 =
    7.11              if metis_ft
     8.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Feb 24 11:23:33 2012 +0100
     8.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Feb 24 11:23:34 2012 +0100
     8.3 @@ -24,7 +24,7 @@
     8.4  val quickcheck_mtd : (Proof.context -> Proof.context) -> string -> mtd
     8.5  
     8.6  val solve_direct_mtd : mtd
     8.7 -val try_methods_mtd : mtd
     8.8 +val try0_mtd : mtd
     8.9  (*
    8.10  val sledgehammer_mtd : mtd
    8.11  *)
    8.12 @@ -138,18 +138,18 @@
    8.13  
    8.14  val solve_direct_mtd = ("solve_direct", invoke_solve_direct) 
    8.15  
    8.16 -(** try **)
    8.17 +(** try0 **)
    8.18  
    8.19 -fun invoke_try_methods thy t =
    8.20 +fun invoke_try0 thy t =
    8.21    let
    8.22      val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (Proof_Context.init_global thy)
    8.23    in
    8.24 -    case Try_Methods.try_methods (SOME (seconds 5.0)) ([], [], [], []) state of
    8.25 +    case Try0.try0 (SOME (seconds 5.0)) ([], [], [], []) state of
    8.26        true => (Solved, [])
    8.27      | false => (Unsolved, [])
    8.28    end
    8.29  
    8.30 -val try_methods_mtd = ("try_methods", invoke_try_methods)
    8.31 +val try0_mtd = ("try0", invoke_try0)
    8.32  
    8.33  (** sledgehammer **)
    8.34  (*
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Tools/try0.ML	Fri Feb 24 11:23:34 2012 +0100
     9.3 @@ -0,0 +1,199 @@
     9.4 +(*  Title:      HOL/Tools/try0.ML
     9.5 +    Author:     Jasmin Blanchette, TU Muenchen
     9.6 +
     9.7 +Try a combination of proof methods.
     9.8 +*)
     9.9 +
    9.10 +signature TRY0 =
    9.11 +sig
    9.12 +  val try0N : string
    9.13 +  val noneN : string
    9.14 +  val auto : bool Unsynchronized.ref
    9.15 +  val try0 :
    9.16 +    Time.time option -> string list * string list * string list * string list
    9.17 +    -> Proof.state -> bool
    9.18 +  val setup : theory -> theory
    9.19 +end;
    9.20 +
    9.21 +structure Try0 : TRY0 =
    9.22 +struct
    9.23 +
    9.24 +datatype mode = Auto_Try | Try | Normal
    9.25 +
    9.26 +val try0N = "try0"
    9.27 +
    9.28 +val noneN = "none"
    9.29 +
    9.30 +val auto = Unsynchronized.ref false
    9.31 +
    9.32 +val _ =
    9.33 +  ProofGeneralPgip.add_preference Preferences.category_tracing
    9.34 +      (Preferences.bool_pref auto "auto-try0" "Try standard proof methods.")
    9.35 +
    9.36 +val default_timeout = seconds 5.0
    9.37 +
    9.38 +fun can_apply timeout_opt pre post tac st =
    9.39 +  let val {goal, ...} = Proof.goal st in
    9.40 +    case (case timeout_opt of
    9.41 +            SOME timeout => TimeLimit.timeLimit timeout
    9.42 +          | NONE => fn f => fn x => f x) (Seq.pull o tac) (pre st) of
    9.43 +      SOME (x, _) => nprems_of (post x) < nprems_of goal
    9.44 +    | NONE => false
    9.45 +  end
    9.46 +  handle TimeLimit.TimeOut => false
    9.47 +
    9.48 +fun do_generic timeout_opt command pre post apply st =
    9.49 +  let val timer = Timer.startRealTimer () in
    9.50 +    if can_apply timeout_opt pre post apply st then
    9.51 +      SOME (command, Time.toMilliseconds (Timer.checkRealTimer timer))
    9.52 +    else
    9.53 +      NONE
    9.54 +  end
    9.55 +
    9.56 +val parse_method =
    9.57 +  enclose "(" ")"
    9.58 +  #> Outer_Syntax.scan Position.start
    9.59 +  #> filter Token.is_proper
    9.60 +  #> Scan.read Token.stopper Method.parse
    9.61 +  #> (fn SOME (Method.Source src) => src | _ => raise Fail "expected Source")
    9.62 +
    9.63 +fun apply_named_method_on_first_goal method thy =
    9.64 +  method |> parse_method
    9.65 +         |> Method.method thy
    9.66 +         |> Method.Basic
    9.67 +         |> curry Method.SelectGoals 1
    9.68 +         |> Proof.refine
    9.69 +  handle ERROR _ => K Seq.empty (* e.g., the method isn't available yet *)
    9.70 +
    9.71 +fun add_attr_text (NONE, _) s = s
    9.72 +  | add_attr_text (_, []) s = s
    9.73 +  | add_attr_text (SOME x, fs) s =
    9.74 +    s ^ " " ^ (if x = "" then "" else x ^ ": ") ^ space_implode " " fs
    9.75 +fun attrs_text (sx, ix, ex, dx) (ss, is, es, ds) =
    9.76 +  "" |> fold add_attr_text [(sx, ss), (ix, is), (ex, es), (dx, ds)]
    9.77 +
    9.78 +fun do_named_method (name, ((all_goals, run_if_auto_try), attrs)) mode
    9.79 +                    timeout_opt quad st =
    9.80 +  if mode <> Auto_Try orelse run_if_auto_try then
    9.81 +    let val attrs = attrs_text attrs quad in
    9.82 +      do_generic timeout_opt
    9.83 +                 (name ^ (if all_goals andalso
    9.84 +                             nprems_of (#goal (Proof.goal st)) > 1 then
    9.85 +                            "[1]"
    9.86 +                          else
    9.87 +                            "") ^
    9.88 +                  attrs) I (#goal o Proof.goal)
    9.89 +                 (apply_named_method_on_first_goal (name ^ attrs)
    9.90 +                                                   (Proof.theory_of st)) st
    9.91 +    end
    9.92 +  else
    9.93 +    NONE
    9.94 +
    9.95 +val full_attrs = (SOME "simp", SOME "intro", SOME "elim", SOME "dest")
    9.96 +val clas_attrs = (NONE, SOME "intro", SOME "elim", SOME "dest")
    9.97 +val simp_attrs = (SOME "add", NONE, NONE, NONE)
    9.98 +val metis_attrs = (SOME "", SOME "", SOME "", SOME "")
    9.99 +val no_attrs = (NONE, NONE, NONE, NONE)
   9.100 +
   9.101 +(* name * ((all_goals, run_if_auto_try), (simp, intro, elim, dest) *)
   9.102 +val named_methods =
   9.103 +  [("simp", ((false, true), simp_attrs)),
   9.104 +   ("auto", ((true, true), full_attrs)),
   9.105 +   ("fast", ((false, false), clas_attrs)),
   9.106 +   ("fastforce", ((false, false), full_attrs)),
   9.107 +   ("force", ((false, false), full_attrs)),
   9.108 +   ("blast", ((false, true), clas_attrs)),
   9.109 +   ("metis", ((false, true), metis_attrs)),
   9.110 +   ("linarith", ((false, true), no_attrs)),
   9.111 +   ("presburger", ((false, true), no_attrs))]
   9.112 +val do_methods = map do_named_method named_methods
   9.113 +
   9.114 +fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"
   9.115 +
   9.116 +fun do_try0 mode timeout_opt quad st =
   9.117 +  let
   9.118 +    val st = st |> Proof.map_context (Config.put Metis_Tactic.verbose false #>
   9.119 +      Config.put Lin_Arith.verbose false)
   9.120 +  in
   9.121 +    if mode = Normal then
   9.122 +      "Trying " ^ space_implode " " (Try.serial_commas "and"
   9.123 +                                      (map (quote o fst) named_methods)) ^ "..."
   9.124 +      |> Output.urgent_message
   9.125 +    else
   9.126 +      ();
   9.127 +    case do_methods |> Par_List.map (fn f => f mode timeout_opt quad st)
   9.128 +                    |> map_filter I |> sort (int_ord o pairself snd) of
   9.129 +      [] =>
   9.130 +      (if mode = Normal then Output.urgent_message "No proof found." else ();
   9.131 +       (false, (noneN, st)))
   9.132 +    | xs as (s, _) :: _ =>
   9.133 +      let
   9.134 +        val xs = xs |> map (fn (s, n) => (n, hd (space_explode " " s)))
   9.135 +                    |> AList.coalesce (op =)
   9.136 +                    |> map (swap o apsnd commas)
   9.137 +        val need_parens = exists_string (curry (op =) " ") s
   9.138 +        val message =
   9.139 +          (case mode of
   9.140 +             Auto_Try => "Auto Try Methods found a proof"
   9.141 +           | Try => "Try Methods found a proof"
   9.142 +           | Normal => "Try this") ^ ": " ^
   9.143 +          Markup.markup Isabelle_Markup.sendback
   9.144 +              ((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
   9.145 +                else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^
   9.146 +          "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"
   9.147 +      in
   9.148 +        (true, (s, st |> (if mode = Auto_Try then
   9.149 +                            Proof.goal_message
   9.150 +                                (fn () => Pretty.chunks [Pretty.str "",
   9.151 +                                          Pretty.markup Isabelle_Markup.hilite
   9.152 +                                                        [Pretty.str message]])
   9.153 +                          else
   9.154 +                            tap (fn _ => Output.urgent_message message))))
   9.155 +      end
   9.156 +  end
   9.157 +
   9.158 +fun try0 timeout_opt = fst oo do_try0 Normal timeout_opt
   9.159 +
   9.160 +fun try0_trans quad =
   9.161 +  Toplevel.keep (K () o do_try0 Normal (SOME default_timeout) quad
   9.162 +                 o Toplevel.proof_of)
   9.163 +
   9.164 +fun merge_attrs (s1, i1, e1, d1) (s2, i2, e2, d2) =
   9.165 +  (s1 @ s2, i1 @ i2, e1 @ e2, d1 @ d2)
   9.166 +
   9.167 +fun string_of_xthm (xref, args) =
   9.168 +  Facts.string_of_ref xref ^
   9.169 +  implode (map (enclose "[" "]" o Pretty.str_of
   9.170 +                o Args.pretty_src @{context}) args)
   9.171 +
   9.172 +val parse_fact_refs =
   9.173 +  Scan.repeat1 (Scan.unless (Parse.name -- Args.colon)
   9.174 +                            (Parse_Spec.xthm >> string_of_xthm))
   9.175 +val parse_attr =
   9.176 +     Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs
   9.177 +     >> (fn ss => (ss, [], [], []))
   9.178 +  || Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs
   9.179 +     >> (fn is => ([], is, [], []))
   9.180 +  || Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs
   9.181 +     >> (fn es => ([], [], es, []))
   9.182 +  || Args.$$$ "dest" |-- Args.colon |-- parse_fact_refs
   9.183 +     >> (fn ds => ([], [], [], ds))
   9.184 +fun parse_attrs x =
   9.185 +    (Args.parens parse_attrs
   9.186 +  || Scan.repeat parse_attr
   9.187 +     >> (fn quad => fold merge_attrs quad ([], [], [], []))) x
   9.188 +
   9.189 +val parse_try0_command =
   9.190 +  Scan.optional parse_attrs ([], [], [], []) #>> try0_trans
   9.191 +
   9.192 +val _ =
   9.193 +  Outer_Syntax.improper_command try0N
   9.194 +      "try a combination of proof methods" Keyword.diag
   9.195 +      parse_try0_command
   9.196 +
   9.197 +fun try_try0 auto =
   9.198 +  do_try0 (if auto then Auto_Try else Try) NONE ([], [], [], [])
   9.199 +
   9.200 +val setup = Try.register_tool (try0N, (30, auto, try_try0))
   9.201 +
   9.202 +end;
    10.1 --- a/src/HOL/Tools/try_methods.ML	Fri Feb 24 11:23:33 2012 +0100
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,200 +0,0 @@
    10.4 -(*  Title:      HOL/Tools/try_methods.ML
    10.5 -    Author:     Jasmin Blanchette, TU Muenchen
    10.6 -
    10.7 -Try a combination of proof methods.
    10.8 -*)
    10.9 -
   10.10 -signature TRY_METHODS =
   10.11 -sig
   10.12 -  val try_methodsN : string
   10.13 -  val noneN : string
   10.14 -  val auto : bool Unsynchronized.ref
   10.15 -  val try_methods :
   10.16 -    Time.time option -> string list * string list * string list * string list
   10.17 -    -> Proof.state -> bool
   10.18 -  val setup : theory -> theory
   10.19 -end;
   10.20 -
   10.21 -structure Try_Methods : TRY_METHODS =
   10.22 -struct
   10.23 -
   10.24 -datatype mode = Auto_Try | Try | Normal
   10.25 -
   10.26 -val try_methodsN = "try_methods"
   10.27 -
   10.28 -val noneN = "none"
   10.29 -
   10.30 -val auto = Unsynchronized.ref false
   10.31 -
   10.32 -val _ =
   10.33 -  ProofGeneralPgip.add_preference Preferences.category_tracing
   10.34 -      (Preferences.bool_pref auto "auto-try-methods"
   10.35 -                             "Try standard proof methods.")
   10.36 -
   10.37 -val default_timeout = seconds 5.0
   10.38 -
   10.39 -fun can_apply timeout_opt pre post tac st =
   10.40 -  let val {goal, ...} = Proof.goal st in
   10.41 -    case (case timeout_opt of
   10.42 -            SOME timeout => TimeLimit.timeLimit timeout
   10.43 -          | NONE => fn f => fn x => f x) (Seq.pull o tac) (pre st) of
   10.44 -      SOME (x, _) => nprems_of (post x) < nprems_of goal
   10.45 -    | NONE => false
   10.46 -  end
   10.47 -  handle TimeLimit.TimeOut => false
   10.48 -
   10.49 -fun do_generic timeout_opt command pre post apply st =
   10.50 -  let val timer = Timer.startRealTimer () in
   10.51 -    if can_apply timeout_opt pre post apply st then
   10.52 -      SOME (command, Time.toMilliseconds (Timer.checkRealTimer timer))
   10.53 -    else
   10.54 -      NONE
   10.55 -  end
   10.56 -
   10.57 -val parse_method =
   10.58 -  enclose "(" ")"
   10.59 -  #> Outer_Syntax.scan Position.start
   10.60 -  #> filter Token.is_proper
   10.61 -  #> Scan.read Token.stopper Method.parse
   10.62 -  #> (fn SOME (Method.Source src) => src | _ => raise Fail "expected Source")
   10.63 -
   10.64 -fun apply_named_method_on_first_goal method thy =
   10.65 -  method |> parse_method
   10.66 -         |> Method.method thy
   10.67 -         |> Method.Basic
   10.68 -         |> curry Method.SelectGoals 1
   10.69 -         |> Proof.refine
   10.70 -  handle ERROR _ => K Seq.empty (* e.g., the method isn't available yet *)
   10.71 -
   10.72 -fun add_attr_text (NONE, _) s = s
   10.73 -  | add_attr_text (_, []) s = s
   10.74 -  | add_attr_text (SOME x, fs) s =
   10.75 -    s ^ " " ^ (if x = "" then "" else x ^ ": ") ^ space_implode " " fs
   10.76 -fun attrs_text (sx, ix, ex, dx) (ss, is, es, ds) =
   10.77 -  "" |> fold add_attr_text [(sx, ss), (ix, is), (ex, es), (dx, ds)]
   10.78 -
   10.79 -fun do_named_method (name, ((all_goals, run_if_auto_try), attrs)) mode
   10.80 -                    timeout_opt quad st =
   10.81 -  if mode <> Auto_Try orelse run_if_auto_try then
   10.82 -    let val attrs = attrs_text attrs quad in
   10.83 -      do_generic timeout_opt
   10.84 -                 (name ^ (if all_goals andalso
   10.85 -                             nprems_of (#goal (Proof.goal st)) > 1 then
   10.86 -                            "[1]"
   10.87 -                          else
   10.88 -                            "") ^
   10.89 -                  attrs) I (#goal o Proof.goal)
   10.90 -                 (apply_named_method_on_first_goal (name ^ attrs)
   10.91 -                                                   (Proof.theory_of st)) st
   10.92 -    end
   10.93 -  else
   10.94 -    NONE
   10.95 -
   10.96 -val full_attrs = (SOME "simp", SOME "intro", SOME "elim", SOME "dest")
   10.97 -val clas_attrs = (NONE, SOME "intro", SOME "elim", SOME "dest")
   10.98 -val simp_attrs = (SOME "add", NONE, NONE, NONE)
   10.99 -val metis_attrs = (SOME "", SOME "", SOME "", SOME "")
  10.100 -val no_attrs = (NONE, NONE, NONE, NONE)
  10.101 -
  10.102 -(* name * ((all_goals, run_if_auto_try), (simp, intro, elim, dest) *)
  10.103 -val named_methods =
  10.104 -  [("simp", ((false, true), simp_attrs)),
  10.105 -   ("auto", ((true, true), full_attrs)),
  10.106 -   ("fast", ((false, false), clas_attrs)),
  10.107 -   ("fastforce", ((false, false), full_attrs)),
  10.108 -   ("force", ((false, false), full_attrs)),
  10.109 -   ("blast", ((false, true), clas_attrs)),
  10.110 -   ("metis", ((false, true), metis_attrs)),
  10.111 -   ("linarith", ((false, true), no_attrs)),
  10.112 -   ("presburger", ((false, true), no_attrs))]
  10.113 -val do_methods = map do_named_method named_methods
  10.114 -
  10.115 -fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"
  10.116 -
  10.117 -fun do_try_methods mode timeout_opt quad st =
  10.118 -  let
  10.119 -    val st = st |> Proof.map_context (Config.put Metis_Tactic.verbose false #>
  10.120 -      Config.put Lin_Arith.verbose false)
  10.121 -  in
  10.122 -    if mode = Normal then
  10.123 -      "Trying " ^ space_implode " " (Try.serial_commas "and"
  10.124 -                                      (map (quote o fst) named_methods)) ^ "..."
  10.125 -      |> Output.urgent_message
  10.126 -    else
  10.127 -      ();
  10.128 -    case do_methods |> Par_List.map (fn f => f mode timeout_opt quad st)
  10.129 -                    |> map_filter I |> sort (int_ord o pairself snd) of
  10.130 -      [] =>
  10.131 -      (if mode = Normal then Output.urgent_message "No proof found." else ();
  10.132 -       (false, (noneN, st)))
  10.133 -    | xs as (s, _) :: _ =>
  10.134 -      let
  10.135 -        val xs = xs |> map (fn (s, n) => (n, hd (space_explode " " s)))
  10.136 -                    |> AList.coalesce (op =)
  10.137 -                    |> map (swap o apsnd commas)
  10.138 -        val need_parens = exists_string (curry (op =) " ") s
  10.139 -        val message =
  10.140 -          (case mode of
  10.141 -             Auto_Try => "Auto Try Methods found a proof"
  10.142 -           | Try => "Try Methods found a proof"
  10.143 -           | Normal => "Try this") ^ ": " ^
  10.144 -          Markup.markup Isabelle_Markup.sendback
  10.145 -              ((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
  10.146 -                else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^
  10.147 -          "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"
  10.148 -      in
  10.149 -        (true, (s, st |> (if mode = Auto_Try then
  10.150 -                            Proof.goal_message
  10.151 -                                (fn () => Pretty.chunks [Pretty.str "",
  10.152 -                                          Pretty.markup Isabelle_Markup.hilite
  10.153 -                                                        [Pretty.str message]])
  10.154 -                          else
  10.155 -                            tap (fn _ => Output.urgent_message message))))
  10.156 -      end
  10.157 -  end
  10.158 -
  10.159 -fun try_methods timeout_opt = fst oo do_try_methods Normal timeout_opt
  10.160 -
  10.161 -fun try_methods_trans quad =
  10.162 -  Toplevel.keep (K () o do_try_methods Normal (SOME default_timeout) quad
  10.163 -                 o Toplevel.proof_of)
  10.164 -
  10.165 -fun merge_attrs (s1, i1, e1, d1) (s2, i2, e2, d2) =
  10.166 -  (s1 @ s2, i1 @ i2, e1 @ e2, d1 @ d2)
  10.167 -
  10.168 -fun string_of_xthm (xref, args) =
  10.169 -  Facts.string_of_ref xref ^
  10.170 -  implode (map (enclose "[" "]" o Pretty.str_of
  10.171 -                o Args.pretty_src @{context}) args)
  10.172 -
  10.173 -val parse_fact_refs =
  10.174 -  Scan.repeat1 (Scan.unless (Parse.name -- Args.colon)
  10.175 -                            (Parse_Spec.xthm >> string_of_xthm))
  10.176 -val parse_attr =
  10.177 -     Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs
  10.178 -     >> (fn ss => (ss, [], [], []))
  10.179 -  || Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs
  10.180 -     >> (fn is => ([], is, [], []))
  10.181 -  || Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs
  10.182 -     >> (fn es => ([], [], es, []))
  10.183 -  || Args.$$$ "dest" |-- Args.colon |-- parse_fact_refs
  10.184 -     >> (fn ds => ([], [], [], ds))
  10.185 -fun parse_attrs x =
  10.186 -    (Args.parens parse_attrs
  10.187 -  || Scan.repeat parse_attr
  10.188 -     >> (fn quad => fold merge_attrs quad ([], [], [], []))) x
  10.189 -
  10.190 -val parse_try_methods_command =
  10.191 -  Scan.optional parse_attrs ([], [], [], []) #>> try_methods_trans
  10.192 -
  10.193 -val _ =
  10.194 -  Outer_Syntax.improper_command try_methodsN
  10.195 -      "try a combination of proof methods" Keyword.diag
  10.196 -      parse_try_methods_command
  10.197 -
  10.198 -fun try_try_methods auto =
  10.199 -  do_try_methods (if auto then Auto_Try else Try) NONE ([], [], [], [])
  10.200 -
  10.201 -val setup = Try.register_tool (try_methodsN, (30, auto, try_try_methods))
  10.202 -
  10.203 -end;