# HG changeset patch # User haftmann # Date 1434693213 -7200 # Node ID 0826b7025d07ee2cc09ad801598fb610d76bd353 # Parent 484559628038663be41e4cfcef6471e2f396438d generalized some theorems about integral domains and moved to HOL theories diff -r 484559628038 -r 0826b7025d07 NEWS --- 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. diff -r 484559628038 -r 0826b7025d07 src/HOL/Divides.thy --- 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 \ 0 \ a div a = 1" - using div_mult_self2_is_id [of _ 1] by simp - lemma div_add_self1 [simp]: assumes "b \ 0" shows "(b + a) div b = a div b + 1" diff -r 484559628038 -r 0826b7025d07 src/HOL/NSA/StarDef.thy --- 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 "\b a :: 'a star. b \ 0 \ (a * b) div b = a" - by transfer simp - show "\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 .. diff -r 484559628038 -r 0826b7025d07 src/HOL/Number_Theory/Euclidean_Algorithm.thy --- 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 \ c = 0 \ 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 \ c = 0 \ 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 \ 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 \ b div a * a = b" by (cases "a = 0") (auto elim: dvdE simp add: ac_simps) diff -r 484559628038 -r 0826b7025d07 src/HOL/Rings.thy --- 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 \ c = 0 \ a = b" + and mult_cancel_left [simp]: "c * a = c * b \ c = 0 \ a = b" begin -text{*Cancellation of equalities with a common factor*} -lemma mult_cancel_right [simp]: - "a * c = b * c \ c = 0 \ 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 \ c = 0 \ 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 \ 0 \ c * a = c * b \ 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 \ (a - b) * c = 0" + by (simp add: algebra_simps) + also have "\ \ c = 0 \ a = b" + by auto + finally show "a * c = b * c \ c = 0 \ a = b" . + have "c * a = c * b \ c * (a - b) = 0" + by (simp add: algebra_simps) + also have "\ \ c = 0 \ a = b" + by auto + finally show "c * a = c * b \ c = 0 \ 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 \ (a = b \ a = - b)" +lemma square_eq_iff: "a * a = b * b \ a = b \ a = - b" proof assume "a * a = b * b" then have "(a - b) * (a + b) = 0" @@ -594,6 +599,33 @@ "a \ 0 \ (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 \ c = 0 \ 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 \ c = 0 \ a = b" + by (simp add: ac_simps) +qed + +lemma div_self [simp]: + assumes "a \ 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