src/HOL/Archimedean_Field.thy
 changeset 59984 4f1eccec320c parent 59613 7103019278f0 child 60128 3d696ccb7fa6
```     1.1 --- a/src/HOL/Archimedean_Field.thy	Wed Apr 08 23:00:09 2015 +0200
1.2 +++ b/src/HOL/Archimedean_Field.thy	Thu Apr 09 09:12:47 2015 +0200
1.3 @@ -309,6 +309,71 @@
1.4    finally show ?thesis unfolding of_int_less_iff by simp
1.5  qed
1.6
1.7 +lemma floor_divide_of_int_eq:
1.8 +  fixes k l :: int
1.9 +  shows "\<lfloor>of_int k / of_int l\<rfloor> = of_int (k div l)"
1.10 +proof (cases "l = 0")
1.11 +  case True then show ?thesis by simp
1.12 +next
1.13 +  case False
1.14 +  have *: "\<lfloor>of_int (k mod l) / of_int l :: 'a\<rfloor> = 0"
1.15 +  proof (cases "l > 0")
1.16 +    case True then show ?thesis
1.17 +      by (auto intro: floor_unique)
1.18 +  next
1.19 +    case False
1.20 +    obtain r where "r = - l" by blast
1.21 +    then have l: "l = - r" by simp
1.22 +    moreover with `l \<noteq> 0` False have "r > 0" by simp
1.23 +    ultimately show ?thesis using pos_mod_bound [of r]
1.24 +      by (auto simp add: zmod_zminus2_eq_if less_le field_simps intro: floor_unique)
1.25 +  qed
1.26 +  have "(of_int k :: 'a) = of_int (k div l * l + k mod l)"
1.27 +    by simp
1.28 +  also have "\<dots> = (of_int (k div l) + of_int (k mod l) / of_int l) * of_int l"
1.30 +  finally have "(of_int k / of_int l :: 'a) = \<dots> / of_int l"
1.31 +    by simp
1.32 +  then have "(of_int k / of_int l :: 'a) = of_int (k div l) + of_int (k mod l) / of_int l"
1.33 +    using False by (simp only:) (simp add: field_simps)
1.34 +  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>"
1.35 +    by simp
1.36 +  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>"
1.37 +    by (simp add: ac_simps)
1.38 +  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)"
1.39 +    by simp
1.40 +  with * show ?thesis by simp
1.41 +qed
1.42 +
1.43 +lemma floor_divide_of_nat_eq:
1.44 +  fixes m n :: nat
1.45 +  shows "\<lfloor>of_nat m / of_nat n\<rfloor> = of_nat (m div n)"
1.46 +proof (cases "n = 0")
1.47 +  case True then show ?thesis by simp
1.48 +next
1.49 +  case False
1.50 +  then have *: "\<lfloor>of_nat (m mod n) / of_nat n :: 'a\<rfloor> = 0"
1.51 +    by (auto intro: floor_unique)
1.52 +  have "(of_nat m :: 'a) = of_nat (m div n * n + m mod n)"
1.53 +    by simp
1.54 +  also have "\<dots> = (of_nat (m div n) + of_nat (m mod n) / of_nat n) * of_nat n"
1.55 +    using False by (simp only: of_nat_add) (simp add: field_simps of_nat_mult)
1.56 +  finally have "(of_nat m / of_nat n :: 'a) = \<dots> / of_nat n"
1.57 +    by simp
1.58 +  then have "(of_nat m / of_nat n :: 'a) = of_nat (m div n) + of_nat (m mod n) / of_nat n"
1.59 +    using False by (simp only:) simp
1.60 +  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>"
1.61 +    by simp
1.62 +  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>"
1.63 +    by (simp add: ac_simps)
1.64 +  moreover have "(of_nat (m div n) :: 'a) = of_int (of_nat (m div n))"
1.65 +    by simp
1.66 +  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)"
1.67 +    by (simp only: floor_add_of_int)
1.68 +  with * show ?thesis by simp
1.69 +qed
1.70 +
1.71 +
1.72  subsection {* Ceiling function *}
1.73
1.74  definition
```