src/HOL/Decision_Procs/cooper_tac.ML
 changeset 31240 2c20bcd70fbe parent 31070 ee1ebd405a37 child 31790 05c92381363c
```     1.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Mon May 25 12:29:29 2009 +0200
1.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Mon May 25 12:46:14 2009 +0200
1.3 @@ -2,7 +2,14 @@
1.4      Author:     Amine Chaieb, TU Muenchen
1.5  *)
1.6
1.7 -structure Cooper_Tac =
1.8 +signature COOPER_TAC =
1.9 +sig
1.10 +  val trace: bool ref
1.11 +  val linz_tac: Proof.context -> bool -> int -> tactic
1.12 +  val setup: theory -> theory
1.13 +end
1.14 +
1.15 +structure Cooper_Tac: COOPER_TAC =
1.16  struct
1.17
1.18  val trace = ref false;
1.19 @@ -33,7 +40,7 @@
1.22
1.23 -fun prepare_for_linz q fm =
1.24 +fun prepare_for_linz q fm =
1.25    let
1.26      val ps = Logic.strip_params fm
1.27      val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
1.28 @@ -66,8 +73,8 @@
1.29      (* Transform the term*)
1.30      val (t,np,nh) = prepare_for_linz q g
1.31      (* Some simpsets for dealing with mod div abs and nat*)
1.32 -    val mod_div_simpset = HOL_basic_ss
1.34 +    val mod_div_simpset = HOL_basic_ss
1.38  				  @{thm mod_self}, @{thm "zmod_self"},
1.39 @@ -105,30 +112,24 @@
1.40      val (th, tac) = case (prop_of pre_thm) of
1.41          Const ("==>", _) \$ (Const ("Trueprop", _) \$ t1) \$ _ =>
1.42      let val pth = linzqe_oracle (cterm_of thy (Pattern.eta_long [] t1))
1.43 -    in
1.44 +    in
1.45            ((pth RS iffD2) RS pre_thm,
1.46              assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))
1.47      end
1.48        | _ => (pre_thm, assm_tac i)
1.49 -  in (rtac (((mp_step nh) o (spec_step np)) th) i
1.50 +  in (rtac (((mp_step nh) o (spec_step np)) th) i
1.51        THEN tac) st
1.52    end handle Subscript => no_tac st);
1.53
1.54 -fun linz_args meth =
1.55 - let val parse_flag =
1.56 -         Args.\$\$\$ "no_quantify" >> (K (K false));
1.57 - in
1.58 -   Method.simple_args
1.59 -  (Scan.optional (Args.\$\$\$ "(" |-- Scan.repeat1 parse_flag --| Args.\$\$\$ ")") [] >>
1.60 -    curry (Library.foldl op |>) true)
1.61 -    (fn q => fn ctxt => meth ctxt q)
1.62 -  end;
1.63 -
1.64 -fun linz_method ctxt q = SIMPLE_METHOD' (linz_tac ctxt q);
1.65 -
1.66  val setup =
1.68 -     linz_args linz_method,
1.69 -     "decision procedure for linear integer arithmetic");
1.70 +  Method.setup @{binding cooper}
1.71 +    let
1.72 +      val parse_flag = Args.\$\$\$ "no_quantify" >> K (K false)
1.73 +    in
1.74 +      Scan.lift (Scan.optional (Args.\$\$\$ "(" |-- Scan.repeat1 parse_flag --| Args.\$\$\$ ")") [] >>
1.75 +        curry (Library.foldl op |>) true) >>
1.76 +      (fn q => fn ctxt => SIMPLE_METHOD' (linz_tac ctxt q))
1.77 +    end
1.78 +    "decision procedure for linear integer arithmetic";
1.79
1.80  end
```