--- a/src/HOL/Euclidean_Division.thy Sat Apr 13 15:13:43 2019 +0200
+++ b/src/HOL/Euclidean_Division.thy Sat Apr 13 15:14:15 2019 +0200
@@ -165,31 +165,25 @@
subsection \<open>Euclidean (semi)rings with cancel rules\<close>
-class euclidean_semiring_cancel = euclidean_semiring + semidom_divide_cancel
+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
-context
- fixes b
- assumes "b \<noteq> 0"
-begin
-
-lemma div_mult_self1 [simp]:
- "(a + c * b) div b = c + a div b"
- using \<open>b \<noteq> 0\<close> by (rule div_mult_self1)
-
lemma div_mult_self2 [simp]:
- "(a + b * c) div b = c + a div b"
- using \<open>b \<noteq> 0\<close> by (rule div_mult_self2)
+ 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]:
- "(c * b + a) div b = c + a div b"
- using \<open>b \<noteq> 0\<close> by (rule div_mult_self3)
+ 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]:
- "(b * c + a) div b = c + a div b"
- using \<open>b \<noteq> 0\<close> by (rule div_mult_self4)
-
-end
+ 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")
@@ -200,7 +194,7 @@
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)
+ 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"
@@ -228,6 +222,16 @@
"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)
@@ -280,6 +284,14 @@
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")
@@ -436,14 +448,23 @@
class euclidean_ring_cancel = euclidean_ring + euclidean_semiring_cancel
begin
-subclass idom_divide_cancel ..
+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
--- a/src/HOL/Fields.thy Sat Apr 13 15:13:43 2019 +0200
+++ b/src/HOL/Fields.thy Sat Apr 13 15:14:15 2019 +0200
@@ -378,42 +378,30 @@
by (simp add: divide_inverse)
qed
-subclass idom_divide_cancel
-proof
- fix a b c
- assume [simp]: "c \<noteq> 0"
- show "(c * a) / (c * b) = a / b"
- proof (cases "b = 0")
- case True then show ?thesis
- by simp
- next
- case False
- then have "(c * a) / (c * b) = c * a * (inverse b * inverse c)"
- by (simp add: divide_inverse nonzero_inverse_mult_distrib)
- also have "... = a * inverse b * (inverse c * c)"
- by (simp only: ac_simps)
- also have "... = a * inverse b" by simp
- finally show ?thesis by (simp add: divide_inverse)
- qed
-next
- fix a b c
- assume "b \<noteq> 0"
- have "((a * inverse b) * b + c * b) = (c + a * inverse b) * b"
- using distrib [of c "a * inverse b" b] by (simp add: ac_simps)
- also have "(a * inverse b) * b = a"
- using \<open>b \<noteq> 0\<close> by (simp add: ac_simps)
- finally show "(a + c * b) / b = c + a / b"
- using \<open>b \<noteq> 0\<close> by (simp add: ac_simps divide_inverse [symmetric])
-qed
-
-lemmas nonzero_mult_divide_mult_cancel_left = div_mult_mult1 \<comment> \<open>duplicate\<close>
-lemmas nonzero_mult_divide_mult_cancel_right = div_mult_mult2 \<comment> \<open>duplicate\<close>
-
text\<open>There is no slick version using division by zero.\<close>
lemma inverse_add:
"a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a + inverse b = (a + b) * inverse a * inverse b"
by (simp add: division_ring_inverse_add ac_simps)
+lemma nonzero_mult_divide_mult_cancel_left [simp]:
+ assumes [simp]: "c \<noteq> 0"
+ shows "(c * a) / (c * b) = a / b"
+proof (cases "b = 0")
+ case True then show ?thesis by simp
+next
+ case False
+ then have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
+ by (simp add: divide_inverse nonzero_inverse_mult_distrib)
+ also have "... = a * inverse b * (inverse c * c)"
+ by (simp only: ac_simps)
+ also have "... = a * inverse b" by simp
+ finally show ?thesis by (simp add: divide_inverse)
+qed
+
+lemma nonzero_mult_divide_mult_cancel_right [simp]:
+ "c \<noteq> 0 \<Longrightarrow> (a * c) / (b * c) = a / b"
+ using nonzero_mult_divide_mult_cancel_left [of c a b] by (simp add: ac_simps)
+
lemma times_divide_eq_left [simp]: "(b / c) * a = (b * a) / c"
by (simp add: divide_inverse ac_simps)
--- a/src/HOL/Rings.thy Sat Apr 13 15:13:43 2019 +0200
+++ b/src/HOL/Rings.thy Sat Apr 13 15:14:15 2019 +0200
@@ -13,6 +13,8 @@
imports Groups Set Fun
begin
+subsection \<open>Semirings and rings\<close>
+
class semiring = ab_semigroup_add + semigroup_mult +
assumes distrib_right[algebra_simps]: "(a + b) * c = a * c + b * c"
assumes distrib_left[algebra_simps]: "a * (b + c) = a * b + a * c"
@@ -120,13 +122,14 @@
class semiring_1 = zero_neq_one + semiring_0 + monoid_mult
begin
-lemma (in semiring_1) of_bool_conj:
+lemma of_bool_conj:
"of_bool (P \<and> Q) = of_bool P * of_bool Q"
by auto
end
-text \<open>Abstract divisibility\<close>
+
+subsection \<open>Abstract divisibility\<close>
class dvd = times
begin
@@ -157,9 +160,9 @@
shows "a dvd c"
proof -
from assms obtain v where "b = a * v"
- by (auto elim!: dvdE)
+ by auto
moreover from assms obtain w where "c = b * w"
- by (auto elim!: dvdE)
+ by auto
ultimately have "c = a * (v * w)"
by (simp add: mult.assoc)
then show ?thesis ..
@@ -172,13 +175,13 @@
by (auto simp add: subset_iff intro: dvd_trans)
lemma one_dvd [simp]: "1 dvd a"
- by (auto intro!: dvdI)
-
-lemma dvd_mult [simp]: "a dvd c \<Longrightarrow> a dvd (b * c)"
- by (auto intro!: mult.left_commute dvdI elim!: dvdE)
-
-lemma dvd_mult2 [simp]: "a dvd b \<Longrightarrow> a dvd (b * c)"
- using dvd_mult [of a b c] by (simp add: ac_simps)
+ by (auto intro: dvdI)
+
+lemma dvd_mult [simp]: "a dvd (b * c)" if "a dvd c"
+ using that by rule (auto intro: mult.left_commute dvdI)
+
+lemma dvd_mult2 [simp]: "a dvd (b * c)" if "a dvd b"
+ using that dvd_mult [of a b c] by (simp add: ac_simps)
lemma dvd_triv_right [simp]: "a dvd b * a"
by (rule dvd_mult) (rule dvd_refl)
@@ -212,7 +215,7 @@
subclass semiring_1 ..
lemma dvd_0_left_iff [simp]: "0 dvd a \<longleftrightarrow> a = 0"
- by (auto intro: dvd_refl elim!: dvdE)
+ by auto
lemma dvd_0_right [iff]: "a dvd 0"
proof
@@ -372,7 +375,7 @@
subclass ring_1 ..
subclass comm_semiring_1_cancel
- by unfold_locales (simp add: algebra_simps)
+ by standard (simp add: algebra_simps)
lemma dvd_minus_iff [simp]: "x dvd - y \<longleftrightarrow> x dvd y"
proof
@@ -403,6 +406,9 @@
end
+
+subsection \<open>Towards integral domains\<close>
+
class semiring_no_zero_divisors = semiring_0 +
assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
begin
@@ -507,23 +513,19 @@
subclass ring_1_no_zero_divisors ..
-lemma dvd_mult_cancel_right [simp]: "a * c dvd b * c \<longleftrightarrow> c = 0 \<or> a dvd b"
+lemma dvd_mult_cancel_right [simp]:
+ "a * c dvd b * c \<longleftrightarrow> c = 0 \<or> a dvd b"
proof -
have "a * c dvd b * c \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
- unfolding dvd_def by (simp add: ac_simps)
+ by (auto simp add: ac_simps)
also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
- unfolding dvd_def by simp
+ by auto
finally show ?thesis .
qed
-lemma dvd_mult_cancel_left [simp]: "c * a dvd c * b \<longleftrightarrow> c = 0 \<or> a dvd b"
-proof -
- have "c * a dvd c * b \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
- unfolding dvd_def by (simp add: ac_simps)
- also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
- unfolding dvd_def by simp
- finally show ?thesis .
-qed
+lemma dvd_mult_cancel_left [simp]:
+ "c * a dvd c * b \<longleftrightarrow> c = 0 \<or> a dvd b"
+ using dvd_mult_cancel_right [of a c b] by (simp add: ac_simps)
lemma square_eq_iff: "a * a = b * b \<longleftrightarrow> a = b \<or> a = - b"
proof
@@ -633,17 +635,8 @@
end
-text \<open>
- The theory of partially ordered rings is taken from the books:
- \<^item> \<^emph>\<open>Lattice Theory\<close> by Garret Birkhoff, American Mathematical Society, 1979
- \<^item> \<^emph>\<open>Partially Ordered Algebraic Systems\<close>, Pergamon Press, 1963
-
- Most of the used notions can also be looked up in
- \<^item> \<^url>\<open>http://www.mathworld.com\<close> by Eric Weisstein et. al.
- \<^item> \<^emph>\<open>Algebra I\<close> by van der Waerden, Springer
-\<close>
-
-text \<open>Syntactic division operator\<close>
+
+subsection \<open>(Partial) Division\<close>
class divide =
fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "div" 70)
@@ -843,7 +836,7 @@
next
case False
moreover from assms obtain k l where "b = a * k" and "c = a * l"
- by (auto elim!: dvdE)
+ by blast
ultimately show ?thesis by simp
qed
@@ -856,7 +849,7 @@
next
case False
moreover from assms obtain k l where "a = c * k" and "b = c * l"
- by (auto elim!: dvdE)
+ by blast
moreover have "c * k + c * l = c * (k + l)"
by (simp add: algebra_simps)
ultimately show ?thesis
@@ -872,7 +865,7 @@
next
case False
moreover from assms obtain k l where "a = b * k" and "c = d * l"
- by (auto elim!: dvdE)
+ by blast
moreover have "b * k * (d * l) div (b * d) = (b * d) * (k * l) div (b * d)"
by (simp add: ac_simps)
ultimately show ?thesis by simp
@@ -889,12 +882,12 @@
assume ?lhs
then have "b div a * a = c * a" by simp
moreover from assms have "b div a * a = b"
- by (auto elim!: dvdE simp add: ac_simps)
+ by (auto simp add: ac_simps)
ultimately show ?rhs by simp
qed
lemma dvd_div_mult_self [simp]: "a dvd b \<Longrightarrow> b div a * a = b"
- by (cases "a = 0") (auto elim: dvdE simp add: ac_simps)
+ by (cases "a = 0") (auto simp add: ac_simps)
lemma dvd_mult_div_cancel [simp]: "a dvd b \<Longrightarrow> a * (b div a) = b"
using dvd_div_mult_self [of a b] by (simp add: ac_simps)
@@ -964,7 +957,7 @@
next
case False
from assms obtain r s where "b = c * r" and "a = c * r * s"
- by (blast elim: dvdE)
+ by blast
moreover with False have "r \<noteq> 0"
by auto
ultimately show ?thesis using False
@@ -982,7 +975,7 @@
case False
from assms obtain r s
where "a = d * r * s" and "b = d * r"
- by (blast elim: dvdE)
+ by blast
with False show ?thesis
by simp (simp add: ac_simps)
qed
@@ -1699,70 +1692,7 @@
end
-text \<open>Integral (semi)domains with cancellation rules\<close>
-
-class semidom_divide_cancel = semidom_divide +
- assumes div_mult_self1: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
- and div_mult_mult1: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
-begin
-
-context
- fixes b
- assumes "b \<noteq> 0"
-begin
-
-lemma div_mult_self2:
- "(a + b * c) div b = c + a div b"
- using \<open>b \<noteq> 0\<close> div_mult_self1 [of b a c] by (simp add: ac_simps)
-
-lemma div_mult_self3:
- "(c * b + a) div b = c + a div b"
- using \<open>b \<noteq> 0\<close> div_mult_self1 [of b a c] by (simp add: ac_simps)
-
-lemma div_mult_self4:
- "(b * c + a) div b = c + a div b"
- using \<open>b \<noteq> 0\<close> div_mult_self1 [of b a c] by (simp add: ac_simps)
-
-lemma div_add_self1:
- "(b + a) div b = a div b + 1"
- using \<open>b \<noteq> 0\<close> div_mult_self1 [of b a 1] by (simp add: ac_simps)
-
-lemma div_add_self2:
- "(a + b) div b = a div b + 1"
- using \<open>b \<noteq> 0\<close> div_add_self1 [of a] by (simp add: ac_simps)
-
-end
-
-lemma div_mult_mult2:
- "(a * c) div (b * c) = a div b" if "c \<noteq> 0"
- using that div_mult_mult1 [of c a b] by (simp add: ac_simps)
-
-lemma div_mult_mult1_if [simp]:
- "(c * a) div (c * b) = (if c = 0 then 0 else a div b)"
- by (simp add: div_mult_mult1)
-
-lemma div_mult_mult2_if [simp]:
- "(a * c) div (b * c) = (if c = 0 then 0 else a div b)"
- using div_mult_mult1_if [of c a b] by (simp add: ac_simps)
-
-end
-
-class idom_divide_cancel = idom_divide + semidom_divide_cancel
-begin
-
-lemma div_minus_minus [simp]: "(- a) div (- b) = a div b"
- using div_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 div_minus1_right [simp]: "a div (- 1) = - a"
- using div_minus_right [of a 1] by simp
-
-end
-
-
-text \<open>Quotient and remainder in integral domains\<close>
+subsection \<open>Quotient and remainder in integral domains\<close>
class semidom_modulo = algebraic_semidom + semiring_modulo
begin
@@ -1833,7 +1763,19 @@
end
-text \<open>Interlude: basic tool support for algebraic and arithmetic calculations\<close>
+class idom_modulo = idom + semidom_modulo
+begin
+
+subclass idom_divide ..
+
+lemma div_diff [simp]:
+ "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> (a - b) div c = a div c - b div c"
+ using div_add [of _ _ "- b"] by (simp add: dvd_neg_div)
+
+end
+
+
+subsection \<open>Interlude: basic tool support for algebraic and arithmetic calculations\<close>
named_theorems arith "arith facts -- only ground formulas"
ML_file \<open>Tools/arith_data.ML\<close>
@@ -1859,17 +1801,18 @@
simproc_setup cancel_div_mod_int ("(a::'a::semidom_modulo) + b") =
\<open>K Cancel_Div_Mod_Ring.proc\<close>
-class idom_modulo = idom + semidom_modulo
-begin
-
-subclass idom_divide ..
-
-lemma div_diff [simp]:
- "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> (a - b) div c = a div c - b div c"
- using div_add [of _ _ "- b"] by (simp add: dvd_neg_div)
-
-end
-
+
+subsection \<open>Ordered semirings and rings\<close>
+
+text \<open>
+ The theory of partially ordered rings is taken from the books:
+ \<^item> \<^emph>\<open>Lattice Theory\<close> by Garret Birkhoff, American Mathematical Society, 1979
+ \<^item> \<^emph>\<open>Partially Ordered Algebraic Systems\<close>, Pergamon Press, 1963
+
+ Most of the used notions can also be looked up in
+ \<^item> \<^url>\<open>http://www.mathworld.com\<close> by Eric Weisstein et. al.
+ \<^item> \<^emph>\<open>Algebra I\<close> by van der Waerden, Springer
+\<close>
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"
@@ -2669,6 +2612,7 @@
end
+
subsection \<open>Dioids\<close>
text \<open>