add simp rules for divisions of numerals in floor and ceiling.
authorhoelzl
Fri Aug 29 11:24:31 2014 +0200 (2014-08-29)
changeset 58097cfd3cff9387b
parent 58096 5a48fef59fab
child 58098 ff478d85129b
add simp rules for divisions of numerals in floor and ceiling.
src/HOL/Archimedean_Field.thy
src/HOL/Real.thy
     1.1 --- a/src/HOL/Archimedean_Field.thy	Fri Aug 29 14:48:23 2014 +0200
     1.2 +++ b/src/HOL/Archimedean_Field.thy	Fri Aug 29 11:24:31 2014 +0200
     1.3 @@ -288,6 +288,19 @@
     1.4  lemma floor_diff_one [simp]: "floor (x - 1) = floor x - 1"
     1.5    using floor_diff_of_int [of x 1] by simp
     1.6  
     1.7 +lemma le_mult_floor:
     1.8 +  assumes "0 \<le> a" and "0 \<le> b"
     1.9 +  shows "floor a * floor b \<le> floor (a * b)"
    1.10 +proof -
    1.11 +  have "of_int (floor a) \<le> a"
    1.12 +    and "of_int (floor b) \<le> b" by (auto intro: of_int_floor_le)
    1.13 +  hence "of_int (floor a * floor b) \<le> a * b"
    1.14 +    using assms by (auto intro!: mult_mono)
    1.15 +  also have "a * b < of_int (floor (a * b) + 1)"  
    1.16 +    using floor_correct[of "a * b"] by auto
    1.17 +  finally show ?thesis unfolding of_int_less_iff by simp
    1.18 +qed
    1.19 +
    1.20  subsection {* Ceiling function *}
    1.21  
    1.22  definition
     2.1 --- a/src/HOL/Real.thy	Fri Aug 29 14:48:23 2014 +0200
     2.2 +++ b/src/HOL/Real.thy	Fri Aug 29 11:24:31 2014 +0200
     2.3 @@ -1724,18 +1724,6 @@
     2.4  lemma floor_subtract [simp]: "floor (x - real a) = floor x - a"
     2.5    by linarith
     2.6  
     2.7 -lemma le_mult_floor:
     2.8 -  assumes "0 \<le> (a :: real)" and "0 \<le> b"
     2.9 -  shows "floor a * floor b \<le> floor (a * b)"
    2.10 -proof -
    2.11 -  have "real (floor a) \<le> a"
    2.12 -    and "real (floor b) \<le> b" by auto
    2.13 -  hence "real (floor a * floor b) \<le> a * b"
    2.14 -    using assms by (auto intro!: mult_mono)
    2.15 -  also have "a * b < real (floor (a * b) + 1)" by auto
    2.16 -  finally show ?thesis unfolding real_of_int_less_iff by simp
    2.17 -qed
    2.18 -
    2.19  lemma floor_divide_eq_div:
    2.20    "floor (real a / real b) = a div b"
    2.21  proof cases
    2.22 @@ -1746,6 +1734,12 @@
    2.23                real_of_int_zero_cancel right_inverse_eq div_self mod_div_trivial)
    2.24  qed (auto simp: real_of_int_div)
    2.25  
    2.26 +lemma floor_divide_eq_div_numeral[simp]: "\<lfloor>numeral a / numeral b::real\<rfloor> = numeral a div numeral b"
    2.27 +  using floor_divide_eq_div[of "numeral a" "numeral b"] by simp
    2.28 +
    2.29 +lemma floor_minus_divide_eq_div_numeral[simp]: "\<lfloor>- (numeral a / numeral b)::real\<rfloor> = - numeral a div numeral b"
    2.30 +  using floor_divide_eq_div[of "- numeral a" "numeral b"] by simp
    2.31 +
    2.32  lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n"
    2.33    by linarith
    2.34  
    2.35 @@ -1798,6 +1792,16 @@
    2.36  lemma ceiling_subtract [simp]: "ceiling (x - real a) = ceiling x - a"
    2.37    by linarith
    2.38  
    2.39 +lemma ceiling_divide_eq_div: "\<lceil>real a / real b\<rceil> = - (- a div b)"
    2.40 +  unfolding ceiling_def minus_divide_left real_of_int_minus[symmetric] floor_divide_eq_div by simp_all
    2.41 +
    2.42 +lemma ceiling_divide_eq_div_numeral [simp]:
    2.43 +  "\<lceil>numeral a / numeral b :: real\<rceil> = - (- numeral a div numeral b)"
    2.44 +  using ceiling_divide_eq_div[of "numeral a" "numeral b"] by simp
    2.45 +
    2.46 +lemma ceiling_minus_divide_eq_div_numeral [simp]:
    2.47 +  "\<lceil>- (numeral a / numeral b :: real)\<rceil> = - (numeral a div numeral b)"
    2.48 +  using ceiling_divide_eq_div[of "- numeral a" "numeral b"] by simp
    2.49  
    2.50  subsubsection {* Versions for the natural numbers *}
    2.51  
    2.52 @@ -1911,6 +1915,10 @@
    2.53      by (simp add: divide_less_eq natfloor_less_iff distrib_right)
    2.54  qed
    2.55  
    2.56 +lemma natfloor_div_numeral[simp]:
    2.57 +  "natfloor (numeral x / numeral y) = numeral x div numeral y"
    2.58 +  using natfloor_div_nat[of "numeral x" "numeral y"] by simp
    2.59 +
    2.60  lemma le_mult_natfloor:
    2.61    shows "natfloor a * natfloor b \<le> natfloor (a * b)"
    2.62    by (cases "0 <= a & 0 <= b")