515 apply (erule ssubst) |
515 apply (erule ssubst) |
516 apply (simp del: real_of_int_of_nat_eq) |
516 apply (simp del: real_of_int_of_nat_eq) |
517 apply simp |
517 apply simp |
518 done |
518 done |
519 |
519 |
520 lemma natfloor_div_nat: "1 <= x ==> y > 0 ==> |
520 lemma natfloor_div_nat: |
521 natfloor (x / real y) = natfloor x div y" |
521 assumes "1 <= x" and "y > 0" |
522 proof - |
522 shows "natfloor (x / real y) = natfloor x div y" |
523 assume "1 <= (x::real)" and "(y::nat) > 0" |
523 proof - |
524 have "natfloor x = (natfloor x) div y * y + (natfloor x) mod y" |
524 have "natfloor x = (natfloor x) div y * y + (natfloor x) mod y" |
525 by simp |
525 by simp |
526 then have a: "real(natfloor x) = real ((natfloor x) div y) * real y + |
526 then have a: "real(natfloor x) = real ((natfloor x) div y) * real y + |
527 real((natfloor x) mod y)" |
527 real((natfloor x) mod y)" |
528 by (simp only: real_of_nat_add [THEN sym] real_of_nat_mult [THEN sym]) |
528 by (simp only: real_of_nat_add [THEN sym] real_of_nat_mult [THEN sym]) |
533 by (simp add: a) |
533 by (simp add: a) |
534 then have "x / real y = ... / real y" |
534 then have "x / real y = ... / real y" |
535 by simp |
535 by simp |
536 also have "... = real((natfloor x) div y) + real((natfloor x) mod y) / |
536 also have "... = real((natfloor x) div y) + real((natfloor x) mod y) / |
537 real y + (x - real(natfloor x)) / real y" |
537 real y + (x - real(natfloor x)) / real y" |
538 by (auto simp add: algebra_simps add_divide_distrib |
538 by (auto simp add: algebra_simps add_divide_distrib diff_divide_distrib) |
539 diff_divide_distrib prems) |
|
540 finally have "natfloor (x / real y) = natfloor(...)" by simp |
539 finally have "natfloor (x / real y) = natfloor(...)" by simp |
541 also have "... = natfloor(real((natfloor x) mod y) / |
540 also have "... = natfloor(real((natfloor x) mod y) / |
542 real y + (x - real(natfloor x)) / real y + real((natfloor x) div y))" |
541 real y + (x - real(natfloor x)) / real y + real((natfloor x) div y))" |
543 by (simp add: add_ac) |
542 by (simp add: add_ac) |
544 also have "... = natfloor(real((natfloor x) mod y) / |
543 also have "... = natfloor(real((natfloor x) mod y) / |
545 real y + (x - real(natfloor x)) / real y) + (natfloor x) div y" |
544 real y + (x - real(natfloor x)) / real y) + (natfloor x) div y" |
546 apply (rule natfloor_add) |
545 apply (rule natfloor_add) |
547 apply (rule add_nonneg_nonneg) |
546 apply (rule add_nonneg_nonneg) |
548 apply (rule divide_nonneg_pos) |
547 apply (rule divide_nonneg_pos) |
549 apply simp |
548 apply simp |
550 apply (simp add: prems) |
549 apply (simp add: assms) |
551 apply (rule divide_nonneg_pos) |
550 apply (rule divide_nonneg_pos) |
552 apply (simp add: algebra_simps) |
551 apply (simp add: algebra_simps) |
553 apply (rule real_natfloor_le) |
552 apply (rule real_natfloor_le) |
554 apply (insert prems, auto) |
553 using assms apply auto |
555 done |
554 done |
556 also have "natfloor(real((natfloor x) mod y) / |
555 also have "natfloor(real((natfloor x) mod y) / |
557 real y + (x - real(natfloor x)) / real y) = 0" |
556 real y + (x - real(natfloor x)) / real y) = 0" |
558 apply (rule natfloor_eq) |
557 apply (rule natfloor_eq) |
559 apply simp |
558 apply simp |
560 apply (rule add_nonneg_nonneg) |
559 apply (rule add_nonneg_nonneg) |
561 apply (rule divide_nonneg_pos) |
560 apply (rule divide_nonneg_pos) |
562 apply force |
561 apply force |
563 apply (force simp add: prems) |
562 apply (force simp add: assms) |
564 apply (rule divide_nonneg_pos) |
563 apply (rule divide_nonneg_pos) |
565 apply (simp add: algebra_simps) |
564 apply (simp add: algebra_simps) |
566 apply (rule real_natfloor_le) |
565 apply (rule real_natfloor_le) |
567 apply (auto simp add: prems) |
566 apply (auto simp add: assms) |
568 apply (insert prems, arith) |
567 using assms apply arith |
569 apply (simp add: add_divide_distrib [THEN sym]) |
568 using assms apply (simp add: add_divide_distrib [THEN sym]) |
570 apply (subgoal_tac "real y = real y - 1 + 1") |
569 apply (subgoal_tac "real y = real y - 1 + 1") |
571 apply (erule ssubst) |
570 apply (erule ssubst) |
572 apply (rule add_le_less_mono) |
571 apply (rule add_le_less_mono) |
573 apply (simp add: algebra_simps) |
572 apply (simp add: algebra_simps) |
574 apply (subgoal_tac "1 + real(natfloor x mod y) = |
573 apply (subgoal_tac "1 + real(natfloor x mod y) = |