src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML

 
   datatype proof_method =
     Metis_Method of string option * string option |
     Meson_Method |
     SMT_Method |
+    Blast_Method |
     Simp_Method |
     Simp_Size_Method |
     Auto_Method |
     Fastforce_Method |
     Force_Method |
-    Arith_Method |
-    Blast_Method |
+    Linarith_Method |
+    Presburger_Method |
     Algebra_Method
 
   datatype play_outcome =
     Played of Time.time |
     Play_Timed_Out of Time.time |

     Not_Played
 
   type minimize_command = string list -> string
   type one_line_params =
     (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
-
-  val smtN : string
 
   val string_of_proof_method : proof_method -> string
   val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
   val string_of_play_outcome : play_outcome -> string
   val play_outcome_ord : play_outcome * play_outcome -> order

 
 datatype proof_method =
   Metis_Method of string option * string option |
   Meson_Method |
   SMT_Method |
+  Blast_Method |
   Simp_Method |
   Simp_Size_Method |
   Auto_Method |
   Fastforce_Method |
   Force_Method |
-  Arith_Method |
-  Blast_Method |
+  Linarith_Method |
+  Presburger_Method |
   Algebra_Method
 
 datatype play_outcome =
   Played of Time.time |
   Play_Timed_Out of Time.time |

   Not_Played
 
 type minimize_command = string list -> string
 type one_line_params =
   (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
-
-val smtN = "smt"
 
 fun string_of_proof_method meth =
   (case meth of
     Metis_Method (NONE, NONE) => "metis"
   | Metis_Method (type_enc_opt, lam_trans_opt) =>
     "metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")"
   | Meson_Method => "meson"
   | SMT_Method => "smt"
+  | Blast_Method => "blast"
   | Simp_Method => "simp"
   | Simp_Size_Method => "simp add: size_ne_size_imp_ne"
   | Auto_Method => "auto"
   | Fastforce_Method => "fastforce"
   | Force_Method => "force"
-  | Arith_Method => "arith"
-  | Blast_Method => "blast"
+  | Linarith_Method => "linarith"
+  | Presburger_Method => "presburger"
   | Algebra_Method => "algebra")
 
 fun tac_of_proof_method ctxt (local_facts, global_facts) meth =
   Method.insert_tac local_facts THEN'
   (case meth of
     Metis_Method (type_enc_opt, lam_trans_opt) =>
     Metis_Tactic.metis_tac [type_enc_opt |> the_default (hd partial_type_encs)]
       (lam_trans_opt |> the_default default_metis_lam_trans) ctxt global_facts
+  | Meson_Method => Meson.meson_tac ctxt global_facts
   | SMT_Method => SMT_Solver.smt_tac ctxt global_facts
-  | Meson_Method => Meson.meson_tac ctxt global_facts
   | _ =>
     Method.insert_tac global_facts THEN'
     (case meth of
-      Simp_Method => Simplifier.asm_full_simp_tac ctxt
+      Blast_Method => blast_tac ctxt
+    | Simp_Method => Simplifier.asm_full_simp_tac ctxt
     | Simp_Size_Method =>
       Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)
     | Auto_Method => K (Clasimp.auto_tac ctxt)
     | Fastforce_Method => Clasimp.fast_force_tac ctxt
     | Force_Method => Clasimp.force_tac ctxt
-    | Arith_Method => Arith_Data.arith_tac ctxt
-    | Blast_Method => blast_tac ctxt
+    | Linarith_Method => Lin_Arith.tac ctxt
+    | Presburger_Method => Cooper.tac true [] [] ctxt
     | Algebra_Method => Groebner.algebra_tac [] [] ctxt))
 
 fun string_of_play_outcome (Played time) = string_of_ext_time (false, time)
   | string_of_play_outcome (Play_Timed_Out time) = string_of_ext_time (true, time) ^ ", timed out"
   | string_of_play_outcome Play_Failed = "failed"