--- a/src/HOL/Binomial.thy Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Binomial.thy Sun Oct 08 22:28:21 2017 +0200
@@ -1011,7 +1011,7 @@
by (subst binomial_fact_lemma [symmetric]) auto
lemma choose_dvd:
- "k \<le> n \<Longrightarrow> fact k * fact (n - k) dvd (fact n :: 'a::{semiring_div,linordered_semidom})"
+ "k \<le> n \<Longrightarrow> fact k * fact (n - k) dvd (fact n :: 'a::linordered_semidom)"
unfolding dvd_def
apply (rule exI [where x="of_nat (n choose k)"])
using binomial_fact_lemma [of k n, THEN arg_cong [where f = of_nat and 'b='a]]
@@ -1019,7 +1019,7 @@
done
lemma fact_fact_dvd_fact:
- "fact k * fact n dvd (fact (k + n) :: 'a::{semiring_div,linordered_semidom})"
+ "fact k * fact n dvd (fact (k + n) :: 'a::linordered_semidom)"
by (metis add.commute add_diff_cancel_left' choose_dvd le_add2)
lemma choose_mult_lemma:
--- a/src/HOL/Code_Numeral.thy Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Code_Numeral.thy Sun Oct 08 22:28:21 2017 +0200
@@ -247,7 +247,7 @@
end
-instantiation integer :: ring_div
+instantiation integer :: unique_euclidean_ring
begin
lift_definition modulo_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
@@ -256,12 +256,33 @@
declare modulo_integer.rep_eq [simp]
+lift_definition euclidean_size_integer :: "integer \<Rightarrow> nat"
+ is "euclidean_size :: int \<Rightarrow> nat"
+ .
+
+declare euclidean_size_integer.rep_eq [simp]
+
+lift_definition uniqueness_constraint_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
+ is "uniqueness_constraint :: int \<Rightarrow> int \<Rightarrow> bool"
+ .
+
+declare uniqueness_constraint_integer.rep_eq [simp]
+
instance
- by (standard; transfer) simp_all
+ by (standard; transfer)
+ (use mult_le_mono2 [of 1] in \<open>auto simp add: sgn_mult_abs abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib\<close>, rule div_eqI, simp_all)
end
-instantiation integer :: semiring_numeral_div
+lemma [code]:
+ "euclidean_size = nat_of_integer \<circ> abs"
+ by (simp add: fun_eq_iff nat_of_integer.rep_eq)
+
+lemma [code]:
+ "uniqueness_constraint (k :: integer) l \<longleftrightarrow> unit_factor k = unit_factor l"
+ by (simp add: integer_eq_iff)
+
+instantiation integer :: unique_euclidean_semiring_numeral
begin
definition divmod_integer :: "num \<Rightarrow> num \<Rightarrow> integer \<times> integer"
@@ -283,15 +304,15 @@
by (fact divmod_step_integer_def)
qed (transfer,
fact le_add_diff_inverse2
- semiring_numeral_div_class.div_less
- semiring_numeral_div_class.mod_less
- semiring_numeral_div_class.div_positive
- semiring_numeral_div_class.mod_less_eq_dividend
- semiring_numeral_div_class.pos_mod_bound
- semiring_numeral_div_class.pos_mod_sign
- semiring_numeral_div_class.mod_mult2_eq
- semiring_numeral_div_class.div_mult2_eq
- semiring_numeral_div_class.discrete)+
+ unique_euclidean_semiring_numeral_class.div_less
+ unique_euclidean_semiring_numeral_class.mod_less
+ unique_euclidean_semiring_numeral_class.div_positive
+ unique_euclidean_semiring_numeral_class.mod_less_eq_dividend
+ unique_euclidean_semiring_numeral_class.pos_mod_bound
+ unique_euclidean_semiring_numeral_class.pos_mod_sign
+ unique_euclidean_semiring_numeral_class.mod_mult2_eq
+ unique_euclidean_semiring_numeral_class.div_mult2_eq
+ unique_euclidean_semiring_numeral_class.discrete)+
end
@@ -853,7 +874,7 @@
"nat_of_natural (max k l) = max (nat_of_natural k) (nat_of_natural l)"
by transfer rule
-instantiation natural :: "{semiring_div, normalization_semidom}"
+instantiation natural :: unique_euclidean_semiring
begin
lift_definition normalize_natural :: "natural \<Rightarrow> natural"
@@ -880,11 +901,32 @@
declare modulo_natural.rep_eq [simp]
+lift_definition euclidean_size_natural :: "natural \<Rightarrow> nat"
+ is "euclidean_size :: nat \<Rightarrow> nat"
+ .
+
+declare euclidean_size_natural.rep_eq [simp]
+
+lift_definition uniqueness_constraint_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool"
+ is "uniqueness_constraint :: nat \<Rightarrow> nat \<Rightarrow> bool"
+ .
+
+declare uniqueness_constraint_natural.rep_eq [simp]
+
instance
- by standard (transfer, auto simp add: algebra_simps unit_factor_nat_def gr0_conv_Suc)+
+ by (standard; transfer)
+ (auto simp add: algebra_simps unit_factor_nat_def gr0_conv_Suc)
end
+lemma [code]:
+ "euclidean_size = nat_of_natural"
+ by (simp add: fun_eq_iff)
+
+lemma [code]:
+ "uniqueness_constraint = (\<top> :: natural \<Rightarrow> natural \<Rightarrow> bool)"
+ by (simp add: fun_eq_iff)
+
lift_definition natural_of_integer :: "integer \<Rightarrow> natural"
is "nat :: int \<Rightarrow> nat"
.
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy Sun Oct 08 22:28:21 2017 +0200
@@ -1181,7 +1181,7 @@
end
-instantiation fps :: (field) ring_div
+instantiation fps :: (field) idom_modulo
begin
definition fps_mod_def:
@@ -1224,39 +1224,6 @@
from assms show "f mod g = 0" by (intro fps_mod_eq_zero) auto
qed
-context
-begin
-private lemma fps_divide_cancel_aux1:
- assumes "h$0 \<noteq> (0 :: 'a :: field)"
- shows "(h * f) div (h * g) = f div g"
-proof (cases "g = 0")
- assume "g \<noteq> 0"
- from assms have "h \<noteq> 0" by auto
- note nz [simp] = \<open>g \<noteq> 0\<close> \<open>h \<noteq> 0\<close>
- from assms have [simp]: "subdegree h = 0" by (simp add: subdegree_eq_0_iff)
-
- have "(h * f) div (h * g) =
- fps_shift (subdegree g) (h * f * inverse (fps_shift (subdegree g) (h*g)))"
- by (simp add: fps_divide_def Let_def)
- also have "h * f * inverse (fps_shift (subdegree g) (h*g)) =
- (inverse h * h) * f * inverse (fps_shift (subdegree g) g)"
- by (subst fps_shift_mult) (simp_all add: algebra_simps fps_inverse_mult)
- also from assms have "inverse h * h = 1" by (rule inverse_mult_eq_1)
- finally show "(h * f) div (h * g) = f div g" by (simp_all add: fps_divide_def Let_def)
-qed (simp_all add: fps_divide_def)
-
-private lemma fps_divide_cancel_aux2:
- "(f * fps_X^m) div (g * fps_X^m) = f div (g :: 'a :: field fps)"
-proof (cases "g = 0")
- assume [simp]: "g \<noteq> 0"
- have "(f * fps_X^m) div (g * fps_X^m) =
- fps_shift (subdegree g + m) (f*inverse (fps_shift (subdegree g + m) (g*fps_X^m))*fps_X^m)"
- by (simp add: fps_divide_def Let_def algebra_simps)
- also have "... = f div g"
- by (simp add: fps_shift_times_fps_X_power'' fps_divide_def Let_def)
- finally show ?thesis .
-qed (simp_all add: fps_divide_def)
-
instance proof
fix f g :: "'a fps"
define n where "n = subdegree g"
@@ -1284,39 +1251,9 @@
finally show ?thesis by simp
qed
qed (auto simp: fps_mod_def fps_divide_def Let_def)
-next
-
- fix f g h :: "'a fps"
- assume "h \<noteq> 0"
- show "(h * f) div (h * g) = f div g"
- proof -
- define m where "m = subdegree h"
- define h' where "h' = fps_shift m h"
- have h_decomp: "h = h' * fps_X ^ m" unfolding h'_def m_def by (rule subdegree_decompose)
- from \<open>h \<noteq> 0\<close> have [simp]: "h'$0 \<noteq> 0" by (simp add: h'_def m_def)
- have "(h * f) div (h * g) = (h' * f * fps_X^m) div (h' * g * fps_X^m)"
- by (simp add: h_decomp algebra_simps)
- also have "... = f div g" by (simp add: fps_divide_cancel_aux1 fps_divide_cancel_aux2)
- finally show ?thesis .
- qed
-
-next
- fix f g h :: "'a fps"
- assume [simp]: "h \<noteq> 0"
- define n h' where dfs: "n = subdegree h" "h' = fps_shift n h"
- have "(f + g * h) div h = fps_shift n (f * inverse h') + fps_shift n (g * (h * inverse h'))"
- by (simp add: fps_divide_def Let_def dfs[symmetric] algebra_simps fps_shift_add)
- also have "h * inverse h' = (inverse h' * h') * fps_X^n"
- by (subst subdegree_decompose) (simp_all add: dfs)
- also have "... = fps_X^n" by (subst inverse_mult_eq_1) (simp_all add: dfs)
- also have "fps_shift n (g * fps_X^n) = g" by simp
- also have "fps_shift n (f * inverse h') = f div h"
- by (simp add: fps_divide_def Let_def dfs)
- finally show "(f + g * h) div h = g + f div h" by simp
qed
end
-end
lemma subdegree_mod:
assumes "f \<noteq> 0" "subdegree f < subdegree g"
@@ -1411,6 +1348,40 @@
definition fps_euclidean_size_def:
"euclidean_size f = (if f = 0 then 0 else 2 ^ subdegree f)"
+context
+begin
+
+private lemma fps_divide_cancel_aux1:
+ assumes "h$0 \<noteq> (0 :: 'a :: field)"
+ shows "(h * f) div (h * g) = f div g"
+proof (cases "g = 0")
+ assume "g \<noteq> 0"
+ from assms have "h \<noteq> 0" by auto
+ note nz [simp] = \<open>g \<noteq> 0\<close> \<open>h \<noteq> 0\<close>
+ from assms have [simp]: "subdegree h = 0" by (simp add: subdegree_eq_0_iff)
+
+ have "(h * f) div (h * g) =
+ fps_shift (subdegree g) (h * f * inverse (fps_shift (subdegree g) (h*g)))"
+ by (simp add: fps_divide_def Let_def)
+ also have "h * f * inverse (fps_shift (subdegree g) (h*g)) =
+ (inverse h * h) * f * inverse (fps_shift (subdegree g) g)"
+ by (subst fps_shift_mult) (simp_all add: algebra_simps fps_inverse_mult)
+ also from assms have "inverse h * h = 1" by (rule inverse_mult_eq_1)
+ finally show "(h * f) div (h * g) = f div g" by (simp_all add: fps_divide_def Let_def)
+qed (simp_all add: fps_divide_def)
+
+private lemma fps_divide_cancel_aux2:
+ "(f * fps_X^m) div (g * fps_X^m) = f div (g :: 'a :: field fps)"
+proof (cases "g = 0")
+ assume [simp]: "g \<noteq> 0"
+ have "(f * fps_X^m) div (g * fps_X^m) =
+ fps_shift (subdegree g + m) (f*inverse (fps_shift (subdegree g + m) (g*fps_X^m))*fps_X^m)"
+ by (simp add: fps_divide_def Let_def algebra_simps)
+ also have "... = f div g"
+ by (simp add: fps_shift_times_fps_X_power'' fps_divide_def Let_def)
+ finally show ?thesis .
+qed (simp_all add: fps_divide_def)
+
instance proof
fix f g :: "'a fps" assume [simp]: "g \<noteq> 0"
show "euclidean_size f \<le> euclidean_size (f * g)"
@@ -1420,10 +1391,40 @@
apply (rule disjE[OF le_less_linear[of "subdegree g" "subdegree f"]])
apply (simp_all add: fps_mod_eq_zero fps_euclidean_size_def subdegree_mod)
done
+ show "(h * f) div (h * g) = f div g" if "h \<noteq> 0"
+ for f g h :: "'a fps"
+ proof -
+ define m where "m = subdegree h"
+ define h' where "h' = fps_shift m h"
+ have h_decomp: "h = h' * fps_X ^ m" unfolding h'_def m_def by (rule subdegree_decompose)
+ from \<open>h \<noteq> 0\<close> have [simp]: "h'$0 \<noteq> 0" by (simp add: h'_def m_def)
+ have "(h * f) div (h * g) = (h' * f * fps_X^m) div (h' * g * fps_X^m)"
+ by (simp add: h_decomp algebra_simps)
+ also have "... = f div g"
+ by (simp add: fps_divide_cancel_aux1 fps_divide_cancel_aux2)
+ finally show ?thesis .
+ qed
+ show "(f + g * h) div h = g + f div h"
+ if "h \<noteq> 0" for f g h :: "'a fps"
+ proof -
+ define n h' where dfs: "n = subdegree h" "h' = fps_shift n h"
+ have "(f + g * h) div h = fps_shift n (f * inverse h') + fps_shift n (g * (h * inverse h'))"
+ by (simp add: fps_divide_def Let_def dfs [symmetric] algebra_simps fps_shift_add that)
+ also have "h * inverse h' = (inverse h' * h') * fps_X^n"
+ by (subst subdegree_decompose) (simp_all add: dfs)
+ also have "... = fps_X^n"
+ by (subst inverse_mult_eq_1) (simp_all add: dfs that)
+ also have "fps_shift n (g * fps_X^n) = g" by simp
+ also have "fps_shift n (f * inverse h') = f div h"
+ by (simp add: fps_divide_def Let_def dfs)
+ finally show ?thesis by simp
+ qed
qed (simp_all add: fps_euclidean_size_def)
end
+end
+
instantiation fps :: (field) euclidean_ring_gcd
begin
definition fps_gcd_def: "(gcd :: 'a fps \<Rightarrow> _) = Euclidean_Algorithm.gcd"
--- a/src/HOL/Computational_Algebra/Polynomial.thy Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy Sun Oct 08 22:28:21 2017 +0200
@@ -3637,40 +3637,7 @@
for x :: "'a::field poly"
by (rule eucl_rel_poly_unique_mod [OF eucl_rel_poly])
-instance poly :: (field) ring_div
-proof
- fix x y z :: "'a poly"
- assume "y \<noteq> 0"
- with eucl_rel_poly [of x y] have "eucl_rel_poly (x + z * y) y (z + x div y, x mod y)"
- by (simp add: eucl_rel_poly_iff distrib_right)
- then show "(x + z * y) div y = z + x div y"
- by (rule div_poly_eq)
-next
- fix x y z :: "'a poly"
- assume "x \<noteq> 0"
- show "(x * y) div (x * z) = y div z"
- proof (cases "y \<noteq> 0 \<and> z \<noteq> 0")
- have "\<And>x::'a poly. eucl_rel_poly x 0 (0, x)"
- by (rule eucl_rel_poly_by_0)
- then have [simp]: "\<And>x::'a poly. x div 0 = 0"
- by (rule div_poly_eq)
- have "\<And>x::'a poly. eucl_rel_poly 0 x (0, 0)"
- by (rule eucl_rel_poly_0)
- then have [simp]: "\<And>x::'a poly. 0 div x = 0"
- by (rule div_poly_eq)
- case False
- then show ?thesis by auto
- next
- case True
- then have "y \<noteq> 0" and "z \<noteq> 0" by auto
- with \<open>x \<noteq> 0\<close> have "\<And>q r. eucl_rel_poly y z (q, r) \<Longrightarrow> eucl_rel_poly (x * y) (x * z) (q, x * r)"
- by (auto simp: eucl_rel_poly_iff algebra_simps) (rule classical, simp add: degree_mult_eq)
- moreover from eucl_rel_poly have "eucl_rel_poly y z (y div z, y mod z)" .
- ultimately have "eucl_rel_poly (x * y) (x * z) (y div z, x * (y mod z))" .
- then show ?thesis
- by (simp add: div_poly_eq)
- qed
-qed
+instance poly :: (field) idom_modulo ..
lemma div_pCons_eq:
"pCons a p div q =
--- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy Sun Oct 08 22:28:21 2017 +0200
@@ -459,11 +459,17 @@
ultimately show "(if p * s = 0 then (0::nat) else 2 ^ degree (p * s)) < (if q * s = 0 then 0 else 2 ^ degree (q * s))"
by (auto simp add: degree_mult_eq)
next
- fix p q r :: "'a poly" assume "p \<noteq> 0"
+ fix p q r :: "'a poly"
+ assume "p \<noteq> 0"
+ with eucl_rel_poly [of r p] have "eucl_rel_poly (r + q * p) p (q + r div p, r mod p)"
+ by (simp add: eucl_rel_poly_iff distrib_right)
+ then have "(r + q * p) div p = q + r div p"
+ by (rule div_poly_eq)
moreover assume "(if r = 0 then (0::nat) else 2 ^ degree r)
- < (if p = 0 then 0 else 2 ^ degree p)"
+ < (if p = 0 then 0 else 2 ^ degree p)"
ultimately show "(q * p + r) div p = q"
- by (cases "r = 0") (auto simp add: div_poly_less)
+ using \<open>p \<noteq> 0\<close>
+ by (cases "r = 0") (simp_all add: div_poly_less ac_simps)
qed (auto simp: lead_coeff_mult Rings.div_mult_mod_eq intro!: degree_mod_less' degree_mult_right_le)
qed
@@ -761,9 +767,18 @@
definition uniqueness_constraint_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> bool"
where [simp]: "uniqueness_constraint_poly = top"
-instance
- 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
+instance proof
+ show "(q * p + r) div p = q" if "p \<noteq> 0"
+ and "euclidean_size r < euclidean_size p" for q p r :: "'a poly"
+ proof -
+ from \<open>p \<noteq> 0\<close> eucl_rel_poly [of r p] have "eucl_rel_poly (r + q * p) p (q + r div p, r mod p)"
+ by (simp add: eucl_rel_poly_iff distrib_right)
+ then have "(r + q * p) div p = q + r div p"
+ by (rule div_poly_eq)
+ with that show ?thesis
+ by (cases "r = 0") (simp_all add: euclidean_size_poly_def div_poly_less ac_simps)
+ qed
+qed (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
--- a/src/HOL/Divides.thy Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Divides.thy Sun Oct 08 22:28:21 2017 +0200
@@ -9,433 +9,9 @@
imports Parity
begin
-subsection \<open>Quotient and remainder in integral domains with additional properties\<close>
-
-class semiring_div = semidom_modulo +
- assumes 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"
-begin
-
-lemma div_mult_self2 [simp]:
- assumes "b \<noteq> 0"
- shows "(a + b * c) div b = c + a div b"
- using assms div_mult_self1 [of b a c] by (simp add: mult.commute)
-
-lemma div_mult_self3 [simp]:
- assumes "b \<noteq> 0"
- shows "(c * b + a) div b = c + a div b"
- using assms by (simp add: add.commute)
-
-lemma div_mult_self4 [simp]:
- assumes "b \<noteq> 0"
- shows "(b * c + a) div b = c + a div b"
- using assms by (simp add: add.commute)
-
-lemma mod_mult_self1 [simp]: "(a + c * b) mod b = a mod b"
-proof (cases "b = 0")
- case True then show ?thesis by simp
-next
- case False
- have "a + c * b = (a + c * b) div b * b + (a + c * b) mod b"
- by (simp add: div_mult_mod_eq)
- also from False div_mult_self1 [of b a c] have
- "\<dots> = (c + a div b) * b + (a + c * b) mod b"
- by (simp add: algebra_simps)
- finally have "a = a div b * b + (a + c * b) mod b"
- by (simp add: add.commute [of a] add.assoc distrib_right)
- then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b"
- by (simp add: div_mult_mod_eq)
- then show ?thesis by simp
-qed
-
-lemma mod_mult_self2 [simp]:
- "(a + b * c) mod b = a mod b"
- by (simp add: mult.commute [of b])
-
-lemma mod_mult_self3 [simp]:
- "(c * b + a) mod b = a mod b"
- by (simp add: add.commute)
-
-lemma mod_mult_self4 [simp]:
- "(b * c + a) mod b = a mod b"
- by (simp add: add.commute)
-
-lemma mod_mult_self1_is_0 [simp]:
- "b * a mod b = 0"
- using mod_mult_self2 [of 0 b a] by simp
-
-lemma mod_mult_self2_is_0 [simp]:
- "a * b mod b = 0"
- using mod_mult_self1 [of 0 a b] by simp
-
-lemma div_add_self1:
- assumes "b \<noteq> 0"
- shows "(b + a) div b = a div b + 1"
- using assms div_mult_self1 [of b a 1] by (simp add: add.commute)
-
-lemma div_add_self2:
- assumes "b \<noteq> 0"
- shows "(a + b) div b = a div b + 1"
- using assms div_add_self1 [of b a] by (simp add: add.commute)
-
-lemma mod_add_self1 [simp]:
- "(b + a) mod b = a mod b"
- using mod_mult_self1 [of a 1 b] by (simp add: add.commute)
-
-lemma mod_add_self2 [simp]:
- "(a + b) mod b = a mod b"
- using mod_mult_self1 [of a 1 b] by simp
-
-lemma mod_div_trivial [simp]:
- "a mod b div b = 0"
-proof (cases "b = 0")
- assume "b = 0"
- thus ?thesis by simp
-next
- assume "b \<noteq> 0"
- 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_mult_eq)
- also have "\<dots> = a div b + 0"
- by simp
- finally show ?thesis
- by (rule add_left_imp_eq)
-qed
-
-lemma mod_mod_trivial [simp]:
- "a mod b mod b = a mod b"
-proof -
- 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_mult_eq)
- finally show ?thesis .
-qed
-
-lemma mod_mod_cancel:
- assumes "c dvd b"
- shows "a mod b mod c = a mod c"
-proof -
- from \<open>c dvd b\<close> obtain k where "b = c * k"
- by (rule dvdE)
- have "a mod b mod c = a mod (c * k) mod c"
- by (simp only: \<open>b = c * k\<close>)
- also have "\<dots> = (a mod (c * k) + a div (c * k) * k * c) mod c"
- by (simp only: mod_mult_self1)
- also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c"
- by (simp only: ac_simps)
- also have "\<dots> = a mod c"
- by (simp only: div_mult_mod_eq)
- finally show ?thesis .
-qed
-
-lemma div_mult_mult2 [simp]:
- "c \<noteq> 0 \<Longrightarrow> (a * c) div (b * c) = a div b"
- by (drule div_mult_mult1) (simp add: mult.commute)
-
-lemma div_mult_mult1_if [simp]:
- "(c * a) div (c * b) = (if c = 0 then 0 else a div b)"
- by simp_all
-
-lemma mod_mult_mult1:
- "(c * a) mod (c * b) = c * (a mod b)"
-proof (cases "c = 0")
- case True then show ?thesis by simp
-next
- case False
- from div_mult_mod_eq
- have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" .
- with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b)
- = c * a + c * (a mod b)" by (simp add: algebra_simps)
- with div_mult_mod_eq show ?thesis by simp
-qed
-
-lemma mod_mult_mult2:
- "(a * c) mod (b * c) = (a mod b) * c"
- using mod_mult_mult1 [of c a b] by (simp add: mult.commute)
-
-lemma mult_mod_left: "(a mod b) * c = (a * c) mod (b * c)"
- by (fact mod_mult_mult2 [symmetric])
-
-lemma mult_mod_right: "c * (a mod b) = (c * a) mod (c * b)"
- by (fact mod_mult_mult1 [symmetric])
-
-lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
- unfolding dvd_def by (auto simp add: mod_mult_mult1)
-
-lemma div_plus_div_distrib_dvd_left:
- "c dvd a \<Longrightarrow> (a + b) div c = a div c + b div c"
- by (cases "c = 0") (auto elim: dvdE)
-
-lemma div_plus_div_distrib_dvd_right:
- "c dvd b \<Longrightarrow> (a + b) div c = a div c + b div c"
- using div_plus_div_distrib_dvd_left [of c b a]
- by (simp add: ac_simps)
-
-named_theorems mod_simps
-
-text \<open>Addition respects modular equivalence.\<close>
-
-lemma mod_add_left_eq [mod_simps]:
- "(a mod c + b) mod c = (a + b) mod c"
-proof -
- have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
- by (simp only: div_mult_mod_eq)
- also have "\<dots> = (a mod c + b + a div c * c) mod c"
- by (simp only: ac_simps)
- also have "\<dots> = (a mod c + b) mod c"
- by (rule mod_mult_self1)
- finally show ?thesis
- by (rule sym)
-qed
-
-lemma mod_add_right_eq [mod_simps]:
- "(a + b mod c) mod c = (a + b) mod c"
- using mod_add_left_eq [of b c a] by (simp add: ac_simps)
-
-lemma mod_add_eq:
- "(a mod c + b mod c) mod c = (a + b) mod c"
- by (simp add: mod_add_left_eq mod_add_right_eq)
-
-lemma mod_sum_eq [mod_simps]:
- "(\<Sum>i\<in>A. f i mod a) mod a = sum f A mod a"
-proof (induct A rule: infinite_finite_induct)
- case (insert i A)
- then have "(\<Sum>i\<in>insert i A. f i mod a) mod a
- = (f i mod a + (\<Sum>i\<in>A. f i mod a)) mod a"
- by simp
- also have "\<dots> = (f i + (\<Sum>i\<in>A. f i mod a) mod a) mod a"
- by (simp add: mod_simps)
- also have "\<dots> = (f i + (\<Sum>i\<in>A. f i) mod a) mod a"
- by (simp add: insert.hyps)
- finally show ?case
- by (simp add: insert.hyps mod_simps)
-qed simp_all
-
-lemma mod_add_cong:
- assumes "a mod c = a' mod c"
- assumes "b mod c = b' mod c"
- shows "(a + b) mod c = (a' + b') mod c"
-proof -
- have "(a mod c + b mod c) mod c = (a' mod c + b' mod c) mod c"
- unfolding assms ..
- then show ?thesis
- by (simp add: mod_add_eq)
-qed
-
-text \<open>Multiplication respects modular equivalence.\<close>
-
-lemma mod_mult_left_eq [mod_simps]:
- "((a mod c) * b) mod c = (a * b) mod c"
-proof -
- have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
- by (simp only: div_mult_mod_eq)
- also have "\<dots> = (a mod c * b + a div c * b * c) mod c"
- by (simp only: algebra_simps)
- also have "\<dots> = (a mod c * b) mod c"
- by (rule mod_mult_self1)
- finally show ?thesis
- by (rule sym)
-qed
-
-lemma mod_mult_right_eq [mod_simps]:
- "(a * (b mod c)) mod c = (a * b) mod c"
- using mod_mult_left_eq [of b c a] by (simp add: ac_simps)
-
-lemma mod_mult_eq:
- "((a mod c) * (b mod c)) mod c = (a * b) mod c"
- by (simp add: mod_mult_left_eq mod_mult_right_eq)
-
-lemma mod_prod_eq [mod_simps]:
- "(\<Prod>i\<in>A. f i mod a) mod a = prod f A mod a"
-proof (induct A rule: infinite_finite_induct)
- case (insert i A)
- then have "(\<Prod>i\<in>insert i A. f i mod a) mod a
- = (f i mod a * (\<Prod>i\<in>A. f i mod a)) mod a"
- by simp
- also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i mod a) mod a)) mod a"
- by (simp add: mod_simps)
- also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i) mod a)) mod a"
- by (simp add: insert.hyps)
- finally show ?case
- by (simp add: insert.hyps mod_simps)
-qed simp_all
-
-lemma mod_mult_cong:
- assumes "a mod c = a' mod c"
- assumes "b mod c = b' mod c"
- shows "(a * b) mod c = (a' * b') mod c"
-proof -
- have "(a mod c * (b mod c)) mod c = (a' mod c * (b' mod c)) mod c"
- unfolding assms ..
- then show ?thesis
- by (simp add: mod_mult_eq)
-qed
-
-text \<open>Exponentiation respects modular equivalence.\<close>
-
-lemma power_mod [mod_simps]:
- "((a mod b) ^ n) mod b = (a ^ n) mod b"
-proof (induct n)
- case 0
- then show ?case by simp
-next
- case (Suc n)
- have "(a mod b) ^ Suc n mod b = (a mod b) * ((a mod b) ^ n mod b) mod b"
- by (simp add: mod_mult_right_eq)
- with Suc show ?case
- by (simp add: mod_mult_left_eq mod_mult_right_eq)
-qed
-
-end
-
-class ring_div = comm_ring_1 + semiring_div
-begin
-
-subclass idom_divide ..
-
-lemma div_minus_minus [simp]: "(- a) div (- b) = a div b"
- using div_mult_mult1 [of "- 1" a b] by simp
-
-lemma mod_minus_minus [simp]: "(- a) mod (- b) = - (a mod b)"
- using mod_mult_mult1 [of "- 1" a b] by simp
-
-lemma div_minus_right: "a div (- b) = (- a) div b"
- using div_minus_minus [of "- a" b] by simp
-
-lemma mod_minus_right: "a mod (- b) = - ((- a) mod b)"
- using mod_minus_minus [of "- a" b] by simp
-
-lemma div_minus1_right [simp]: "a div (- 1) = - a"
- using div_minus_right [of a 1] by simp
-
-lemma mod_minus1_right [simp]: "a mod (- 1) = 0"
- using mod_minus_right [of a 1] by simp
-
-text \<open>Negation respects modular equivalence.\<close>
-
-lemma mod_minus_eq [mod_simps]:
- "(- (a mod b)) mod b = (- a) mod b"
-proof -
- have "(- a) mod b = (- (a div b * b + a mod b)) mod b"
- by (simp only: div_mult_mod_eq)
- also have "\<dots> = (- (a mod b) + - (a div b) * b) mod b"
- by (simp add: ac_simps)
- also have "\<dots> = (- (a mod b)) mod b"
- by (rule mod_mult_self1)
- finally show ?thesis
- by (rule sym)
-qed
-
-lemma mod_minus_cong:
- assumes "a mod b = a' mod b"
- shows "(- a) mod b = (- a') mod b"
-proof -
- have "(- (a mod b)) mod b = (- (a' mod b)) mod b"
- unfolding assms ..
- then show ?thesis
- by (simp add: mod_minus_eq)
-qed
-
-text \<open>Subtraction respects modular equivalence.\<close>
-
-lemma mod_diff_left_eq [mod_simps]:
- "(a mod c - b) mod c = (a - b) mod c"
- using mod_add_cong [of a c "a mod c" "- b" "- b"]
- by simp
-
-lemma mod_diff_right_eq [mod_simps]:
- "(a - b mod c) mod c = (a - b) mod c"
- using mod_add_cong [of a c a "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
- by simp
-
-lemma mod_diff_eq:
- "(a mod c - b mod c) mod c = (a - b) mod c"
- using mod_add_cong [of a c "a mod c" "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
- by simp
-
-lemma mod_diff_cong:
- assumes "a mod c = a' mod c"
- assumes "b mod c = b' mod c"
- shows "(a - b) mod c = (a' - b') mod c"
- using assms mod_add_cong [of a c a' "- b" "- b'"] mod_minus_cong [of b c "b'"]
- by simp
-
-lemma minus_mod_self2 [simp]:
- "(a - b) mod b = a mod b"
- using mod_diff_right_eq [of a b b]
- by (simp add: mod_diff_right_eq)
-
-lemma minus_mod_self1 [simp]:
- "(b - a) mod b = - a mod b"
- using mod_add_self2 [of "- a" b] by simp
-
-end
-
-
-subsection \<open>Euclidean (semi)rings with cancel rules\<close>
-
-class euclidean_semiring_cancel = euclidean_semiring + semiring_div
-
-class euclidean_ring_cancel = euclidean_ring + ring_div
-
-context unique_euclidean_semiring
-begin
-
-subclass euclidean_semiring_cancel
-proof
- show "(a + c * b) div b = c + a div b" if "b \<noteq> 0" for a b c
- proof (cases a b rule: divmod_cases)
- case by0
- with \<open>b \<noteq> 0\<close> 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 \<noteq> 0" for a b c
- proof (cases a b rule: divmod_cases)
- case by0
- then show ?thesis
- by simp
- next
- case (divides q)
- with \<open>c \<noteq> 0\<close> show ?thesis
- by (simp add: mult.left_commute [of c])
- next
- case (remainder q r)
- from \<open>b \<noteq> 0\<close> \<open>c \<noteq> 0\<close> have "b * c \<noteq> 0"
- by simp
- from remainder \<open>c \<noteq> 0\<close>
- 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 \<open>b * c \<noteq> 0\<close> in simp)
- qed
-qed
-
-end
-
-context unique_euclidean_ring
-begin
-
-subclass euclidean_ring_cancel ..
-
-end
-
-
subsection \<open>Parity\<close>
-class semiring_div_parity = semiring_div + comm_semiring_1_cancel + numeral +
+class unique_euclidean_semiring_parity = unique_euclidean_semiring +
assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1"
assumes zero_not_eq_two: "0 \<noteq> 2"
@@ -532,7 +108,7 @@
and less technical class hierarchy.
\<close>
-class semiring_numeral_div = semiring_div + comm_semiring_1_cancel + linordered_semidom +
+class unique_euclidean_semiring_numeral = unique_euclidean_semiring + linordered_semidom +
assumes div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
and mod_less: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"
and div_positive: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0"
@@ -553,7 +129,7 @@
yields a significant speedup.\<close>
begin
-subclass semiring_div_parity
+subclass unique_euclidean_semiring_parity
proof
fix a
show "a mod 2 = 0 \<or> a mod 2 = 1"
@@ -1050,58 +626,6 @@
end
-instance nat :: semiring_div
-proof
- fix m n q :: nat
- assume "n \<noteq> 0"
- then show "(q + m * n) div n = m + q div n"
- by (induct m) (simp_all add: le_div_geq)
-next
- fix m n q :: nat
- assume "m \<noteq> 0"
- show "(m * n) div (m * q) = n div q"
- proof (cases "q = 0")
- case True
- then show ?thesis
- by simp
- next
- case False
- show ?thesis
- proof (rule div_nat_unique [of _ _ _ "m * (n mod q)"])
- show "eucl_rel_nat (m * n) (m * q) (n div q, m * (n mod q))"
- by (rule eucl_rel_natI)
- (use \<open>m \<noteq> 0\<close> \<open>q \<noteq> 0\<close> div_mult_mod_eq [of n q] in \<open>auto simp add: algebra_simps distrib_left [symmetric]\<close>)
- qed
- qed
-qed
-
-lemma div_by_Suc_0 [simp]:
- "m div Suc 0 = m"
- using div_by_1 [of m] by simp
-
-lemma mod_by_Suc_0 [simp]:
- "m mod Suc 0 = 0"
- using mod_by_1 [of m] by simp
-
-lemma mod_greater_zero_iff_not_dvd:
- fixes m n :: nat
- shows "m mod n > 0 \<longleftrightarrow> \<not> n dvd m"
- by (simp add: dvd_eq_mod_eq_0)
-
-instantiation nat :: unique_euclidean_semiring
-begin
-
-definition [simp]:
- "euclidean_size_nat = (id :: nat \<Rightarrow> nat)"
-
-definition [simp]:
- "uniqueness_constraint_nat = (top :: nat \<Rightarrow> nat \<Rightarrow> bool)"
-
-instance
- by standard (use mult_le_mono2 [of 1] in \<open>simp_all add: unit_factor_nat_def mod_greater_zero_iff_not_dvd\<close>)
-
-end
-
text \<open>Simproc for cancelling @{const divide} and @{const modulo}\<close>
lemma (in semiring_modulo) cancel_div_mod_rules:
@@ -1142,6 +666,41 @@
simproc_setup cancel_div_mod_nat ("(m::nat) + n") =
\<open>K Cancel_Div_Mod_Nat.proc\<close>
+lemma div_by_Suc_0 [simp]:
+ "m div Suc 0 = m"
+ using div_by_1 [of m] by simp
+
+lemma mod_by_Suc_0 [simp]:
+ "m mod Suc 0 = 0"
+ using mod_by_1 [of m] by simp
+
+lemma mod_greater_zero_iff_not_dvd:
+ fixes m n :: nat
+ shows "m mod n > 0 \<longleftrightarrow> \<not> n dvd m"
+ by (simp add: dvd_eq_mod_eq_0)
+
+instantiation nat :: unique_euclidean_semiring
+begin
+
+definition [simp]:
+ "euclidean_size_nat = (id :: nat \<Rightarrow> nat)"
+
+definition [simp]:
+ "uniqueness_constraint_nat = (top :: nat \<Rightarrow> nat \<Rightarrow> bool)"
+
+instance proof
+ fix n q r :: nat
+ assume "euclidean_size r < euclidean_size n"
+ then have "n > r"
+ by simp_all
+ then have "eucl_rel_nat (q * n + r) n (q, r)"
+ by (rule eucl_rel_natI) rule
+ then show "(q * n + r) div n = q"
+ by (rule div_nat_unique)
+qed (use mult_le_mono2 [of 1] in \<open>simp_all\<close>)
+
+end
+
lemma divmod_nat_if [code]:
"Divides.divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
@@ -1262,7 +821,7 @@
lemma mod_mult2_eq: "a mod (b * c) = b * (a div b mod c) + a mod (b::nat)"
by (auto simp add: mult.commute eucl_rel_nat [THEN eucl_rel_nat_mult2_eq, THEN mod_nat_unique])
-instantiation nat :: semiring_numeral_div
+instantiation nat :: unique_euclidean_semiring_numeral
begin
definition divmod_nat :: "num \<Rightarrow> num \<Rightarrow> nat \<times> nat"
@@ -1820,6 +1379,25 @@
end
+ML \<open>
+structure Cancel_Div_Mod_Int = Cancel_Div_Mod
+(
+ val div_name = @{const_name divide};
+ val mod_name = @{const_name modulo};
+ val mk_binop = HOLogic.mk_binop;
+ val mk_sum = Arith_Data.mk_sum HOLogic.intT;
+ val dest_sum = Arith_Data.dest_sum;
+
+ val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
+
+ val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
+ @{thms diff_conv_add_uminus add_0_left add_0_right ac_simps})
+)
+\<close>
+
+simproc_setup cancel_div_mod_int ("(k::int) + l") =
+ \<open>K Cancel_Div_Mod_Int.proc\<close>
+
lemma is_unit_int:
"is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
by auto
@@ -1921,50 +1499,28 @@
using assms unfolding modulo_int_def [of k l]
by (auto simp add: not_less int_dvd_iff mod_greater_zero_iff_not_dvd elim: pos_int_cases neg_int_cases nonneg_int_cases nonpos_int_cases)
-instance int :: ring_div
-proof
- fix k l s :: int
- assume "l \<noteq> 0"
- then have "eucl_rel_int (k + s * l) l (s + k div l, k mod l)"
- using eucl_rel_int [of k l]
- unfolding eucl_rel_int_iff by (auto simp: algebra_simps)
- then show "(k + s * l) div l = s + k div l"
+instantiation int :: unique_euclidean_ring
+begin
+
+definition [simp]:
+ "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
+
+definition [simp]:
+ "uniqueness_constraint_int (k :: int) l \<longleftrightarrow> unit_factor k = unit_factor l"
+
+instance proof
+ fix l q r:: int
+ assume "uniqueness_constraint r l"
+ and "euclidean_size r < euclidean_size l"
+ then have "sgn r = sgn l" and "\<bar>r\<bar> < \<bar>l\<bar>"
+ by simp_all
+ then have "eucl_rel_int (q * l + r) l (q, r)"
+ by (rule eucl_rel_int_remainderI) simp
+ then show "(q * l + r) div l = q"
by (rule div_int_unique)
-next
- fix k l s :: int
- assume "s \<noteq> 0"
- have "\<And>q r. eucl_rel_int k l (q, r)
- \<Longrightarrow> eucl_rel_int (s * k) (s * l) (q, s * r)"
- unfolding eucl_rel_int_iff
- by (rule linorder_cases [of 0 l])
- (use \<open>s \<noteq> 0\<close> in \<open>auto simp: algebra_simps
- mult_less_0_iff zero_less_mult_iff mult_strict_right_mono
- mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff\<close>)
- then have "eucl_rel_int (s * k) (s * l) (k div l, s * (k mod l))"
- using eucl_rel_int [of k l] .
- then show "(s * k) div (s * l) = k div l"
- by (rule div_int_unique)
-qed
+qed (use mult_le_mono2 [of 1] in \<open>auto simp add: abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib\<close>)
-ML \<open>
-structure Cancel_Div_Mod_Int = Cancel_Div_Mod
-(
- val div_name = @{const_name divide};
- val mod_name = @{const_name modulo};
- val mk_binop = HOLogic.mk_binop;
- val mk_sum = Arith_Data.mk_sum HOLogic.intT;
- val dest_sum = Arith_Data.dest_sum;
-
- val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
-
- val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
- @{thms diff_conv_add_uminus add_0_left add_0_right ac_simps})
-)
-\<close>
-
-simproc_setup cancel_div_mod_int ("(k::int) + l") =
- \<open>K Cancel_Div_Mod_Int.proc\<close>
-
+end
text\<open>Basic laws about division and remainder\<close>
@@ -2420,21 +1976,6 @@
by simp
qed
-instantiation int :: unique_euclidean_ring
-begin
-
-definition [simp]:
- "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
-
-definition [simp]:
- "uniqueness_constraint_int (k :: int) l \<longleftrightarrow> unit_factor k = unit_factor l"
-
-instance
- by standard
- (use mult_le_mono2 [of 1] in \<open>auto simp add: abs_mult nat_mult_distrib sgn_mod zdiv_eq_0_iff sgn_1_pos sgn_mult split: abs_split\<close>)
-
-end
-
subsubsection \<open>Quotients of Signs\<close>
@@ -2506,7 +2047,7 @@
subsubsection \<open>Computation of Division and Remainder\<close>
-instantiation int :: semiring_numeral_div
+instantiation int :: unique_euclidean_semiring_numeral
begin
definition divmod_int :: "num \<Rightarrow> num \<Rightarrow> int \<times> int"
@@ -2687,22 +2228,6 @@
apply (rule Divides.div_less_dividend, simp_all)
done
-lemma (in ring_div) mod_eq_dvd_iff:
- "a mod c = b mod c \<longleftrightarrow> c dvd a - b" (is "?P \<longleftrightarrow> ?Q")
-proof
- assume ?P
- then have "(a mod c - b mod c) mod c = 0"
- by simp
- then show ?Q
- by (simp add: dvd_eq_mod_eq_0 mod_simps)
-next
- assume ?Q
- then obtain d where d: "a - b = c * d" ..
- then have "a = c * d + b"
- by (simp add: algebra_simps)
- then show ?P by simp
-qed
-
lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y mod n" and xy:"y \<le> x"
shows "\<exists>q. x = y + n * q"
proof-
@@ -2742,23 +2267,23 @@
\<close>
simproc_setup numeral_divmod
- ("0 div 0 :: 'a :: semiring_numeral_div" | "0 mod 0 :: 'a :: semiring_numeral_div" |
- "0 div 1 :: 'a :: semiring_numeral_div" | "0 mod 1 :: 'a :: semiring_numeral_div" |
+ ("0 div 0 :: 'a :: unique_euclidean_semiring_numeral" | "0 mod 0 :: 'a :: unique_euclidean_semiring_numeral" |
+ "0 div 1 :: 'a :: unique_euclidean_semiring_numeral" | "0 mod 1 :: 'a :: unique_euclidean_semiring_numeral" |
"0 div - 1 :: int" | "0 mod - 1 :: int" |
- "0 div numeral b :: 'a :: semiring_numeral_div" | "0 mod numeral b :: 'a :: semiring_numeral_div" |
+ "0 div numeral b :: 'a :: unique_euclidean_semiring_numeral" | "0 mod numeral b :: 'a :: unique_euclidean_semiring_numeral" |
"0 div - numeral b :: int" | "0 mod - numeral b :: int" |
- "1 div 0 :: 'a :: semiring_numeral_div" | "1 mod 0 :: 'a :: semiring_numeral_div" |
- "1 div 1 :: 'a :: semiring_numeral_div" | "1 mod 1 :: 'a :: semiring_numeral_div" |
+ "1 div 0 :: 'a :: unique_euclidean_semiring_numeral" | "1 mod 0 :: 'a :: unique_euclidean_semiring_numeral" |
+ "1 div 1 :: 'a :: unique_euclidean_semiring_numeral" | "1 mod 1 :: 'a :: unique_euclidean_semiring_numeral" |
"1 div - 1 :: int" | "1 mod - 1 :: int" |
- "1 div numeral b :: 'a :: semiring_numeral_div" | "1 mod numeral b :: 'a :: semiring_numeral_div" |
+ "1 div numeral b :: 'a :: unique_euclidean_semiring_numeral" | "1 mod numeral b :: 'a :: unique_euclidean_semiring_numeral" |
"1 div - numeral b :: int" |"1 mod - numeral b :: int" |
"- 1 div 0 :: int" | "- 1 mod 0 :: int" | "- 1 div 1 :: int" | "- 1 mod 1 :: int" |
"- 1 div - 1 :: int" | "- 1 mod - 1 :: int" | "- 1 div numeral b :: int" | "- 1 mod numeral b :: int" |
"- 1 div - numeral b :: int" | "- 1 mod - numeral b :: int" |
- "numeral a div 0 :: 'a :: semiring_numeral_div" | "numeral a mod 0 :: 'a :: semiring_numeral_div" |
- "numeral a div 1 :: 'a :: semiring_numeral_div" | "numeral a mod 1 :: 'a :: semiring_numeral_div" |
+ "numeral a div 0 :: 'a :: unique_euclidean_semiring_numeral" | "numeral a mod 0 :: 'a :: unique_euclidean_semiring_numeral" |
+ "numeral a div 1 :: 'a :: unique_euclidean_semiring_numeral" | "numeral a mod 1 :: 'a :: unique_euclidean_semiring_numeral" |
"numeral a div - 1 :: int" | "numeral a mod - 1 :: int" |
- "numeral a div numeral b :: 'a :: semiring_numeral_div" | "numeral a mod numeral b :: 'a :: semiring_numeral_div" |
+ "numeral a div numeral b :: 'a :: unique_euclidean_semiring_numeral" | "numeral a mod numeral b :: 'a :: unique_euclidean_semiring_numeral" |
"numeral a div - numeral b :: int" | "numeral a mod - numeral b :: int" |
"- numeral a div 0 :: int" | "- numeral a mod 0 :: int" |
"- numeral a div 1 :: int" | "- numeral a mod 1 :: int" |
@@ -2818,7 +2343,7 @@
code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
lemma dvd_eq_mod_eq_0_numeral:
- "numeral x dvd (numeral y :: 'a) \<longleftrightarrow> numeral y mod numeral x = (0 :: 'a::semiring_div)"
+ "numeral x dvd (numeral y :: 'a) \<longleftrightarrow> numeral y mod numeral x = (0 :: 'a::semidom_modulo)"
by (fact dvd_eq_mod_eq_0)
declare minus_div_mult_eq_mod [symmetric, nitpick_unfold]
--- a/src/HOL/Enum.thy Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Enum.thy Sun Oct 08 22:28:21 2017 +0200
@@ -683,7 +683,7 @@
instance finite_2 :: complete_linorder ..
-instantiation finite_2 :: "{field, idom_abs_sgn}" begin
+instantiation finite_2 :: "{field, idom_abs_sgn, idom_modulo}" begin
definition [simp]: "0 = a\<^sub>1"
definition [simp]: "1 = a\<^sub>2"
definition "x + y = (case (x, y) of (a\<^sub>1, a\<^sub>1) \<Rightarrow> a\<^sub>1 | (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>1 | _ \<Rightarrow> a\<^sub>2)"
@@ -692,12 +692,15 @@
definition "x * y = (case (x, y) of (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
definition "inverse = (\<lambda>x :: finite_2. x)"
definition "divide = (op * :: finite_2 \<Rightarrow> _)"
+definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
definition "abs = (\<lambda>x :: finite_2. x)"
definition "sgn = (\<lambda>x :: finite_2. x)"
instance
by standard
- (simp_all add: plus_finite_2_def uminus_finite_2_def minus_finite_2_def times_finite_2_def
- inverse_finite_2_def divide_finite_2_def abs_finite_2_def sgn_finite_2_def
+ (simp_all add: plus_finite_2_def uminus_finite_2_def minus_finite_2_def
+ times_finite_2_def
+ inverse_finite_2_def divide_finite_2_def modulo_finite_2_def
+ abs_finite_2_def sgn_finite_2_def
split: finite_2.splits)
end
@@ -709,14 +712,15 @@
"x dvd y \<longleftrightarrow> x = a\<^sub>2 \<or> y = a\<^sub>1"
by (auto simp add: dvd_def times_finite_2_def split: finite_2.splits)
-instantiation finite_2 :: "{ring_div, normalization_semidom}" begin
+instantiation finite_2 :: unique_euclidean_semiring begin
definition [simp]: "normalize = (id :: finite_2 \<Rightarrow> _)"
definition [simp]: "unit_factor = (id :: finite_2 \<Rightarrow> _)"
-definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
+definition [simp]: "euclidean_size x = (case x of a\<^sub>1 \<Rightarrow> 0 | a\<^sub>2 \<Rightarrow> 1)"
+definition [simp]: "uniqueness_constraint = (\<top> :: finite_2 \<Rightarrow> _)"
instance
by standard
- (simp_all add: dvd_finite_2_unfold times_finite_2_def
- divide_finite_2_def modulo_finite_2_def split: finite_2.splits)
+ (auto simp add: divide_finite_2_def times_finite_2_def dvd_finite_2_unfold
+ split: finite_2.splits)
end
@@ -826,7 +830,7 @@
instance finite_3 :: complete_linorder ..
-instantiation finite_3 :: "{field, idom_abs_sgn}" begin
+instantiation finite_3 :: "{field, idom_abs_sgn, idom_modulo}" begin
definition [simp]: "0 = a\<^sub>1"
definition [simp]: "1 = a\<^sub>2"
definition
@@ -839,12 +843,15 @@
definition "x * y = (case (x, y) of (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>2 | (a\<^sub>3, a\<^sub>3) \<Rightarrow> a\<^sub>2 | (a\<^sub>2, a\<^sub>3) \<Rightarrow> a\<^sub>3 | (a\<^sub>3, a\<^sub>2) \<Rightarrow> a\<^sub>3 | _ \<Rightarrow> a\<^sub>1)"
definition "inverse = (\<lambda>x :: finite_3. x)"
definition "x div y = x * inverse (y :: finite_3)"
+definition "x mod y = (case y of a\<^sub>1 \<Rightarrow> x | _ \<Rightarrow> a\<^sub>1)"
definition "abs = (\<lambda>x. case x of a\<^sub>3 \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> x)"
definition "sgn = (\<lambda>x :: finite_3. x)"
instance
by standard
- (simp_all add: plus_finite_3_def uminus_finite_3_def minus_finite_3_def times_finite_3_def
- inverse_finite_3_def divide_finite_3_def abs_finite_3_def sgn_finite_3_def
+ (simp_all add: plus_finite_3_def uminus_finite_3_def minus_finite_3_def
+ times_finite_3_def
+ inverse_finite_3_def divide_finite_3_def modulo_finite_3_def
+ abs_finite_3_def sgn_finite_3_def
less_finite_3_def
split: finite_3.splits)
end
@@ -857,20 +864,21 @@
"x dvd y \<longleftrightarrow> x = a\<^sub>2 \<or> x = a\<^sub>3 \<or> y = a\<^sub>1"
by (cases x) (auto simp add: dvd_def times_finite_3_def split: finite_3.splits)
-instantiation finite_3 :: "{ring_div, normalization_semidom}" begin
-definition "normalize x = (case x of a\<^sub>3 \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> x)"
+instantiation finite_3 :: unique_euclidean_semiring begin
+definition [simp]: "normalize x = (case x of a\<^sub>3 \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> x)"
definition [simp]: "unit_factor = (id :: finite_3 \<Rightarrow> _)"
-definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | (a\<^sub>3, a\<^sub>1) \<Rightarrow> a\<^sub>3 | _ \<Rightarrow> a\<^sub>1)"
-instance
- by standard
- (auto simp add: finite_3_not_eq_unfold plus_finite_3_def
- dvd_finite_3_unfold times_finite_3_def inverse_finite_3_def
- normalize_finite_3_def divide_finite_3_def modulo_finite_3_def
- split: finite_3.splits)
+definition [simp]: "euclidean_size x = (case x of a\<^sub>1 \<Rightarrow> 0 | _ \<Rightarrow> 1)"
+definition [simp]: "uniqueness_constraint = (\<top> :: finite_3 \<Rightarrow> _)"
+instance proof
+ fix x :: finite_3
+ assume "x \<noteq> 0"
+ then show "is_unit (unit_factor x)"
+ by (cases x) (simp_all add: dvd_finite_3_unfold)
+qed (auto simp add: divide_finite_3_def times_finite_3_def
+ dvd_finite_3_unfold inverse_finite_3_def plus_finite_3_def
+ split: finite_3.splits)
end
-
-
hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3
datatype (plugins only: code "quickcheck" extraction) finite_4 =
--- a/src/HOL/Euclidean_Division.thy Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Euclidean_Division.thy Sun Oct 08 22:28:21 2017 +0200
@@ -201,6 +201,388 @@
class euclidean_ring = idom_modulo + euclidean_semiring
+subsection \<open>Euclidean (semi)rings with cancel rules\<close>
+
+class euclidean_semiring_cancel = euclidean_semiring +
+ assumes 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"
+begin
+
+lemma div_mult_self2 [simp]:
+ assumes "b \<noteq> 0"
+ shows "(a + b * c) div b = c + a div b"
+ using assms div_mult_self1 [of b a c] by (simp add: mult.commute)
+
+lemma div_mult_self3 [simp]:
+ assumes "b \<noteq> 0"
+ shows "(c * b + a) div b = c + a div b"
+ using assms by (simp add: add.commute)
+
+lemma div_mult_self4 [simp]:
+ assumes "b \<noteq> 0"
+ shows "(b * c + a) div b = c + a div b"
+ using assms by (simp add: add.commute)
+
+lemma mod_mult_self1 [simp]: "(a + c * b) mod b = a mod b"
+proof (cases "b = 0")
+ case True then show ?thesis by simp
+next
+ case False
+ have "a + c * b = (a + c * b) div b * b + (a + c * b) mod b"
+ by (simp add: div_mult_mod_eq)
+ also from False div_mult_self1 [of b a c] have
+ "\<dots> = (c + a div b) * b + (a + c * b) mod b"
+ by (simp add: algebra_simps)
+ finally have "a = a div b * b + (a + c * b) mod b"
+ by (simp add: add.commute [of a] add.assoc distrib_right)
+ then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b"
+ by (simp add: div_mult_mod_eq)
+ then show ?thesis by simp
+qed
+
+lemma mod_mult_self2 [simp]:
+ "(a + b * c) mod b = a mod b"
+ by (simp add: mult.commute [of b])
+
+lemma mod_mult_self3 [simp]:
+ "(c * b + a) mod b = a mod b"
+ by (simp add: add.commute)
+
+lemma mod_mult_self4 [simp]:
+ "(b * c + a) mod b = a mod b"
+ by (simp add: add.commute)
+
+lemma mod_mult_self1_is_0 [simp]:
+ "b * a mod b = 0"
+ using mod_mult_self2 [of 0 b a] by simp
+
+lemma mod_mult_self2_is_0 [simp]:
+ "a * b mod b = 0"
+ using mod_mult_self1 [of 0 a b] by simp
+
+lemma div_add_self1:
+ assumes "b \<noteq> 0"
+ shows "(b + a) div b = a div b + 1"
+ using assms div_mult_self1 [of b a 1] by (simp add: add.commute)
+
+lemma div_add_self2:
+ assumes "b \<noteq> 0"
+ shows "(a + b) div b = a div b + 1"
+ using assms div_add_self1 [of b a] by (simp add: add.commute)
+
+lemma mod_add_self1 [simp]:
+ "(b + a) mod b = a mod b"
+ using mod_mult_self1 [of a 1 b] by (simp add: add.commute)
+
+lemma mod_add_self2 [simp]:
+ "(a + b) mod b = a mod b"
+ using mod_mult_self1 [of a 1 b] by simp
+
+lemma mod_div_trivial [simp]:
+ "a mod b div b = 0"
+proof (cases "b = 0")
+ assume "b = 0"
+ thus ?thesis by simp
+next
+ assume "b \<noteq> 0"
+ 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_mult_eq)
+ also have "\<dots> = a div b + 0"
+ by simp
+ finally show ?thesis
+ by (rule add_left_imp_eq)
+qed
+
+lemma mod_mod_trivial [simp]:
+ "a mod b mod b = a mod b"
+proof -
+ 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_mult_eq)
+ finally show ?thesis .
+qed
+
+lemma mod_mod_cancel:
+ assumes "c dvd b"
+ shows "a mod b mod c = a mod c"
+proof -
+ from \<open>c dvd b\<close> obtain k where "b = c * k"
+ by (rule dvdE)
+ have "a mod b mod c = a mod (c * k) mod c"
+ by (simp only: \<open>b = c * k\<close>)
+ also have "\<dots> = (a mod (c * k) + a div (c * k) * k * c) mod c"
+ by (simp only: mod_mult_self1)
+ also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c"
+ by (simp only: ac_simps)
+ also have "\<dots> = a mod c"
+ by (simp only: div_mult_mod_eq)
+ finally show ?thesis .
+qed
+
+lemma div_mult_mult2 [simp]:
+ "c \<noteq> 0 \<Longrightarrow> (a * c) div (b * c) = a div b"
+ by (drule div_mult_mult1) (simp add: mult.commute)
+
+lemma div_mult_mult1_if [simp]:
+ "(c * a) div (c * b) = (if c = 0 then 0 else a div b)"
+ by simp_all
+
+lemma mod_mult_mult1:
+ "(c * a) mod (c * b) = c * (a mod b)"
+proof (cases "c = 0")
+ case True then show ?thesis by simp
+next
+ case False
+ from div_mult_mod_eq
+ have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" .
+ with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b)
+ = c * a + c * (a mod b)" by (simp add: algebra_simps)
+ with div_mult_mod_eq show ?thesis by simp
+qed
+
+lemma mod_mult_mult2:
+ "(a * c) mod (b * c) = (a mod b) * c"
+ using mod_mult_mult1 [of c a b] by (simp add: mult.commute)
+
+lemma mult_mod_left: "(a mod b) * c = (a * c) mod (b * c)"
+ by (fact mod_mult_mult2 [symmetric])
+
+lemma mult_mod_right: "c * (a mod b) = (c * a) mod (c * b)"
+ by (fact mod_mult_mult1 [symmetric])
+
+lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
+ unfolding dvd_def by (auto simp add: mod_mult_mult1)
+
+lemma div_plus_div_distrib_dvd_left:
+ "c dvd a \<Longrightarrow> (a + b) div c = a div c + b div c"
+ by (cases "c = 0") (auto elim: dvdE)
+
+lemma div_plus_div_distrib_dvd_right:
+ "c dvd b \<Longrightarrow> (a + b) div c = a div c + b div c"
+ using div_plus_div_distrib_dvd_left [of c b a]
+ by (simp add: ac_simps)
+
+named_theorems mod_simps
+
+text \<open>Addition respects modular equivalence.\<close>
+
+lemma mod_add_left_eq [mod_simps]:
+ "(a mod c + b) mod c = (a + b) mod c"
+proof -
+ have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
+ by (simp only: div_mult_mod_eq)
+ also have "\<dots> = (a mod c + b + a div c * c) mod c"
+ by (simp only: ac_simps)
+ also have "\<dots> = (a mod c + b) mod c"
+ by (rule mod_mult_self1)
+ finally show ?thesis
+ by (rule sym)
+qed
+
+lemma mod_add_right_eq [mod_simps]:
+ "(a + b mod c) mod c = (a + b) mod c"
+ using mod_add_left_eq [of b c a] by (simp add: ac_simps)
+
+lemma mod_add_eq:
+ "(a mod c + b mod c) mod c = (a + b) mod c"
+ by (simp add: mod_add_left_eq mod_add_right_eq)
+
+lemma mod_sum_eq [mod_simps]:
+ "(\<Sum>i\<in>A. f i mod a) mod a = sum f A mod a"
+proof (induct A rule: infinite_finite_induct)
+ case (insert i A)
+ then have "(\<Sum>i\<in>insert i A. f i mod a) mod a
+ = (f i mod a + (\<Sum>i\<in>A. f i mod a)) mod a"
+ by simp
+ also have "\<dots> = (f i + (\<Sum>i\<in>A. f i mod a) mod a) mod a"
+ by (simp add: mod_simps)
+ also have "\<dots> = (f i + (\<Sum>i\<in>A. f i) mod a) mod a"
+ by (simp add: insert.hyps)
+ finally show ?case
+ by (simp add: insert.hyps mod_simps)
+qed simp_all
+
+lemma mod_add_cong:
+ assumes "a mod c = a' mod c"
+ assumes "b mod c = b' mod c"
+ shows "(a + b) mod c = (a' + b') mod c"
+proof -
+ have "(a mod c + b mod c) mod c = (a' mod c + b' mod c) mod c"
+ unfolding assms ..
+ then show ?thesis
+ by (simp add: mod_add_eq)
+qed
+
+text \<open>Multiplication respects modular equivalence.\<close>
+
+lemma mod_mult_left_eq [mod_simps]:
+ "((a mod c) * b) mod c = (a * b) mod c"
+proof -
+ have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
+ by (simp only: div_mult_mod_eq)
+ also have "\<dots> = (a mod c * b + a div c * b * c) mod c"
+ by (simp only: algebra_simps)
+ also have "\<dots> = (a mod c * b) mod c"
+ by (rule mod_mult_self1)
+ finally show ?thesis
+ by (rule sym)
+qed
+
+lemma mod_mult_right_eq [mod_simps]:
+ "(a * (b mod c)) mod c = (a * b) mod c"
+ using mod_mult_left_eq [of b c a] by (simp add: ac_simps)
+
+lemma mod_mult_eq:
+ "((a mod c) * (b mod c)) mod c = (a * b) mod c"
+ by (simp add: mod_mult_left_eq mod_mult_right_eq)
+
+lemma mod_prod_eq [mod_simps]:
+ "(\<Prod>i\<in>A. f i mod a) mod a = prod f A mod a"
+proof (induct A rule: infinite_finite_induct)
+ case (insert i A)
+ then have "(\<Prod>i\<in>insert i A. f i mod a) mod a
+ = (f i mod a * (\<Prod>i\<in>A. f i mod a)) mod a"
+ by simp
+ also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i mod a) mod a)) mod a"
+ by (simp add: mod_simps)
+ also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i) mod a)) mod a"
+ by (simp add: insert.hyps)
+ finally show ?case
+ by (simp add: insert.hyps mod_simps)
+qed simp_all
+
+lemma mod_mult_cong:
+ assumes "a mod c = a' mod c"
+ assumes "b mod c = b' mod c"
+ shows "(a * b) mod c = (a' * b') mod c"
+proof -
+ have "(a mod c * (b mod c)) mod c = (a' mod c * (b' mod c)) mod c"
+ unfolding assms ..
+ then show ?thesis
+ by (simp add: mod_mult_eq)
+qed
+
+text \<open>Exponentiation respects modular equivalence.\<close>
+
+lemma power_mod [mod_simps]:
+ "((a mod b) ^ n) mod b = (a ^ n) mod b"
+proof (induct n)
+ case 0
+ then show ?case by simp
+next
+ case (Suc n)
+ have "(a mod b) ^ Suc n mod b = (a mod b) * ((a mod b) ^ n mod b) mod b"
+ by (simp add: mod_mult_right_eq)
+ with Suc show ?case
+ by (simp add: mod_mult_left_eq mod_mult_right_eq)
+qed
+
+end
+
+
+class euclidean_ring_cancel = euclidean_ring + euclidean_semiring_cancel
+begin
+
+subclass idom_divide ..
+
+lemma div_minus_minus [simp]: "(- a) div (- b) = a div b"
+ using div_mult_mult1 [of "- 1" a b] by simp
+
+lemma mod_minus_minus [simp]: "(- a) mod (- b) = - (a mod b)"
+ using mod_mult_mult1 [of "- 1" a b] by simp
+
+lemma div_minus_right: "a div (- b) = (- a) div b"
+ using div_minus_minus [of "- a" b] by simp
+
+lemma mod_minus_right: "a mod (- b) = - ((- a) mod b)"
+ using mod_minus_minus [of "- a" b] by simp
+
+lemma div_minus1_right [simp]: "a div (- 1) = - a"
+ using div_minus_right [of a 1] by simp
+
+lemma mod_minus1_right [simp]: "a mod (- 1) = 0"
+ using mod_minus_right [of a 1] by simp
+
+text \<open>Negation respects modular equivalence.\<close>
+
+lemma mod_minus_eq [mod_simps]:
+ "(- (a mod b)) mod b = (- a) mod b"
+proof -
+ have "(- a) mod b = (- (a div b * b + a mod b)) mod b"
+ by (simp only: div_mult_mod_eq)
+ also have "\<dots> = (- (a mod b) + - (a div b) * b) mod b"
+ by (simp add: ac_simps)
+ also have "\<dots> = (- (a mod b)) mod b"
+ by (rule mod_mult_self1)
+ finally show ?thesis
+ by (rule sym)
+qed
+
+lemma mod_minus_cong:
+ assumes "a mod b = a' mod b"
+ shows "(- a) mod b = (- a') mod b"
+proof -
+ have "(- (a mod b)) mod b = (- (a' mod b)) mod b"
+ unfolding assms ..
+ then show ?thesis
+ by (simp add: mod_minus_eq)
+qed
+
+text \<open>Subtraction respects modular equivalence.\<close>
+
+lemma mod_diff_left_eq [mod_simps]:
+ "(a mod c - b) mod c = (a - b) mod c"
+ using mod_add_cong [of a c "a mod c" "- b" "- b"]
+ by simp
+
+lemma mod_diff_right_eq [mod_simps]:
+ "(a - b mod c) mod c = (a - b) mod c"
+ using mod_add_cong [of a c a "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
+ by simp
+
+lemma mod_diff_eq:
+ "(a mod c - b mod c) mod c = (a - b) mod c"
+ using mod_add_cong [of a c "a mod c" "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
+ by simp
+
+lemma mod_diff_cong:
+ assumes "a mod c = a' mod c"
+ assumes "b mod c = b' mod c"
+ shows "(a - b) mod c = (a' - b') mod c"
+ using assms mod_add_cong [of a c a' "- b" "- b'"] mod_minus_cong [of b c "b'"]
+ by simp
+
+lemma minus_mod_self2 [simp]:
+ "(a - b) mod b = a mod b"
+ using mod_diff_right_eq [of a b b]
+ by (simp add: mod_diff_right_eq)
+
+lemma minus_mod_self1 [simp]:
+ "(b - a) mod b = - a mod b"
+ using mod_add_self2 [of "- a" b] by simp
+
+lemma mod_eq_dvd_iff:
+ "a mod c = b mod c \<longleftrightarrow> c dvd a - b" (is "?P \<longleftrightarrow> ?Q")
+proof
+ assume ?P
+ then have "(a mod c - b mod c) mod c = 0"
+ by simp
+ then show ?Q
+ by (simp add: dvd_eq_mod_eq_0 mod_simps)
+next
+ assume ?Q
+ then obtain d where d: "a - b = c * d" ..
+ then have "a = c * d + b"
+ by (simp add: algebra_simps)
+ then show ?P by simp
+qed
+
+end
+
+
subsection \<open>Uniquely determined division\<close>
class unique_euclidean_semiring = euclidean_semiring +
@@ -284,8 +666,53 @@
by simp
qed
+subclass euclidean_semiring_cancel
+proof
+ show "(a + c * b) div b = c + a div b" if "b \<noteq> 0" for a b c
+ proof (cases a b rule: divmod_cases)
+ case by0
+ with \<open>b \<noteq> 0\<close> 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 \<noteq> 0" for a b c
+ proof (cases a b rule: divmod_cases)
+ case by0
+ then show ?thesis
+ by simp
+ next
+ case (divides q)
+ with \<open>c \<noteq> 0\<close> show ?thesis
+ by (simp add: mult.left_commute [of c])
+ next
+ case (remainder q r)
+ from \<open>b \<noteq> 0\<close> \<open>c \<noteq> 0\<close> have "b * c \<noteq> 0"
+ by simp
+ from remainder \<open>c \<noteq> 0\<close>
+ 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 \<open>b * c \<noteq> 0\<close> in simp)
+ qed
+qed
+
end
class unique_euclidean_ring = euclidean_ring + unique_euclidean_semiring
+begin
+
+subclass euclidean_ring_cancel ..
end
+
+end
--- a/src/HOL/Factorial.thy Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Factorial.thy Sun Oct 08 22:28:21 2017 +0200
@@ -130,11 +130,11 @@
lemma fact_ge_self: "fact n \<ge> n"
by (cases "n = 0") (simp_all add: dvd_imp_le dvd_fact)
-lemma fact_dvd: "n \<le> m \<Longrightarrow> fact n dvd (fact m :: 'a::{semiring_div,linordered_semidom})"
+lemma fact_dvd: "n \<le> m \<Longrightarrow> fact n dvd (fact m :: 'a::linordered_semidom)"
by (induct m) (auto simp: le_Suc_eq)
-lemma fact_mod: "m \<le> n \<Longrightarrow> fact n mod (fact m :: 'a::{semiring_div,linordered_semidom}) = 0"
- by (auto simp add: fact_dvd)
+lemma fact_mod: "m \<le> n \<Longrightarrow> fact n mod (fact m :: 'a::{semidom_modulo, linordered_semidom}) = 0"
+ by (simp add: mod_eq_0_iff_dvd fact_dvd)
lemma fact_div_fact:
assumes "m \<ge> n"
--- a/src/HOL/Nonstandard_Analysis/StarDef.thy Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Nonstandard_Analysis/StarDef.thy Sun Oct 08 22:28:21 2017 +0200
@@ -772,9 +772,6 @@
instance star :: (semidom_divide) semidom_divide
by (intro_classes; transfer) simp_all
-instance star :: (semiring_div) semiring_div
- by (intro_classes; transfer) (simp_all add: div_mult_mod_eq)
-
instance star :: (ring_no_zero_divisors) ring_no_zero_divisors ..
instance star :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors ..
instance star :: (idom) idom ..
@@ -821,6 +818,22 @@
instance star :: (linordered_field) linordered_field ..
+instance star :: (algebraic_semidom) algebraic_semidom ..
+
+instantiation star :: (normalization_semidom) normalization_semidom
+begin
+
+definition unit_factor_star :: "'a star \<Rightarrow> 'a star"
+ where [transfer_unfold]: "unit_factor_star = *f* unit_factor"
+
+definition normalize_star :: "'a star \<Rightarrow> 'a star"
+ where [transfer_unfold]: "normalize_star = *f* normalize"
+
+instance
+ by standard (transfer; simp add: is_unit_unit_factor unit_factor_mult)+
+
+end
+
subsection \<open>Power\<close>
@@ -912,49 +925,6 @@
apply (transfer, erule odd_ex_decrement)
done
-instance star :: (semiring_div_parity) semiring_div_parity
- apply intro_classes
- apply (transfer, rule parity)
- apply (transfer, rule one_mod_two_eq_one)
- apply (transfer, rule zero_not_eq_two)
- done
-
-instantiation star :: (semiring_numeral_div) semiring_numeral_div
-begin
-
-definition divmod_star :: "num \<Rightarrow> num \<Rightarrow> 'a star \<times> 'a star"
- where divmod_star_def: "divmod_star m n = (numeral m div numeral n, numeral m mod numeral n)"
-
-definition divmod_step_star :: "num \<Rightarrow> 'a star \<times> 'a star \<Rightarrow> 'a star \<times> 'a star"
- where "divmod_step_star l qr =
- (let (q, r) = qr
- in if r \<ge> numeral l then (2 * q + 1, r - numeral l) else (2 * q, r))"
-
-instance
-proof
- show "divmod m n = (numeral m div numeral n :: 'a star, numeral m mod numeral n)" for m n
- by (fact divmod_star_def)
- show "divmod_step l qr =
- (let (q, r) = qr
- in if r \<ge> numeral l then (2 * q + 1, r - numeral l) else (2 * q, r))"
- for l and qr :: "'a star \<times> 'a star"
- by (fact divmod_step_star_def)
-qed (transfer,
- fact
- semiring_numeral_div_class.div_less
- semiring_numeral_div_class.mod_less
- semiring_numeral_div_class.div_positive
- semiring_numeral_div_class.mod_less_eq_dividend
- semiring_numeral_div_class.pos_mod_bound
- semiring_numeral_div_class.pos_mod_sign
- semiring_numeral_div_class.mod_mult2_eq
- semiring_numeral_div_class.div_mult2_eq
- semiring_numeral_div_class.discrete)+
-
-end
-
-declare divmod_algorithm_code [where ?'a = "'a::semiring_numeral_div star", code]
-
subsection \<open>Finite class\<close>
--- a/src/HOL/Numeral_Simprocs.thy Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Numeral_Simprocs.thy Sun Oct 08 22:28:21 2017 +0200
@@ -169,8 +169,8 @@
(* TODO: remove comm_ring_1 constraint if possible *)
simproc_setup int_div_cancel_numeral_factors
- ("((l::'a::{semiring_div,comm_ring_1,ring_char_0}) * m) div n"
- |"(l::'a::{semiring_div,comm_ring_1,ring_char_0}) div (m * n)") =
+ ("((l::'a::{euclidean_semiring_cancel,comm_ring_1,ring_char_0}) * m) div n"
+ |"(l::'a::{euclidean_semiring_cancel,comm_ring_1,ring_char_0}) div (m * n)") =
\<open>fn phi => Numeral_Simprocs.div_cancel_numeral_factor\<close>
simproc_setup divide_cancel_numeral_factor
@@ -194,13 +194,13 @@
\<open>fn phi => Numeral_Simprocs.less_cancel_factor\<close>
simproc_setup int_div_cancel_factor
- ("((l::'a::semiring_div) * m) div n"
- |"(l::'a::semiring_div) div (m * n)") =
+ ("((l::'a::euclidean_semiring_cancel) * m) div n"
+ |"(l::'a::euclidean_semiring_cancel) div (m * n)") =
\<open>fn phi => Numeral_Simprocs.div_cancel_factor\<close>
simproc_setup int_mod_cancel_factor
- ("((l::'a::semiring_div) * m) mod n"
- |"(l::'a::semiring_div) mod (m * n)") =
+ ("((l::'a::euclidean_semiring_cancel) * m) mod n"
+ |"(l::'a::euclidean_semiring_cancel) mod (m * n)") =
\<open>fn phi => Numeral_Simprocs.mod_cancel_factor\<close>
simproc_setup dvd_cancel_factor
--- a/src/HOL/Rat.thy Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Rat.thy Sun Oct 08 22:28:21 2017 +0200
@@ -199,12 +199,12 @@
(* We cannot state these two rules earlier because of pending sort hypotheses *)
lemma div_add_self1_no_field [simp]:
- assumes "NO_MATCH (x :: 'b :: field) b" "(b :: 'a :: semiring_div) \<noteq> 0"
+ assumes "NO_MATCH (x :: 'b :: field) b" "(b :: 'a :: euclidean_semiring_cancel) \<noteq> 0"
shows "(b + a) div b = a div b + 1"
using assms(2) by (fact div_add_self1)
lemma div_add_self2_no_field [simp]:
- assumes "NO_MATCH (x :: 'b :: field) b" "(b :: 'a :: semiring_div) \<noteq> 0"
+ assumes "NO_MATCH (x :: 'b :: field) b" "(b :: 'a :: euclidean_semiring_cancel) \<noteq> 0"
shows "(a + b) div b = a div b + 1"
using assms(2) by (fact div_add_self2)
--- a/src/HOL/ex/Simproc_Tests.thy Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/ex/Simproc_Tests.thy Sun Oct 08 22:28:21 2017 +0200
@@ -199,7 +199,7 @@
subsection \<open>\<open>int_div_cancel_numeral_factors\<close>\<close>
notepad begin
- fix x y z :: "'a::{semiring_div,comm_ring_1,ring_char_0}"
+ fix x y z :: "'a::{unique_euclidean_semiring,comm_ring_1,ring_char_0}"
{
assume "(3*x) div (4*y) = z" have "(9*x) div (12*y) = z"
by (tactic \<open>test @{context} [@{simproc int_div_cancel_numeral_factors}]\<close>) fact
@@ -325,7 +325,7 @@
subsection \<open>\<open>int_div_cancel_factor\<close>\<close>
notepad begin
- fix a b c d k uu x y :: "'a::semiring_div"
+ fix a b c d k uu x y :: "'a::unique_euclidean_semiring"
{
assume "(if k = 0 then 0 else x div y) = uu"
have "(x*k) div (k*y) = uu"
--- a/src/HOL/ex/Word_Type.thy Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/ex/Word_Type.thy Sun Oct 08 22:28:21 2017 +0200
@@ -11,7 +11,7 @@
subsection \<open>Truncating bit representations of numeric types\<close>
-class semiring_bits = semiring_div_parity +
+class semiring_bits = unique_euclidean_semiring_parity +
assumes semiring_bits: "(1 + 2 * a) mod of_nat (2 * n) = 1 + 2 * (a mod of_nat n)"
begin