1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Fri May 27 10:30:08 2011 +0200
1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Fri May 27 10:30:08 2011 +0200
1.3 @@ -931,13 +931,13 @@
1.4
1.5 \begin{matharray}{rcl}
1.6 @{command_def (HOL) "solve_direct"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
1.7 - @{command_def (HOL) "try"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
1.8 + @{command_def (HOL) "try_methods"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
1.9 @{command_def (HOL) "sledgehammer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
1.10 @{command_def (HOL) "sledgehammer_params"} & : & @{text "theory \<rightarrow> theory"}
1.11 \end{matharray}
1.12
1.13 @{rail "
1.14 - @@{command (HOL) try} ( ( ( 'simp' | 'intro' | 'elim' | 'dest' ) ':' @{syntax thmrefs} ) + ) ?
1.15 + @@{command (HOL) try_methods} ( ( ( 'simp' | 'intro' | 'elim' | 'dest' ) ':' @{syntax thmrefs} ) + ) ?
1.16 @{syntax nat}?
1.17 ;
1.18 @@{command (HOL) sledgehammer} ( '[' args ']' )? facts? @{syntax nat}?
1.19 @@ -951,7 +951,7 @@
1.20
1.21 facts: '(' ( ( ( ( 'add' | 'del' ) ':' ) ? @{syntax thmrefs} ) + ) ? ')'
1.22 ;
1.23 - "} % FIXME try: proper clasimpmod!?
1.24 + "} % FIXME try_methods: proper clasimpmod!?
1.25 % FIXME check args "value"
1.26
1.27 \begin{description}
1.28 @@ -960,7 +960,7 @@
1.29 be solved directly by an existing theorem. Duplicate lemmas can be detected
1.30 in this way.
1.31
1.32 - \item @{command (HOL) "try"} attempts to prove a subgoal using a combination
1.33 + \item @{command (HOL) "try_methods"} attempts to prove a subgoal using a combination
1.34 of standard proof methods (@{text auto}, @{text simp}, @{text blast}, etc.).
1.35 Additional facts supplied via @{text "simp:"}, @{text "intro:"},
1.36 @{text "elim:"}, and @{text "dest:"} are passed to the appropriate proof
2.1 --- a/src/HOL/IsaMakefile Fri May 27 10:30:08 2011 +0200
2.2 +++ b/src/HOL/IsaMakefile Fri May 27 10:30:08 2011 +0200
2.3 @@ -245,7 +245,7 @@
2.4 Tools/sat_funcs.ML \
2.5 Tools/sat_solver.ML \
2.6 Tools/split_rule.ML \
2.7 - Tools/try.ML \
2.8 + Tools/try_methods.ML \
2.9 Tools/typedef.ML \
2.10 Tools/enriched_type.ML \
2.11 Transitive_Closure.thy \
3.1 --- a/src/HOL/Metis.thy Fri May 27 10:30:08 2011 +0200
3.2 +++ b/src/HOL/Metis.thy Fri May 27 10:30:08 2011 +0200
3.3 @@ -12,7 +12,7 @@
3.4 ("Tools/Metis/metis_translate.ML")
3.5 ("Tools/Metis/metis_reconstruct.ML")
3.6 ("Tools/Metis/metis_tactics.ML")
3.7 - ("Tools/try.ML")
3.8 + ("Tools/try_methods.ML")
3.9 begin
3.10
3.11
3.12 @@ -70,10 +70,10 @@
3.13 fequal_def select_def not_atomize atomize_not_select not_atomize_select
3.14 select_FalseI
3.15
3.16 -subsection {* Try *}
3.17 +subsection {* Try Methods *}
3.18
3.19 -use "Tools/try.ML"
3.20 +use "Tools/try_methods.ML"
3.21
3.22 -setup {* Try.setup *}
3.23 +setup {* Try_Methods.setup *}
3.24
3.25 end
4.1 --- a/src/HOL/Tools/try.ML Fri May 27 10:30:08 2011 +0200
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,179 +0,0 @@
4.4 -(* Title: HOL/Tools/try.ML
4.5 - Author: Jasmin Blanchette, TU Muenchen
4.6 -
4.7 -Try a combination of proof methods.
4.8 -*)
4.9 -
4.10 -signature TRY =
4.11 -sig
4.12 - val auto : bool Unsynchronized.ref
4.13 - val invoke_try :
4.14 - Time.time option -> string list * string list * string list * string list
4.15 - -> Proof.state -> bool
4.16 - val setup : theory -> theory
4.17 -end;
4.18 -
4.19 -structure Try : TRY =
4.20 -struct
4.21 -
4.22 -val auto = Unsynchronized.ref false
4.23 -
4.24 -val _ =
4.25 - ProofGeneralPgip.add_preference Preferences.category_tracing
4.26 - (Preferences.bool_pref auto "auto-try" "Try standard proof methods.")
4.27 -
4.28 -val default_timeout = seconds 5.0
4.29 -
4.30 -fun can_apply timeout_opt pre post tac st =
4.31 - let val {goal, ...} = Proof.goal st in
4.32 - case (case timeout_opt of
4.33 - SOME timeout => TimeLimit.timeLimit timeout
4.34 - | NONE => fn f => fn x => f x) (Seq.pull o tac) (pre st) of
4.35 - SOME (x, _) => nprems_of (post x) < nprems_of goal
4.36 - | NONE => false
4.37 - end
4.38 - handle TimeLimit.TimeOut => false
4.39 -
4.40 -fun do_generic timeout_opt command pre post apply st =
4.41 - let val timer = Timer.startRealTimer () in
4.42 - if can_apply timeout_opt pre post apply st then
4.43 - SOME (command, Time.toMilliseconds (Timer.checkRealTimer timer))
4.44 - else
4.45 - NONE
4.46 - end
4.47 -
4.48 -val parse_method =
4.49 - enclose "(" ")"
4.50 - #> Outer_Syntax.scan Position.start
4.51 - #> filter Token.is_proper
4.52 - #> Scan.read Token.stopper Method.parse
4.53 - #> (fn SOME (Method.Source src) => src | _ => raise Fail "expected Source")
4.54 -
4.55 -fun apply_named_method_on_first_goal method thy =
4.56 - method |> parse_method
4.57 - |> Method.method thy
4.58 - |> Method.Basic
4.59 - |> curry Method.SelectGoals 1
4.60 - |> Proof.refine
4.61 - handle ERROR _ => K Seq.empty (* e.g., the method isn't available yet *)
4.62 -
4.63 -fun add_attr_text (NONE, _) s = s
4.64 - | add_attr_text (_, []) s = s
4.65 - | add_attr_text (SOME x, fs) s =
4.66 - s ^ " " ^ (if x = "" then "" else x ^ ": ") ^ space_implode " " fs
4.67 -fun attrs_text (sx, ix, ex, dx) (ss, is, es, ds) =
4.68 - "" |> fold add_attr_text [(sx, ss), (ix, is), (ex, es), (dx, ds)]
4.69 -
4.70 -fun do_named_method (name, ((all_goals, run_if_auto), attrs)) auto timeout_opt
4.71 - quad st =
4.72 - if not auto orelse run_if_auto then
4.73 - let val attrs = attrs_text attrs quad in
4.74 - do_generic timeout_opt
4.75 - (name ^ (if all_goals andalso
4.76 - nprems_of (#goal (Proof.goal st)) > 1 then
4.77 - "[1]"
4.78 - else
4.79 - "") ^
4.80 - attrs) I (#goal o Proof.goal)
4.81 - (apply_named_method_on_first_goal (name ^ attrs)
4.82 - (Proof.theory_of st)) st
4.83 - end
4.84 - else
4.85 - NONE
4.86 -
4.87 -val full_attrs = (SOME "simp", SOME "intro", SOME "elim", SOME "dest")
4.88 -val clas_attrs = (NONE, SOME "intro", SOME "elim", SOME "dest")
4.89 -val simp_attrs = (SOME "add", NONE, NONE, NONE)
4.90 -val metis_attrs = (SOME "", SOME "", SOME "", SOME "")
4.91 -val no_attrs = (NONE, NONE, NONE, NONE)
4.92 -
4.93 -(* name * ((all_goals, run_if_auto), (simp, intro, elim, dest) *)
4.94 -val named_methods =
4.95 - [("simp", ((false, true), simp_attrs)),
4.96 - ("auto", ((true, true), full_attrs)),
4.97 - ("fast", ((false, false), clas_attrs)),
4.98 - ("fastsimp", ((false, false), full_attrs)),
4.99 - ("force", ((false, false), full_attrs)),
4.100 - ("blast", ((false, true), clas_attrs)),
4.101 - ("metis", ((false, true), metis_attrs)),
4.102 - ("linarith", ((false, true), no_attrs)),
4.103 - ("presburger", ((false, true), no_attrs))]
4.104 -val do_methods = map do_named_method named_methods
4.105 -
4.106 -fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"
4.107 -
4.108 -fun do_try auto timeout_opt quad st =
4.109 - let
4.110 - val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose false)
4.111 - in
4.112 - case do_methods |> Par_List.map (fn f => f auto timeout_opt quad st)
4.113 - |> map_filter I |> sort (int_ord o pairself snd) of
4.114 - [] => (if auto then () else writeln "No proof found."; (false, st))
4.115 - | xs as (s, _) :: _ =>
4.116 - let
4.117 - val xs = xs |> map (fn (s, n) => (n, hd (space_explode " " s)))
4.118 - |> AList.coalesce (op =)
4.119 - |> map (swap o apsnd commas)
4.120 - val need_parens = exists_string (curry (op =) " ") s
4.121 - val message =
4.122 - (if auto then "Auto Try found a proof" else "Try this command") ^
4.123 - ": " ^
4.124 - Markup.markup Markup.sendback
4.125 - ((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
4.126 - else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^
4.127 - "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"
4.128 - in
4.129 - (true, st |> (if auto then
4.130 - Proof.goal_message
4.131 - (fn () => Pretty.chunks [Pretty.str "",
4.132 - Pretty.markup Markup.hilite
4.133 - [Pretty.str message]])
4.134 - else
4.135 - tap (fn _ => Output.urgent_message message)))
4.136 - end
4.137 - end
4.138 -
4.139 -fun invoke_try timeout_opt = fst oo do_try false timeout_opt
4.140 -
4.141 -val tryN = "try"
4.142 -
4.143 -fun try_trans quad =
4.144 - Toplevel.keep (K () o do_try false (SOME default_timeout) quad
4.145 - o Toplevel.proof_of)
4.146 -
4.147 -fun merge_attrs (s1, i1, e1, d1) (s2, i2, e2, d2) =
4.148 - (s1 @ s2, i1 @ i2, e1 @ e2, d1 @ d2)
4.149 -
4.150 -fun string_of_xthm (xref, args) =
4.151 - Facts.string_of_ref xref ^
4.152 - implode (map (enclose "[" "]" o Pretty.str_of
4.153 - o Args.pretty_src @{context}) args)
4.154 -
4.155 -val parse_fact_refs =
4.156 - Scan.repeat1 (Scan.unless (Parse.name -- Args.colon)
4.157 - (Parse_Spec.xthm >> string_of_xthm))
4.158 -val parse_attr =
4.159 - Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs
4.160 - >> (fn ss => (ss, [], [], []))
4.161 - || Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs
4.162 - >> (fn is => ([], is, [], []))
4.163 - || Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs
4.164 - >> (fn es => ([], [], es, []))
4.165 - || Args.$$$ "dest" |-- Args.colon |-- parse_fact_refs
4.166 - >> (fn ds => ([], [], [], ds))
4.167 -fun parse_attrs x =
4.168 - (Args.parens parse_attrs
4.169 - || Scan.repeat parse_attr
4.170 - >> (fn quad => fold merge_attrs quad ([], [], [], []))) x
4.171 -
4.172 -val parse_try_command = Scan.optional parse_attrs ([], [], [], []) #>> try_trans
4.173 -
4.174 -val _ =
4.175 - Outer_Syntax.improper_command tryN
4.176 - "try a combination of proof methods" Keyword.diag parse_try_command
4.177 -
4.178 -val auto_try = do_try true NONE ([], [], [], [])
4.179 -
4.180 -val setup = Auto_Tools.register_tool (auto, auto_try)
4.181 -
4.182 -end;
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/HOL/Tools/try_methods.ML Fri May 27 10:30:08 2011 +0200
5.3 @@ -0,0 +1,182 @@
5.4 +(* Title: HOL/Tools/try_methods.ML
5.5 + Author: Jasmin Blanchette, TU Muenchen
5.6 +
5.7 +Try a combination of proof methods.
5.8 +*)
5.9 +
5.10 +signature TRY_METHODS =
5.11 +sig
5.12 + val auto : bool Unsynchronized.ref
5.13 + val try_methods :
5.14 + Time.time option -> string list * string list * string list * string list
5.15 + -> Proof.state -> bool
5.16 + val setup : theory -> theory
5.17 +end;
5.18 +
5.19 +structure Try_Methods : TRY_METHODS =
5.20 +struct
5.21 +
5.22 +val auto = Unsynchronized.ref false
5.23 +
5.24 +val _ =
5.25 + ProofGeneralPgip.add_preference Preferences.category_tracing
5.26 + (Preferences.bool_pref auto "auto-try-methods"
5.27 + "Try standard proof methods.")
5.28 +
5.29 +val default_timeout = seconds 5.0
5.30 +
5.31 +fun can_apply timeout_opt pre post tac st =
5.32 + let val {goal, ...} = Proof.goal st in
5.33 + case (case timeout_opt of
5.34 + SOME timeout => TimeLimit.timeLimit timeout
5.35 + | NONE => fn f => fn x => f x) (Seq.pull o tac) (pre st) of
5.36 + SOME (x, _) => nprems_of (post x) < nprems_of goal
5.37 + | NONE => false
5.38 + end
5.39 + handle TimeLimit.TimeOut => false
5.40 +
5.41 +fun do_generic timeout_opt command pre post apply st =
5.42 + let val timer = Timer.startRealTimer () in
5.43 + if can_apply timeout_opt pre post apply st then
5.44 + SOME (command, Time.toMilliseconds (Timer.checkRealTimer timer))
5.45 + else
5.46 + NONE
5.47 + end
5.48 +
5.49 +val parse_method =
5.50 + enclose "(" ")"
5.51 + #> Outer_Syntax.scan Position.start
5.52 + #> filter Token.is_proper
5.53 + #> Scan.read Token.stopper Method.parse
5.54 + #> (fn SOME (Method.Source src) => src | _ => raise Fail "expected Source")
5.55 +
5.56 +fun apply_named_method_on_first_goal method thy =
5.57 + method |> parse_method
5.58 + |> Method.method thy
5.59 + |> Method.Basic
5.60 + |> curry Method.SelectGoals 1
5.61 + |> Proof.refine
5.62 + handle ERROR _ => K Seq.empty (* e.g., the method isn't available yet *)
5.63 +
5.64 +fun add_attr_text (NONE, _) s = s
5.65 + | add_attr_text (_, []) s = s
5.66 + | add_attr_text (SOME x, fs) s =
5.67 + s ^ " " ^ (if x = "" then "" else x ^ ": ") ^ space_implode " " fs
5.68 +fun attrs_text (sx, ix, ex, dx) (ss, is, es, ds) =
5.69 + "" |> fold add_attr_text [(sx, ss), (ix, is), (ex, es), (dx, ds)]
5.70 +
5.71 +fun do_named_method (name, ((all_goals, run_if_auto), attrs)) auto timeout_opt
5.72 + quad st =
5.73 + if not auto orelse run_if_auto then
5.74 + let val attrs = attrs_text attrs quad in
5.75 + do_generic timeout_opt
5.76 + (name ^ (if all_goals andalso
5.77 + nprems_of (#goal (Proof.goal st)) > 1 then
5.78 + "[1]"
5.79 + else
5.80 + "") ^
5.81 + attrs) I (#goal o Proof.goal)
5.82 + (apply_named_method_on_first_goal (name ^ attrs)
5.83 + (Proof.theory_of st)) st
5.84 + end
5.85 + else
5.86 + NONE
5.87 +
5.88 +val full_attrs = (SOME "simp", SOME "intro", SOME "elim", SOME "dest")
5.89 +val clas_attrs = (NONE, SOME "intro", SOME "elim", SOME "dest")
5.90 +val simp_attrs = (SOME "add", NONE, NONE, NONE)
5.91 +val metis_attrs = (SOME "", SOME "", SOME "", SOME "")
5.92 +val no_attrs = (NONE, NONE, NONE, NONE)
5.93 +
5.94 +(* name * ((all_goals, run_if_auto), (simp, intro, elim, dest) *)
5.95 +val named_methods =
5.96 + [("simp", ((false, true), simp_attrs)),
5.97 + ("auto", ((true, true), full_attrs)),
5.98 + ("fast", ((false, false), clas_attrs)),
5.99 + ("fastsimp", ((false, false), full_attrs)),
5.100 + ("force", ((false, false), full_attrs)),
5.101 + ("blast", ((false, true), clas_attrs)),
5.102 + ("metis", ((false, true), metis_attrs)),
5.103 + ("linarith", ((false, true), no_attrs)),
5.104 + ("presburger", ((false, true), no_attrs))]
5.105 +val do_methods = map do_named_method named_methods
5.106 +
5.107 +fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"
5.108 +
5.109 +fun do_try_methods auto timeout_opt quad st =
5.110 + let
5.111 + val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose false)
5.112 + in
5.113 + case do_methods |> Par_List.map (fn f => f auto timeout_opt quad st)
5.114 + |> map_filter I |> sort (int_ord o pairself snd) of
5.115 + [] => (if auto then () else writeln "No proof found."; (false, st))
5.116 + | xs as (s, _) :: _ =>
5.117 + let
5.118 + val xs = xs |> map (fn (s, n) => (n, hd (space_explode " " s)))
5.119 + |> AList.coalesce (op =)
5.120 + |> map (swap o apsnd commas)
5.121 + val need_parens = exists_string (curry (op =) " ") s
5.122 + val message =
5.123 + (if auto then "Auto Try Methods found a proof"
5.124 + else "Try this command") ^ ": " ^
5.125 + Markup.markup Markup.sendback
5.126 + ((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
5.127 + else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^
5.128 + "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"
5.129 + in
5.130 + (true, st |> (if auto then
5.131 + Proof.goal_message
5.132 + (fn () => Pretty.chunks [Pretty.str "",
5.133 + Pretty.markup Markup.hilite
5.134 + [Pretty.str message]])
5.135 + else
5.136 + tap (fn _ => Output.urgent_message message)))
5.137 + end
5.138 + end
5.139 +
5.140 +fun try_methods timeout_opt = fst oo do_try_methods false timeout_opt
5.141 +
5.142 +val try_methodsN = "try_methods"
5.143 +
5.144 +fun try_methods_trans quad =
5.145 + Toplevel.keep (K () o do_try_methods false (SOME default_timeout) quad
5.146 + o Toplevel.proof_of)
5.147 +
5.148 +fun merge_attrs (s1, i1, e1, d1) (s2, i2, e2, d2) =
5.149 + (s1 @ s2, i1 @ i2, e1 @ e2, d1 @ d2)
5.150 +
5.151 +fun string_of_xthm (xref, args) =
5.152 + Facts.string_of_ref xref ^
5.153 + implode (map (enclose "[" "]" o Pretty.str_of
5.154 + o Args.pretty_src @{context}) args)
5.155 +
5.156 +val parse_fact_refs =
5.157 + Scan.repeat1 (Scan.unless (Parse.name -- Args.colon)
5.158 + (Parse_Spec.xthm >> string_of_xthm))
5.159 +val parse_attr =
5.160 + Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs
5.161 + >> (fn ss => (ss, [], [], []))
5.162 + || Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs
5.163 + >> (fn is => ([], is, [], []))
5.164 + || Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs
5.165 + >> (fn es => ([], [], es, []))
5.166 + || Args.$$$ "dest" |-- Args.colon |-- parse_fact_refs
5.167 + >> (fn ds => ([], [], [], ds))
5.168 +fun parse_attrs x =
5.169 + (Args.parens parse_attrs
5.170 + || Scan.repeat parse_attr
5.171 + >> (fn quad => fold merge_attrs quad ([], [], [], []))) x
5.172 +
5.173 +val parse_try_methods_command =
5.174 + Scan.optional parse_attrs ([], [], [], []) #>> try_methods_trans
5.175 +
5.176 +val _ =
5.177 + Outer_Syntax.improper_command try_methodsN
5.178 + "try a combination of proof methods" Keyword.diag
5.179 + parse_try_methods_command
5.180 +
5.181 +val auto_try_methods = do_try_methods true NONE ([], [], [], [])
5.182 +
5.183 +val setup = Auto_Tools.register_tool (auto, auto_try_methods)
5.184 +
5.185 +end;