1124 qed |
1124 qed |
1125 |
1125 |
1126 lemma truncate_down_nonneg: "0 \<le> y \<Longrightarrow> 0 \<le> truncate_down prec y" |
1126 lemma truncate_down_nonneg: "0 \<le> y \<Longrightarrow> 0 \<le> truncate_down prec y" |
1127 by (auto simp: truncate_down_def round_down_def) |
1127 by (auto simp: truncate_down_def round_down_def) |
1128 |
1128 |
1129 lemma truncate_down_ge1: "1 \<le> x \<Longrightarrow> 1 \<le> p \<Longrightarrow> 1 \<le> truncate_down p x" |
1129 lemma truncate_down_ge1: "1 \<le> x \<Longrightarrow> 1 \<le> truncate_down p x" |
1130 by (auto simp: truncate_down_def algebra_simps intro!: round_down_ge1 add_mono) |
1130 apply (auto simp: truncate_down_def algebra_simps intro!: round_down_ge1) |
|
1131 apply linarith |
|
1132 done |
1131 |
1133 |
1132 lemma truncate_up_nonpos: "x \<le> 0 \<Longrightarrow> truncate_up prec x \<le> 0" |
1134 lemma truncate_up_nonpos: "x \<le> 0 \<Longrightarrow> truncate_up prec x \<le> 0" |
1133 by (auto simp: truncate_up_def round_up_def intro!: mult_nonpos_nonneg) |
1135 by (auto simp: truncate_up_def round_up_def intro!: mult_nonpos_nonneg) |
1134 |
1136 |
1135 lemma truncate_up_le1: |
1137 lemma truncate_up_le1: |
1136 assumes "x \<le> 1" "1 \<le> p" |
1138 assumes "x \<le> 1" |
1137 shows "truncate_up p x \<le> 1" |
1139 shows "truncate_up p x \<le> 1" |
1138 proof - |
1140 proof - |
1139 consider "x \<le> 0" | "x > 0" |
1141 consider "x \<le> 0" | "x > 0" |
1140 by arith |
1142 by arith |
1141 then show ?thesis |
1143 then show ?thesis |
1145 by simp |
1147 by simp |
1146 next |
1148 next |
1147 case 2 |
1149 case 2 |
1148 then have le: "\<lfloor>log 2 \<bar>x\<bar>\<rfloor> \<le> 0" |
1150 then have le: "\<lfloor>log 2 \<bar>x\<bar>\<rfloor> \<le> 0" |
1149 using assms by (auto simp: log_less_iff) |
1151 using assms by (auto simp: log_less_iff) |
1150 from assms have "1 \<le> int p" by simp |
1152 from assms have "0 \<le> int p" by simp |
1151 from add_mono[OF this le] |
1153 from add_mono[OF this le] |
1152 show ?thesis |
1154 show ?thesis |
1153 using assms by (simp add: truncate_up_def round_up_le1 add_mono) |
1155 using assms by (simp add: truncate_up_def round_up_le1 add_mono) |
1154 qed |
1156 qed |
1155 qed |
1157 qed |
1156 |
1158 |
|
1159 lemma truncate_down_shift_int: "truncate_down p (x * 2 powr real_of_int k) = truncate_down p x * 2 powr k" |
|
1160 by (cases "x = 0") |
|
1161 (simp_all add: algebra_simps abs_mult log_mult truncate_down_def round_down_shift[of _ _ k, simplified]) |
|
1162 |
|
1163 lemma truncate_down_shift_nat: "truncate_down p (x * 2 powr real k) = truncate_down p x * 2 powr k" |
|
1164 by (metis of_int_of_nat_eq truncate_down_shift_int) |
|
1165 |
|
1166 lemma truncate_up_shift_int: "truncate_up p (x * 2 powr real_of_int k) = truncate_up p x * 2 powr k" |
|
1167 by (cases "x = 0") |
|
1168 (simp_all add: algebra_simps abs_mult log_mult truncate_up_def round_up_shift[of _ _ k, simplified]) |
|
1169 |
|
1170 lemma truncate_up_shift_nat: "truncate_up p (x * 2 powr real k) = truncate_up p x * 2 powr k" |
|
1171 by (metis of_int_of_nat_eq truncate_up_shift_int) |
|
1172 |
1157 |
1173 |
1158 subsection \<open>Truncating Floats\<close> |
1174 subsection \<open>Truncating Floats\<close> |
1159 |
1175 |
1160 lift_definition float_round_up :: "nat \<Rightarrow> float \<Rightarrow> float" is truncate_up |
1176 lift_definition float_round_up :: "nat \<Rightarrow> float \<Rightarrow> float" is truncate_up |
1161 by (simp add: truncate_up_def) |
1177 by (simp add: truncate_up_def) |
1184 |
1200 |
1185 context |
1201 context |
1186 begin |
1202 begin |
1187 |
1203 |
1188 qualified lemma compute_float_round_down[code]: |
1204 qualified lemma compute_float_round_down[code]: |
1189 "float_round_down prec (Float m e) = (let d = bitlen \<bar>m\<bar> - int prec in |
1205 "float_round_down prec (Float m e) = (let d = bitlen \<bar>m\<bar> - int prec - 1 in |
1190 if 0 < d then Float (div_twopow m (nat d)) (e + d) |
1206 if 0 < d then Float (div_twopow m (nat d)) (e + d) |
1191 else Float m e)" |
1207 else Float m e)" |
1192 using Float.compute_float_down[of "prec - bitlen \<bar>m\<bar> - e" m e, symmetric] |
1208 using Float.compute_float_down[of "Suc prec - bitlen \<bar>m\<bar> - e" m e, symmetric] |
1193 by transfer (simp add: field_simps abs_mult log_mult bitlen_def truncate_down_def |
1209 by transfer |
1194 cong del: if_weak_cong) |
1210 (simp add: field_simps abs_mult log_mult bitlen_def truncate_down_def |
|
1211 cong del: if_weak_cong) |
1195 |
1212 |
1196 qualified lemma compute_float_round_up[code]: |
1213 qualified lemma compute_float_round_up[code]: |
1197 "float_round_up prec x = - float_round_down prec (-x)" |
1214 "float_round_up prec x = - float_round_down prec (-x)" |
1198 by transfer (simp add: truncate_down_uminus_eq) |
1215 by transfer (simp add: truncate_down_uminus_eq) |
1199 |
1216 |
1210 lemma real_div_nat_eq_floor_of_divide: |
1227 lemma real_div_nat_eq_floor_of_divide: |
1211 fixes a b :: nat |
1228 fixes a b :: nat |
1212 shows "a div b = real_of_int \<lfloor>a / b\<rfloor>" |
1229 shows "a div b = real_of_int \<lfloor>a / b\<rfloor>" |
1213 by (simp add: floor_divide_of_nat_eq [of a b]) |
1230 by (simp add: floor_divide_of_nat_eq [of a b]) |
1214 |
1231 |
1215 definition "rat_precision prec x y = int prec - (bitlen x - bitlen y)" |
1232 definition "rat_precision prec x y = |
|
1233 (let d = bitlen x - bitlen y in int prec - d + |
|
1234 (if Float (abs x) 0 < Float (abs y) d then 1 else 0))" |
|
1235 |
|
1236 lemma floor_log_divide_eq: |
|
1237 assumes "i > 0" "j > 0" "p > 1" |
|
1238 shows "\<lfloor>log p (i / j)\<rfloor> = floor (log p i) - floor (log p j) - |
|
1239 (if i \<ge> j * p powr (floor (log p i) - floor (log p j)) then 0 else 1)" |
|
1240 proof - |
|
1241 let ?l = "log p" |
|
1242 let ?fl = "\<lambda>x. floor (?l x)" |
|
1243 have "\<lfloor>?l (i / j)\<rfloor> = \<lfloor>?l i - ?l j\<rfloor>" using assms |
|
1244 by (auto simp: log_divide) |
|
1245 also have "\<dots> = floor (real_of_int (?fl i - ?fl j) + (?l i - ?fl i - (?l j - ?fl j)))" |
|
1246 (is "_ = floor (_ + ?r)") |
|
1247 by (simp add: algebra_simps) |
|
1248 also note floor_add2 |
|
1249 also note \<open>p > 1\<close> |
|
1250 note powr = powr_le_cancel_iff[symmetric, OF \<open>1 < p\<close>, THEN iffD2] |
|
1251 note powr_strict = powr_less_cancel_iff[symmetric, OF \<open>1 < p\<close>, THEN iffD2] |
|
1252 have "floor ?r = (if i \<ge> j * p powr (?fl i - ?fl j) then 0 else -1)" (is "_ = ?if") |
|
1253 using assms |
|
1254 by (linarith | |
|
1255 auto |
|
1256 intro!: floor_eq2 |
|
1257 intro: powr_strict powr |
|
1258 simp: powr_divide2[symmetric] powr_add divide_simps algebra_simps bitlen_def)+ |
|
1259 finally |
|
1260 show ?thesis by simp |
|
1261 qed |
|
1262 |
|
1263 lemma truncate_down_rat_precision: |
|
1264 "truncate_down prec (real x / real y) = round_down (rat_precision prec x y) (real x / real y)" |
|
1265 and truncate_up_rat_precision: |
|
1266 "truncate_up prec (real x / real y) = round_up (rat_precision prec x y) (real x / real y)" |
|
1267 unfolding truncate_down_def truncate_up_def rat_precision_def |
|
1268 by (cases x; cases y) (auto simp: floor_log_divide_eq algebra_simps bitlen_def) |
1216 |
1269 |
1217 lift_definition lapprox_posrat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float" |
1270 lift_definition lapprox_posrat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float" |
1218 is "\<lambda>prec (x::nat) (y::nat). round_down (rat_precision prec x y) (x / y)" |
1271 is "\<lambda>prec (x::nat) (y::nat). truncate_down prec (x / y)" |
1219 by simp |
1272 by simp |
1220 |
1273 |
1221 context |
1274 context |
1222 begin |
1275 begin |
1223 |
1276 |
1228 l = rat_precision prec x y; |
1281 l = rat_precision prec x y; |
1229 d = if 0 \<le> l then x * 2^nat l div y else x div 2^nat (- l) div y |
1282 d = if 0 \<le> l then x * 2^nat l div y else x div 2^nat (- l) div y |
1230 in normfloat (Float d (- l)))" |
1283 in normfloat (Float d (- l)))" |
1231 unfolding div_mult_twopow_eq |
1284 unfolding div_mult_twopow_eq |
1232 by transfer |
1285 by transfer |
1233 (simp add: round_down_def powr_int real_div_nat_eq_floor_of_divide field_simps Let_def |
1286 (simp add: round_down_def powr_int real_div_nat_eq_floor_of_divide field_simps Let_def |
1234 del: two_powr_minus_int_float) |
1287 truncate_down_rat_precision del: two_powr_minus_int_float) |
1235 |
1288 |
1236 end |
1289 end |
1237 |
1290 |
1238 lift_definition rapprox_posrat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float" |
1291 lift_definition rapprox_posrat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float" |
1239 is "\<lambda>prec (x::nat) (y::nat). round_up (rat_precision prec x y) (x / y)" by |
1292 is "\<lambda>prec (x::nat) (y::nat). truncate_up prec (x / y)" |
1240 simp |
1293 by simp |
1241 |
1294 |
1242 context |
1295 context |
1243 begin |
1296 begin |
1244 |
1297 |
1245 qualified lemma compute_rapprox_posrat[code]: |
1298 qualified lemma compute_rapprox_posrat[code]: |
1280 by (simp add: powr_realpow[symmetric] powr_minus y'_def field_simps) |
1333 by (simp add: powr_realpow[symmetric] powr_minus y'_def field_simps) |
1281 ultimately show ?thesis |
1334 ultimately show ?thesis |
1282 using ceil_divide_floor_conv[of y' x] \<open>\<not> 0 \<le> l\<close> \<open>y' \<noteq> 0\<close> \<open>y \<noteq> 0\<close> |
1335 using ceil_divide_floor_conv[of y' x] \<open>\<not> 0 \<le> l\<close> \<open>y' \<noteq> 0\<close> \<open>y \<noteq> 0\<close> |
1283 l_def[symmetric, THEN meta_eq_to_obj_eq] |
1336 l_def[symmetric, THEN meta_eq_to_obj_eq] |
1284 apply transfer |
1337 apply transfer |
1285 apply (auto simp add: round_up_def ceil_divide_floor_conv) |
1338 apply (auto simp add: round_up_def ceil_divide_floor_conv truncate_up_rat_precision) |
1286 by (metis floor_divide_of_int_eq of_int_of_nat_eq) |
1339 by (metis floor_divide_of_int_eq of_int_of_nat_eq) |
1287 qed |
1340 qed |
1288 qed |
1341 qed |
1289 |
1342 |
1290 end |
1343 end |
1291 |
1344 |
1292 lemma rat_precision_pos: |
1345 lemma rat_precision_pos: |
1293 assumes "0 \<le> x" |
1346 assumes "0 \<le> x" |
1294 and "0 < y" |
1347 and "0 < y" |
1295 and "2 * x < y" |
1348 and "2 * x < y" |
1296 and "0 < n" |
|
1297 shows "rat_precision n (int x) (int y) > 0" |
1349 shows "rat_precision n (int x) (int y) > 0" |
1298 proof - |
1350 proof - |
1299 have "0 < x \<Longrightarrow> log 2 x + 1 = log 2 (2 * x)" |
1351 have "0 < x \<Longrightarrow> log 2 x + 1 = log 2 (2 * x)" |
1300 by (simp add: log_mult) |
1352 by (simp add: log_mult) |
1301 then have "bitlen (int x) < bitlen (int y)" |
1353 then have "bitlen (int x) < bitlen (int y)" |
1325 (if 0 < y then lapprox_posrat prec (nat x) (nat y) |
1377 (if 0 < y then lapprox_posrat prec (nat x) (nat y) |
1326 else - (rapprox_posrat prec (nat x) (nat (-y)))) |
1378 else - (rapprox_posrat prec (nat x) (nat (-y)))) |
1327 else (if 0 < y |
1379 else (if 0 < y |
1328 then - (rapprox_posrat prec (nat (-x)) (nat y)) |
1380 then - (rapprox_posrat prec (nat (-x)) (nat y)) |
1329 else lapprox_posrat prec (nat (-x)) (nat (-y))))" |
1381 else lapprox_posrat prec (nat (-x)) (nat (-y))))" |
1330 by transfer (auto simp: round_up_def round_down_def ceiling_def ac_simps) |
1382 by transfer (simp add: truncate_up_uminus_eq) |
1331 |
1383 |
1332 lift_definition rapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float" is |
1384 lift_definition rapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float" is |
1333 "\<lambda>prec (x::int) (y::int). round_up (rat_precision prec \<bar>x\<bar> \<bar>y\<bar>) (x / y)" |
1385 "\<lambda>prec (x::int) (y::int). truncate_up prec (x / y)" |
1334 by simp |
1386 by simp |
1335 |
1387 |
1336 lemma "rapprox_rat = rapprox_posrat" |
1388 lemma "rapprox_rat = rapprox_posrat" |
1337 by transfer auto |
1389 by transfer auto |
1338 |
1390 |
1339 lemma "lapprox_rat = lapprox_posrat" |
1391 lemma "lapprox_rat = lapprox_posrat" |
1340 by transfer auto |
1392 by transfer auto |
1341 |
1393 |
1342 qualified lemma compute_rapprox_rat[code]: |
1394 qualified lemma compute_rapprox_rat[code]: |
1343 "rapprox_rat prec x y = - lapprox_rat prec (-x) y" |
1395 "rapprox_rat prec x y = - lapprox_rat prec (-x) y" |
1344 by transfer (simp add: round_down_uminus_eq) |
1396 by transfer (simp add: truncate_down_uminus_eq) |
|
1397 |
|
1398 qualified lemma compute_truncate_down[code]: "truncate_down p (Ratreal r) = (let (a, b) = quotient_of r in lapprox_rat p a b)" |
|
1399 by transfer (auto split: prod.split simp: of_rat_divide dest!: quotient_of_div) |
|
1400 |
|
1401 qualified lemma compute_truncate_up[code]: "truncate_up p (Ratreal r) = (let (a, b) = quotient_of r in rapprox_rat p a b)" |
|
1402 by transfer (auto split: prod.split simp: of_rat_divide dest!: quotient_of_div) |
1345 |
1403 |
1346 end |
1404 end |
1347 |
1405 |
1348 |
1406 |
1349 subsection \<open>Division\<close> |
1407 subsection \<open>Division\<close> |
1350 |
1408 |
1351 definition "real_divl prec a b = round_down (int prec + \<lfloor> log 2 \<bar>b\<bar> \<rfloor> - \<lfloor> log 2 \<bar>a\<bar> \<rfloor>) (a / b)" |
1409 definition "real_divl prec a b = truncate_down prec (a / b)" |
1352 |
1410 |
1353 definition "real_divr prec a b = round_up (int prec + \<lfloor> log 2 \<bar>b\<bar> \<rfloor> - \<lfloor> log 2 \<bar>a\<bar> \<rfloor>) (a / b)" |
1411 definition "real_divr prec a b = truncate_up prec (a / b)" |
1354 |
1412 |
1355 lift_definition float_divl :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" is real_divl |
1413 lift_definition float_divl :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" is real_divl |
1356 by (simp add: real_divl_def) |
1414 by (simp add: real_divl_def) |
1357 |
1415 |
1358 context |
1416 context |
1359 begin |
1417 begin |
1360 |
1418 |
1361 qualified lemma compute_float_divl[code]: |
1419 qualified lemma compute_float_divl[code]: |
1362 "float_divl prec (Float m1 s1) (Float m2 s2) = lapprox_rat prec m1 m2 * Float 1 (s1 - s2)" |
1420 "float_divl prec (Float m1 s1) (Float m2 s2) = lapprox_rat prec m1 m2 * Float 1 (s1 - s2)" |
1363 proof (cases "m1 \<noteq> 0 \<and> m2 \<noteq> 0") |
1421 apply transfer |
1364 case True |
1422 unfolding real_divl_def of_int_1 mult_1 truncate_down_shift_int[symmetric] |
1365 let ?f1 = "real_of_int m1 * 2 powr real_of_int s1" and ?f2 = "real_of_int m2 * 2 powr real_of_int s2" |
1423 apply (simp add: powr_divide2[symmetric] powr_minus) |
1366 let ?m = "real_of_int m1 / real_of_int m2" and ?s = "2 powr real_of_int (s1 - s2)" |
1424 done |
1367 from True have eq2: "(int prec + \<lfloor>log 2 \<bar>?f2\<bar>\<rfloor> - \<lfloor>log 2 \<bar>?f1\<bar>\<rfloor>) = |
|
1368 rat_precision prec \<bar>m1\<bar> \<bar>m2\<bar> + (s2 - s1)" |
|
1369 by (simp add: abs_mult log_mult rat_precision_def bitlen_def) |
|
1370 have eq1: "real_of_int m1 * 2 powr real_of_int s1 / (real_of_int m2 * 2 powr real_of_int s2) = ?m * ?s" |
|
1371 by (simp add: field_simps powr_divide2[symmetric]) |
|
1372 from True show ?thesis |
|
1373 by (transfer fixing: m1 s1 m2 s2 prec) (unfold eq1 eq2 round_down_shift real_divl_def, |
|
1374 simp add: field_simps) |
|
1375 next |
|
1376 case False |
|
1377 then show ?thesis by transfer (auto simp: real_divl_def) |
|
1378 qed |
|
1379 |
1425 |
1380 lift_definition float_divr :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" is real_divr |
1426 lift_definition float_divr :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" is real_divr |
1381 by (simp add: real_divr_def) |
1427 by (simp add: real_divr_def) |
1382 |
1428 |
1383 qualified lemma compute_float_divr[code]: |
1429 qualified lemma compute_float_divr[code]: |
1384 "float_divr prec x y = - float_divl prec (-x) y" |
1430 "float_divr prec x y = - float_divl prec (-x) y" |
1385 by transfer (simp add: real_divr_def real_divl_def round_down_uminus_eq) |
1431 by transfer (simp add: real_divr_def real_divl_def truncate_down_uminus_eq) |
1386 |
1432 |
1387 end |
1433 end |
1388 |
1434 |
1389 |
1435 |
1390 subsection \<open>Approximate Power\<close> |
1436 subsection \<open>Approximate Power\<close> |
1530 using truncate_down_uminus_eq[of p "x + y"] |
1576 using truncate_down_uminus_eq[of p "x + y"] |
1531 by (auto simp: plus_down_def plus_up_def) |
1577 by (auto simp: plus_down_def plus_up_def) |
1532 |
1578 |
1533 lemma truncate_down_log2_eqI: |
1579 lemma truncate_down_log2_eqI: |
1534 assumes "\<lfloor>log 2 \<bar>x\<bar>\<rfloor> = \<lfloor>log 2 \<bar>y\<bar>\<rfloor>" |
1580 assumes "\<lfloor>log 2 \<bar>x\<bar>\<rfloor> = \<lfloor>log 2 \<bar>y\<bar>\<rfloor>" |
1535 assumes "\<lfloor>x * 2 powr (p - \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - 1)\<rfloor> = \<lfloor>y * 2 powr (p - \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - 1)\<rfloor>" |
1581 assumes "\<lfloor>x * 2 powr (p - \<lfloor>log 2 \<bar>x\<bar>\<rfloor>)\<rfloor> = \<lfloor>y * 2 powr (p - \<lfloor>log 2 \<bar>x\<bar>\<rfloor>)\<rfloor>" |
1536 shows "truncate_down p x = truncate_down p y" |
1582 shows "truncate_down p x = truncate_down p y" |
1537 using assms by (auto simp: truncate_down_def round_down_def) |
1583 using assms by (auto simp: truncate_down_def round_down_def) |
1538 |
1584 |
1539 lemma bitlen_eq_zero_iff: "bitlen x = 0 \<longleftrightarrow> x \<le> 0" |
1585 lemma bitlen_eq_zero_iff: "bitlen x = 0 \<longleftrightarrow> x \<le> 0" |
1540 by (clarsimp simp add: bitlen_def) |
1586 by (clarsimp simp add: bitlen_def) |
1789 have "\<lfloor>log 2 \<bar>?sum\<bar>\<rfloor> = \<lfloor>log 2 \<bar>real_of_float (Float (?m1*2 + sgn m2) (?e - 1))\<bar>\<rfloor>" . |
1835 have "\<lfloor>log 2 \<bar>?sum\<bar>\<rfloor> = \<lfloor>log 2 \<bar>real_of_float (Float (?m1*2 + sgn m2) (?e - 1))\<bar>\<rfloor>" . |
1790 then have "plus_down p (Float m1 e1) (Float m2 e2) = |
1836 then have "plus_down p (Float m1 e1) (Float m2 e2) = |
1791 truncate_down p (Float (?m1*2 + sgn m2) (?e - 1))" |
1837 truncate_down p (Float (?m1*2 + sgn m2) (?e - 1))" |
1792 unfolding plus_down_def |
1838 unfolding plus_down_def |
1793 proof (rule truncate_down_log2_eqI) |
1839 proof (rule truncate_down_log2_eqI) |
1794 let ?f = "(int p - \<lfloor>log 2 \<bar>real_of_float (Float m1 e1) + real_of_float (Float m2 e2)\<bar>\<rfloor> - 1)" |
1840 let ?f = "(int p - \<lfloor>log 2 \<bar>real_of_float (Float m1 e1) + real_of_float (Float m2 e2)\<bar>\<rfloor>)" |
1795 let ?ai = "m1 * 2 ^ (Suc k1)" |
1841 let ?ai = "m1 * 2 ^ (Suc k1)" |
1796 have "\<lfloor>(?a + ?b) * 2 powr real_of_int ?f\<rfloor> = \<lfloor>(real_of_int (2 * ?ai) + sgn ?b) * 2 powr real_of_int (?f - - ?e - 1)\<rfloor>" |
1842 have "\<lfloor>(?a + ?b) * 2 powr real_of_int ?f\<rfloor> = \<lfloor>(real_of_int (2 * ?ai) + sgn ?b) * 2 powr real_of_int (?f - - ?e - 1)\<rfloor>" |
1797 proof (rule floor_sum_times_2_powr_sgn_eq) |
1843 proof (rule floor_sum_times_2_powr_sgn_eq) |
1798 show "?a * 2 powr real_of_int (-?e) = real_of_int ?ai" |
1844 show "?a * 2 powr real_of_int (-?e) = real_of_int ?ai" |
1799 by (simp add: powr_add powr_realpow[symmetric] powr_divide2[symmetric]) |
1845 by (simp add: powr_add powr_realpow[symmetric] powr_divide2[symmetric]) |
1809 unfolding floor_diff_of_int[symmetric] |
1855 unfolding floor_diff_of_int[symmetric] |
1810 by (auto simp add: log_minus_eq_powr powr_minus_divide intro!: floor_mono) |
1856 by (auto simp add: log_minus_eq_powr powr_minus_divide intro!: floor_mono) |
1811 finally |
1857 finally |
1812 have "int p - \<lfloor>log 2 \<bar>?a + ?b\<bar>\<rfloor> \<le> p - (bitlen \<bar>m1\<bar>) - e1 + 2" |
1858 have "int p - \<lfloor>log 2 \<bar>?a + ?b\<bar>\<rfloor> \<le> p - (bitlen \<bar>m1\<bar>) - e1 + 2" |
1813 by (auto simp: algebra_simps bitlen_def \<open>m1 \<noteq> 0\<close>) |
1859 by (auto simp: algebra_simps bitlen_def \<open>m1 \<noteq> 0\<close>) |
1814 also have "\<dots> \<le> 1 - ?e" |
1860 also have "\<dots> \<le> - ?e" |
1815 using bitlen_nonneg[of "\<bar>m1\<bar>"] by (simp add: k1_def) |
1861 using bitlen_nonneg[of "\<bar>m1\<bar>"] by (simp add: k1_def) |
1816 finally show "?f \<le> - ?e" by simp |
1862 finally show "?f \<le> - ?e" by simp |
1817 qed |
1863 qed |
1818 also have "sgn ?b = sgn m2" |
1864 also have "sgn ?b = sgn m2" |
1819 using powr_gt_zero[of 2 e2] |
1865 using powr_gt_zero[of 2 e2] |
1836 shows "float_plus_down p (Float m1 e1) (Float m2 e2) = |
1882 shows "float_plus_down p (Float m1 e1) (Float m2 e2) = |
1837 (if m1 = 0 then float_round_down p (Float m2 e2) |
1883 (if m1 = 0 then float_round_down p (Float m2 e2) |
1838 else if m2 = 0 then float_round_down p (Float m1 e1) |
1884 else if m2 = 0 then float_round_down p (Float m1 e1) |
1839 else (if e1 \<ge> e2 then |
1885 else (if e1 \<ge> e2 then |
1840 (let |
1886 (let |
1841 k1 = p - nat (bitlen \<bar>m1\<bar>) |
1887 k1 = Suc p - nat (bitlen \<bar>m1\<bar>) |
1842 in |
1888 in |
1843 if bitlen \<bar>m2\<bar> > e1 - e2 - k1 - 2 then float_round_down p ((Float m1 e1) + (Float m2 e2)) |
1889 if bitlen \<bar>m2\<bar> > e1 - e2 - k1 - 2 then float_round_down p ((Float m1 e1) + (Float m2 e2)) |
1844 else float_round_down p (Float (m1 * 2 ^ (Suc (Suc k1)) + sgn m2) (e1 - int k1 - 2))) |
1890 else float_round_down p (Float (m1 * 2 ^ (Suc (Suc k1)) + sgn m2) (e1 - int k1 - 2))) |
1845 else float_plus_down p (Float m2 e2) (Float m1 e1)))" |
1891 else float_plus_down p (Float m2 e2) (Float m1 e1)))" |
1846 proof - |
1892 proof - |
1847 { |
1893 { |
1848 assume "bitlen \<bar>m2\<bar> \<le> e1 - e2 - (p - nat (bitlen \<bar>m1\<bar>)) - 2" "m1 \<noteq> 0" "m2 \<noteq> 0" "e1 \<ge> e2" |
1894 assume "bitlen \<bar>m2\<bar> \<le> e1 - e2 - (Suc p - nat (bitlen \<bar>m1\<bar>)) - 2" "m1 \<noteq> 0" "m2 \<noteq> 0" "e1 \<ge> e2" |
1849 note compute_far_float_plus_down[OF this] |
1895 note compute_far_float_plus_down[OF this] |
1850 } |
1896 } |
1851 then show ?thesis |
1897 then show ?thesis |
1852 by transfer (simp add: Let_def plus_down_def ac_simps) |
1898 by transfer (simp add: Let_def plus_down_def ac_simps) |
1853 qed |
1899 qed |
1870 "real_of_float (Float 1 2) = 4" |
1916 "real_of_float (Float 1 2) = 4" |
1871 "real_of_float (Float 1 (- 1)) = 1/2" |
1917 "real_of_float (Float 1 (- 1)) = 1/2" |
1872 "real_of_float (Float 1 (- 2)) = 1/4" |
1918 "real_of_float (Float 1 (- 2)) = 1/4" |
1873 "real_of_float (Float 1 (- 3)) = 1/8" |
1919 "real_of_float (Float 1 (- 3)) = 1/8" |
1874 "real_of_float (Float (- 1) 0) = -1" |
1920 "real_of_float (Float (- 1) 0) = -1" |
1875 "real_of_float (Float (number_of n) 0) = number_of n" |
1921 "real_of_float (Float (numeral n) 0) = numeral n" |
|
1922 "real_of_float (Float (- numeral n) 0) = - numeral n" |
1876 using two_powr_int_float[of 2] two_powr_int_float[of "-1"] two_powr_int_float[of "-2"] |
1923 using two_powr_int_float[of 2] two_powr_int_float[of "-1"] two_powr_int_float[of "-2"] |
1877 two_powr_int_float[of "-3"] |
1924 two_powr_int_float[of "-3"] |
1878 using powr_realpow[of 2 2] powr_realpow[of 2 3] |
1925 using powr_realpow[of 2 2] powr_realpow[of 2 3] |
1879 using powr_minus[of 2 1] powr_minus[of 2 2] powr_minus[of 2 3] |
1926 using powr_minus[of 2 1] powr_minus[of 2 2] powr_minus[of 2 3] |
1880 by auto |
1927 by auto |
1909 |
1956 |
1910 lemma lapprox_rat_nonneg: |
1957 lemma lapprox_rat_nonneg: |
1911 fixes n x y |
1958 fixes n x y |
1912 assumes "0 \<le> x" and "0 \<le> y" |
1959 assumes "0 \<le> x" and "0 \<le> y" |
1913 shows "0 \<le> real_of_float (lapprox_rat n x y)" |
1960 shows "0 \<le> real_of_float (lapprox_rat n x y)" |
1914 using assms by (auto simp: lapprox_rat_def simp: round_down_nonneg) |
1961 using assms |
|
1962 by transfer (simp add: truncate_down_nonneg) |
1915 |
1963 |
1916 lemma rapprox_rat: "real_of_int x / real_of_int y \<le> real_of_float (rapprox_rat prec x y)" |
1964 lemma rapprox_rat: "real_of_int x / real_of_int y \<le> real_of_float (rapprox_rat prec x y)" |
1917 using round_up by (simp add: rapprox_rat_def) |
1965 by transfer (simp add: truncate_up) |
1918 |
1966 |
1919 lemma rapprox_rat_le1: |
1967 lemma rapprox_rat_le1: |
1920 fixes n x y |
1968 fixes n x y |
1921 assumes xy: "0 \<le> x" "0 < y" "x \<le> y" |
1969 assumes xy: "0 \<le> x" "0 < y" "x \<le> y" |
1922 shows "real_of_float (rapprox_rat n x y) \<le> 1" |
1970 shows "real_of_float (rapprox_rat n x y) \<le> 1" |
1923 proof - |
1971 using assms |
1924 have "bitlen \<bar>x\<bar> \<le> bitlen \<bar>y\<bar>" |
1972 by transfer (simp add: truncate_up_le1) |
1925 using xy unfolding bitlen_def by (auto intro!: floor_mono) |
|
1926 from this assms show ?thesis |
|
1927 by transfer (auto intro!: round_up_le1 simp: rat_precision_def) |
|
1928 qed |
|
1929 |
1973 |
1930 lemma rapprox_rat_nonneg_nonpos: "0 \<le> x \<Longrightarrow> y \<le> 0 \<Longrightarrow> real_of_float (rapprox_rat n x y) \<le> 0" |
1974 lemma rapprox_rat_nonneg_nonpos: "0 \<le> x \<Longrightarrow> y \<le> 0 \<Longrightarrow> real_of_float (rapprox_rat n x y) \<le> 0" |
1931 by transfer (simp add: round_up_le0 divide_nonneg_nonpos) |
1975 by transfer (simp add: truncate_up_nonpos divide_nonneg_nonpos) |
1932 |
1976 |
1933 lemma rapprox_rat_nonpos_nonneg: "x \<le> 0 \<Longrightarrow> 0 \<le> y \<Longrightarrow> real_of_float (rapprox_rat n x y) \<le> 0" |
1977 lemma rapprox_rat_nonpos_nonneg: "x \<le> 0 \<Longrightarrow> 0 \<le> y \<Longrightarrow> real_of_float (rapprox_rat n x y) \<le> 0" |
1934 by transfer (simp add: round_up_le0 divide_nonpos_nonneg) |
1978 by transfer (simp add: truncate_up_nonpos divide_nonpos_nonneg) |
1935 |
1979 |
1936 lemma real_divl: "real_divl prec x y \<le> x / y" |
1980 lemma real_divl: "real_divl prec x y \<le> x / y" |
1937 by (simp add: real_divl_def round_down) |
1981 by (simp add: real_divl_def truncate_down) |
1938 |
1982 |
1939 lemma real_divr: "x / y \<le> real_divr prec x y" |
1983 lemma real_divr: "x / y \<le> real_divr prec x y" |
1940 using round_up by (simp add: real_divr_def) |
1984 by (simp add: real_divr_def truncate_up) |
1941 |
1985 |
1942 lemma float_divl: "real_of_float (float_divl prec x y) \<le> x / y" |
1986 lemma float_divl: "real_of_float (float_divl prec x y) \<le> x / y" |
1943 by transfer (rule real_divl) |
1987 by transfer (rule real_divl) |
1944 |
1988 |
1945 lemma real_divl_lower_bound: |
1989 lemma real_divl_lower_bound: |
1946 "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> real_divl prec x y" |
1990 "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> real_divl prec x y" |
1947 by (simp add: real_divl_def round_down_nonneg) |
1991 by (simp add: real_divl_def truncate_down_nonneg) |
1948 |
1992 |
1949 lemma float_divl_lower_bound: |
1993 lemma float_divl_lower_bound: |
1950 "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> real_of_float (float_divl prec x y)" |
1994 "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> real_of_float (float_divl prec x y)" |
1951 by transfer (rule real_divl_lower_bound) |
1995 by transfer (rule real_divl_lower_bound) |
1952 |
1996 |
1990 by (auto simp del: of_int_abs simp add: powr_int) |
2034 by (auto simp del: of_int_abs simp add: powr_int) |
1991 finally show ?thesis by (simp add: powr_add) |
2035 finally show ?thesis by (simp add: powr_add) |
1992 qed |
2036 qed |
1993 |
2037 |
1994 lemma real_divl_pos_less1_bound: |
2038 lemma real_divl_pos_less1_bound: |
1995 assumes "0 < x" "x \<le> 1" "prec \<ge> 1" |
2039 assumes "0 < x" "x \<le> 1" |
1996 shows "1 \<le> real_divl prec 1 x" |
2040 shows "1 \<le> real_divl prec 1 x" |
1997 proof - |
2041 using assms |
1998 have "log 2 x \<le> real_of_int prec + real_of_int \<lfloor>log 2 x\<rfloor>" |
2042 by (auto intro!: truncate_down_ge1 simp: real_divl_def) |
1999 using \<open>prec \<ge> 1\<close> by arith |
|
2000 from this assms show ?thesis |
|
2001 by (simp add: real_divl_def log_divide round_down_ge1) |
|
2002 qed |
|
2003 |
2043 |
2004 lemma float_divl_pos_less1_bound: |
2044 lemma float_divl_pos_less1_bound: |
2005 "0 < real_of_float x \<Longrightarrow> real_of_float x \<le> 1 \<Longrightarrow> prec \<ge> 1 \<Longrightarrow> 1 \<le> real_of_float (float_divl prec 1 x)" |
2045 "0 < real_of_float x \<Longrightarrow> real_of_float x \<le> 1 \<Longrightarrow> prec \<ge> 1 \<Longrightarrow> 1 \<le> real_of_float (float_divl prec 1 x)" |
2006 by transfer (rule real_divl_pos_less1_bound) |
2046 by transfer (rule real_divl_pos_less1_bound) |
2007 |
2047 |
2023 lemma float_divr_pos_less1_lower_bound: "0 < x \<Longrightarrow> x \<le> 1 \<Longrightarrow> 1 \<le> float_divr prec 1 x" |
2063 lemma float_divr_pos_less1_lower_bound: "0 < x \<Longrightarrow> x \<le> 1 \<Longrightarrow> 1 \<le> float_divr prec 1 x" |
2024 by transfer (rule real_divr_pos_less1_lower_bound) |
2064 by transfer (rule real_divr_pos_less1_lower_bound) |
2025 |
2065 |
2026 lemma real_divr_nonpos_pos_upper_bound: |
2066 lemma real_divr_nonpos_pos_upper_bound: |
2027 "x \<le> 0 \<Longrightarrow> 0 \<le> y \<Longrightarrow> real_divr prec x y \<le> 0" |
2067 "x \<le> 0 \<Longrightarrow> 0 \<le> y \<Longrightarrow> real_divr prec x y \<le> 0" |
2028 by (simp add: real_divr_def round_up_le0 divide_le_0_iff) |
2068 by (simp add: real_divr_def truncate_up_nonpos divide_le_0_iff) |
2029 |
2069 |
2030 lemma float_divr_nonpos_pos_upper_bound: |
2070 lemma float_divr_nonpos_pos_upper_bound: |
2031 "real_of_float x \<le> 0 \<Longrightarrow> 0 \<le> real_of_float y \<Longrightarrow> real_of_float (float_divr prec x y) \<le> 0" |
2071 "real_of_float x \<le> 0 \<Longrightarrow> 0 \<le> real_of_float y \<Longrightarrow> real_of_float (float_divr prec x y) \<le> 0" |
2032 by transfer (rule real_divr_nonpos_pos_upper_bound) |
2072 by transfer (rule real_divr_nonpos_pos_upper_bound) |
2033 |
2073 |
2034 lemma real_divr_nonneg_neg_upper_bound: |
2074 lemma real_divr_nonneg_neg_upper_bound: |
2035 "0 \<le> x \<Longrightarrow> y \<le> 0 \<Longrightarrow> real_divr prec x y \<le> 0" |
2075 "0 \<le> x \<Longrightarrow> y \<le> 0 \<Longrightarrow> real_divr prec x y \<le> 0" |
2036 by (simp add: real_divr_def round_up_le0 divide_le_0_iff) |
2076 by (simp add: real_divr_def truncate_up_nonpos divide_le_0_iff) |
2037 |
2077 |
2038 lemma float_divr_nonneg_neg_upper_bound: |
2078 lemma float_divr_nonneg_neg_upper_bound: |
2039 "0 \<le> real_of_float x \<Longrightarrow> real_of_float y \<le> 0 \<Longrightarrow> real_of_float (float_divr prec x y) \<le> 0" |
2079 "0 \<le> real_of_float x \<Longrightarrow> real_of_float y \<le> 0 \<Longrightarrow> real_of_float (float_divr prec x y) \<le> 0" |
2040 by transfer (rule real_divr_nonneg_neg_upper_bound) |
2080 by transfer (rule real_divr_nonneg_neg_upper_bound) |
2041 |
2081 |
2057 by auto |
2097 by auto |
2058 with \<open>\<lfloor>log 2 x\<rfloor> \<noteq> \<lfloor>log 2 y\<rfloor>\<close> |
2098 with \<open>\<lfloor>log 2 x\<rfloor> \<noteq> \<lfloor>log 2 y\<rfloor>\<close> |
2059 have logless: "log 2 x < log 2 y" and flogless: "\<lfloor>log 2 x\<rfloor> < \<lfloor>log 2 y\<rfloor>" |
2099 have logless: "log 2 x < log 2 y" and flogless: "\<lfloor>log 2 x\<rfloor> < \<lfloor>log 2 y\<rfloor>" |
2060 by (metis floor_less_cancel linorder_cases not_le)+ |
2100 by (metis floor_less_cancel linorder_cases not_le)+ |
2061 have "truncate_up prec x = |
2101 have "truncate_up prec x = |
2062 real_of_int \<lceil>x * 2 powr real_of_int (int prec - \<lfloor>log 2 x\<rfloor> - 1)\<rceil> * 2 powr - real_of_int (int prec - \<lfloor>log 2 x\<rfloor> - 1)" |
2102 real_of_int \<lceil>x * 2 powr real_of_int (int prec - \<lfloor>log 2 x\<rfloor> )\<rceil> * 2 powr - real_of_int (int prec - \<lfloor>log 2 x\<rfloor>)" |
2063 using assms by (simp add: truncate_up_def round_up_def) |
2103 using assms by (simp add: truncate_up_def round_up_def) |
2064 also have "\<lceil>x * 2 powr real_of_int (int prec - \<lfloor>log 2 x\<rfloor> - 1)\<rceil> \<le> (2 ^ prec)" |
2104 also have "\<lceil>x * 2 powr real_of_int (int prec - \<lfloor>log 2 x\<rfloor>)\<rceil> \<le> (2 ^ (Suc prec))" |
2065 proof (unfold ceiling_le_iff) |
2105 proof (unfold ceiling_le_iff) |
2066 have "x * 2 powr real_of_int (int prec - \<lfloor>log 2 x\<rfloor> - 1) \<le> x * (2 powr real prec / (2 powr log 2 x))" |
2106 have "x * 2 powr real_of_int (int prec - \<lfloor>log 2 x\<rfloor>) \<le> x * (2 powr real (Suc prec) / (2 powr log 2 x))" |
2067 using real_of_int_floor_add_one_ge[of "log 2 x"] assms |
2107 using real_of_int_floor_add_one_ge[of "log 2 x"] assms |
2068 by (auto simp add: algebra_simps powr_divide2 intro!: mult_left_mono) |
2108 by (auto simp add: algebra_simps powr_divide2 intro!: mult_left_mono) |
2069 then show "x * 2 powr real_of_int (int prec - \<lfloor>log 2 x\<rfloor> - 1) \<le> real_of_int ((2::int) ^ prec)" |
2109 then show "x * 2 powr real_of_int (int prec - \<lfloor>log 2 x\<rfloor>) \<le> real_of_int ((2::int) ^ (Suc prec))" |
2070 using \<open>0 < x\<close> by (simp add: powr_realpow) |
2110 using \<open>0 < x\<close> by (simp add: powr_realpow powr_add) |
2071 qed |
2111 qed |
2072 then have "real_of_int \<lceil>x * 2 powr real_of_int (int prec - \<lfloor>log 2 x\<rfloor> - 1)\<rceil> \<le> 2 powr int prec" |
2112 then have "real_of_int \<lceil>x * 2 powr real_of_int (int prec - \<lfloor>log 2 x\<rfloor>)\<rceil> \<le> 2 powr int (Suc prec)" |
2073 by (auto simp: powr_realpow) |
2113 apply (auto simp: powr_realpow powr_add) |
|
2114 by (metis power_Suc real_of_int_le_numeral_power_cancel_iff) |
2074 also |
2115 also |
2075 have "2 powr - real_of_int (int prec - \<lfloor>log 2 x\<rfloor> - 1) \<le> 2 powr - real_of_int (int prec - \<lfloor>log 2 y\<rfloor>)" |
2116 have "2 powr - real_of_int (int prec - \<lfloor>log 2 x\<rfloor>) \<le> 2 powr - real_of_int (int prec - \<lfloor>log 2 y\<rfloor> + 1)" |
2076 using logless flogless by (auto intro!: floor_mono) |
2117 using logless flogless by (auto intro!: floor_mono) |
2077 also have "2 powr real_of_int (int prec) \<le> 2 powr (log 2 y + real_of_int (int prec - \<lfloor>log 2 y\<rfloor>))" |
2118 also have "2 powr real_of_int (int (Suc prec)) \<le> 2 powr (log 2 y + real_of_int (int prec - \<lfloor>log 2 y\<rfloor> + 1))" |
2078 using assms \<open>0 < x\<close> |
2119 using assms \<open>0 < x\<close> |
2079 by (auto simp: algebra_simps) |
2120 by (auto simp: algebra_simps) |
2080 finally have "truncate_up prec x \<le> 2 powr (log 2 y + real_of_int (int prec - \<lfloor>log 2 y\<rfloor>)) * 2 powr - real_of_int (int prec - \<lfloor>log 2 y\<rfloor>)" |
2121 finally have "truncate_up prec x \<le> 2 powr (log 2 y + real_of_int (int prec - \<lfloor>log 2 y\<rfloor> + 1)) * 2 powr - real_of_int (int prec - \<lfloor>log 2 y\<rfloor> + 1)" |
2081 by simp |
2122 by simp |
2082 also have "\<dots> = 2 powr (log 2 y + real_of_int (int prec - \<lfloor>log 2 y\<rfloor>) - real_of_int (int prec - \<lfloor>log 2 y\<rfloor>))" |
2123 also have "\<dots> = 2 powr (log 2 y + real_of_int (int prec - \<lfloor>log 2 y\<rfloor>) - real_of_int (int prec - \<lfloor>log 2 y\<rfloor>))" |
2083 by (subst powr_add[symmetric]) simp |
2124 by (subst powr_add[symmetric]) simp |
2084 also have "\<dots> = y" |
2125 also have "\<dots> = y" |
2085 using \<open>0 < x\<close> assms |
2126 using \<open>0 < x\<close> assms |
2102 note truncate_up_nonpos[OF \<open>x \<le> 0\<close>] |
2143 note truncate_up_nonpos[OF \<open>x \<le> 0\<close>] |
2103 also note truncate_up_le[OF \<open>0 \<le> y\<close>] |
2144 also note truncate_up_le[OF \<open>0 \<le> y\<close>] |
2104 finally show ?thesis . |
2145 finally show ?thesis . |
2105 qed |
2146 qed |
2106 |
2147 |
2107 lemma truncate_down_zeroprec_mono: |
|
2108 assumes "0 < x" "x \<le> y" |
|
2109 shows "truncate_down 0 x \<le> truncate_down 0 y" |
|
2110 proof - |
|
2111 have "x * 2 powr (- real_of_int \<lfloor>log 2 x\<rfloor> - 1) = x * inverse (2 powr ((real_of_int \<lfloor>log 2 x\<rfloor> + 1)))" |
|
2112 by (simp add: powr_divide2[symmetric] powr_add powr_minus inverse_eq_divide) |
|
2113 also have "\<dots> = 2 powr (log 2 x - (real_of_int \<lfloor>log 2 x\<rfloor>) - 1)" |
|
2114 using \<open>0 < x\<close> |
|
2115 by (auto simp: field_simps powr_add powr_divide2[symmetric]) |
|
2116 also have "\<dots> < 2 powr 0" |
|
2117 using real_of_int_floor_add_one_gt |
|
2118 unfolding neg_less_iff_less |
|
2119 by (intro powr_less_mono) (auto simp: algebra_simps) |
|
2120 finally have "\<lfloor>x * 2 powr (- real_of_int \<lfloor>log 2 x\<rfloor> - 1)\<rfloor> < 1" |
|
2121 unfolding less_ceiling_iff of_int_minus of_int_1 |
|
2122 by simp |
|
2123 moreover have "0 \<le> \<lfloor>x * 2 powr (- real_of_int \<lfloor>log 2 x\<rfloor> - 1)\<rfloor>" |
|
2124 using \<open>x > 0\<close> by auto |
|
2125 ultimately have "\<lfloor>x * 2 powr (- real_of_int \<lfloor>log 2 x\<rfloor> - 1)\<rfloor> \<in> {0 ..< 1}" |
|
2126 by simp |
|
2127 also have "\<dots> \<subseteq> {0}" |
|
2128 by auto |
|
2129 finally have "\<lfloor>x * 2 powr (- real_of_int \<lfloor>log 2 x\<rfloor> - 1)\<rfloor> = 0" |
|
2130 by simp |
|
2131 with assms show ?thesis |
|
2132 by (auto simp: truncate_down_def round_down_def) |
|
2133 qed |
|
2134 |
|
2135 lemma truncate_down_switch_sign_mono: |
2148 lemma truncate_down_switch_sign_mono: |
2136 assumes "x \<le> 0" |
2149 assumes "x \<le> 0" |
2137 and "0 \<le> y" |
2150 and "0 \<le> y" |
2138 and "x \<le> y" |
2151 and "x \<le> y" |
2139 shows "truncate_down prec x \<le> truncate_down prec y" |
2152 shows "truncate_down prec x \<le> truncate_down prec y" |
2145 |
2158 |
2146 lemma truncate_down_nonneg_mono: |
2159 lemma truncate_down_nonneg_mono: |
2147 assumes "0 \<le> x" "x \<le> y" |
2160 assumes "0 \<le> x" "x \<le> y" |
2148 shows "truncate_down prec x \<le> truncate_down prec y" |
2161 shows "truncate_down prec x \<le> truncate_down prec y" |
2149 proof - |
2162 proof - |
2150 consider "0 < x" "prec = 0" | "x \<le> 0" | "\<lfloor>log 2 \<bar>x\<bar>\<rfloor> = \<lfloor>log 2 \<bar>y\<bar>\<rfloor>" | |
2163 consider "x \<le> 0" | "\<lfloor>log 2 \<bar>x\<bar>\<rfloor> = \<lfloor>log 2 \<bar>y\<bar>\<rfloor>" | |
2151 "0 < x" "\<lfloor>log 2 \<bar>x\<bar>\<rfloor> \<noteq> \<lfloor>log 2 \<bar>y\<bar>\<rfloor>" "prec \<noteq> 0" |
2164 "0 < x" "\<lfloor>log 2 \<bar>x\<bar>\<rfloor> \<noteq> \<lfloor>log 2 \<bar>y\<bar>\<rfloor>" |
2152 by arith |
2165 by arith |
2153 then show ?thesis |
2166 then show ?thesis |
2154 proof cases |
2167 proof cases |
2155 case 1 |
2168 case 1 |
2156 with assms show ?thesis |
|
2157 by (simp add: truncate_down_zeroprec_mono) |
|
2158 next |
|
2159 case 2 |
|
2160 with assms have "x = 0" "0 \<le> y" by simp_all |
2169 with assms have "x = 0" "0 \<le> y" by simp_all |
2161 then show ?thesis |
2170 then show ?thesis |
2162 by (auto intro!: truncate_down_nonneg) |
2171 by (auto intro!: truncate_down_nonneg) |
2163 next |
2172 next |
2164 case 3 |
2173 case 2 |
2165 then show ?thesis |
2174 then show ?thesis |
2166 using assms |
2175 using assms |
2167 by (auto simp: truncate_down_def round_down_def intro!: floor_mono) |
2176 by (auto simp: truncate_down_def round_down_def intro!: floor_mono) |
2168 next |
2177 next |
2169 case 4 |
2178 case 3 |
2170 from \<open>0 < x\<close> have "log 2 x \<le> log 2 y" "0 < y" "0 \<le> y" |
2179 from \<open>0 < x\<close> have "log 2 x \<le> log 2 y" "0 < y" "0 \<le> y" |
2171 using assms by auto |
2180 using assms by auto |
2172 with \<open>\<lfloor>log 2 \<bar>x\<bar>\<rfloor> \<noteq> \<lfloor>log 2 \<bar>y\<bar>\<rfloor>\<close> |
2181 with \<open>\<lfloor>log 2 \<bar>x\<bar>\<rfloor> \<noteq> \<lfloor>log 2 \<bar>y\<bar>\<rfloor>\<close> |
2173 have logless: "log 2 x < log 2 y" and flogless: "\<lfloor>log 2 x\<rfloor> < \<lfloor>log 2 y\<rfloor>" |
2182 have logless: "log 2 x < log 2 y" and flogless: "\<lfloor>log 2 x\<rfloor> < \<lfloor>log 2 y\<rfloor>" |
2174 unfolding atomize_conj abs_of_pos[OF \<open>0 < x\<close>] abs_of_pos[OF \<open>0 < y\<close>] |
2183 unfolding atomize_conj abs_of_pos[OF \<open>0 < x\<close>] abs_of_pos[OF \<open>0 < y\<close>] |
2175 by (metis floor_less_cancel linorder_cases not_le) |
2184 by (metis floor_less_cancel linorder_cases not_le) |
2176 from \<open>prec \<noteq> 0\<close> have [simp]: "prec \<ge> Suc 0" |
2185 have "2 powr prec \<le> y * 2 powr real prec / (2 powr log 2 y)" |
2177 by auto |
|
2178 have "2 powr (prec - 1) \<le> y * 2 powr real (prec - 1) / (2 powr log 2 y)" |
|
2179 using \<open>0 < y\<close> by simp |
2186 using \<open>0 < y\<close> by simp |
2180 also have "\<dots> \<le> y * 2 powr real prec / (2 powr (real_of_int \<lfloor>log 2 y\<rfloor> + 1))" |
2187 also have "\<dots> \<le> y * 2 powr real (Suc prec) / (2 powr (real_of_int \<lfloor>log 2 y\<rfloor> + 1))" |
2181 using \<open>0 \<le> y\<close> \<open>0 \<le> x\<close> assms(2) |
2188 using \<open>0 \<le> y\<close> \<open>0 \<le> x\<close> assms(2) |
2182 by (auto intro!: powr_mono divide_left_mono |
2189 by (auto intro!: powr_mono divide_left_mono |
2183 simp: of_nat_diff powr_add |
2190 simp: of_nat_diff powr_add |
2184 powr_divide2[symmetric]) |
2191 powr_divide2[symmetric]) |
2185 also have "\<dots> = y * 2 powr real prec / (2 powr real_of_int \<lfloor>log 2 y\<rfloor> * 2)" |
2192 also have "\<dots> = y * 2 powr real (Suc prec) / (2 powr real_of_int \<lfloor>log 2 y\<rfloor> * 2)" |
2186 by (auto simp: powr_add) |
2193 by (auto simp: powr_add) |
2187 finally have "(2 ^ (prec - 1)) \<le> \<lfloor>y * 2 powr real_of_int (int prec - \<lfloor>log 2 \<bar>y\<bar>\<rfloor> - 1)\<rfloor>" |
2194 finally have "(2 ^ prec) \<le> \<lfloor>y * 2 powr real_of_int (int (Suc prec) - \<lfloor>log 2 \<bar>y\<bar>\<rfloor> - 1)\<rfloor>" |
2188 using \<open>0 \<le> y\<close> |
2195 using \<open>0 \<le> y\<close> |
2189 by (auto simp: powr_divide2[symmetric] le_floor_iff powr_realpow) |
2196 by (auto simp: powr_divide2[symmetric] le_floor_iff powr_realpow powr_add) |
2190 then have "(2 ^ (prec - 1)) * 2 powr - real_of_int (int prec - \<lfloor>log 2 \<bar>y\<bar>\<rfloor> - 1) \<le> truncate_down prec y" |
2197 then have "(2 ^ (prec)) * 2 powr - real_of_int (int prec - \<lfloor>log 2 \<bar>y\<bar>\<rfloor>) \<le> truncate_down prec y" |
2191 by (auto simp: truncate_down_def round_down_def) |
2198 by (auto simp: truncate_down_def round_down_def) |
2192 moreover |
2199 moreover |
2193 { |
2200 { |
2194 have "x = 2 powr (log 2 \<bar>x\<bar>)" using \<open>0 < x\<close> by simp |
2201 have "x = 2 powr (log 2 \<bar>x\<bar>)" using \<open>0 < x\<close> by simp |
2195 also have "\<dots> \<le> (2 ^ (prec )) * 2 powr - real_of_int (int prec - \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - 1)" |
2202 also have "\<dots> \<le> (2 ^ (Suc prec )) * 2 powr - real_of_int (int prec - \<lfloor>log 2 \<bar>x\<bar>\<rfloor>)" |
2196 using real_of_int_floor_add_one_ge[of "log 2 \<bar>x\<bar>"] |
2203 using real_of_int_floor_add_one_ge[of "log 2 \<bar>x\<bar>"] \<open>0 < x\<close> |
2197 by (auto simp: powr_realpow[symmetric] powr_add[symmetric] algebra_simps) |
2204 by (auto simp: powr_realpow[symmetric] powr_add[symmetric] algebra_simps |
|
2205 powr_mult_base le_powr_iff) |
2198 also |
2206 also |
2199 have "2 powr - real_of_int (int prec - \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - 1) \<le> 2 powr - real_of_int (int prec - \<lfloor>log 2 \<bar>y\<bar>\<rfloor>)" |
2207 have "2 powr - real_of_int (int prec - \<lfloor>log 2 \<bar>x\<bar>\<rfloor>) \<le> 2 powr - real_of_int (int prec - \<lfloor>log 2 \<bar>y\<bar>\<rfloor> + 1)" |
2200 using logless flogless \<open>x > 0\<close> \<open>y > 0\<close> |
2208 using logless flogless \<open>x > 0\<close> \<open>y > 0\<close> |
2201 by (auto intro!: floor_mono) |
2209 by (auto intro!: floor_mono) |
2202 finally have "x \<le> (2 ^ (prec - 1)) * 2 powr - real_of_int (int prec - \<lfloor>log 2 \<bar>y\<bar>\<rfloor> - 1)" |
2210 finally have "x \<le> (2 ^ prec) * 2 powr - real_of_int (int prec - \<lfloor>log 2 \<bar>y\<bar>\<rfloor>)" |
2203 by (auto simp: powr_realpow[symmetric] powr_divide2[symmetric] assms of_nat_diff) |
2211 by (auto simp: powr_realpow[symmetric] powr_divide2[symmetric] assms of_nat_diff) |
2204 } |
2212 } |
2205 ultimately show ?thesis |
2213 ultimately show ?thesis |
2206 by (metis dual_order.trans truncate_down) |
2214 by (metis dual_order.trans truncate_down) |
2207 qed |
2215 qed |