# HG changeset patch # User wenzelm # Date 1476302766 -7200 # Node ID 54479f7b668552b1bc4be11e5dfc5b89d2f2814b # Parent 38c40744640038e9f3da31e152daa499494cd322# Parent 85ff21510ba9e788451154e24d0e152e6b56b4bc merged diff -r 85ff21510ba9 -r 54479f7b6685 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Wed Oct 12 21:53:30 2016 +0200 +++ b/src/HOL/Divides.thy Wed Oct 12 22:06:06 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 85ff21510ba9 -r 54479f7b6685 src/HOL/Library/Polynomial_Factorial.thy --- a/src/HOL/Library/Polynomial_Factorial.thy Wed Oct 12 21:53:30 2016 +0200 +++ b/src/HOL/Library/Polynomial_Factorial.thy Wed Oct 12 22:06:06 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 85ff21510ba9 -r 54479f7b6685 src/HOL/Number_Theory/Euclidean_Algorithm.thy --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Wed Oct 12 21:53:30 2016 +0200 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Wed Oct 12 22:06:06 2016 +0200 @@ -17,7 +17,7 @@ The existence of these functions makes it possible to derive gcd and lcm functions for any Euclidean semiring. \ -class euclidean_semiring = semiring_div + 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: @@ -26,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") @@ -48,7 +72,7 @@ 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 @@ -58,6 +82,7 @@ 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 @@ -434,8 +459,6 @@ class euclidean_ring = euclidean_semiring + idom begin -subclass ring_div .. - function euclid_ext_aux :: "'a \ _" where "euclid_ext_aux r' r s' s t' t = ( if r = 0 then let c = 1 div unit_factor r' in (s' * c, t' * c, normalize r') @@ -484,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 mod_div_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 85ff21510ba9 -r 54479f7b6685 src/HOL/Rings.thy --- a/src/HOL/Rings.thy Wed Oct 12 21:53:30 2016 +0200 +++ b/src/HOL/Rings.thy Wed Oct 12 22:06:06 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"