generalize natfloor_div_nat, add floor variant: floor_divide_real_eq_div
authorhoelzl
Mon Oct 27 12:03:13 2014 +0100 (2014-10-27)
changeset 58788d17b3844b726
parent 58787 af9eb5e566dd
child 58789 387f65e69dd5
generalize natfloor_div_nat, add floor variant: floor_divide_real_eq_div
src/HOL/Real.thy
     1.1 --- a/src/HOL/Real.thy	Sun Oct 26 19:11:16 2014 +0100
     1.2 +++ b/src/HOL/Real.thy	Mon Oct 27 12:03:13 2014 +0100
     1.3 @@ -1724,6 +1724,23 @@
     1.4  lemma floor_subtract [simp]: "floor (x - real a) = floor x - a"
     1.5    by linarith
     1.6  
     1.7 +lemma floor_divide_real_eq_div: "0 \<le> b \<Longrightarrow> floor (a / real b) = floor a div b"
     1.8 +proof cases
     1.9 +  assume "0 < b"
    1.10 +  { fix i j :: int assume "real i \<le> a" "a < 1 + real i"
    1.11 +      "real j * real b \<le> a" "a < real b + real j * real b"
    1.12 +    then have "i < b + j * b" "j * b < 1 + i"
    1.13 +      unfolding real_of_int_less_iff[symmetric] by auto
    1.14 +    then have "(j - i div b) * b \<le> i mod b" "i mod b < ((j - i div b) + 1) * b"
    1.15 +      by (auto simp: field_simps)
    1.16 +    then have "(j - i div b) * b < 1 * b" "0 * b < ((j - i div b) + 1) * b"
    1.17 +      using pos_mod_bound[OF `0<b`, of i] pos_mod_sign[OF `0<b`, of i] by linarith+
    1.18 +    then have "j = i div b"
    1.19 +      using `0 < b` unfolding mult_less_cancel_right by auto }
    1.20 +  with `0 < b` show ?thesis
    1.21 +    by (auto split: floor_split simp: field_simps)
    1.22 +qed auto
    1.23 +
    1.24  lemma floor_divide_eq_div:
    1.25    "floor (real a / real b) = a div b"
    1.26  proof cases
    1.27 @@ -1896,24 +1913,9 @@
    1.28      "natfloor(x - real a) = natfloor x - a"
    1.29    by linarith
    1.30  
    1.31 -lemma natfloor_div_nat:
    1.32 -  assumes "1 <= x" and "y > 0"
    1.33 -  shows "natfloor (x / real y) = natfloor x div y"
    1.34 -proof (rule natfloor_eq)
    1.35 -  have "(natfloor x) div y * y \<le> natfloor x"
    1.36 -    by (rule add_leD1 [where k="natfloor x mod y"], simp)
    1.37 -  thus "real (natfloor x div y) \<le> x / real y"
    1.38 -    using assms by (simp add: le_divide_eq le_natfloor_eq)
    1.39 -  have "natfloor x < (natfloor x) div y * y + y"
    1.40 -    apply (subst mod_div_equality [symmetric])
    1.41 -    apply (rule add_strict_left_mono)
    1.42 -    apply (rule mod_less_divisor)
    1.43 -    apply fact
    1.44 -    done
    1.45 -  thus "x / real y < real (natfloor x div y) + 1"
    1.46 -    using assms
    1.47 -    by (simp add: divide_less_eq natfloor_less_iff distrib_right)
    1.48 -qed
    1.49 +lemma natfloor_div_nat: "0 \<le> x \<Longrightarrow> natfloor (x / real y) = natfloor x div y"
    1.50 +  unfolding natfloor_def real_of_int_of_nat_eq[symmetric]
    1.51 +  by (subst floor_divide_real_eq_div) (simp_all add: nat_div_distrib)
    1.52  
    1.53  lemma natfloor_div_numeral[simp]:
    1.54    "natfloor (numeral x / numeral y) = numeral x div numeral y"