src/HOL/arith_data.ML
changeset 15965 f422f8283491
parent 15958 b4ea8bf8e2f7
child 16358 2e2a506553a3
     1.1 --- a/src/HOL/arith_data.ML	Mon May 16 09:35:05 2005 +0200
     1.2 +++ b/src/HOL/arith_data.ML	Mon May 16 10:29:15 2005 +0200
     1.3 @@ -265,27 +265,27 @@
     1.4  let
     1.5  fun demult((mC as Const("op *",_)) $ s $ t,m) = ((case s of
     1.6          Const("Numeral.number_of",_)$n
     1.7 -        => demult(t,ratmul(m,rat_of_int(HOLogic.dest_binum n)))
     1.8 +        => demult(t,ratmul(m,rat_of_intinf(HOLogic.dest_binum n)))
     1.9        | Const("uminus",_)$(Const("Numeral.number_of",_)$n)
    1.10 -        => demult(t,ratmul(m,rat_of_int(~(HOLogic.dest_binum n))))
    1.11 +        => demult(t,ratmul(m,rat_of_intinf(~(HOLogic.dest_binum n))))
    1.12        | Const("Suc",_) $ _
    1.13          => demult(t,ratmul(m,rat_of_int(number_of_Sucs s)))
    1.14        | Const("op *",_) $ s1 $ s2 => demult(mC $ s1 $ (mC $ s2 $ t),m)
    1.15        | Const("HOL.divide",_) $ numt $ (Const("Numeral.number_of",_)$dent) =>
    1.16            let val den = HOLogic.dest_binum dent
    1.17            in if den = 0 then raise Zero
    1.18 -             else demult(mC $ numt $ t,ratmul(m, ratinv(rat_of_int den)))
    1.19 +             else demult(mC $ numt $ t,ratmul(m, ratinv(rat_of_intinf den)))
    1.20            end
    1.21        | _ => atomult(mC,s,t,m)
    1.22        ) handle TERM _ => atomult(mC,s,t,m))
    1.23    | demult(atom as Const("HOL.divide",_) $ t $ (Const("Numeral.number_of",_)$dent), m) =
    1.24        (let val den = HOLogic.dest_binum dent
    1.25 -       in if den = 0 then raise Zero else demult(t,ratmul(m, ratinv(rat_of_int den))) end
    1.26 +       in if den = 0 then raise Zero else demult(t,ratmul(m, ratinv(rat_of_intinf den))) end
    1.27         handle TERM _ => (SOME atom,m))
    1.28    | demult(Const("0",_),m) = (NONE, rat_of_int 0)
    1.29    | demult(Const("1",_),m) = (NONE, m)
    1.30    | demult(t as Const("Numeral.number_of",_)$n,m) =
    1.31 -      ((NONE,ratmul(m,rat_of_int(HOLogic.dest_binum n)))
    1.32 +      ((NONE,ratmul(m,rat_of_intinf(HOLogic.dest_binum n)))
    1.33         handle TERM _ => (SOME t,m))
    1.34    | demult(Const("uminus",_)$t, m) = demult(t,ratmul(m,rat_of_int(~1)))
    1.35    | demult(t as Const f $ x, m) =
    1.36 @@ -316,7 +316,7 @@
    1.37           (NONE,m') => (p,ratadd(i,m'))
    1.38         | (SOME u,m') => add_atom(u,m',pi))
    1.39    | poly(all as (Const("Numeral.number_of",_)$t,m,(p,i))) =
    1.40 -      ((p,ratadd(i,ratmul(m,rat_of_int(HOLogic.dest_binum t))))
    1.41 +      ((p,ratadd(i,ratmul(m,rat_of_intinf(HOLogic.dest_binum t))))
    1.42         handle TERM _ => add_atom all)
    1.43    | poly(all as Const f $ x, m, pi) =
    1.44        if f mem inj_consts then poly(x,m,pi) else add_atom(all,m,pi)
    1.45 @@ -363,7 +363,8 @@
    1.46    let val {discrete, inj_consts, ...} = ArithTheoryData.get_sg sg
    1.47    in decomp2 (sg,discrete,inj_consts) end
    1.48  
    1.49 -fun number_of(n,T) = HOLogic.number_of_const T $ (HOLogic.mk_bin n)
    1.50 +(*FIXME: remove the IntInf.fromInt when linear arithmetic is converted to IntInfs*)
    1.51 +fun number_of(n,T) = HOLogic.number_of_const T $ (HOLogic.mk_bin (IntInf.fromInt n))
    1.52  
    1.53  end;
    1.54