# HG changeset patch # User haftmann # Date 1476297527 -7200 # Node ID 38c40744640038e9f3da31e152daa499494cd322 # Parent 62c9e5c05928c14e0db40ae683866b4a846d28af separate type class for arbitrary quotient and remainder partitions diff -r 62c9e5c05928 -r 38c407446400 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Tue Oct 11 16:44:13 2016 +0200 +++ b/src/HOL/Divides.thy Wed Oct 12 20:38:47 2016 +0200 @@ -11,9 +11,8 @@ subsection \Abstract division in commutative semirings.\ -class semiring_div = semidom + modulo + - assumes mod_div_equality: "a div b * b + a mod b = a" - and div_by_0: "a div 0 = 0" +class semiring_div = semidom + semiring_modulo + + assumes div_by_0: "a div 0 = 0" and div_0: "0 div a = 0" and div_mult_self1 [simp]: "b \ 0 \ (a + c * b) div b = c + a div b" and div_mult_mult1 [simp]: "c \ 0 \ (c * a) div (c * b) = a div b" @@ -41,14 +40,6 @@ text \@{const divide} and @{const modulo}\ -lemma mod_div_equality2: "b * (a div b) + a mod b = a" - unfolding mult.commute [of b] - by (rule mod_div_equality) - -lemma mod_div_equality': "a mod b + a div b * b = a" - using mod_div_equality [of a b] - by (simp only: ac_simps) - lemma div_mod_equality: "((a div b) * b + a mod b) + c = a + c" by (simp add: mod_div_equality) @@ -143,17 +134,6 @@ "(a + b) mod b = a mod b" using mod_mult_self1 [of a 1 b] by simp -lemma mod_div_decomp: - fixes a b - obtains q r where "q = a div b" and "r = a mod b" - and "a = q * b + r" -proof - - from mod_div_equality have "a = a div b * b + a mod b" by simp - moreover have "a div b = a div b" .. - moreover have "a mod b = a mod b" .. - note that ultimately show thesis by blast -qed - lemma dvd_imp_mod_0 [simp]: assumes "a dvd b" shows "b mod a = 0" @@ -189,7 +169,7 @@ hence "a div b + a mod b div b = (a mod b + a div b * b) div b" by (rule div_mult_self1 [symmetric]) also have "\ = a div b" - by (simp only: mod_div_equality') + by (simp only: mod_div_equality3) also have "\ = a div b + 0" by simp finally show ?thesis @@ -202,7 +182,7 @@ have "a mod b mod b = (a mod b + a div b * b) mod b" by (simp only: mod_mult_self1) also have "\ = a mod b" - by (simp only: mod_div_equality') + by (simp only: mod_div_equality3) finally show ?thesis . qed diff -r 62c9e5c05928 -r 38c407446400 src/HOL/Library/Polynomial_Factorial.thy --- a/src/HOL/Library/Polynomial_Factorial.thy Tue Oct 11 16:44:13 2016 +0200 +++ b/src/HOL/Library/Polynomial_Factorial.thy Wed Oct 12 20:38:47 2016 +0200 @@ -1018,8 +1018,12 @@ by (intro ext) (simp_all add: dvd.dvd_def dvd_def) interpretation field_poly: - euclidean_ring "op div" "op *" "op mod" "op +" "op -" 0 "1 :: 'a :: field poly" - normalize_field_poly unit_factor_field_poly euclidean_size_field_poly uminus + 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 divide = divide and modulo = modulo proof (standard, unfold dvd_field_poly) fix p :: "'a poly" show "unit_factor_field_poly p * normalize_field_poly p = p" @@ -1034,7 +1038,7 @@ thus "is_unit (unit_factor_field_poly p)" by (simp add: unit_factor_field_poly_def lead_coeff_nonzero is_unit_pCons_iff) qed (auto simp: unit_factor_field_poly_def normalize_field_poly_def lead_coeff_mult - euclidean_size_field_poly_def intro!: degree_mod_less' degree_mult_right_le) + euclidean_size_field_poly_def Rings.mod_div_equality intro!: degree_mod_less' degree_mult_right_le) lemma field_poly_irreducible_imp_prime: assumes "irreducible (p :: 'a :: field poly)" @@ -1352,7 +1356,7 @@ "euclidean_size_poly p = (if p = 0 then 0 else 2 ^ degree p)" instance - by standard (auto simp: euclidean_size_poly_def intro!: degree_mod_less' degree_mult_right_le) + by standard (auto simp: euclidean_size_poly_def Rings.mod_div_equality intro!: degree_mod_less' degree_mult_right_le) end @@ -1423,7 +1427,7 @@ by auto termination by (relation "measure ((\p. if p = 0 then 0 else Suc (degree p)) \ snd)") - (auto simp: degree_primitive_part degree_pseudo_mod_less) + (auto simp: degree_pseudo_mod_less) declare gcd_poly_code_aux.simps [simp del] diff -r 62c9e5c05928 -r 38c407446400 src/HOL/Number_Theory/Euclidean_Algorithm.thy --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Tue Oct 11 16:44:13 2016 +0200 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Wed Oct 12 20:38:47 2016 +0200 @@ -6,39 +6,6 @@ imports "~~/src/HOL/GCD" Factorial_Ring begin -class divide_modulo = semidom_divide + modulo + - assumes div_mod_equality: "((a div b) * b + a mod b) + c = a + c" -begin - -lemma zero_mod_left [simp]: "0 mod a = 0" - using div_mod_equality[of 0 a 0] by simp - -lemma dvd_mod_iff [simp]: - assumes "k dvd n" - shows "(k dvd m mod n) = (k dvd m)" -proof - - thm div_mod_equality - from assms have "(k dvd m mod n) \ (k dvd ((m div n) * n + m mod n))" - by (simp add: dvd_add_right_iff) - also have "(m div n) * n + m mod n = m" - using div_mod_equality[of m n 0] by simp - finally show ?thesis . -qed - -lemma mod_0_imp_dvd: - assumes "a mod b = 0" - shows "b dvd a" -proof - - have "b dvd ((a div b) * b)" by simp - also have "(a div b) * b = a" - using div_mod_equality[of a b 0] by (simp add: assms) - finally show ?thesis . -qed - -end - - - text \ A Euclidean semiring is a semiring upon which the Euclidean algorithm can be implemented. It must provide: @@ -50,7 +17,7 @@ The existence of these functions makes it possible to derive gcd and lcm functions for any Euclidean semiring. \ -class euclidean_semiring = divide_modulo + normalization_semidom + +class euclidean_semiring = semiring_modulo + normalization_semidom + fixes euclidean_size :: "'a \ nat" assumes size_0 [simp]: "euclidean_size 0 = 0" assumes mod_size_less: @@ -59,6 +26,30 @@ "b \ 0 \ euclidean_size a \ euclidean_size (a * b)" begin +lemma zero_mod_left [simp]: "0 mod a = 0" + using mod_div_equality [of 0 a] by simp + +lemma dvd_mod_iff: + assumes "k dvd n" + shows "(k dvd m mod n) = (k dvd m)" +proof - + from assms have "(k dvd m mod n) \ (k dvd ((m div n) * n + m mod n))" + by (simp add: dvd_add_right_iff) + also have "(m div n) * n + m mod n = m" + using mod_div_equality [of m n] by simp + finally show ?thesis . +qed + +lemma mod_0_imp_dvd: + assumes "a mod b = 0" + shows "b dvd a" +proof - + have "b dvd ((a div b) * b)" by simp + also have "(a div b) * b = a" + using mod_div_equality [of a b] by (simp add: assms) + finally show ?thesis . +qed + lemma euclidean_size_normalize [simp]: "euclidean_size (normalize a) = euclidean_size a" proof (cases "a = 0") @@ -81,36 +72,11 @@ obtains s and t where "a = s * b + t" and "euclidean_size t < euclidean_size b" proof - - from div_mod_equality [of a b 0] + from mod_div_equality [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 zero_mod_left [simp]: "0 mod a = 0" - using div_mod_equality[of 0 a 0] by simp - -lemma dvd_mod_iff [simp]: - assumes "k dvd n" - shows "(k dvd m mod n) = (k dvd m)" -proof - - thm div_mod_equality - from assms have "(k dvd m mod n) \ (k dvd ((m div n) * n + m mod n))" - by (simp add: dvd_add_right_iff) - also have "(m div n) * n + m mod n = m" - using div_mod_equality[of m n 0] by simp - finally show ?thesis . -qed - -lemma mod_0_imp_dvd: - assumes "a mod b = 0" - shows "b dvd a" -proof - - have "b dvd ((a div b) * b)" by simp - also have "(a div b) * b = a" - using div_mod_equality[of a b 0] by (simp add: assms) - finally show ?thesis . -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" @@ -118,7 +84,7 @@ 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 + 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" @@ -541,7 +507,7 @@ (s' * x + t' * y) - r' div r * (s * x + t * y)" by (simp add: algebra_simps) also have "s' * x + t' * y = r'" by fact also have "s * x + t * y = r" by fact - also have "r' - r' div r * r = r' mod r" using div_mod_equality[of r' r] + also have "r' - r' div r * r = r' mod r" using mod_div_equality [of r' r] by (simp add: algebra_simps) finally show "(s' - r' div r * s) * x + (t' - r' div r * t) * y = r' mod r" . qed (auto simp: gcd_eucl_non_0 algebra_simps div_mod_equality') diff -r 62c9e5c05928 -r 38c407446400 src/HOL/Rings.thy --- a/src/HOL/Rings.thy Tue Oct 11 16:44:13 2016 +0200 +++ b/src/HOL/Rings.thy Wed Oct 12 20:38:47 2016 +0200 @@ -571,11 +571,6 @@ setup \Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::divide \ 'a \ 'a"})\ -text \Syntactic division remainder operator\ - -class modulo = dvd + divide + - fixes modulo :: "'a \ 'a \ 'a" (infixl "mod" 70) - text \Algebraic classes with division\ class semidom_divide = semidom + divide + @@ -1286,6 +1281,53 @@ end + +text \Syntactic division remainder operator\ + +class modulo = dvd + divide + + fixes modulo :: "'a \ 'a \ 'a" (infixl "mod" 70) + +text \Arbitrary quotient and remainder partitions\ + +class semiring_modulo = comm_semiring_1_cancel + divide + modulo + + assumes mod_div_equality: "a div b * b + a mod b = a" +begin + +lemma mod_div_decomp: + fixes a b + obtains q r where "q = a div b" and "r = a mod b" + and "a = q * b + r" +proof - + from mod_div_equality have "a = a div b * b + a mod b" by simp + moreover have "a div b = a div b" .. + moreover have "a mod b = a mod b" .. + note that ultimately show thesis by blast +qed + +lemma mod_div_equality2: "b * (a div b) + a mod b = a" + using mod_div_equality [of a b] by (simp add: ac_simps) + +lemma mod_div_equality3: "a mod b + a div b * b = a" + using mod_div_equality [of a b] by (simp add: ac_simps) + +lemma mod_div_equality4: "a mod b + b * (a div b) = a" + using mod_div_equality [of a b] by (simp add: ac_simps) + +lemma minus_div_eq_mod: "a - a div b * b = a mod b" + by (rule add_implies_diff [symmetric]) (fact mod_div_equality3) + +lemma minus_div_eq_mod2: "a - b * (a div b) = a mod b" + by (rule add_implies_diff [symmetric]) (fact mod_div_equality4) + +lemma minus_mod_eq_div: "a - a mod b = a div b * b" + by (rule add_implies_diff [symmetric]) (fact mod_div_equality) + +lemma minus_mod_eq_div2: "a - a mod b = b * (a div b)" + by (rule add_implies_diff [symmetric]) (fact mod_div_equality2) + +end + + class ordered_semiring = semiring + ordered_comm_monoid_add + assumes mult_left_mono: "a \ b \ 0 \ c \ c * a \ c * b" assumes mult_right_mono: "a \ b \ 0 \ c \ a * c \ b * c"