# HG changeset patch
# User hoelzl
# Date 1334752159 -7200
# Node ID c031e65c8ddc7aa52c63a86c0cba874915565704
# Parent  836b4c4d7c86fe23f35ed0d682ad99b1286e02b7
add lemma to equate floor and div

diff -r 836b4c4d7c86 -r c031e65c8ddc src/HOL/RComplete.thy
--- a/src/HOL/RComplete.thy	Wed Apr 18 14:29:18 2012 +0200
+++ b/src/HOL/RComplete.thy	Wed Apr 18 14:29:19 2012 +0200
@@ -252,6 +252,16 @@
   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
+  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)
+
 lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n"
   unfolding real_of_nat_def by simp