# HG changeset patch # User haftmann # Date 1483561708 -3600 # Node ID 5cb5e7ecb2846b54b54e72b3f0875a67dea31436 # Parent 0be08e4cd0ecf6036356bebac3075dc911911450 reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion diff -r 0be08e4cd0ec -r 5cb5e7ecb284 src/HOL/Library/Field_as_Ring.thy --- a/src/HOL/Library/Field_as_Ring.thy Wed Jan 04 22:57:39 2017 +0100 +++ b/src/HOL/Library/Field_as_Ring.thy Wed Jan 04 21:28:28 2017 +0100 @@ -24,15 +24,19 @@ end -instantiation real :: euclidean_ring +instantiation real :: unique_euclidean_ring begin definition [simp]: "normalize_real = (normalize_field :: real \ _)" definition [simp]: "unit_factor_real = (unit_factor_field :: real \ _)" definition [simp]: "euclidean_size_real = (euclidean_size_field :: real \ _)" +definition [simp]: "uniqueness_constraint_real = (top :: real \ real \ bool)" definition [simp]: "modulo_real = (mod_field :: real \ _)" -instance by standard (simp_all add: dvd_field_iff divide_simps) +instance + by standard + (simp_all add: dvd_field_iff divide_simps split: if_splits) + end instantiation real :: euclidean_ring_gcd @@ -51,15 +55,19 @@ end -instantiation rat :: euclidean_ring +instantiation rat :: unique_euclidean_ring begin definition [simp]: "normalize_rat = (normalize_field :: rat \ _)" definition [simp]: "unit_factor_rat = (unit_factor_field :: rat \ _)" definition [simp]: "euclidean_size_rat = (euclidean_size_field :: rat \ _)" +definition [simp]: "uniqueness_constraint_rat = (top :: rat \ rat \ bool)" definition [simp]: "modulo_rat = (mod_field :: rat \ _)" -instance by standard (simp_all add: dvd_field_iff divide_simps) +instance + by standard + (simp_all add: dvd_field_iff divide_simps split: if_splits) + end instantiation rat :: euclidean_ring_gcd @@ -78,15 +86,19 @@ end -instantiation complex :: euclidean_ring +instantiation complex :: unique_euclidean_ring begin definition [simp]: "normalize_complex = (normalize_field :: complex \ _)" definition [simp]: "unit_factor_complex = (unit_factor_field :: complex \ _)" definition [simp]: "euclidean_size_complex = (euclidean_size_field :: complex \ _)" +definition [simp]: "uniqueness_constraint_complex = (top :: complex \ complex \ bool)" definition [simp]: "modulo_complex = (mod_field :: complex \ _)" -instance by standard (simp_all add: dvd_field_iff divide_simps) +instance + by standard + (simp_all add: dvd_field_iff divide_simps split: if_splits) + end instantiation complex :: euclidean_ring_gcd diff -r 0be08e4cd0ec -r 5cb5e7ecb284 src/HOL/Library/Formal_Power_Series.thy --- a/src/HOL/Library/Formal_Power_Series.thy Wed Jan 04 22:57:39 2017 +0100 +++ b/src/HOL/Library/Formal_Power_Series.thy Wed Jan 04 21:28:28 2017 +0100 @@ -1400,7 +1400,7 @@ subsection \Formal power series form a Euclidean ring\ -instantiation fps :: (field) euclidean_ring +instantiation fps :: (field) euclidean_ring_cancel begin definition fps_euclidean_size_def: diff -r 0be08e4cd0ec -r 5cb5e7ecb284 src/HOL/Library/Polynomial_Factorial.thy --- a/src/HOL/Library/Polynomial_Factorial.thy Wed Jan 04 22:57:39 2017 +0100 +++ b/src/HOL/Library/Polynomial_Factorial.thy Wed Jan 04 21:28:28 2017 +0100 @@ -676,14 +676,15 @@ "euclidean_size_field_poly p = (if p = 0 then 0 else 2 ^ degree p)" lemma dvd_field_poly: "dvd.dvd (op * :: 'a :: field poly \ _) = op dvd" - by (intro ext) (simp_all add: dvd.dvd_def dvd_def) + by (intro ext) (simp_all add: dvd.dvd_def dvd_def) interpretation field_poly: - euclidean_ring where zero = "0 :: 'a :: field poly" + unique_euclidean_ring where zero = "0 :: 'a :: field poly" and one = 1 and plus = plus and uminus = uminus and minus = minus and times = times and normalize = normalize_field_poly and unit_factor = unit_factor_field_poly and euclidean_size = euclidean_size_field_poly + and uniqueness_constraint = top and divide = divide and modulo = modulo proof (standard, unfold dvd_field_poly) fix p :: "'a poly" @@ -698,6 +699,17 @@ fix p :: "'a poly" assume "p \ 0" thus "is_unit (unit_factor_field_poly p)" by (simp add: unit_factor_field_poly_def lead_coeff_nonzero is_unit_pCons_iff) +next + fix p q s :: "'a poly" assume "s \ 0" + moreover assume "euclidean_size_field_poly p < euclidean_size_field_poly q" + ultimately show "euclidean_size_field_poly (p * s) < euclidean_size_field_poly (q * s)" + by (auto simp add: euclidean_size_field_poly_def degree_mult_eq) +next + fix p q r :: "'a poly" assume "p \ 0" + moreover assume "euclidean_size_field_poly r < euclidean_size_field_poly p" + ultimately show "(q * p + r) div p = q" + by (cases "r = 0") + (auto simp add: unit_factor_field_poly_def euclidean_size_field_poly_def div_poly_less) qed (auto simp: unit_factor_field_poly_def normalize_field_poly_def lead_coeff_mult euclidean_size_field_poly_def Rings.div_mult_mod_eq intro!: degree_mod_less' degree_mult_right_le) @@ -1011,17 +1023,22 @@ end -instantiation poly :: ("{field,factorial_ring_gcd}") euclidean_ring +instantiation poly :: ("{field,factorial_ring_gcd}") unique_euclidean_ring begin -definition euclidean_size_poly :: "'a poly \ nat" where - "euclidean_size_poly p = (if p = 0 then 0 else 2 ^ degree p)" +definition euclidean_size_poly :: "'a poly \ nat" + where "euclidean_size_poly p = (if p = 0 then 0 else 2 ^ degree p)" + +definition uniqueness_constraint_poly :: "'a poly \ 'a poly \ bool" + where [simp]: "uniqueness_constraint_poly = top" instance - by standard (auto simp: euclidean_size_poly_def Rings.div_mult_mod_eq intro!: degree_mod_less' degree_mult_right_le) + by standard + (auto simp: euclidean_size_poly_def Rings.div_mult_mod_eq div_poly_less degree_mult_eq intro!: degree_mod_less' degree_mult_right_le + split: if_splits) + end - instance poly :: ("{field,factorial_ring_gcd}") euclidean_ring_gcd by standard (simp_all add: gcd_poly_def lcm_poly_def Gcd_poly_def Lcm_poly_def eucl_eq_factorial) diff -r 0be08e4cd0ec -r 5cb5e7ecb284 src/HOL/Number_Theory/Euclidean_Algorithm.thy --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Wed Jan 04 22:57:39 2017 +0100 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Wed Jan 04 21:28:28 2017 +0100 @@ -1,133 +1,17 @@ -(* Author: Manuel Eberl *) +(* Title: HOL/Number_Theory/Euclidean_Algorithm.thy + Author: Manuel Eberl, TU Muenchen +*) -section \Abstract euclidean algorithm\ +section \Abstract euclidean algorithm in euclidean (semi)rings\ theory Euclidean_Algorithm -imports "~~/src/HOL/GCD" Factorial_Ring -begin - -text \ - A Euclidean semiring is a semiring upon which the Euclidean algorithm can be - implemented. It must provide: - \begin{itemize} - \item division with remainder - \item a size function such that @{term "size (a mod b) < size b"} - for any @{term "b \ 0"} - \end{itemize} - The existence of these functions makes it possible to derive gcd and lcm functions - for any Euclidean semiring. -\ -class euclidean_semiring = semidom_modulo + normalization_semidom + - fixes euclidean_size :: "'a \ nat" - assumes size_0 [simp]: "euclidean_size 0 = 0" - assumes mod_size_less: - "b \ 0 \ euclidean_size (a mod b) < euclidean_size b" - assumes size_mult_mono: - "b \ 0 \ euclidean_size a \ euclidean_size (a * b)" + imports "~~/src/HOL/GCD" + "~~/src/HOL/Number_Theory/Factorial_Ring" + "~~/src/HOL/Number_Theory/Euclidean_Division" begin -lemma euclidean_size_normalize [simp]: - "euclidean_size (normalize a) = euclidean_size a" -proof (cases "a = 0") - case True - then show ?thesis - by simp -next - case [simp]: False - have "euclidean_size (normalize a) \ euclidean_size (normalize a * unit_factor a)" - by (rule size_mult_mono) simp - moreover have "euclidean_size a \ euclidean_size (a * (1 div unit_factor a))" - by (rule size_mult_mono) simp - ultimately show ?thesis - by simp -qed - -lemma euclidean_division: - fixes a :: 'a and b :: 'a - assumes "b \ 0" - obtains s and t where "a = s * b + t" - and "euclidean_size t < euclidean_size b" -proof - - from div_mult_mod_eq [of a b] - have "a = a div b * b + a mod b" by simp - with that and assms show ?thesis by (auto simp add: mod_size_less) -qed - -lemma dvd_euclidean_size_eq_imp_dvd: - assumes "a \ 0" and b_dvd_a: "b dvd a" and size_eq: "euclidean_size a = euclidean_size b" - shows "a dvd b" -proof (rule ccontr) - assume "\ a dvd b" - hence "b mod a \ 0" using mod_0_imp_dvd[of b a] by blast - then have "b mod a \ 0" by (simp add: mod_eq_0_iff_dvd) - from b_dvd_a have b_dvd_mod: "b dvd b mod a" by (simp add: dvd_mod_iff) - from b_dvd_mod obtain c where "b mod a = b * c" unfolding dvd_def by blast - with \b mod a \ 0\ have "c \ 0" by auto - with \b mod a = b * c\ have "euclidean_size (b mod a) \ euclidean_size b" - using size_mult_mono by force - moreover from \\ a dvd b\ and \a \ 0\ - have "euclidean_size (b mod a) < euclidean_size a" - using mod_size_less by blast - ultimately show False using size_eq by simp -qed - -lemma size_mult_mono': "b \ 0 \ euclidean_size a \ euclidean_size (b * a)" - by (subst mult.commute) (rule size_mult_mono) - -lemma euclidean_size_times_unit: - assumes "is_unit a" - shows "euclidean_size (a * b) = euclidean_size b" -proof (rule antisym) - from assms have [simp]: "a \ 0" by auto - thus "euclidean_size (a * b) \ euclidean_size b" by (rule size_mult_mono') - from assms have "is_unit (1 div a)" by simp - hence "1 div a \ 0" by (intro notI) simp_all - hence "euclidean_size (a * b) \ euclidean_size ((1 div a) * (a * b))" - by (rule size_mult_mono') - also from assms have "(1 div a) * (a * b) = b" - by (simp add: algebra_simps unit_div_mult_swap) - finally show "euclidean_size (a * b) \ euclidean_size b" . -qed - -lemma euclidean_size_unit: "is_unit a \ euclidean_size a = euclidean_size 1" - using euclidean_size_times_unit[of a 1] by simp - -lemma unit_iff_euclidean_size: - "is_unit a \ euclidean_size a = euclidean_size 1 \ a \ 0" -proof safe - assume A: "a \ 0" and B: "euclidean_size a = euclidean_size 1" - show "is_unit a" by (rule dvd_euclidean_size_eq_imp_dvd[OF A _ B]) simp_all -qed (auto intro: euclidean_size_unit) - -lemma euclidean_size_times_nonunit: - assumes "a \ 0" "b \ 0" "\is_unit a" - shows "euclidean_size b < euclidean_size (a * b)" -proof (rule ccontr) - assume "\euclidean_size b < euclidean_size (a * b)" - with size_mult_mono'[OF assms(1), of b] - have eq: "euclidean_size (a * b) = euclidean_size b" by simp - have "a * b dvd b" - by (rule dvd_euclidean_size_eq_imp_dvd[OF _ _ eq]) (insert assms, simp_all) - hence "a * b dvd 1 * b" by simp - with \b \ 0\ have "is_unit a" by (subst (asm) dvd_times_right_cancel_iff) - with assms(3) show False by contradiction -qed - -lemma dvd_imp_size_le: - assumes "a dvd b" "b \ 0" - shows "euclidean_size a \ euclidean_size b" - using assms by (auto elim!: dvdE simp: size_mult_mono) - -lemma dvd_proper_imp_size_less: - assumes "a dvd b" "\b dvd a" "b \ 0" - shows "euclidean_size a < euclidean_size b" -proof - - from assms(1) obtain c where "b = a * c" by (erule dvdE) - hence z: "b = c * a" by (simp add: mult.commute) - from z assms have "\is_unit c" by (auto simp: mult.commute mult_unit_dvd_iff) - with z assms show ?thesis - by (auto intro!: euclidean_size_times_nonunit simp: ) -qed +context euclidean_semiring +begin function gcd_eucl :: "'a \ 'a \ 'a" where @@ -432,7 +316,7 @@ end -class euclidean_ring = euclidean_semiring + idom +context euclidean_ring begin function euclid_ext_aux :: "'a \ _" where @@ -680,27 +564,6 @@ subsection \Typical instances\ -instantiation nat :: euclidean_semiring -begin - -definition [simp]: - "euclidean_size_nat = (id :: nat \ nat)" - -instance by standard simp_all - -end - - -instantiation int :: euclidean_ring -begin - -definition [simp]: - "euclidean_size_int = (nat \ abs :: int \ nat)" - -instance by standard (auto simp add: abs_mult nat_mult_distrib split: abs_split) - -end - instance nat :: euclidean_semiring_gcd proof show [simp]: "gcd = (gcd_eucl :: nat \ _)" "Lcm = (Lcm_eucl :: nat set \ _)" diff -r 0be08e4cd0ec -r 5cb5e7ecb284 src/HOL/Number_Theory/Euclidean_Division.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Number_Theory/Euclidean_Division.thy Wed Jan 04 21:28:28 2017 +0100 @@ -0,0 +1,295 @@ +(* Title: HOL/Number_Theory/Euclidean_Division.thy + Author: Manuel Eberl, TU Muenchen + Author: Florian Haftmann, TU Muenchen +*) + +section \Division with remainder in euclidean (semi)rings\ + +theory Euclidean_Division + imports Main +begin + +subsection \Euclidean (semi)rings with explicit division and remainder\ + +class euclidean_semiring = semidom_modulo + normalization_semidom + + fixes euclidean_size :: "'a \ nat" + assumes size_0 [simp]: "euclidean_size 0 = 0" + assumes mod_size_less: + "b \ 0 \ euclidean_size (a mod b) < euclidean_size b" + assumes size_mult_mono: + "b \ 0 \ euclidean_size a \ euclidean_size (a * b)" +begin + +lemma size_mult_mono': "b \ 0 \ euclidean_size a \ euclidean_size (b * a)" + by (subst mult.commute) (rule size_mult_mono) + +lemma euclidean_size_normalize [simp]: + "euclidean_size (normalize a) = euclidean_size a" +proof (cases "a = 0") + case True + then show ?thesis + by simp +next + case [simp]: False + have "euclidean_size (normalize a) \ euclidean_size (normalize a * unit_factor a)" + by (rule size_mult_mono) simp + moreover have "euclidean_size a \ euclidean_size (a * (1 div unit_factor a))" + by (rule size_mult_mono) simp + ultimately show ?thesis + by simp +qed + +lemma dvd_euclidean_size_eq_imp_dvd: + assumes "a \ 0" and "euclidean_size a = euclidean_size b" + and "b dvd a" + shows "a dvd b" +proof (rule ccontr) + assume "\ a dvd b" + hence "b mod a \ 0" using mod_0_imp_dvd [of b a] by blast + then have "b mod a \ 0" by (simp add: mod_eq_0_iff_dvd) + from \b dvd a\ have "b dvd b mod a" by (simp add: dvd_mod_iff) + then obtain c where "b mod a = b * c" unfolding dvd_def by blast + with \b mod a \ 0\ have "c \ 0" by auto + with \b mod a = b * c\ have "euclidean_size (b mod a) \ euclidean_size b" + using size_mult_mono by force + moreover from \\ a dvd b\ and \a \ 0\ + have "euclidean_size (b mod a) < euclidean_size a" + using mod_size_less by blast + ultimately show False using \euclidean_size a = euclidean_size b\ + by simp +qed + +lemma euclidean_size_times_unit: + assumes "is_unit a" + shows "euclidean_size (a * b) = euclidean_size b" +proof (rule antisym) + from assms have [simp]: "a \ 0" by auto + thus "euclidean_size (a * b) \ euclidean_size b" by (rule size_mult_mono') + from assms have "is_unit (1 div a)" by simp + hence "1 div a \ 0" by (intro notI) simp_all + hence "euclidean_size (a * b) \ euclidean_size ((1 div a) * (a * b))" + by (rule size_mult_mono') + also from assms have "(1 div a) * (a * b) = b" + by (simp add: algebra_simps unit_div_mult_swap) + finally show "euclidean_size (a * b) \ euclidean_size b" . +qed + +lemma euclidean_size_unit: + "is_unit a \ euclidean_size a = euclidean_size 1" + using euclidean_size_times_unit [of a 1] by simp + +lemma unit_iff_euclidean_size: + "is_unit a \ euclidean_size a = euclidean_size 1 \ a \ 0" +proof safe + assume A: "a \ 0" and B: "euclidean_size a = euclidean_size 1" + show "is_unit a" + by (rule dvd_euclidean_size_eq_imp_dvd [OF A B]) simp_all +qed (auto intro: euclidean_size_unit) + +lemma euclidean_size_times_nonunit: + assumes "a \ 0" "b \ 0" "\ is_unit a" + shows "euclidean_size b < euclidean_size (a * b)" +proof (rule ccontr) + assume "\euclidean_size b < euclidean_size (a * b)" + with size_mult_mono'[OF assms(1), of b] + have eq: "euclidean_size (a * b) = euclidean_size b" by simp + have "a * b dvd b" + by (rule dvd_euclidean_size_eq_imp_dvd [OF _ eq]) (insert assms, simp_all) + hence "a * b dvd 1 * b" by simp + with \b \ 0\ have "is_unit a" by (subst (asm) dvd_times_right_cancel_iff) + with assms(3) show False by contradiction +qed + +lemma dvd_imp_size_le: + assumes "a dvd b" "b \ 0" + shows "euclidean_size a \ euclidean_size b" + using assms by (auto elim!: dvdE simp: size_mult_mono) + +lemma dvd_proper_imp_size_less: + assumes "a dvd b" "\ b dvd a" "b \ 0" + shows "euclidean_size a < euclidean_size b" +proof - + from assms(1) obtain c where "b = a * c" by (erule dvdE) + hence z: "b = c * a" by (simp add: mult.commute) + from z assms have "\is_unit c" by (auto simp: mult.commute mult_unit_dvd_iff) + with z assms show ?thesis + by (auto intro!: euclidean_size_times_nonunit) +qed + +end + +class euclidean_ring = idom_modulo + euclidean_semiring + + +subsection \Euclidean (semi)rings with cancel rules\ + +class euclidean_semiring_cancel = euclidean_semiring + semiring_div + +class euclidean_ring_cancel = euclidean_ring + ring_div + + +subsection \Uniquely determined division\ + +class unique_euclidean_semiring = euclidean_semiring + + fixes uniqueness_constraint :: "'a \ 'a \ bool" + assumes size_mono_mult: + "b \ 0 \ euclidean_size a < euclidean_size c + \ euclidean_size (a * b) < euclidean_size (c * b)" + -- \FIXME justify\ + assumes uniqueness_constraint_mono_mult: + "uniqueness_constraint a b \ uniqueness_constraint (a * c) (b * c)" + assumes uniqueness_constraint_mod: + "b \ 0 \ \ b dvd a \ uniqueness_constraint (a mod b) b" + assumes div_bounded: + "b \ 0 \ uniqueness_constraint r b + \ euclidean_size r < euclidean_size b + \ (q * b + r) div b = q" +begin + +lemma divmod_cases [case_names divides remainder by0]: + obtains + (divides) q where "b \ 0" + and "a div b = q" + and "a mod b = 0" + and "a = q * b" + | (remainder) q r where "b \ 0" and "r \ 0" + and "uniqueness_constraint r b" + and "euclidean_size r < euclidean_size b" + and "a div b = q" + and "a mod b = r" + and "a = q * b + r" + | (by0) "b = 0" +proof (cases "b = 0") + case True + then show thesis + by (rule by0) +next + case False + show thesis + proof (cases "b dvd a") + case True + then obtain q where "a = b * q" .. + with \b \ 0\ divides + show thesis + by (simp add: ac_simps) + next + case False + then have "a mod b \ 0" + by (simp add: mod_eq_0_iff_dvd) + moreover from \b \ 0\ \\ b dvd a\ have "uniqueness_constraint (a mod b) b" + by (rule uniqueness_constraint_mod) + moreover have "euclidean_size (a mod b) < euclidean_size b" + using \b \ 0\ by (rule mod_size_less) + moreover have "a = a div b * b + a mod b" + by (simp add: div_mult_mod_eq) + ultimately show thesis + using \b \ 0\ by (blast intro: remainder) + qed +qed + +lemma div_eqI: + "a div b = q" if "b \ 0" "uniqueness_constraint r b" + "euclidean_size r < euclidean_size b" "q * b + r = a" +proof - + from that have "(q * b + r) div b = q" + by (auto intro: div_bounded) + with that show ?thesis + by simp +qed + +lemma mod_eqI: + "a mod b = r" if "b \ 0" "uniqueness_constraint r b" + "euclidean_size r < euclidean_size b" "q * b + r = a" +proof - + from that have "a div b = q" + by (rule div_eqI) + moreover have "a div b * b + a mod b = a" + by (fact div_mult_mod_eq) + ultimately have "a div b * b + a mod b = a div b * b + r" + using \q * b + r = a\ by simp + then show ?thesis + by simp +qed + +subclass euclidean_semiring_cancel +proof + show "(a + c * b) div b = c + a div b" if "b \ 0" for a b c + proof (cases a b rule: divmod_cases) + case by0 + with \b \ 0\ show ?thesis + by simp + next + case (divides q) + then show ?thesis + by (simp add: ac_simps) + next + case (remainder q r) + then show ?thesis + by (auto intro: div_eqI simp add: algebra_simps) + qed +next + show"(c * a) div (c * b) = a div b" if "c \ 0" for a b c + proof (cases a b rule: divmod_cases) + case by0 + then show ?thesis + by simp + next + case (divides q) + with \c \ 0\ show ?thesis + by (simp add: mult.left_commute [of c]) + next + case (remainder q r) + from \b \ 0\ \c \ 0\ have "b * c \ 0" + by simp + from remainder \c \ 0\ + have "uniqueness_constraint (r * c) (b * c)" + and "euclidean_size (r * c) < euclidean_size (b * c)" + by (simp_all add: uniqueness_constraint_mono_mult uniqueness_constraint_mod size_mono_mult) + with remainder show ?thesis + by (auto intro!: div_eqI [of _ "c * (a mod b)"] simp add: algebra_simps) + (use \b * c \ 0\ in simp) + qed +qed + +end + +class unique_euclidean_ring = euclidean_ring + unique_euclidean_semiring +begin + +subclass euclidean_ring_cancel .. + +end + +subsection \Typical instances\ + +instantiation nat :: unique_euclidean_semiring +begin + +definition [simp]: + "euclidean_size_nat = (id :: nat \ nat)" + +definition [simp]: + "uniqueness_constraint_nat = (top :: nat \ nat \ bool)" + +instance + by standard + (simp_all add: unit_factor_nat_def mod_greater_zero_iff_not_dvd) + +end + +instantiation int :: unique_euclidean_ring +begin + +definition [simp]: + "euclidean_size_int = (nat \ abs :: int \ nat)" + +definition [simp]: + "uniqueness_constraint_int (k :: int) l \ unit_factor k = unit_factor l" + +instance + by standard + (auto simp add: abs_mult nat_mult_distrib sgn_mod zdiv_eq_0_iff sgn_1_pos sgn_mult split: abs_split) + +end + +end