src/HOL/Integ/cooper_dec.ML
 changeset 15965 f422f8283491 parent 15859 7bc8b9683224 child 16299 872ad146bb14
```     1.1 --- a/src/HOL/Integ/cooper_dec.ML	Mon May 16 09:35:05 2005 +0200
1.2 +++ b/src/HOL/Integ/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)
```