separate type class for arbitrary quotient and remainder partitions
authorhaftmann
Wed Oct 12 20:38:47 2016 +0200 (2016-10-12)
changeset 6416438c407446400
parent 64163 62c9e5c05928
child 64174 54479f7b6685
separate type class for arbitrary quotient and remainder partitions
src/HOL/Divides.thy
src/HOL/Library/Polynomial_Factorial.thy
src/HOL/Number_Theory/Euclidean_Algorithm.thy
src/HOL/Rings.thy
     1.1 --- a/src/HOL/Divides.thy	Tue Oct 11 16:44:13 2016 +0200
     1.2 +++ b/src/HOL/Divides.thy	Wed Oct 12 20:38:47 2016 +0200
     1.3 @@ -11,9 +11,8 @@
     1.4  
     1.5  subsection \<open>Abstract division in commutative semirings.\<close>
     1.6  
     1.7 -class semiring_div = semidom + modulo +
     1.8 -  assumes mod_div_equality: "a div b * b + a mod b = a"
     1.9 -    and div_by_0: "a div 0 = 0"
    1.10 +class semiring_div = semidom + semiring_modulo +
    1.11 +  assumes div_by_0: "a div 0 = 0"
    1.12      and div_0: "0 div a = 0"
    1.13      and div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
    1.14      and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
    1.15 @@ -41,14 +40,6 @@
    1.16  
    1.17  text \<open>@{const divide} and @{const modulo}\<close>
    1.18  
    1.19 -lemma mod_div_equality2: "b * (a div b) + a mod b = a"
    1.20 -  unfolding mult.commute [of b]
    1.21 -  by (rule mod_div_equality)
    1.22 -
    1.23 -lemma mod_div_equality': "a mod b + a div b * b = a"
    1.24 -  using mod_div_equality [of a b]
    1.25 -  by (simp only: ac_simps)
    1.26 -
    1.27  lemma div_mod_equality: "((a div b) * b + a mod b) + c = a + c"
    1.28    by (simp add: mod_div_equality)
    1.29  
    1.30 @@ -143,17 +134,6 @@
    1.31    "(a + b) mod b = a mod b"
    1.32    using mod_mult_self1 [of a 1 b] by simp
    1.33  
    1.34 -lemma mod_div_decomp:
    1.35 -  fixes a b
    1.36 -  obtains q r where "q = a div b" and "r = a mod b"
    1.37 -    and "a = q * b + r"
    1.38 -proof -
    1.39 -  from mod_div_equality have "a = a div b * b + a mod b" by simp
    1.40 -  moreover have "a div b = a div b" ..
    1.41 -  moreover have "a mod b = a mod b" ..
    1.42 -  note that ultimately show thesis by blast
    1.43 -qed
    1.44 -
    1.45  lemma dvd_imp_mod_0 [simp]:
    1.46    assumes "a dvd b"
    1.47    shows "b mod a = 0"
    1.48 @@ -189,7 +169,7 @@
    1.49    hence "a div b + a mod b div b = (a mod b + a div b * b) div b"
    1.50      by (rule div_mult_self1 [symmetric])
    1.51    also have "\<dots> = a div b"
    1.52 -    by (simp only: mod_div_equality')
    1.53 +    by (simp only: mod_div_equality3)
    1.54    also have "\<dots> = a div b + 0"
    1.55      by simp
    1.56    finally show ?thesis
    1.57 @@ -202,7 +182,7 @@
    1.58    have "a mod b mod b = (a mod b + a div b * b) mod b"
    1.59      by (simp only: mod_mult_self1)
    1.60    also have "\<dots> = a mod b"
    1.61 -    by (simp only: mod_div_equality')
    1.62 +    by (simp only: mod_div_equality3)
    1.63    finally show ?thesis .
    1.64  qed
    1.65  
     2.1 --- a/src/HOL/Library/Polynomial_Factorial.thy	Tue Oct 11 16:44:13 2016 +0200
     2.2 +++ b/src/HOL/Library/Polynomial_Factorial.thy	Wed Oct 12 20:38:47 2016 +0200
     2.3 @@ -1018,8 +1018,12 @@
     2.4      by (intro ext) (simp_all add: dvd.dvd_def dvd_def)
     2.5  
     2.6  interpretation field_poly: 
     2.7 -  euclidean_ring "op div" "op *" "op mod" "op +" "op -" 0 "1 :: 'a :: field poly" 
     2.8 -    normalize_field_poly unit_factor_field_poly euclidean_size_field_poly uminus
     2.9 +  euclidean_ring where zero = "0 :: 'a :: field poly"
    2.10 +    and one = 1 and plus = plus and uminus = uminus and minus = minus
    2.11 +    and times = times
    2.12 +    and normalize = normalize_field_poly and unit_factor = unit_factor_field_poly
    2.13 +    and euclidean_size = euclidean_size_field_poly
    2.14 +    and divide = divide and modulo = modulo
    2.15  proof (standard, unfold dvd_field_poly)
    2.16    fix p :: "'a poly"
    2.17    show "unit_factor_field_poly p * normalize_field_poly p = p"
    2.18 @@ -1034,7 +1038,7 @@
    2.19    thus "is_unit (unit_factor_field_poly p)"
    2.20      by (simp add: unit_factor_field_poly_def lead_coeff_nonzero is_unit_pCons_iff)
    2.21  qed (auto simp: unit_factor_field_poly_def normalize_field_poly_def lead_coeff_mult 
    2.22 -       euclidean_size_field_poly_def intro!: degree_mod_less' degree_mult_right_le)
    2.23 +       euclidean_size_field_poly_def Rings.mod_div_equality intro!: degree_mod_less' degree_mult_right_le)
    2.24  
    2.25  lemma field_poly_irreducible_imp_prime:
    2.26    assumes "irreducible (p :: 'a :: field poly)"
    2.27 @@ -1352,7 +1356,7 @@
    2.28    "euclidean_size_poly p = (if p = 0 then 0 else 2 ^ degree p)"
    2.29  
    2.30  instance 
    2.31 -  by standard (auto simp: euclidean_size_poly_def intro!: degree_mod_less' degree_mult_right_le)
    2.32 +  by standard (auto simp: euclidean_size_poly_def Rings.mod_div_equality intro!: degree_mod_less' degree_mult_right_le)
    2.33  end
    2.34  
    2.35  
    2.36 @@ -1423,7 +1427,7 @@
    2.37  by auto
    2.38  termination
    2.39    by (relation "measure ((\<lambda>p. if p = 0 then 0 else Suc (degree p)) \<circ> snd)")
    2.40 -     (auto simp: degree_primitive_part degree_pseudo_mod_less)
    2.41 +     (auto simp: degree_pseudo_mod_less)
    2.42  
    2.43  declare gcd_poly_code_aux.simps [simp del]
    2.44  
     3.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Tue Oct 11 16:44:13 2016 +0200
     3.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Oct 12 20:38:47 2016 +0200
     3.3 @@ -6,39 +6,6 @@
     3.4  imports "~~/src/HOL/GCD" Factorial_Ring
     3.5  begin
     3.6  
     3.7 -class divide_modulo = semidom_divide + modulo +
     3.8 -  assumes div_mod_equality: "((a div b) * b + a mod b) + c = a + c"
     3.9 -begin
    3.10 -
    3.11 -lemma zero_mod_left [simp]: "0 mod a = 0"
    3.12 -  using div_mod_equality[of 0 a 0] by simp
    3.13 -
    3.14 -lemma dvd_mod_iff [simp]: 
    3.15 -  assumes "k dvd n"
    3.16 -  shows   "(k dvd m mod n) = (k dvd m)"
    3.17 -proof -
    3.18 -  thm div_mod_equality
    3.19 -  from assms have "(k dvd m mod n) \<longleftrightarrow> (k dvd ((m div n) * n + m mod n))" 
    3.20 -    by (simp add: dvd_add_right_iff)
    3.21 -  also have "(m div n) * n + m mod n = m"
    3.22 -    using div_mod_equality[of m n 0] by simp
    3.23 -  finally show ?thesis .
    3.24 -qed
    3.25 -
    3.26 -lemma mod_0_imp_dvd: 
    3.27 -  assumes "a mod b = 0"
    3.28 -  shows   "b dvd a"
    3.29 -proof -
    3.30 -  have "b dvd ((a div b) * b)" by simp
    3.31 -  also have "(a div b) * b = a"
    3.32 -    using div_mod_equality[of a b 0] by (simp add: assms)
    3.33 -  finally show ?thesis .
    3.34 -qed
    3.35 -
    3.36 -end
    3.37 -
    3.38 -
    3.39 -
    3.40  text \<open>
    3.41    A Euclidean semiring is a semiring upon which the Euclidean algorithm can be
    3.42    implemented. It must provide:
    3.43 @@ -50,7 +17,7 @@
    3.44    The existence of these functions makes it possible to derive gcd and lcm functions 
    3.45    for any Euclidean semiring.
    3.46  \<close> 
    3.47 -class euclidean_semiring = divide_modulo + normalization_semidom + 
    3.48 +class euclidean_semiring = semiring_modulo + normalization_semidom + 
    3.49    fixes euclidean_size :: "'a \<Rightarrow> nat"
    3.50    assumes size_0 [simp]: "euclidean_size 0 = 0"
    3.51    assumes mod_size_less: 
    3.52 @@ -59,6 +26,30 @@
    3.53      "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)"
    3.54  begin
    3.55  
    3.56 +lemma zero_mod_left [simp]: "0 mod a = 0"
    3.57 +  using mod_div_equality [of 0 a] by simp
    3.58 +
    3.59 +lemma dvd_mod_iff: 
    3.60 +  assumes "k dvd n"
    3.61 +  shows   "(k dvd m mod n) = (k dvd m)"
    3.62 +proof -
    3.63 +  from assms have "(k dvd m mod n) \<longleftrightarrow> (k dvd ((m div n) * n + m mod n))" 
    3.64 +    by (simp add: dvd_add_right_iff)
    3.65 +  also have "(m div n) * n + m mod n = m"
    3.66 +    using mod_div_equality [of m n] by simp
    3.67 +  finally show ?thesis .
    3.68 +qed
    3.69 +
    3.70 +lemma mod_0_imp_dvd: 
    3.71 +  assumes "a mod b = 0"
    3.72 +  shows   "b dvd a"
    3.73 +proof -
    3.74 +  have "b dvd ((a div b) * b)" by simp
    3.75 +  also have "(a div b) * b = a"
    3.76 +    using mod_div_equality [of a b] by (simp add: assms)
    3.77 +  finally show ?thesis .
    3.78 +qed
    3.79 +
    3.80  lemma euclidean_size_normalize [simp]:
    3.81    "euclidean_size (normalize a) = euclidean_size a"
    3.82  proof (cases "a = 0")
    3.83 @@ -81,36 +72,11 @@
    3.84    obtains s and t where "a = s * b + t" 
    3.85      and "euclidean_size t < euclidean_size b"
    3.86  proof -
    3.87 -  from div_mod_equality [of a b 0] 
    3.88 +  from mod_div_equality [of a b] 
    3.89       have "a = a div b * b + a mod b" by simp
    3.90    with that and assms show ?thesis by (auto simp add: mod_size_less)
    3.91  qed
    3.92  
    3.93 -lemma zero_mod_left [simp]: "0 mod a = 0"
    3.94 -  using div_mod_equality[of 0 a 0] by simp
    3.95 -
    3.96 -lemma dvd_mod_iff [simp]: 
    3.97 -  assumes "k dvd n"
    3.98 -  shows   "(k dvd m mod n) = (k dvd m)"
    3.99 -proof -
   3.100 -  thm div_mod_equality
   3.101 -  from assms have "(k dvd m mod n) \<longleftrightarrow> (k dvd ((m div n) * n + m mod n))" 
   3.102 -    by (simp add: dvd_add_right_iff)
   3.103 -  also have "(m div n) * n + m mod n = m"
   3.104 -    using div_mod_equality[of m n 0] by simp
   3.105 -  finally show ?thesis .
   3.106 -qed
   3.107 -
   3.108 -lemma mod_0_imp_dvd: 
   3.109 -  assumes "a mod b = 0"
   3.110 -  shows   "b dvd a"
   3.111 -proof -
   3.112 -  have "b dvd ((a div b) * b)" by simp
   3.113 -  also have "(a div b) * b = a"
   3.114 -    using div_mod_equality[of a b 0] by (simp add: assms)
   3.115 -  finally show ?thesis .
   3.116 -qed
   3.117 -
   3.118  lemma dvd_euclidean_size_eq_imp_dvd:
   3.119    assumes "a \<noteq> 0" and b_dvd_a: "b dvd a" and size_eq: "euclidean_size a = euclidean_size b"
   3.120    shows "a dvd b"
   3.121 @@ -118,7 +84,7 @@
   3.122    assume "\<not> a dvd b"
   3.123    hence "b mod a \<noteq> 0" using mod_0_imp_dvd[of b a] by blast
   3.124    then have "b mod a \<noteq> 0" by (simp add: mod_eq_0_iff_dvd)
   3.125 -  from b_dvd_a have b_dvd_mod: "b dvd b mod a" by simp
   3.126 +  from b_dvd_a have b_dvd_mod: "b dvd b mod a" by (simp add: dvd_mod_iff)
   3.127    from b_dvd_mod obtain c where "b mod a = b * c" unfolding dvd_def by blast
   3.128      with \<open>b mod a \<noteq> 0\<close> have "c \<noteq> 0" by auto
   3.129    with \<open>b mod a = b * c\<close> have "euclidean_size (b mod a) \<ge> euclidean_size b"
   3.130 @@ -541,7 +507,7 @@
   3.131                (s' * x + t' * y) - r' div r * (s * x + t * y)" by (simp add: algebra_simps)
   3.132        also have "s' * x + t' * y = r'" by fact
   3.133        also have "s * x + t * y = r" by fact
   3.134 -      also have "r' - r' div r * r = r' mod r" using div_mod_equality[of r' r]
   3.135 +      also have "r' - r' div r * r = r' mod r" using mod_div_equality [of r' r]
   3.136          by (simp add: algebra_simps)
   3.137        finally show "(s' - r' div r * s) * x + (t' - r' div r * t) * y = r' mod r" .
   3.138      qed (auto simp: gcd_eucl_non_0 algebra_simps div_mod_equality')
     4.1 --- a/src/HOL/Rings.thy	Tue Oct 11 16:44:13 2016 +0200
     4.2 +++ b/src/HOL/Rings.thy	Wed Oct 12 20:38:47 2016 +0200
     4.3 @@ -571,11 +571,6 @@
     4.4  
     4.5  setup \<open>Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::divide \<Rightarrow> 'a \<Rightarrow> 'a"})\<close>
     4.6  
     4.7 -text \<open>Syntactic division remainder operator\<close>
     4.8 -
     4.9 -class modulo = dvd + divide +
    4.10 -  fixes modulo :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "mod" 70)
    4.11 -
    4.12  text \<open>Algebraic classes with division\<close>
    4.13    
    4.14  class semidom_divide = semidom + divide +
    4.15 @@ -1286,6 +1281,53 @@
    4.16  
    4.17  end
    4.18  
    4.19 +
    4.20 +text \<open>Syntactic division remainder operator\<close>
    4.21 +
    4.22 +class modulo = dvd + divide +
    4.23 +  fixes modulo :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "mod" 70)
    4.24 +
    4.25 +text \<open>Arbitrary quotient and remainder partitions\<close>
    4.26 +
    4.27 +class semiring_modulo = comm_semiring_1_cancel + divide + modulo +
    4.28 +  assumes mod_div_equality: "a div b * b + a mod b = a"
    4.29 +begin
    4.30 +
    4.31 +lemma mod_div_decomp:
    4.32 +  fixes a b
    4.33 +  obtains q r where "q = a div b" and "r = a mod b"
    4.34 +    and "a = q * b + r"
    4.35 +proof -
    4.36 +  from mod_div_equality have "a = a div b * b + a mod b" by simp
    4.37 +  moreover have "a div b = a div b" ..
    4.38 +  moreover have "a mod b = a mod b" ..
    4.39 +  note that ultimately show thesis by blast
    4.40 +qed
    4.41 +
    4.42 +lemma mod_div_equality2: "b * (a div b) + a mod b = a"
    4.43 +  using mod_div_equality [of a b] by (simp add: ac_simps)
    4.44 +
    4.45 +lemma mod_div_equality3: "a mod b + a div b * b = a"
    4.46 +  using mod_div_equality [of a b] by (simp add: ac_simps)
    4.47 +
    4.48 +lemma mod_div_equality4: "a mod b + b * (a div b) = a"
    4.49 +  using mod_div_equality [of a b] by (simp add: ac_simps)
    4.50 +
    4.51 +lemma minus_div_eq_mod: "a - a div b * b = a mod b"
    4.52 +  by (rule add_implies_diff [symmetric]) (fact mod_div_equality3)
    4.53 +
    4.54 +lemma minus_div_eq_mod2: "a - b * (a div b) = a mod b"
    4.55 +  by (rule add_implies_diff [symmetric]) (fact mod_div_equality4)
    4.56 +
    4.57 +lemma minus_mod_eq_div: "a - a mod b = a div b * b"
    4.58 +  by (rule add_implies_diff [symmetric]) (fact mod_div_equality)
    4.59 +
    4.60 +lemma minus_mod_eq_div2: "a - a mod b = b * (a div b)"
    4.61 +  by (rule add_implies_diff [symmetric]) (fact mod_div_equality2)
    4.62 +
    4.63 +end
    4.64 +  
    4.65 +
    4.66  class ordered_semiring = semiring + ordered_comm_monoid_add +
    4.67    assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
    4.68    assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"