author haftmann Wed, 12 Oct 2016 20:38:47 +0200 changeset 64164 38c407446400 parent 64163 62c9e5c05928 child 64174 54479f7b6685
separate type class for arbitrary quotient and remainder partitions
 src/HOL/Divides.thy file | annotate | diff | comparison | revisions src/HOL/Library/Polynomial_Factorial.thy file | annotate | diff | comparison | revisions src/HOL/Number_Theory/Euclidean_Algorithm.thy file | annotate | diff | comparison | revisions src/HOL/Rings.thy file | annotate | diff | comparison | revisions
```--- 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 \<open>Abstract division in commutative semirings.\<close>

-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 \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
@@ -41,14 +40,6 @@

text \<open>@{const divide} and @{const modulo}\<close>

-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"

@@ -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 "\<dots> = a div b"
-    by (simp only: mod_div_equality')
+    by (simp only: mod_div_equality3)
also have "\<dots> = 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 "\<dots> = a mod b"
-    by (simp only: mod_div_equality')
+    by (simp only: mod_div_equality3)
finally show ?thesis .
qed
```
```--- 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)"
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 ((\<lambda>p. if p = 0 then 0 else Suc (degree p)) \<circ> snd)")
-     (auto simp: degree_primitive_part degree_pseudo_mod_less)
+     (auto simp: degree_pseudo_mod_less)

declare gcd_poly_code_aux.simps [simp del]
```
```--- 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) \<longleftrightarrow> (k dvd ((m div n) * n + m mod n))"
-  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 \<open>
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.
\<close>
-class euclidean_semiring = divide_modulo + normalization_semidom +
+class euclidean_semiring = semiring_modulo + normalization_semidom +
fixes euclidean_size :: "'a \<Rightarrow> nat"
assumes size_0 [simp]: "euclidean_size 0 = 0"
assumes mod_size_less:
@@ -59,6 +26,30 @@
"b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> 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) \<longleftrightarrow> (k dvd ((m div n) * n + m mod n))"
+  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) \<longleftrightarrow> (k dvd ((m div n) * n + m mod n))"
-  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 \<noteq> 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 "\<not> a dvd b"
hence "b mod a \<noteq> 0" using mod_0_imp_dvd[of b a] by blast
then have "b mod a \<noteq> 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 \<open>b mod a \<noteq> 0\<close> have "c \<noteq> 0" by auto
with \<open>b mod a = b * c\<close> have "euclidean_size (b mod a) \<ge> 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]
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')```
```--- 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 \<open>Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::divide \<Rightarrow> 'a \<Rightarrow> 'a"})\<close>

-text \<open>Syntactic division remainder operator\<close>
-
-class modulo = dvd + divide +
-  fixes modulo :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "mod" 70)
-
text \<open>Algebraic classes with division\<close>

class semidom_divide = semidom + divide +
@@ -1286,6 +1281,53 @@

end

+
+text \<open>Syntactic division remainder operator\<close>
+
+class modulo = dvd + divide +
+  fixes modulo :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "mod" 70)
+
+text \<open>Arbitrary quotient and remainder partitions\<close>
+
+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 \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"```