src/HOL/Tools/Presburger/cooper_dec.ML
changeset 15965 f422f8283491
parent 15859 7bc8b9683224
child 16299 872ad146bb14
     1.1 --- a/src/HOL/Tools/Presburger/cooper_dec.ML	Mon May 16 09:35:05 2005 +0200
     1.2 +++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Mon May 16 10:29:15 2005 +0200
     1.3 @@ -85,13 +85,14 @@
     1.4   
     1.5  fun mk_numeral 0 = Const("0",HOLogic.intT)
     1.6     |mk_numeral 1 = Const("1",HOLogic.intT)
     1.7 -   |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_bin n); 
     1.8 +   |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_bin (IntInf.fromInt n)); 
     1.9   
    1.10  (*Transform an Term to an natural number*)	  
    1.11  	  
    1.12  fun dest_numeral (Const("0",Type ("IntDef.int", []))) = 0
    1.13     |dest_numeral (Const("1",Type ("IntDef.int", []))) = 1
    1.14 -   |dest_numeral (Const ("Numeral.number_of",_) $ n)= HOLogic.dest_binum n; 
    1.15 +   |dest_numeral (Const ("Numeral.number_of",_) $ n) = 
    1.16 +       IntInf.toInt (HOLogic.dest_binum n);
    1.17  (*Some terms often used for pattern matching*) 
    1.18   
    1.19  val zero = mk_numeral 0; 
    1.20 @@ -245,12 +246,13 @@
    1.21  (* ------------------------------------------------------------------------- *) 
    1.22  (*gcd calculates gcd (a,b) and helps lcm_num calculating lcm (a,b)*) 
    1.23   
    1.24 +(*BEWARE: replaces Library.gcd!! There is also Library.lcm!*)
    1.25  fun gcd a b = if a=0 then b else gcd (b mod a) a ; 
    1.26  fun lcm_num a b = (abs a*b) div (gcd (abs a) (abs b)); 
    1.27   
    1.28  fun formlcm x fm = case fm of 
    1.29      (Const (p,_)$ _ $(Const ("op +", _)$(Const ("op *",_)$ c $ y ) $z ) ) =>  if 
    1.30 -    (is_arith_rel fm) andalso (x = y) then abs(dest_numeral c) else 1 
    1.31 +    (is_arith_rel fm) andalso (x = y) then  (abs(dest_numeral c)) else 1 
    1.32    | ( Const ("Not", _) $p) => formlcm x p 
    1.33    | ( Const ("op &",_) $ p $ q) => lcm_num (formlcm x p) (formlcm x q) 
    1.34    | ( Const ("op |",_) $ p $ q )=> lcm_num (formlcm x p) (formlcm x q) 
    1.35 @@ -281,7 +283,7 @@
    1.36  (* ------------------------------------------------------------------------- *) 
    1.37   
    1.38  fun unitycoeff x fm = 
    1.39 -  let val l = formlcm x fm 
    1.40 +  let val l = formlcm x fm
    1.41        val fm' = adjustcoeff x l fm in
    1.42        if l = 1 then fm' 
    1.43  	 else 
    1.44 @@ -453,7 +455,8 @@
    1.45  
    1.46  
    1.47  val operations = 
    1.48 -  [("op =",op=), ("op <",op<), ("op >",op>), ("op <=",op<=) , ("op >=",op>=), 
    1.49 +  [("op =",op=), ("op <",Int.<), ("op >",Int.>), ("op <=",Int.<=) , 
    1.50 +   ("op >=",Int.>=), 
    1.51     ("Divides.op dvd",fn (x,y) =>((y mod x) = 0))]; 
    1.52   
    1.53  fun applyoperation (SOME f) (a,b) = f (a, b) 
    1.54 @@ -486,13 +489,14 @@
    1.55  fun evalc_atom at = case at of  
    1.56    (Const (p,_) $ s $ t) =>
    1.57     ( case assoc (operations,p) of 
    1.58 -    SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const)  
    1.59 +    SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const 
    1.60 +                else HOLogic.false_const)  
    1.61      handle _ => at) 
    1.62        | _ =>  at) 
    1.63        |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
    1.64    case assoc (operations,p) of 
    1.65 -    SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then 
    1.66 -    HOLogic.false_const else HOLogic.true_const)  
    1.67 +    SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) 
    1.68 +               then HOLogic.false_const else HOLogic.true_const)  
    1.69      handle _ => at) 
    1.70        | _ =>  at) 
    1.71        | _ =>  at; 
    1.72 @@ -678,7 +682,8 @@
    1.73  (* Minusinfinity Version*) 
    1.74  fun coopermi vars1 fm = 
    1.75    case fm of 
    1.76 -   Const ("Ex",_) $ Abs(x0,T,p0) => let 
    1.77 +   Const ("Ex",_) $ Abs(x0,T,p0) => 
    1.78 +   let 
    1.79      val (xn,p1) = variant_abs (x0,T,p0) 
    1.80      val x = Free (xn,T)  
    1.81      val vars = (xn::vars1)