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.29 +    using False by (simp only: of_int_add) (simp add: field_simps)
    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