conversion between division on nat/int and division in archmedean fields

--- a/src/HOL/Archimedean_Field.thy	Wed Apr 08 23:00:09 2015 +0200
+++ b/src/HOL/Archimedean_Field.thy	Thu Apr 09 09:12:47 2015 +0200
@@ -309,6 +309,71 @@
   finally show ?thesis unfolding of_int_less_iff by simp
 qed
 
+lemma floor_divide_of_int_eq:
+  fixes k l :: int
+  shows "\<lfloor>of_int k / of_int l\<rfloor> = of_int (k div l)"
+proof (cases "l = 0")
+  case True then show ?thesis by simp
+next
+  case False
+  have *: "\<lfloor>of_int (k mod l) / of_int l :: 'a\<rfloor> = 0"
+  proof (cases "l > 0")
+    case True then show ?thesis
+      by (auto intro: floor_unique)
+  next
+    case False
+    obtain r where "r = - l" by blast
+    then have l: "l = - r" by simp
+    moreover with `l \<noteq> 0` False have "r > 0" by simp
+    ultimately show ?thesis using pos_mod_bound [of r]
+      by (auto simp add: zmod_zminus2_eq_if less_le field_simps intro: floor_unique)
+  qed
+  have "(of_int k :: 'a) = of_int (k div l * l + k mod l)"
+    by simp
+  also have "\<dots> = (of_int (k div l) + of_int (k mod l) / of_int l) * of_int l"
+    using False by (simp only: of_int_add) (simp add: field_simps)
+  finally have "(of_int k / of_int l :: 'a) = \<dots> / of_int l"
+    by simp 
+  then have "(of_int k / of_int l :: 'a) = of_int (k div l) + of_int (k mod l) / of_int l"
+    using False by (simp only:) (simp add: field_simps)
+  then have "\<lfloor>of_int k / of_int l :: 'a\<rfloor> = \<lfloor>of_int (k div l) + of_int (k mod l) / of_int l :: 'a\<rfloor>" 
+    by simp
+  then have "\<lfloor>of_int k / of_int l :: 'a\<rfloor> = \<lfloor>of_int (k mod l) / of_int l + of_int (k div l) :: 'a\<rfloor>"
+    by (simp add: ac_simps)
+  then have "\<lfloor>of_int k / of_int l :: 'a\<rfloor> = \<lfloor>of_int (k mod l) / of_int l :: 'a\<rfloor> + of_int (k div l)"
+    by simp
+  with * show ?thesis by simp
+qed
+
+lemma floor_divide_of_nat_eq:
+  fixes m n :: nat
+  shows "\<lfloor>of_nat m / of_nat n\<rfloor> = of_nat (m div n)"
+proof (cases "n = 0")
+  case True then show ?thesis by simp
+next
+  case False
+  then have *: "\<lfloor>of_nat (m mod n) / of_nat n :: 'a\<rfloor> = 0"
+    by (auto intro: floor_unique)
+  have "(of_nat m :: 'a) = of_nat (m div n * n + m mod n)"
+    by simp
+  also have "\<dots> = (of_nat (m div n) + of_nat (m mod n) / of_nat n) * of_nat n"
+    using False by (simp only: of_nat_add) (simp add: field_simps of_nat_mult)
+  finally have "(of_nat m / of_nat n :: 'a) = \<dots> / of_nat n"
+    by simp 
+  then have "(of_nat m / of_nat n :: 'a) = of_nat (m div n) + of_nat (m mod n) / of_nat n"
+    using False by (simp only:) simp
+  then have "\<lfloor>of_nat m / of_nat n :: 'a\<rfloor> = \<lfloor>of_nat (m div n) + of_nat (m mod n) / of_nat n :: 'a\<rfloor>" 
+    by simp
+  then have "\<lfloor>of_nat m / of_nat n :: 'a\<rfloor> = \<lfloor>of_nat (m mod n) / of_nat n + of_nat (m div n) :: 'a\<rfloor>"
+    by (simp add: ac_simps)
+  moreover have "(of_nat (m div n) :: 'a) = of_int (of_nat (m div n))"
+    by simp
+  ultimately have "\<lfloor>of_nat m / of_nat n :: 'a\<rfloor> = \<lfloor>of_nat (m mod n) / of_nat n :: 'a\<rfloor> + of_nat (m div n)"
+    by (simp only: floor_add_of_int)
+  with * show ?thesis by simp
+qed
+
+
 subsection {* Ceiling function *}
 
 definition

--- a/src/HOL/Library/Float.thy	Wed Apr 08 23:00:09 2015 +0200
+++ b/src/HOL/Library/Float.thy	Thu Apr 09 09:12:47 2015 +0200
@@ -1093,9 +1093,9 @@
   by (cases "b=0") (simp_all add: div_mult2_eq[symmetric] ac_simps)
 
 lemma real_div_nat_eq_floor_of_divide:
-  fixes a b::nat
-  shows "a div b = real (floor (a/b))"
-by (metis floor_divide_eq_div real_of_int_of_nat_eq zdiv_int)
+  fixes a b :: nat
+  shows "a div b = real \<lfloor>a / b\<rfloor>"
+  by (simp add: floor_divide_of_nat_eq [of a b] real_eq_of_nat)
 
 definition "rat_precision prec x y = int prec - (bitlen x - bitlen y)"
 

--- a/src/HOL/Rat.thy	Wed Apr 08 23:00:09 2015 +0200
+++ b/src/HOL/Rat.thy	Thu Apr 09 09:12:47 2015 +0200
@@ -610,8 +610,7 @@
 end
 
 lemma floor_Fract: "floor (Fract a b) = a div b"
-  using rat_floor_lemma [of a b]
-  by (simp add: floor_unique)
+  by (simp add: Fract_of_int_quotient floor_divide_of_int_eq)
 
 
 subsection {* Linear arithmetic setup *}

--- a/src/HOL/Real.thy	Wed Apr 08 23:00:09 2015 +0200
+++ b/src/HOL/Real.thy	Thu Apr 09 09:12:47 2015 +0200
@@ -1793,13 +1793,7 @@
 
 lemma floor_divide_eq_div:
   "floor (real a / real b) = a div b"
-proof cases
-  assume "b \<noteq> 0 \<or> b dvd a"
-  with real_of_int_div3[of a b] show ?thesis
-    by (auto simp: real_of_int_div[symmetric] intro!: floor_eq2 real_of_int_div4 neq_le_trans)
-       (metis add_left_cancel zero_neq_one real_of_int_div_aux real_of_int_inject
-              real_of_int_zero_cancel right_inverse_eq div_self mod_div_trivial)
-qed (auto simp: real_of_int_div)
+  using floor_divide_of_int_eq [of a b] real_eq_of_int by simp
 
 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