summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Thu, 09 Apr 2015 09:12:47 +0200 | |

changeset 59984 | 4f1eccec320c |

parent 59980 | 070f04c94b2e |

child 59985 | 5574138cf97c |

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