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.20  val nat_div_add_eq = @{thm div_add1_eq} RS sym;
    1.21  val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym;
    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.33 -			addsimps [refl,mod_add_eq, mod_add_left_eq, 
    1.34 +    val mod_div_simpset = HOL_basic_ss
    1.35 +			addsimps [refl,mod_add_eq, mod_add_left_eq,
    1.36  				  mod_add_right_eq,
    1.37  				  nat_div_add_eq, int_div_add_eq,
    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.67 -  Method.add_method ("cooper",
    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