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.38         | (SOME u,m') => add_atom(u,m',pi))
1.39    | poly(all as (Const("Numeral.number_of",_)\$t,m,(p,i))) =
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
```