374 hence "inverse (real (Suc n)) * x < 1" |
374 hence "inverse (real (Suc n)) * x < 1" |
375 using x_greater_zero by simp |
375 using x_greater_zero by simp |
376 hence "real (Suc n) * (inverse (real (Suc n)) * x) < real (Suc n) * 1" |
376 hence "real (Suc n) * (inverse (real (Suc n)) * x) < real (Suc n) * 1" |
377 by (rule mult_strict_left_mono) simp |
377 by (rule mult_strict_left_mono) simp |
378 hence "x < real (Suc n)" |
378 hence "x < real (Suc n)" |
379 by (simp add: ring_simps) |
379 by (simp add: algebra_simps) |
380 thus "\<exists>(n::nat). x < real n" .. |
380 thus "\<exists>(n::nat). x < real n" .. |
381 qed |
381 qed |
382 |
382 |
383 lemma reals_Archimedean3: |
383 lemma reals_Archimedean3: |
384 assumes x_greater_zero: "0 < x" |
384 assumes x_greater_zero: "0 < x" |
389 obtain n where "y * inverse x < real (n::nat)" |
389 obtain n where "y * inverse x < real (n::nat)" |
390 using reals_Archimedean2 .. |
390 using reals_Archimedean2 .. |
391 hence "y * inverse x * x < real n * x" |
391 hence "y * inverse x * x < real n * x" |
392 using x_greater_zero by (simp add: mult_strict_right_mono) |
392 using x_greater_zero by (simp add: mult_strict_right_mono) |
393 hence "x * inverse x * y < x * real n" |
393 hence "x * inverse x * y < x * real n" |
394 by (simp add: ring_simps) |
394 by (simp add: algebra_simps) |
395 hence "y < real (n::nat) * x" |
395 hence "y < real (n::nat) * x" |
396 using x_not_zero by (simp add: ring_simps) |
396 using x_not_zero by (simp add: algebra_simps) |
397 thus "\<exists>(n::nat). y < real n * x" .. |
397 thus "\<exists>(n::nat). y < real n * x" .. |
398 qed |
398 qed |
399 |
399 |
400 lemma reals_Archimedean6: |
400 lemma reals_Archimedean6: |
401 "0 \<le> r ==> \<exists>(n::nat). real (n - 1) \<le> r & r < real (n)" |
401 "0 \<le> r ==> \<exists>(n::nat). real (n - 1) \<le> r & r < real (n)" |
1082 apply simp |
1082 apply simp |
1083 apply simp_all |
1083 apply simp_all |
1084 done |
1084 done |
1085 |
1085 |
1086 lemma real_natfloor_gt_diff_one: "x - 1 < real(natfloor x)" |
1086 lemma real_natfloor_gt_diff_one: "x - 1 < real(natfloor x)" |
1087 apply (simp add: compare_rls) |
1087 using real_natfloor_add_one_gt by (simp add: algebra_simps) |
1088 apply (rule real_natfloor_add_one_gt) |
|
1089 done |
|
1090 |
1088 |
1091 lemma ge_natfloor_plus_one_imp_gt: "natfloor z + 1 <= n ==> z < real n" |
1089 lemma ge_natfloor_plus_one_imp_gt: "natfloor z + 1 <= n ==> z < real n" |
1092 apply (subgoal_tac "z < real(natfloor z) + 1") |
1090 apply (subgoal_tac "z < real(natfloor z) + 1") |
1093 apply arith |
1091 apply arith |
1094 apply (rule real_natfloor_add_one_gt) |
1092 apply (rule real_natfloor_add_one_gt) |
1277 by (simp add: a) |
1275 by (simp add: a) |
1278 then have "x / real y = ... / real y" |
1276 then have "x / real y = ... / real y" |
1279 by simp |
1277 by simp |
1280 also have "... = real((natfloor x) div y) + real((natfloor x) mod y) / |
1278 also have "... = real((natfloor x) div y) + real((natfloor x) mod y) / |
1281 real y + (x - real(natfloor x)) / real y" |
1279 real y + (x - real(natfloor x)) / real y" |
1282 by (auto simp add: ring_simps add_divide_distrib |
1280 by (auto simp add: algebra_simps add_divide_distrib |
1283 diff_divide_distrib prems) |
1281 diff_divide_distrib prems) |
1284 finally have "natfloor (x / real y) = natfloor(...)" by simp |
1282 finally have "natfloor (x / real y) = natfloor(...)" by simp |
1285 also have "... = natfloor(real((natfloor x) mod y) / |
1283 also have "... = natfloor(real((natfloor x) mod y) / |
1286 real y + (x - real(natfloor x)) / real y + real((natfloor x) div y))" |
1284 real y + (x - real(natfloor x)) / real y + real((natfloor x) div y))" |
1287 by (simp add: add_ac) |
1285 by (simp add: add_ac) |
1291 apply (rule add_nonneg_nonneg) |
1289 apply (rule add_nonneg_nonneg) |
1292 apply (rule divide_nonneg_pos) |
1290 apply (rule divide_nonneg_pos) |
1293 apply simp |
1291 apply simp |
1294 apply (simp add: prems) |
1292 apply (simp add: prems) |
1295 apply (rule divide_nonneg_pos) |
1293 apply (rule divide_nonneg_pos) |
1296 apply (simp add: compare_rls) |
1294 apply (simp add: algebra_simps) |
1297 apply (rule real_natfloor_le) |
1295 apply (rule real_natfloor_le) |
1298 apply (insert prems, auto) |
1296 apply (insert prems, auto) |
1299 done |
1297 done |
1300 also have "natfloor(real((natfloor x) mod y) / |
1298 also have "natfloor(real((natfloor x) mod y) / |
1301 real y + (x - real(natfloor x)) / real y) = 0" |
1299 real y + (x - real(natfloor x)) / real y) = 0" |
1304 apply (rule add_nonneg_nonneg) |
1302 apply (rule add_nonneg_nonneg) |
1305 apply (rule divide_nonneg_pos) |
1303 apply (rule divide_nonneg_pos) |
1306 apply force |
1304 apply force |
1307 apply (force simp add: prems) |
1305 apply (force simp add: prems) |
1308 apply (rule divide_nonneg_pos) |
1306 apply (rule divide_nonneg_pos) |
1309 apply (simp add: compare_rls) |
1307 apply (simp add: algebra_simps) |
1310 apply (rule real_natfloor_le) |
1308 apply (rule real_natfloor_le) |
1311 apply (auto simp add: prems) |
1309 apply (auto simp add: prems) |
1312 apply (insert prems, arith) |
1310 apply (insert prems, arith) |
1313 apply (simp add: add_divide_distrib [THEN sym]) |
1311 apply (simp add: add_divide_distrib [THEN sym]) |
1314 apply (subgoal_tac "real y = real y - 1 + 1") |
1312 apply (subgoal_tac "real y = real y - 1 + 1") |
1315 apply (erule ssubst) |
1313 apply (erule ssubst) |
1316 apply (rule add_le_less_mono) |
1314 apply (rule add_le_less_mono) |
1317 apply (simp add: compare_rls) |
1315 apply (simp add: algebra_simps) |
1318 apply (subgoal_tac "real(natfloor x mod y) + 1 = |
1316 apply (subgoal_tac "1 + real(natfloor x mod y) = |
1319 real(natfloor x mod y + 1)") |
1317 real(natfloor x mod y + 1)") |
1320 apply (erule ssubst) |
1318 apply (erule ssubst) |
1321 apply (subst real_of_nat_le_iff) |
1319 apply (subst real_of_nat_le_iff) |
1322 apply (subgoal_tac "natfloor x mod y < y") |
1320 apply (subgoal_tac "natfloor x mod y < y") |
1323 apply arith |
1321 apply arith |
1324 apply (rule mod_less_divisor) |
1322 apply (rule mod_less_divisor) |
1325 apply auto |
1323 apply auto |
1326 apply (simp add: compare_rls) |
1324 using real_natfloor_add_one_gt |
1327 apply (subst add_commute) |
1325 apply (simp add: algebra_simps) |
1328 apply (rule real_natfloor_add_one_gt) |
|
1329 done |
1326 done |
1330 finally show ?thesis by simp |
1327 finally show ?thesis by simp |
1331 qed |
1328 qed |
1332 |
1329 |
1333 end |
1330 end |