# HG changeset patch # User haftmann # Date 1433177962 -7200 # Node ID 838025c6e278d2daed6d1fe4a301a06125f1383b # Parent d46de31a50c483faf71434410114d1567f57ea62 implicit partial divison operation in integral domains diff -r d46de31a50c4 -r 838025c6e278 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Mon Jun 01 18:59:21 2015 +0200 +++ b/src/HOL/Divides.thy Mon Jun 01 18:59:22 2015 +0200 @@ -31,7 +31,13 @@ and div_mult_mult1 [simp]: "c \ 0 \ (c * a) div (c * b) = a div b" begin -subclass semiring_no_zero_divisors .. +subclass semidom_divide +proof + fix b a + assume "b \ 0" + then show "a * b div b = a" + using div_mult_self1 [of b 0 a] by (simp add: ac_simps) +qed simp lemma power_not_zero: -- \FIXME cf. @{text field_power_not_zero}\ "a \ 0 \ a ^ n \ 0" @@ -107,11 +113,13 @@ "(b * c + a) mod b = a mod b" by (simp add: add.commute) -lemma div_mult_self1_is_id [simp]: "b \ 0 \ b * a div b = a" - using div_mult_self2 [of b 0 a] by simp - -lemma div_mult_self2_is_id [simp]: "b \ 0 \ a * b div b = a" - using div_mult_self1 [of b 0 a] by simp +lemma div_mult_self1_is_id: + "b \ 0 \ b * a div b = a" + by (fact nonzero_mult_divide_cancel_left) + +lemma div_mult_self2_is_id: + "b \ 0 \ a * b div b = a" + by (fact nonzero_mult_divide_cancel_right) lemma mod_mult_self1_is_0 [simp]: "b * a mod b = 0" using mod_mult_self2 [of 0 b a] by simp @@ -439,21 +447,21 @@ next assume "b div a = c" then have "b div a * a = c * a" by simp - moreover from `a dvd b` have "b div a * a = b" by (simp add: dvd_div_mult_self) + moreover from `a dvd b` have "b div a * a = b" by simp ultimately show "b = c * a" by simp qed lemma dvd_div_div_eq_mult: assumes "a \ 0" "c \ 0" and "a dvd b" "c dvd d" shows "b div a = d div c \ b * c = a * d" - using assms by (auto simp add: mult.commute [of _ a] dvd_div_mult_self dvd_div_eq_mult div_mult_swap intro: sym) + using assms by (auto simp add: mult.commute [of _ a] dvd_div_eq_mult div_mult_swap intro: sym) end class ring_div = comm_ring_1 + semiring_div begin -subclass idom .. +subclass idom_divide .. text {* Negation respects modular equivalence. *} diff -r d46de31a50c4 -r 838025c6e278 src/HOL/Fields.thy --- a/src/HOL/Fields.thy Mon Jun 01 18:59:21 2015 +0200 +++ b/src/HOL/Fields.thy Mon Jun 01 18:59:22 2015 +0200 @@ -221,7 +221,7 @@ "z \ 0 \ - (x / z) - y = (- x - y * z) / z" by (simp add: divide_diff_eq_iff[symmetric]) -lemma divide_zero [simp]: +lemma division_ring_divide_zero [simp]: "a / 0 = 0" by (simp add: divide_inverse) @@ -300,18 +300,31 @@ by (fact field_inverse_zero) qed -subclass idom .. +subclass idom_divide +proof + fix b a + assume "b \ 0" + then show "a * b / b = a" + by (simp add: divide_inverse ac_simps) +next + fix a + show "a / 0 = 0" + by (simp add: divide_inverse) +qed text{*There is no slick version using division by zero.*} lemma inverse_add: - "[| a \ 0; b \ 0 |] - ==> inverse a + inverse b = (a + b) * inverse a * inverse b" -by (simp add: division_ring_inverse_add ac_simps) + "a \ 0 \ b \ 0 \ 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]: "b\0" and [simp]: "c\0" shows "(c*a)/(c*b) = a/b" -proof - - have "(c*a)/(c*b) = c * a * (inverse b * inverse c)" + assumes [simp]: "c \ 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) @@ -320,8 +333,8 @@ qed lemma nonzero_mult_divide_mult_cancel_right [simp]: - "\b \ 0; c \ 0\ \ (a * c) / (b * c) = a / b" -by (simp add: mult.commute [of _ c]) + "c \ 0 \ (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) @@ -340,33 +353,24 @@ text{*Special Cancellation Simprules for Division*} -lemma nonzero_mult_divide_cancel_right [simp]: - "b \ 0 \ a * b / b = a" - using nonzero_mult_divide_mult_cancel_right [of 1 b a] by simp - -lemma nonzero_mult_divide_cancel_left [simp]: - "a \ 0 \ a * b / a = b" -using nonzero_mult_divide_mult_cancel_left [of 1 a b] by simp - lemma nonzero_divide_mult_cancel_right [simp]: - "\a \ 0; b \ 0\ \ b / (a * b) = 1 / a" -using nonzero_mult_divide_mult_cancel_right [of a b 1] by simp + "b \ 0 \ b / (a * b) = 1 / a" + using nonzero_mult_divide_mult_cancel_right [of b 1 a] by simp lemma nonzero_divide_mult_cancel_left [simp]: - "\a \ 0; b \ 0\ \ a / (a * b) = 1 / b" -using nonzero_mult_divide_mult_cancel_left [of b a 1] by simp + "a \ 0 \ a / (a * b) = 1 / b" + using nonzero_mult_divide_mult_cancel_left [of a 1 b] by simp lemma nonzero_mult_divide_mult_cancel_left2 [simp]: - "\b \ 0; c \ 0\ \ (c * a) / (b * c) = a / b" -using nonzero_mult_divide_mult_cancel_left [of b c a] by (simp add: ac_simps) + "c \ 0 \ (c * a) / (b * c) = a / b" + using nonzero_mult_divide_mult_cancel_left [of c a b] by (simp add: ac_simps) lemma nonzero_mult_divide_mult_cancel_right2 [simp]: - "\b \ 0; c \ 0\ \ (a * c) / (c * b) = a / b" -using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: ac_simps) + "c \ 0 \ (a * c) / (c * b) = a / b" + using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: ac_simps) lemma diff_frac_eq: "y \ 0 \ z \ 0 \ x / y - w / z = (x * z - w * y) / (y * z)" - thm field_simps by (simp add: field_simps) lemma frac_eq_eq: @@ -427,7 +431,7 @@ lemma mult_divide_mult_cancel_left_if [simp]: shows "(c * a) / (c * b) = (if c = 0 then 0 else a / b)" - by (simp add: mult_divide_mult_cancel_left) + by simp text {* Division and Unary Minus *} diff -r d46de31a50c4 -r 838025c6e278 src/HOL/Groups_Big.thy --- a/src/HOL/Groups_Big.thy Mon Jun 01 18:59:21 2015 +0200 +++ b/src/HOL/Groups_Big.thy Mon Jun 01 18:59:22 2015 +0200 @@ -1153,10 +1153,29 @@ shows "setprod f A = (0::'a::semidom) \ (\a\A. f a = 0)" using assms by (induct A) (auto simp: no_zero_divisors) -lemma (in field) setprod_diff1: - "finite A \ f a \ 0 \ - (setprod f (A - {a})) = (if a \ A then setprod f A / f a else setprod f A)" - by (induct A rule: finite_induct) (auto simp add: insert_Diff_if) +lemma (in semidom_divide) setprod_diff1: + assumes "finite A" and "f a \ 0" + shows "setprod f (A - {a}) = (if a \ A then divide (setprod f A) (f a) else setprod f A)" +proof (cases "a \ A") + case True then show ?thesis by simp +next + case False with assms show ?thesis + proof (induct A rule: finite_induct) + case empty then show ?case by simp + next + case (insert b B) + then show ?case + proof (cases "a = b") + case True with insert show ?thesis by simp + next + case False with insert have "a \ B" by simp + def C \ "B - {a}" + with `finite B` `a \ B` + have *: "B = insert a C" "finite C" "a \ C" by auto + with insert show ?thesis by (auto simp add: insert_commute ac_simps) + qed + qed +qed lemma (in field) setprod_inversef: "finite A \ setprod (inverse \ f) A = inverse (setprod f A)" diff -r d46de31a50c4 -r 838025c6e278 src/HOL/NSA/StarDef.thy --- a/src/HOL/NSA/StarDef.thy Mon Jun 01 18:59:21 2015 +0200 +++ b/src/HOL/NSA/StarDef.thy Mon Jun 01 18:59:22 2015 +0200 @@ -853,6 +853,13 @@ 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 \ divide (a * b) b = a" + by transfer simp + show "\a :: 'a star. divide a 0 = 0" + by transfer simp +qed instance star :: (semiring_div) semiring_div apply intro_classes apply(transfer, rule mod_div_equality) @@ -865,6 +872,7 @@ 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 .. +instance star :: (idom_divide) idom_divide .. instance star :: (division_ring) division_ring apply (intro_classes) diff -r d46de31a50c4 -r 838025c6e278 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Mon Jun 01 18:59:21 2015 +0200 +++ b/src/HOL/Nat.thy Mon Jun 01 18:59:22 2015 +0200 @@ -1484,6 +1484,14 @@ lemma of_nat_eq_0_iff [simp]: "of_nat m = 0 \ m = 0" by (fact of_nat_eq_iff [of m 0, unfolded of_nat_0]) +lemma of_nat_neq_0 [simp]: + "of_nat (Suc n) \ 0" + unfolding of_nat_eq_0_iff by simp + +lemma of_nat_0_neq [simp]: + "0 \ of_nat (Suc n)" + unfolding of_nat_0_eq_iff by simp + end context linordered_semidom diff -r d46de31a50c4 -r 838025c6e278 src/HOL/Rings.thy --- a/src/HOL/Rings.thy Mon Jun 01 18:59:21 2015 +0200 +++ b/src/HOL/Rings.thy Mon Jun 01 18:59:22 2015 +0200 @@ -415,33 +415,6 @@ end -class divide = - fixes divide :: "'a \ 'a \ 'a" - -setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \ 'a \ 'a"}) *} - -context semiring -begin - -lemma [field_simps]: - shows distrib_left_NO_MATCH: "NO_MATCH (divide x y) a \ a * (b + c) = a * b + a * c" - and distrib_right_NO_MATCH: "NO_MATCH (divide x y) c \ (a + b) * c = a * c + b * c" - by (rule distrib_left distrib_right)+ - -end - -context ring -begin - -lemma [field_simps]: - shows left_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) c \ (a - b) * c = a * c - b * c" - and right_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) a \ a * (b - c) = a * b - a * c" - by (rule left_diff_distrib right_diff_distrib)+ - -end - -setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::divide \ 'a \ 'a"}) *} - class semiring_no_zero_divisors = semiring_0 + assumes no_zero_divisors: "a \ 0 \ b \ 0 \ a * b \ 0" begin @@ -585,6 +558,46 @@ \end{itemize} *} +class divide = + fixes divide :: "'a \ 'a \ 'a" + +setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \ 'a \ 'a"}) *} + +context semiring +begin + +lemma [field_simps]: + shows distrib_left_NO_MATCH: "NO_MATCH (divide x y) a \ a * (b + c) = a * b + a * c" + and distrib_right_NO_MATCH: "NO_MATCH (divide x y) c \ (a + b) * c = a * c + b * c" + by (rule distrib_left distrib_right)+ + +end + +context ring +begin + +lemma [field_simps]: + shows left_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) c \ (a - b) * c = a * c - b * c" + and right_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) a \ a * (b - c) = a * b - a * c" + by (rule left_diff_distrib right_diff_distrib)+ + +end + +setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::divide \ 'a \ 'a"}) *} + +class semidom_divide = semidom + divide + + assumes nonzero_mult_divide_cancel_right [simp]: "b \ 0 \ divide (a * b) b = a" + assumes divide_zero [simp]: "divide a 0 = 0" +begin + +lemma nonzero_mult_divide_cancel_left [simp]: + "a \ 0 \ divide (a * b) a = b" + using nonzero_mult_divide_cancel_right [of a b] by (simp add: ac_simps) + +end + +class idom_divide = idom + semidom_divide + class ordered_semiring = semiring + comm_monoid_add + ordered_ab_semigroup_add + assumes mult_left_mono: "a \ b \ 0 \ c \ c * a \ c * b" assumes mult_right_mono: "a \ b \ 0 \ c \ a * c \ b * c"