# HG changeset patch # User obua # Date 1194299618 -3600 # Node ID bc3a1c9647044026be111934b416a083aa09229c # Parent c3542f70b0fd487cc438aac13423d0a4c1804179 corrected fucked up integer tuning diff -r c3542f70b0fd -r bc3a1c964704 src/HOL/Real/float_arith.ML --- a/src/HOL/Real/float_arith.ML Mon Nov 05 22:51:16 2007 +0100 +++ b/src/HOL/Real/float_arith.ML Mon Nov 05 22:53:38 2007 +0100 @@ -87,6 +87,7 @@ val ln2_10 = Math.ln 10.0 / Math.ln 2.0; fun exp5 x = Integer.pow x 5; fun exp10 x = Integer.pow x 10; +fun exp2 x = Integer.pow x 2; fun find_most_significant q r = let @@ -101,7 +102,7 @@ (q * exp10 (r - r') - q', r') fun bin2dec d = if 0 <= d then - (Integer.square d, 0) + (exp2 d, 0) else (exp5 (~ d), d) @@ -133,7 +134,7 @@ fun approx_dec_by_bin n (q,r) = let fun addseq acc d' [] = acc - | addseq acc d' (d::ds) = addseq (acc + Integer.square (d - d')) d' ds + | addseq acc d' (d::ds) = addseq (acc + exp2 (d - d')) d' ds fun seq2bin [] = (0, 0) | seq2bin (d::ds) = (addseq 0 d ds + 1, d) @@ -151,7 +152,7 @@ let val d' = d0 - precision val x1 = seq2bin (d_seq) - val x2 = (fst x1 * Integer.square (snd x1 - d') + 1, d') (* = seq2bin (d'::d_seq) *) + val x2 = (fst x1 * exp2 (snd x1 - d') + 1, d') (* = seq2bin (d'::d_seq) *) in (x1, x2) end