--- a/NEWS Fri Jun 19 15:55:22 2015 +0200
+++ b/NEWS Fri Jun 19 07:53:33 2015 +0200
@@ -92,11 +92,14 @@
* Nitpick:
- Removed "check_potential" and "check_genuine" options.
+* Tightened specification of class semiring_no_zero_divisors. Slight
+INCOMPATIBILITY.
+
* Former constants Fields.divide (_ / _) and Divides.div (_ div _)
are logically unified to Rings.divide in syntactic type class
Rings.divide, with infix syntax (_ div _). Infix syntax (_ / _)
for field division is added later as abbreviation in class Fields.inverse.
-INCOMPATIBILITY, instantiatios must refer to Rings.divide rather
+INCOMPATIBILITY, instantiations must refer to Rings.divide rather
than the former separate constants, hence infix syntax (_ / _) is usually
not available during instantiation.
--- a/src/HOL/Divides.thy Fri Jun 19 15:55:22 2015 +0200
+++ b/src/HOL/Divides.thy Fri Jun 19 07:53:33 2015 +0200
@@ -131,9 +131,6 @@
lemma mod_self [simp]: "a mod a = 0"
using mod_mult_self2_is_0 [of 1] by simp
-lemma div_self [simp]: "a \<noteq> 0 \<Longrightarrow> a div a = 1"
- using div_mult_self2_is_id [of _ 1] by simp
-
lemma div_add_self1 [simp]:
assumes "b \<noteq> 0"
shows "(b + a) div b = a div b + 1"
--- a/src/HOL/NSA/StarDef.thy Fri Jun 19 15:55:22 2015 +0200
+++ b/src/HOL/NSA/StarDef.thy Fri Jun 19 07:53:33 2015 +0200
@@ -816,24 +816,21 @@
subsection {* Ring and field classes *}
instance star :: (semiring) semiring
-apply (intro_classes)
-apply (transfer, rule distrib_right)
-apply (transfer, rule distrib_left)
-done
+ by (intro_classes; transfer) (fact distrib_right distrib_left)+
instance star :: (semiring_0) semiring_0
-by intro_classes (transfer, simp)+
+ by (intro_classes; transfer) simp_all
instance star :: (semiring_0_cancel) semiring_0_cancel ..
instance star :: (comm_semiring) comm_semiring
-by (intro_classes, transfer, rule distrib_right)
+ by (intro_classes; transfer) (fact distrib_right)
instance star :: (comm_semiring_0) comm_semiring_0 ..
instance star :: (comm_semiring_0_cancel) comm_semiring_0_cancel ..
instance star :: (zero_neq_one) zero_neq_one
-by (intro_classes, transfer, rule zero_neq_one)
+ by (intro_classes; transfer) (fact zero_neq_one)
instance star :: (semiring_1) semiring_1 ..
instance star :: (comm_semiring_1) comm_semiring_1 ..
@@ -841,10 +838,13 @@
declare dvd_def [transfer_refold]
instance star :: (comm_semiring_1_diff_distrib) comm_semiring_1_diff_distrib
-by intro_classes (transfer, fact right_diff_distrib')
+ by (intro_classes; transfer) (fact right_diff_distrib')
instance star :: (semiring_no_zero_divisors) semiring_no_zero_divisors
-by (intro_classes, transfer, rule no_zero_divisors)
+ by (intro_classes; transfer) (fact no_zero_divisors)
+
+instance star :: (semiring_no_zero_divisors_cancel) semiring_no_zero_divisors_cancel
+ by (intro_classes; transfer) simp_all
instance star :: (semiring_1_cancel) semiring_1_cancel ..
instance star :: (comm_semiring_1_cancel) comm_semiring_1_cancel ..
@@ -853,21 +853,12 @@
instance star :: (ring_1) ring_1 ..
instance star :: (comm_ring_1) comm_ring_1 ..
instance star :: (semidom) semidom ..
+
instance star :: (semidom_divide) semidom_divide
-proof
- show "\<And>b a :: 'a star. b \<noteq> 0 \<Longrightarrow> (a * b) div b = a"
- by transfer simp
- show "\<And>a :: 'a star. a div 0 = 0"
- by transfer simp
-qed
+ by (intro_classes; transfer) simp_all
+
instance star :: (semiring_div) semiring_div
-apply intro_classes
-apply(transfer, rule mod_div_equality)
-apply(transfer, rule div_by_0)
-apply(transfer, rule div_0)
-apply(transfer, erule div_mult_self1)
-apply(transfer, erule div_mult_mult1)
-done
+ by (intro_classes; transfer) (simp_all add: mod_div_equality)
instance star :: (ring_no_zero_divisors) ring_no_zero_divisors ..
instance star :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors ..
@@ -875,57 +866,43 @@
instance star :: (idom_divide) idom_divide ..
instance star :: (division_ring) division_ring
-apply (intro_classes)
-apply (transfer, erule left_inverse)
-apply (transfer, erule right_inverse)
-apply (transfer, fact divide_inverse)
-apply (transfer, fact inverse_zero)
-done
+ by (intro_classes; transfer) (simp_all add: divide_inverse)
instance star :: (field) field
-apply (intro_classes)
-apply (transfer, erule left_inverse)
-apply (transfer, rule divide_inverse)
-apply (transfer, fact inverse_zero)
-done
+ by (intro_classes; transfer) (simp_all add: divide_inverse)
instance star :: (ordered_semiring) ordered_semiring
-apply (intro_classes)
-apply (transfer, erule (1) mult_left_mono)
-apply (transfer, erule (1) mult_right_mono)
-done
+ by (intro_classes; transfer) (fact mult_left_mono mult_right_mono)+
instance star :: (ordered_cancel_semiring) ordered_cancel_semiring ..
instance star :: (linordered_semiring_strict) linordered_semiring_strict
-apply (intro_classes)
-apply (transfer, erule (1) mult_strict_left_mono)
-apply (transfer, erule (1) mult_strict_right_mono)
-done
+ by (intro_classes; transfer) (fact mult_strict_left_mono mult_strict_right_mono)+
instance star :: (ordered_comm_semiring) ordered_comm_semiring
-by (intro_classes, transfer, rule mult_left_mono)
+ by (intro_classes; transfer) (fact mult_left_mono)
instance star :: (ordered_cancel_comm_semiring) ordered_cancel_comm_semiring ..
instance star :: (linordered_comm_semiring_strict) linordered_comm_semiring_strict
-by (intro_classes, transfer, rule mult_strict_left_mono)
+ by (intro_classes; transfer) (fact mult_strict_left_mono)
instance star :: (ordered_ring) ordered_ring ..
+
instance star :: (ordered_ring_abs) ordered_ring_abs
- by intro_classes (transfer, rule abs_eq_mult)
+ by (intro_classes; transfer) (fact abs_eq_mult)
instance star :: (abs_if) abs_if
-by (intro_classes, transfer, rule abs_if)
+ by (intro_classes; transfer) (fact abs_if)
instance star :: (sgn_if) sgn_if
-by (intro_classes, transfer, rule sgn_if)
+ by (intro_classes; transfer) (fact sgn_if)
instance star :: (linordered_ring_strict) linordered_ring_strict ..
instance star :: (ordered_comm_ring) ordered_comm_ring ..
instance star :: (linordered_semidom) linordered_semidom
-by (intro_classes, transfer, rule zero_less_one)
+ by (intro_classes; transfer) (fact zero_less_one)
instance star :: (linordered_idom) linordered_idom ..
instance star :: (linordered_field) linordered_field ..
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Fri Jun 19 15:55:22 2015 +0200
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Fri Jun 19 07:53:33 2015 +0200
@@ -9,34 +9,6 @@
context semidom_divide
begin
-lemma mult_cancel_right [simp]:
- "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
-proof (cases "c = 0")
- case True then show ?thesis by simp
-next
- case False
- { assume "a * c = b * c"
- then have "a * c div c = b * c div c"
- by simp
- with False have "a = b"
- by simp
- } then show ?thesis by auto
-qed
-
-lemma mult_cancel_left [simp]:
- "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
- using mult_cancel_right [of a c b] by (simp add: ac_simps)
-
-end
-
-context semidom_divide
-begin
-
-lemma div_self [simp]:
- assumes "a \<noteq> 0"
- shows "a div a = 1"
- using assms nonzero_mult_divide_cancel_left [of a 1] by simp
-
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)
--- a/src/HOL/Rings.thy Fri Jun 19 15:55:22 2015 +0200
+++ b/src/HOL/Rings.thy Fri Jun 19 07:53:33 2015 +0200
@@ -440,26 +440,11 @@
end
-class ring_no_zero_divisors = ring + semiring_no_zero_divisors
+class semiring_no_zero_divisors_cancel = semiring_no_zero_divisors +
+ assumes mult_cancel_right [simp]: "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
+ and mult_cancel_left [simp]: "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
begin
-text{*Cancellation of equalities with a common factor*}
-lemma mult_cancel_right [simp]:
- "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
-proof -
- have "(a * c = b * c) = ((a - b) * c = 0)"
- by (simp add: algebra_simps)
- thus ?thesis by (simp add: disj_commute)
-qed
-
-lemma mult_cancel_left [simp]:
- "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
-proof -
- have "(c * a = c * b) = (c * (a - b) = 0)"
- by (simp add: algebra_simps)
- thus ?thesis by simp
-qed
-
lemma mult_left_cancel:
"c \<noteq> 0 \<Longrightarrow> c * a = c * b \<longleftrightarrow> a = b"
by simp
@@ -470,6 +455,26 @@
end
+class ring_no_zero_divisors = ring + semiring_no_zero_divisors
+begin
+
+subclass semiring_no_zero_divisors_cancel
+proof
+ fix a b c
+ have "a * c = b * c \<longleftrightarrow> (a - b) * c = 0"
+ by (simp add: algebra_simps)
+ also have "\<dots> \<longleftrightarrow> c = 0 \<or> a = b"
+ by auto
+ finally show "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b" .
+ have "c * a = c * b \<longleftrightarrow> c * (a - b) = 0"
+ by (simp add: algebra_simps)
+ also have "\<dots> \<longleftrightarrow> c = 0 \<or> a = b"
+ by auto
+ finally show "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b" .
+qed
+
+end
+
class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
begin
@@ -531,7 +536,7 @@
finally show ?thesis .
qed
-lemma square_eq_iff: "a * a = b * b \<longleftrightarrow> (a = b \<or> a = - b)"
+lemma square_eq_iff: "a * a = b * b \<longleftrightarrow> a = b \<or> a = - b"
proof
assume "a * a = b * b"
then have "(a - b) * (a + b) = 0"
@@ -594,6 +599,33 @@
"a \<noteq> 0 \<Longrightarrow> (a * b) div a = b"
using nonzero_mult_divide_cancel_right [of a b] by (simp add: ac_simps)
+subclass semiring_no_zero_divisors_cancel
+proof
+ fix a b c
+ { fix a b c
+ show "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
+ proof (cases "c = 0")
+ case True then show ?thesis by simp
+ next
+ case False
+ { assume "a * c = b * c"
+ then have "a * c div c = b * c div c"
+ by simp
+ with False have "a = b"
+ by simp
+ } then show ?thesis by auto
+ qed
+ }
+ from this [of a c b]
+ show "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
+ by (simp add: ac_simps)
+qed
+
+lemma div_self [simp]:
+ assumes "a \<noteq> 0"
+ shows "a div a = 1"
+ using assms nonzero_mult_divide_cancel_left [of a 1] by simp
+
end
class idom_divide = idom + semidom_divide