# HG changeset patch
# User blanchet
# Date 1391551878 -3600
# Node ID 253a029335a249739b7cd6747e7f3369164f788f
# Parent  3bf50e3cd72716502b6c8408b85e52b551e4fb49
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)

diff -r 3bf50e3cd727 -r 253a029335a2 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Feb 04 21:29:46 2014 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Feb 04 23:11:18 2014 +0100
@@ -111,9 +111,9 @@
   bool * (string option * string option) * Time.time * real * bool * bool
   * (term, string) atp_step list * thm
 
-val basic_arith_methods = [Arith_Method, Algebra_Method]
-val basic_systematic_methods = [Metis_Method (NONE, NONE), Blast_Method, Meson_Method]
+val basic_systematic_methods = [Metis_Method (NONE, NONE), Meson_Method, Blast_Method]
 val simp_based_methods = [Simp_Method, Auto_Method, Fastforce_Method, Force_Method]
+val basic_arith_methods = [Linarith_Method, Presburger_Method, Algebra_Method]
 
 val arith_methods = basic_arith_methods @ simp_based_methods @ basic_systematic_methods
 val datatype_methods = [Simp_Method, Simp_Size_Method]
diff -r 3bf50e3cd727 -r 253a029335a2 src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Tue Feb 04 21:29:46 2014 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Tue Feb 04 23:11:18 2014 +0100
@@ -84,7 +84,7 @@
         (case Lazy.force outcome of Played _ => true | _ => false)
       end
   in
-    union (op =) meths1 meths2
+    meths2 @ subtract (op =) meths2 meths1
     |> filter (is_method_hopeful l1 andf is_method_hopeful l2)
   end
 
diff -r 3bf50e3cd727 -r 253a029335a2 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Tue Feb 04 21:29:46 2014 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Tue Feb 04 23:11:18 2014 +0100
@@ -13,13 +13,14 @@
     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 =
@@ -32,8 +33,6 @@
   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
@@ -53,13 +52,14 @@
   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 =
@@ -72,8 +72,6 @@
 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"
@@ -81,13 +79,14 @@
     "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 =
@@ -96,19 +95,20 @@
     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)
diff -r 3bf50e3cd727 -r 253a029335a2 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Tue Feb 04 21:29:46 2014 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Tue Feb 04 23:11:18 2014 +0100
@@ -67,6 +67,7 @@
     -> prover_problem -> prover_result
 
   val SledgehammerN : string
+  val smtN : string
   val overlord_file_location_of_prover : string -> string * string
   val proof_banner : mode -> string -> string
   val extract_proof_method : params -> proof_method -> string * (string * string list) list
@@ -110,6 +111,8 @@
    "Async_Manager". *)
 val SledgehammerN = "Sledgehammer"
 
+val smtN = "smt"
+
 val proof_method_names = [metisN, smtN]
 val is_proof_method = member (op =) proof_method_names