author hoelzl Fri Aug 29 11:24:31 2014 +0200 (2014-08-29) changeset 58097 cfd3cff9387b parent 58096 5a48fef59fab child 58098 ff478d85129b
add simp rules for divisions of numerals in floor and ceiling.
 src/HOL/Archimedean_Field.thy file | annotate | diff | revisions src/HOL/Real.thy file | annotate | diff | revisions
```     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")
```