# HG changeset patch
# User hoelzl
# Date 1409304271 -7200
# Node ID cfd3cff9387b935e6de01d52225b475c7f5412aa
# Parent  5a48fef59fabbb88247b6ff1854530b10ab26f10
add simp rules for divisions of numerals in floor and ceiling.

diff -r 5a48fef59fab -r cfd3cff9387b src/HOL/Archimedean_Field.thy
--- a/src/HOL/Archimedean_Field.thy	Fri Aug 29 14:48:23 2014 +0200
+++ b/src/HOL/Archimedean_Field.thy	Fri Aug 29 11:24:31 2014 +0200
@@ -288,6 +288,19 @@
 lemma floor_diff_one [simp]: "floor (x - 1) = floor x - 1"
   using floor_diff_of_int [of x 1] by simp
 
+lemma le_mult_floor:
+  assumes "0 \<le> a" and "0 \<le> b"
+  shows "floor a * floor b \<le> floor (a * b)"
+proof -
+  have "of_int (floor a) \<le> a"
+    and "of_int (floor b) \<le> b" by (auto intro: of_int_floor_le)
+  hence "of_int (floor a * floor b) \<le> a * b"
+    using assms by (auto intro!: mult_mono)
+  also have "a * b < of_int (floor (a * b) + 1)"  
+    using floor_correct[of "a * b"] by auto
+  finally show ?thesis unfolding of_int_less_iff by simp
+qed
+
 subsection {* Ceiling function *}
 
 definition
diff -r 5a48fef59fab -r cfd3cff9387b src/HOL/Real.thy
--- a/src/HOL/Real.thy	Fri Aug 29 14:48:23 2014 +0200
+++ b/src/HOL/Real.thy	Fri Aug 29 11:24:31 2014 +0200
@@ -1724,18 +1724,6 @@
 lemma floor_subtract [simp]: "floor (x - real a) = floor x - a"
   by linarith
 
-lemma le_mult_floor:
-  assumes "0 \<le> (a :: real)" and "0 \<le> b"
-  shows "floor a * floor b \<le> floor (a * b)"
-proof -
-  have "real (floor a) \<le> a"
-    and "real (floor b) \<le> b" by auto
-  hence "real (floor a * floor b) \<le> a * b"
-    using assms by (auto intro!: mult_mono)
-  also have "a * b < real (floor (a * b) + 1)" by auto
-  finally show ?thesis unfolding real_of_int_less_iff by simp
-qed
-
 lemma floor_divide_eq_div:
   "floor (real a / real b) = a div b"
 proof cases
@@ -1746,6 +1734,12 @@
               real_of_int_zero_cancel right_inverse_eq div_self mod_div_trivial)
 qed (auto simp: real_of_int_div)
 
+lemma floor_divide_eq_div_numeral[simp]: "\<lfloor>numeral a / numeral b::real\<rfloor> = numeral a div numeral b"
+  using floor_divide_eq_div[of "numeral a" "numeral b"] by simp
+
+lemma floor_minus_divide_eq_div_numeral[simp]: "\<lfloor>- (numeral a / numeral b)::real\<rfloor> = - numeral a div numeral b"
+  using floor_divide_eq_div[of "- numeral a" "numeral b"] by simp
+
 lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n"
   by linarith
 
@@ -1798,6 +1792,16 @@
 lemma ceiling_subtract [simp]: "ceiling (x - real a) = ceiling x - a"
   by linarith
 
+lemma ceiling_divide_eq_div: "\<lceil>real a / real b\<rceil> = - (- a div b)"
+  unfolding ceiling_def minus_divide_left real_of_int_minus[symmetric] floor_divide_eq_div by simp_all
+
+lemma ceiling_divide_eq_div_numeral [simp]:
+  "\<lceil>numeral a / numeral b :: real\<rceil> = - (- numeral a div numeral b)"
+  using ceiling_divide_eq_div[of "numeral a" "numeral b"] by simp
+
+lemma ceiling_minus_divide_eq_div_numeral [simp]:
+  "\<lceil>- (numeral a / numeral b :: real)\<rceil> = - (numeral a div numeral b)"
+  using ceiling_divide_eq_div[of "- numeral a" "numeral b"] by simp
 
 subsubsection {* Versions for the natural numbers *}
 
@@ -1911,6 +1915,10 @@
     by (simp add: divide_less_eq natfloor_less_iff distrib_right)
 qed
 
+lemma natfloor_div_numeral[simp]:
+  "natfloor (numeral x / numeral y) = numeral x div numeral y"
+  using natfloor_div_nat[of "numeral x" "numeral y"] by simp
+
 lemma le_mult_natfloor:
   shows "natfloor a * natfloor b \<le> natfloor (a * b)"
   by (cases "0 <= a & 0 <= b")