renamed "try" "try_methods"
authorblanchet
Fri May 27 10:30:08 2011 +0200 (2011-05-27)
changeset 4301642330f25142c
parent 43015 21b6baec55b1
child 43017 944b19ab6003
renamed "try" "try_methods"
doc-src/IsarRef/Thy/HOL_Specific.thy
src/HOL/IsaMakefile
src/HOL/Metis.thy
src/HOL/Tools/try.ML
src/HOL/Tools/try_methods.ML
     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;