--- a/NEWS Fri Feb 24 11:23:33 2012 +0100
+++ b/NEWS Fri Feb 24 11:23:34 2012 +0100
@@ -336,6 +336,9 @@
- Added possibility to specify lambda translations scheme as a
parenthesized argument (e.g., "by (metis (lifting) ...)").
+* Command 'try0':
+ - Renamed from 'try_methods'. INCOMPATIBILITY.
+
*** FOL ***
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Feb 24 11:23:33 2012 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Feb 24 11:23:34 2012 +0100
@@ -1571,7 +1571,7 @@
\begin{matharray}{rcl}
@{command_def (HOL) "solve_direct"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
@{command_def (HOL) "try"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
- @{command_def (HOL) "try_methods"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
+ @{command_def (HOL) "try0"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
@{command_def (HOL) "sledgehammer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
@{command_def (HOL) "sledgehammer_params"} & : & @{text "theory \<rightarrow> theory"}
\end{matharray}
@@ -1580,7 +1580,7 @@
@@{command (HOL) try}
;
- @@{command (HOL) try_methods} ( ( ( 'simp' | 'intro' | 'elim' | 'dest' ) ':' @{syntax thmrefs} ) + ) ?
+ @@{command (HOL) try0} ( ( ( 'simp' | 'intro' | 'elim' | 'dest' ) ':' @{syntax thmrefs} ) + ) ?
@{syntax nat}?
;
@@ -1603,7 +1603,7 @@
subgoals can be solved directly by an existing theorem. Duplicate
lemmas can be detected in this way.
- \item @{command (HOL) "try_methods"} attempts to prove a subgoal
+ \item @{command (HOL) "try0"} attempts to prove a subgoal
using a combination of standard proof methods (@{method auto},
@{method simp}, @{method blast}, etc.). Additional facts supplied
via @{text "simp:"}, @{text "intro:"}, @{text "elim:"}, and @{text
@@ -1612,7 +1612,7 @@
\item @{command (HOL) "try"} attempts to prove or disprove a subgoal
using a combination of provers and disprovers (@{command (HOL)
"solve_direct"}, @{command (HOL) "quickcheck"}, @{command (HOL)
- "try_methods"}, @{command (HOL) "sledgehammer"}, @{command (HOL)
+ "try0"}, @{command (HOL) "sledgehammer"}, @{command (HOL)
"nitpick"}).
\item @{command (HOL) "sledgehammer"} attempts to prove a subgoal
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Feb 24 11:23:33 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Feb 24 11:23:34 2012 +0100
@@ -2207,7 +2207,7 @@
\begin{matharray}{rcl}
\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}}} \\
\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}}} \\
- \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}}} \\
+ \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}}} \\
\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}}} \\
\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}}}
\end{matharray}
@@ -2217,7 +2217,7 @@
\rail@term{\hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}}}[]
\rail@end
\rail@begin{6}{}
-\rail@term{\hyperlink{command.HOL.try-methods}{\mbox{\isa{\isacommand{try{\isaliteral{5F}{\isacharunderscore}}methods}}}}}[]
+\rail@term{\hyperlink{command.HOL.try0}{\mbox{\isa{\isacommand{try0}}}}}[]
\rail@bar
\rail@nextbar{1}
\rail@plus
@@ -2304,13 +2304,13 @@
subgoals can be solved directly by an existing theorem. Duplicate
lemmas can be detected in this way.
- \item \hyperlink{command.HOL.try-methods}{\mbox{\isa{\isacommand{try{\isaliteral{5F}{\isacharunderscore}}methods}}}} attempts to prove a subgoal
+ \item \hyperlink{command.HOL.try0}{\mbox{\isa{\isacommand{try0}}}} attempts to prove a subgoal
using a combination of standard proof methods (\hyperlink{method.auto}{\mbox{\isa{auto}}},
\hyperlink{method.simp}{\mbox{\isa{simp}}}, \hyperlink{method.blast}{\mbox{\isa{blast}}}, etc.). Additional facts supplied
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.
\item \hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}} attempts to prove or disprove a subgoal
- 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}}}}).
+ 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}}}}).
\item \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} attempts to prove a subgoal
using external automatic provers (resolution provers and SMT
--- a/etc/isar-keywords.el Fri Feb 24 11:23:33 2012 +0100
+++ b/etc/isar-keywords.el Fri Feb 24 11:23:34 2012 +0100
@@ -254,7 +254,7 @@
"thy_deps"
"translations"
"try"
- "try_methods"
+ "try0"
"txt"
"txt_raw"
"typ"
@@ -413,7 +413,7 @@
"thm_deps"
"thy_deps"
"try"
- "try_methods"
+ "try0"
"typ"
"unused_thms"
"value"
--- a/src/HOL/IsaMakefile Fri Feb 24 11:23:33 2012 +0100
+++ b/src/HOL/IsaMakefile Fri Feb 24 11:23:34 2012 +0100
@@ -263,7 +263,7 @@
Tools/sat_funcs.ML \
Tools/sat_solver.ML \
Tools/split_rule.ML \
- Tools/try_methods.ML \
+ Tools/try0.ML \
Tools/typedef.ML \
Transitive_Closure.thy \
Typedef.thy \
--- a/src/HOL/Metis.thy Fri Feb 24 11:23:33 2012 +0100
+++ b/src/HOL/Metis.thy Fri Feb 24 11:23:34 2012 +0100
@@ -12,7 +12,7 @@
("Tools/Metis/metis_generate.ML")
("Tools/Metis/metis_reconstruct.ML")
("Tools/Metis/metis_tactic.ML")
- ("Tools/try_methods.ML")
+ ("Tools/try0.ML")
begin
subsection {* Literal selection and lambda-lifting helpers *}
@@ -52,10 +52,10 @@
select_FalseI lambda_def eq_lambdaI
-subsection {* Try Methods *}
+subsection {* Try0 *}
-use "Tools/try_methods.ML"
+use "Tools/try0.ML"
-setup {* Try_Methods.setup *}
+setup {* Try0.setup *}
end
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Feb 24 11:23:33 2012 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Feb 24 11:23:34 2012 +0100
@@ -662,7 +662,7 @@
val minimize = AList.defined (op =) args minimizeK
val metis_ft = AList.defined (op =) args metis_ftK
val trivial =
- Try_Methods.try_methods (SOME try_timeout) ([], [], [], []) pre
+ Try0.try0 (SOME try_timeout) ([], [], [], []) pre
handle TimeLimit.TimeOut => false
fun apply_reconstructor m1 m2 =
if metis_ft
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Fri Feb 24 11:23:33 2012 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Fri Feb 24 11:23:34 2012 +0100
@@ -24,7 +24,7 @@
val quickcheck_mtd : (Proof.context -> Proof.context) -> string -> mtd
val solve_direct_mtd : mtd
-val try_methods_mtd : mtd
+val try0_mtd : mtd
(*
val sledgehammer_mtd : mtd
*)
@@ -138,18 +138,18 @@
val solve_direct_mtd = ("solve_direct", invoke_solve_direct)
-(** try **)
+(** try0 **)
-fun invoke_try_methods thy t =
+fun invoke_try0 thy t =
let
val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (Proof_Context.init_global thy)
in
- case Try_Methods.try_methods (SOME (seconds 5.0)) ([], [], [], []) state of
+ case Try0.try0 (SOME (seconds 5.0)) ([], [], [], []) state of
true => (Solved, [])
| false => (Unsolved, [])
end
-val try_methods_mtd = ("try_methods", invoke_try_methods)
+val try0_mtd = ("try0", invoke_try0)
(** sledgehammer **)
(*
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/try0.ML Fri Feb 24 11:23:34 2012 +0100
@@ -0,0 +1,199 @@
+(* Title: HOL/Tools/try0.ML
+ Author: Jasmin Blanchette, TU Muenchen
+
+Try a combination of proof methods.
+*)
+
+signature TRY0 =
+sig
+ val try0N : string
+ val noneN : string
+ val auto : bool Unsynchronized.ref
+ val try0 :
+ Time.time option -> string list * string list * string list * string list
+ -> Proof.state -> bool
+ val setup : theory -> theory
+end;
+
+structure Try0 : TRY0 =
+struct
+
+datatype mode = Auto_Try | Try | Normal
+
+val try0N = "try0"
+
+val noneN = "none"
+
+val auto = Unsynchronized.ref false
+
+val _ =
+ ProofGeneralPgip.add_preference Preferences.category_tracing
+ (Preferences.bool_pref auto "auto-try0" "Try standard proof methods.")
+
+val default_timeout = seconds 5.0
+
+fun can_apply timeout_opt pre post tac st =
+ let val {goal, ...} = Proof.goal st in
+ case (case timeout_opt of
+ SOME timeout => TimeLimit.timeLimit timeout
+ | NONE => fn f => fn x => f x) (Seq.pull o tac) (pre st) of
+ SOME (x, _) => nprems_of (post x) < nprems_of goal
+ | NONE => false
+ end
+ handle TimeLimit.TimeOut => false
+
+fun do_generic timeout_opt command pre post apply st =
+ let val timer = Timer.startRealTimer () in
+ if can_apply timeout_opt pre post apply st then
+ SOME (command, Time.toMilliseconds (Timer.checkRealTimer timer))
+ else
+ NONE
+ end
+
+val parse_method =
+ enclose "(" ")"
+ #> Outer_Syntax.scan Position.start
+ #> filter Token.is_proper
+ #> Scan.read Token.stopper Method.parse
+ #> (fn SOME (Method.Source src) => src | _ => raise Fail "expected Source")
+
+fun apply_named_method_on_first_goal method thy =
+ method |> parse_method
+ |> Method.method thy
+ |> Method.Basic
+ |> curry Method.SelectGoals 1
+ |> Proof.refine
+ handle ERROR _ => K Seq.empty (* e.g., the method isn't available yet *)
+
+fun add_attr_text (NONE, _) s = s
+ | add_attr_text (_, []) s = s
+ | add_attr_text (SOME x, fs) s =
+ s ^ " " ^ (if x = "" then "" else x ^ ": ") ^ space_implode " " fs
+fun attrs_text (sx, ix, ex, dx) (ss, is, es, ds) =
+ "" |> fold add_attr_text [(sx, ss), (ix, is), (ex, es), (dx, ds)]
+
+fun do_named_method (name, ((all_goals, run_if_auto_try), attrs)) mode
+ timeout_opt quad st =
+ if mode <> Auto_Try orelse run_if_auto_try then
+ let val attrs = attrs_text attrs quad in
+ do_generic timeout_opt
+ (name ^ (if all_goals andalso
+ nprems_of (#goal (Proof.goal st)) > 1 then
+ "[1]"
+ else
+ "") ^
+ attrs) I (#goal o Proof.goal)
+ (apply_named_method_on_first_goal (name ^ attrs)
+ (Proof.theory_of st)) st
+ end
+ else
+ NONE
+
+val full_attrs = (SOME "simp", SOME "intro", SOME "elim", SOME "dest")
+val clas_attrs = (NONE, SOME "intro", SOME "elim", SOME "dest")
+val simp_attrs = (SOME "add", NONE, NONE, NONE)
+val metis_attrs = (SOME "", SOME "", SOME "", SOME "")
+val no_attrs = (NONE, NONE, NONE, NONE)
+
+(* name * ((all_goals, run_if_auto_try), (simp, intro, elim, dest) *)
+val named_methods =
+ [("simp", ((false, true), simp_attrs)),
+ ("auto", ((true, true), full_attrs)),
+ ("fast", ((false, false), clas_attrs)),
+ ("fastforce", ((false, false), full_attrs)),
+ ("force", ((false, false), full_attrs)),
+ ("blast", ((false, true), clas_attrs)),
+ ("metis", ((false, true), metis_attrs)),
+ ("linarith", ((false, true), no_attrs)),
+ ("presburger", ((false, true), no_attrs))]
+val do_methods = map do_named_method named_methods
+
+fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"
+
+fun do_try0 mode timeout_opt quad st =
+ let
+ val st = st |> Proof.map_context (Config.put Metis_Tactic.verbose false #>
+ Config.put Lin_Arith.verbose false)
+ in
+ if mode = Normal then
+ "Trying " ^ space_implode " " (Try.serial_commas "and"
+ (map (quote o fst) named_methods)) ^ "..."
+ |> Output.urgent_message
+ else
+ ();
+ case do_methods |> Par_List.map (fn f => f mode timeout_opt quad st)
+ |> map_filter I |> sort (int_ord o pairself snd) of
+ [] =>
+ (if mode = Normal then Output.urgent_message "No proof found." else ();
+ (false, (noneN, st)))
+ | xs as (s, _) :: _ =>
+ let
+ val xs = xs |> map (fn (s, n) => (n, hd (space_explode " " s)))
+ |> AList.coalesce (op =)
+ |> map (swap o apsnd commas)
+ val need_parens = exists_string (curry (op =) " ") s
+ val message =
+ (case mode of
+ Auto_Try => "Auto Try Methods found a proof"
+ | Try => "Try Methods found a proof"
+ | Normal => "Try this") ^ ": " ^
+ Markup.markup Isabelle_Markup.sendback
+ ((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
+ else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^
+ "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"
+ in
+ (true, (s, st |> (if mode = Auto_Try then
+ Proof.goal_message
+ (fn () => Pretty.chunks [Pretty.str "",
+ Pretty.markup Isabelle_Markup.hilite
+ [Pretty.str message]])
+ else
+ tap (fn _ => Output.urgent_message message))))
+ end
+ end
+
+fun try0 timeout_opt = fst oo do_try0 Normal timeout_opt
+
+fun try0_trans quad =
+ Toplevel.keep (K () o do_try0 Normal (SOME default_timeout) quad
+ o Toplevel.proof_of)
+
+fun merge_attrs (s1, i1, e1, d1) (s2, i2, e2, d2) =
+ (s1 @ s2, i1 @ i2, e1 @ e2, d1 @ d2)
+
+fun string_of_xthm (xref, args) =
+ Facts.string_of_ref xref ^
+ implode (map (enclose "[" "]" o Pretty.str_of
+ o Args.pretty_src @{context}) args)
+
+val parse_fact_refs =
+ Scan.repeat1 (Scan.unless (Parse.name -- Args.colon)
+ (Parse_Spec.xthm >> string_of_xthm))
+val parse_attr =
+ Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs
+ >> (fn ss => (ss, [], [], []))
+ || Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs
+ >> (fn is => ([], is, [], []))
+ || Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs
+ >> (fn es => ([], [], es, []))
+ || Args.$$$ "dest" |-- Args.colon |-- parse_fact_refs
+ >> (fn ds => ([], [], [], ds))
+fun parse_attrs x =
+ (Args.parens parse_attrs
+ || Scan.repeat parse_attr
+ >> (fn quad => fold merge_attrs quad ([], [], [], []))) x
+
+val parse_try0_command =
+ Scan.optional parse_attrs ([], [], [], []) #>> try0_trans
+
+val _ =
+ Outer_Syntax.improper_command try0N
+ "try a combination of proof methods" Keyword.diag
+ parse_try0_command
+
+fun try_try0 auto =
+ do_try0 (if auto then Auto_Try else Try) NONE ([], [], [], [])
+
+val setup = Try.register_tool (try0N, (30, auto, try_try0))
+
+end;
--- a/src/HOL/Tools/try_methods.ML Fri Feb 24 11:23:33 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,200 +0,0 @@
-(* Title: HOL/Tools/try_methods.ML
- Author: Jasmin Blanchette, TU Muenchen
-
-Try a combination of proof methods.
-*)
-
-signature TRY_METHODS =
-sig
- val try_methodsN : string
- val noneN : string
- val auto : bool Unsynchronized.ref
- val try_methods :
- Time.time option -> string list * string list * string list * string list
- -> Proof.state -> bool
- val setup : theory -> theory
-end;
-
-structure Try_Methods : TRY_METHODS =
-struct
-
-datatype mode = Auto_Try | Try | Normal
-
-val try_methodsN = "try_methods"
-
-val noneN = "none"
-
-val auto = Unsynchronized.ref false
-
-val _ =
- ProofGeneralPgip.add_preference Preferences.category_tracing
- (Preferences.bool_pref auto "auto-try-methods"
- "Try standard proof methods.")
-
-val default_timeout = seconds 5.0
-
-fun can_apply timeout_opt pre post tac st =
- let val {goal, ...} = Proof.goal st in
- case (case timeout_opt of
- SOME timeout => TimeLimit.timeLimit timeout
- | NONE => fn f => fn x => f x) (Seq.pull o tac) (pre st) of
- SOME (x, _) => nprems_of (post x) < nprems_of goal
- | NONE => false
- end
- handle TimeLimit.TimeOut => false
-
-fun do_generic timeout_opt command pre post apply st =
- let val timer = Timer.startRealTimer () in
- if can_apply timeout_opt pre post apply st then
- SOME (command, Time.toMilliseconds (Timer.checkRealTimer timer))
- else
- NONE
- end
-
-val parse_method =
- enclose "(" ")"
- #> Outer_Syntax.scan Position.start
- #> filter Token.is_proper
- #> Scan.read Token.stopper Method.parse
- #> (fn SOME (Method.Source src) => src | _ => raise Fail "expected Source")
-
-fun apply_named_method_on_first_goal method thy =
- method |> parse_method
- |> Method.method thy
- |> Method.Basic
- |> curry Method.SelectGoals 1
- |> Proof.refine
- handle ERROR _ => K Seq.empty (* e.g., the method isn't available yet *)
-
-fun add_attr_text (NONE, _) s = s
- | add_attr_text (_, []) s = s
- | add_attr_text (SOME x, fs) s =
- s ^ " " ^ (if x = "" then "" else x ^ ": ") ^ space_implode " " fs
-fun attrs_text (sx, ix, ex, dx) (ss, is, es, ds) =
- "" |> fold add_attr_text [(sx, ss), (ix, is), (ex, es), (dx, ds)]
-
-fun do_named_method (name, ((all_goals, run_if_auto_try), attrs)) mode
- timeout_opt quad st =
- if mode <> Auto_Try orelse run_if_auto_try then
- let val attrs = attrs_text attrs quad in
- do_generic timeout_opt
- (name ^ (if all_goals andalso
- nprems_of (#goal (Proof.goal st)) > 1 then
- "[1]"
- else
- "") ^
- attrs) I (#goal o Proof.goal)
- (apply_named_method_on_first_goal (name ^ attrs)
- (Proof.theory_of st)) st
- end
- else
- NONE
-
-val full_attrs = (SOME "simp", SOME "intro", SOME "elim", SOME "dest")
-val clas_attrs = (NONE, SOME "intro", SOME "elim", SOME "dest")
-val simp_attrs = (SOME "add", NONE, NONE, NONE)
-val metis_attrs = (SOME "", SOME "", SOME "", SOME "")
-val no_attrs = (NONE, NONE, NONE, NONE)
-
-(* name * ((all_goals, run_if_auto_try), (simp, intro, elim, dest) *)
-val named_methods =
- [("simp", ((false, true), simp_attrs)),
- ("auto", ((true, true), full_attrs)),
- ("fast", ((false, false), clas_attrs)),
- ("fastforce", ((false, false), full_attrs)),
- ("force", ((false, false), full_attrs)),
- ("blast", ((false, true), clas_attrs)),
- ("metis", ((false, true), metis_attrs)),
- ("linarith", ((false, true), no_attrs)),
- ("presburger", ((false, true), no_attrs))]
-val do_methods = map do_named_method named_methods
-
-fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"
-
-fun do_try_methods mode timeout_opt quad st =
- let
- val st = st |> Proof.map_context (Config.put Metis_Tactic.verbose false #>
- Config.put Lin_Arith.verbose false)
- in
- if mode = Normal then
- "Trying " ^ space_implode " " (Try.serial_commas "and"
- (map (quote o fst) named_methods)) ^ "..."
- |> Output.urgent_message
- else
- ();
- case do_methods |> Par_List.map (fn f => f mode timeout_opt quad st)
- |> map_filter I |> sort (int_ord o pairself snd) of
- [] =>
- (if mode = Normal then Output.urgent_message "No proof found." else ();
- (false, (noneN, st)))
- | xs as (s, _) :: _ =>
- let
- val xs = xs |> map (fn (s, n) => (n, hd (space_explode " " s)))
- |> AList.coalesce (op =)
- |> map (swap o apsnd commas)
- val need_parens = exists_string (curry (op =) " ") s
- val message =
- (case mode of
- Auto_Try => "Auto Try Methods found a proof"
- | Try => "Try Methods found a proof"
- | Normal => "Try this") ^ ": " ^
- Markup.markup Isabelle_Markup.sendback
- ((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
- else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^
- "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"
- in
- (true, (s, st |> (if mode = Auto_Try then
- Proof.goal_message
- (fn () => Pretty.chunks [Pretty.str "",
- Pretty.markup Isabelle_Markup.hilite
- [Pretty.str message]])
- else
- tap (fn _ => Output.urgent_message message))))
- end
- end
-
-fun try_methods timeout_opt = fst oo do_try_methods Normal timeout_opt
-
-fun try_methods_trans quad =
- Toplevel.keep (K () o do_try_methods Normal (SOME default_timeout) quad
- o Toplevel.proof_of)
-
-fun merge_attrs (s1, i1, e1, d1) (s2, i2, e2, d2) =
- (s1 @ s2, i1 @ i2, e1 @ e2, d1 @ d2)
-
-fun string_of_xthm (xref, args) =
- Facts.string_of_ref xref ^
- implode (map (enclose "[" "]" o Pretty.str_of
- o Args.pretty_src @{context}) args)
-
-val parse_fact_refs =
- Scan.repeat1 (Scan.unless (Parse.name -- Args.colon)
- (Parse_Spec.xthm >> string_of_xthm))
-val parse_attr =
- Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs
- >> (fn ss => (ss, [], [], []))
- || Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs
- >> (fn is => ([], is, [], []))
- || Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs
- >> (fn es => ([], [], es, []))
- || Args.$$$ "dest" |-- Args.colon |-- parse_fact_refs
- >> (fn ds => ([], [], [], ds))
-fun parse_attrs x =
- (Args.parens parse_attrs
- || Scan.repeat parse_attr
- >> (fn quad => fold merge_attrs quad ([], [], [], []))) x
-
-val parse_try_methods_command =
- Scan.optional parse_attrs ([], [], [], []) #>> try_methods_trans
-
-val _ =
- Outer_Syntax.improper_command try_methodsN
- "try a combination of proof methods" Keyword.diag
- parse_try_methods_command
-
-fun try_try_methods auto =
- do_try_methods (if auto then Auto_Try else Try) NONE ([], [], [], [])
-
-val setup = Try.register_tool (try_methodsN, (30, auto, try_try_methods))
-
-end;