# HG changeset patch
# User wenzelm
# Date 1243248374 -7200
# Node ID 2c20bcd70fbe6a6ecb50c0e4824addf4f74dd303
# Parent  dcbf876f55928a5209fb54304c8a2016110eda33
proper signature constraints;
modernized method setup;

diff -r dcbf876f5592 -r 2c20bcd70fbe src/HOL/Decision_Procs/cooper_tac.ML
--- a/src/HOL/Decision_Procs/cooper_tac.ML	Mon May 25 12:29:29 2009 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Mon May 25 12:46:14 2009 +0200
@@ -2,7 +2,14 @@
     Author:     Amine Chaieb, TU Muenchen
 *)
 
-structure Cooper_Tac =
+signature COOPER_TAC =
+sig
+  val trace: bool ref
+  val linz_tac: Proof.context -> bool -> int -> tactic
+  val setup: theory -> theory
+end
+
+structure Cooper_Tac: COOPER_TAC =
 struct
 
 val trace = ref false;
@@ -33,7 +40,7 @@
 val nat_div_add_eq = @{thm div_add1_eq} RS sym;
 val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym;
 
-fun prepare_for_linz q fm = 
+fun prepare_for_linz q fm =
   let
     val ps = Logic.strip_params fm
     val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
@@ -66,8 +73,8 @@
     (* Transform the term*)
     val (t,np,nh) = prepare_for_linz q g
     (* Some simpsets for dealing with mod div abs and nat*)
-    val mod_div_simpset = HOL_basic_ss 
-			addsimps [refl,mod_add_eq, mod_add_left_eq, 
+    val mod_div_simpset = HOL_basic_ss
+			addsimps [refl,mod_add_eq, mod_add_left_eq,
 				  mod_add_right_eq,
 				  nat_div_add_eq, int_div_add_eq,
 				  @{thm mod_self}, @{thm "zmod_self"},
@@ -105,30 +112,24 @@
     val (th, tac) = case (prop_of pre_thm) of
         Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
     let val pth = linzqe_oracle (cterm_of thy (Pattern.eta_long [] t1))
-    in 
+    in
           ((pth RS iffD2) RS pre_thm,
             assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))
     end
       | _ => (pre_thm, assm_tac i)
-  in (rtac (((mp_step nh) o (spec_step np)) th) i 
+  in (rtac (((mp_step nh) o (spec_step np)) th) i
       THEN tac) st
   end handle Subscript => no_tac st);
 
-fun linz_args meth =
- let val parse_flag = 
-         Args.$$$ "no_quantify" >> (K (K false));
- in
-   Method.simple_args 
-  (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
-    curry (Library.foldl op |>) true)
-    (fn q => fn ctxt => meth ctxt q)
-  end;
-
-fun linz_method ctxt q = SIMPLE_METHOD' (linz_tac ctxt q);
-
 val setup =
-  Method.add_method ("cooper",
-     linz_args linz_method,
-     "decision procedure for linear integer arithmetic");
+  Method.setup @{binding cooper}
+    let
+      val parse_flag = Args.$$$ "no_quantify" >> K (K false)
+    in
+      Scan.lift (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
+        curry (Library.foldl op |>) true) >>
+      (fn q => fn ctxt => SIMPLE_METHOD' (linz_tac ctxt q))
+    end
+    "decision procedure for linear integer arithmetic";
 
 end
diff -r dcbf876f5592 -r 2c20bcd70fbe src/HOL/Decision_Procs/mir_tac.ML
--- a/src/HOL/Decision_Procs/mir_tac.ML	Mon May 25 12:29:29 2009 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML	Mon May 25 12:46:14 2009 +0200
@@ -2,6 +2,13 @@
     Author:     Amine Chaieb, TU Muenchen
 *)
 
+signature MIR_TAC =
+sig
+  val trace: bool ref
+  val mir_tac: Proof.context -> bool -> int -> tactic
+  val setup: theory -> theory
+end
+
 structure Mir_Tac =
 struct
 
@@ -82,9 +89,9 @@
 
 
 fun mir_tac ctxt q i = 
-    (ObjectLogic.atomize_prems_tac i)
-        THEN (simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms) i)
-        THEN (REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"},@{thm "abs_split"}] i))
+    ObjectLogic.atomize_prems_tac i
+        THEN simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms) i
+        THEN REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}] i)
         THEN (fn st =>
   let
     val g = List.nth (prems_of st, i - 1)
@@ -143,22 +150,15 @@
       THEN tac) st
   end handle Subscript => no_tac st);
 
-fun mir_args meth =
- let val parse_flag = 
-         Args.$$$ "no_quantify" >> (K (K false));
- in
-   Method.simple_args 
-  (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
-    curry (Library.foldl op |>) true)
-    (fn q => fn ctxt => meth ctxt q)
-  end;
-
-fun mir_method ctxt q = SIMPLE_METHOD' (mir_tac ctxt q);
-
 val setup =
-  Method.add_method ("mir",
-     mir_args mir_method,
-     "decision procedure for MIR arithmetic");
-
+  Method.setup @{binding mir}
+    let
+      val parse_flag = Args.$$$ "no_quantify" >> K (K false)
+    in
+      Scan.lift (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
+        curry (Library.foldl op |>) true) >>
+      (fn q => fn ctxt => SIMPLE_METHOD' (mir_tac ctxt q))
+    end
+    "decision procedure for MIR arithmetic";
 
 end