# HG changeset patch # User haftmann # Date 1205565075 -3600 # Node ID 2bdb61a28971a08769d00f683d094c3dd634abb0 # Parent 6c4d534af98d7f8cf9a3733a977c7f8b3a9e1090 continued localization diff -r 6c4d534af98d -r 2bdb61a28971 src/HOL/Ring_and_Field.thy --- a/src/HOL/Ring_and_Field.thy Fri Mar 14 19:58:01 2008 +0100 +++ b/src/HOL/Ring_and_Field.thy Sat Mar 15 08:11:15 2008 +0100 @@ -240,6 +240,25 @@ end class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors +begin + +lemma mult_cancel_right1 [simp]: + "c = b * c \ c = 0 \ b = 1" + by (insert mult_cancel_right [of 1 c b], force) + +lemma mult_cancel_right2 [simp]: + "a * c = c \ c = 0 \ a = 1" + by (insert mult_cancel_right [of a c 1], simp) + +lemma mult_cancel_left1 [simp]: + "c = c * b \ c = 0 \ b = 1" + by (insert mult_cancel_left [of c 1 b], force) + +lemma mult_cancel_left2 [simp]: + "c * a = c \ c = 0 \ a = 1" + by (insert mult_cancel_left [of c a 1], simp) + +end class idom = comm_ring_1 + no_zero_divisors begin @@ -271,6 +290,95 @@ qed qed +lemma nonzero_imp_inverse_nonzero: + "a \ 0 \ inverse a \ 0" +proof + assume ianz: "inverse a = 0" + assume "a \ 0" + hence "1 = a * inverse a" by simp + also have "... = 0" by (simp add: ianz) + finally have "1 = 0" . + thus False by (simp add: eq_commute) +qed + +lemma inverse_zero_imp_zero: + "inverse a = 0 \ a = 0" +apply (rule classical) +apply (drule nonzero_imp_inverse_nonzero) +apply auto +done + +lemma nonzero_inverse_minus_eq: + assumes "a \ 0" + shows "inverse (- a) = - inverse a" +proof - + have "- a * inverse (- a) = - a * - inverse a" + using assms by simp + then show ?thesis unfolding mult_cancel_left using assms by simp +qed + +lemma nonzero_inverse_inverse_eq: + assumes "a \ 0" + shows "inverse (inverse a) = a" +proof - + have "(inverse (inverse a) * inverse a) * a = a" + using assms by (simp add: nonzero_imp_inverse_nonzero) + then show ?thesis using assms by (simp add: mult_assoc) +qed + +lemma nonzero_inverse_eq_imp_eq: + assumes inveq: "inverse a = inverse b" + and anz: "a \ 0" + and bnz: "b \ 0" + shows "a = b" +proof - + have "a * inverse b = a * inverse a" + by (simp add: inveq) + hence "(a * inverse b) * b = (a * inverse a) * b" + by simp + then show "a = b" + by (simp add: mult_assoc anz bnz) +qed + +lemma inverse_1 [simp]: "inverse 1 = 1" +proof - + have "inverse 1 * 1 = 1" + by (rule left_inverse) (rule one_neq_zero) + then show ?thesis by simp +qed + +lemma inverse_unique: + assumes ab: "a * b = 1" + shows "inverse a = b" +proof - + have "a \ 0" using ab by (cases "a = 0") simp_all + moreover have "inverse a * (a * b) = inverse a" by (simp add: ab) + ultimately show ?thesis by (simp add: mult_assoc [symmetric]) +qed + +lemma nonzero_inverse_mult_distrib: + assumes anz: "a \ 0" + and bnz: "b \ 0" + shows "inverse (a * b) = inverse b * inverse a" +proof - + have "inverse (a * b) * (a * b) * inverse b = inverse b" + by (simp add: anz bnz) + hence "inverse (a * b) * a = inverse b" + by (simp add: mult_assoc bnz) + hence "inverse (a * b) * a * inverse a = inverse b * inverse a" + by simp + thus ?thesis + by (simp add: mult_assoc anz) +qed + +lemma division_ring_inverse_add: + "a \ 0 \ b \ 0 \ inverse a + inverse b = inverse a * (a + b) * inverse b" + by (simp add: ring_simps mult_assoc) + +lemma division_ring_inverse_diff: + "a \ 0 \ b \ 0 \ inverse a - inverse b = inverse a * (b - a) * inverse b" + by (simp add: ring_simps mult_assoc) + end class field = comm_ring_1 + inverse + @@ -831,80 +939,46 @@ assumes "x \ y" obtains "x < y" | "y < x" using assms by (rule neqE) +text {* These cancellation simprules also produce two cases when the comparison is a goal. *} + +lemma mult_le_cancel_right1: + "c \ b * c \ (0 < c \ 1 \ b) \ (c < 0 \ b \ 1)" + by (insert mult_le_cancel_right [of 1 c b], simp) + +lemma mult_le_cancel_right2: + "a * c \ c \ (0 < c \ a \ 1) \ (c < 0 \ 1 \ a)" + by (insert mult_le_cancel_right [of a c 1], simp) + +lemma mult_le_cancel_left1: + "c \ c * b \ (0 < c \ 1 \ b) \ (c < 0 \ b \ 1)" + by (insert mult_le_cancel_left [of c 1 b], simp) + +lemma mult_le_cancel_left2: + "c * a \ c \ (0 < c \ a \ 1) \ (c < 0 \ 1 \ a)" + by (insert mult_le_cancel_left [of c a 1], simp) + +lemma mult_less_cancel_right1: + "c < b * c \ (0 \ c \ 1 < b) \ (c \ 0 \ b < 1)" + by (insert mult_less_cancel_right [of 1 c b], simp) + +lemma mult_less_cancel_right2: + "a * c < c \ (0 \ c \ a < 1) \ (c \ 0 \ 1 < a)" + by (insert mult_less_cancel_right [of a c 1], simp) + +lemma mult_less_cancel_left1: + "c < c * b \ (0 \ c \ 1 < b) \ (c \ 0 \ b < 1)" + by (insert mult_less_cancel_left [of c 1 b], simp) + +lemma mult_less_cancel_left2: + "c * a < c \ (0 \ c \ a < 1) \ (c \ 0 \ 1 < a)" + by (insert mult_less_cancel_left [of c a 1], simp) + end class ordered_field = field + ordered_idom -text{*All three types of comparision involving 0 and 1 are covered.*} - --- {* FIXME continue localization here *} - -subsubsection{*Special Cancellation Simprules for Multiplication*} - -text{*These also produce two cases when the comparison is a goal.*} - -lemma mult_le_cancel_right1: - fixes c :: "'a :: ordered_idom" - shows "(c \ b*c) = ((0 1\b) & (c<0 --> b \ 1))" -by (insert mult_le_cancel_right [of 1 c b], simp) - -lemma mult_le_cancel_right2: - fixes c :: "'a :: ordered_idom" - shows "(a*c \ c) = ((0 a\1) & (c<0 --> 1 \ a))" -by (insert mult_le_cancel_right [of a c 1], simp) - -lemma mult_le_cancel_left1: - fixes c :: "'a :: ordered_idom" - shows "(c \ c*b) = ((0 1\b) & (c<0 --> b \ 1))" -by (insert mult_le_cancel_left [of c 1 b], simp) - -lemma mult_le_cancel_left2: - fixes c :: "'a :: ordered_idom" - shows "(c*a \ c) = ((0 a\1) & (c<0 --> 1 \ a))" -by (insert mult_le_cancel_left [of c a 1], simp) - -lemma mult_less_cancel_right1: - fixes c :: "'a :: ordered_idom" - shows "(c < b*c) = ((0 \ c --> 1 0 --> b < 1))" -by (insert mult_less_cancel_right [of 1 c b], simp) +text {* Simprules for comparisons where common factors can be cancelled. *} -lemma mult_less_cancel_right2: - fixes c :: "'a :: ordered_idom" - shows "(a*c < c) = ((0 \ c --> a<1) & (c \ 0 --> 1 < a))" -by (insert mult_less_cancel_right [of a c 1], simp) - -lemma mult_less_cancel_left1: - fixes c :: "'a :: ordered_idom" - shows "(c < c*b) = ((0 \ c --> 1 0 --> b < 1))" -by (insert mult_less_cancel_left [of c 1 b], simp) - -lemma mult_less_cancel_left2: - fixes c :: "'a :: ordered_idom" - shows "(c*a < c) = ((0 \ c --> a<1) & (c \ 0 --> 1 < a))" -by (insert mult_less_cancel_left [of c a 1], simp) - -lemma mult_cancel_right1 [simp]: - fixes c :: "'a :: ring_1_no_zero_divisors" - shows "(c = b*c) = (c = 0 | b=1)" -by (insert mult_cancel_right [of 1 c b], force) - -lemma mult_cancel_right2 [simp]: - fixes c :: "'a :: ring_1_no_zero_divisors" - shows "(a*c = c) = (c = 0 | a=1)" -by (insert mult_cancel_right [of a c 1], simp) - -lemma mult_cancel_left1 [simp]: - fixes c :: "'a :: ring_1_no_zero_divisors" - shows "(c = c*b) = (c = 0 | b=1)" -by (insert mult_cancel_left [of c 1 b], force) - -lemma mult_cancel_left2 [simp]: - fixes c :: "'a :: ring_1_no_zero_divisors" - shows "(c*a = c) = (c = 0 | a=1)" -by (insert mult_cancel_left [of c a 1], simp) - - -text{*Simprules for comparisons where common factors can be cancelled.*} lemmas mult_compare_simps = mult_le_cancel_right mult_le_cancel_left mult_le_cancel_right1 mult_le_cancel_right2 @@ -916,73 +990,11 @@ mult_cancel_right1 mult_cancel_right2 mult_cancel_left1 mult_cancel_left2 - -(* what ordering?? this is a straight instance of mult_eq_0_iff -text{*Compared with @{text mult_eq_0_iff}, this version removes the requirement - of an ordering.*} -lemma field_mult_eq_0_iff [simp]: - "(a*b = (0::'a::division_ring)) = (a = 0 | b = 0)" -by simp -*) -(* subsumed by mult_cancel lemmas on ring_no_zero_divisors -text{*Cancellation of equalities with a common factor*} -lemma field_mult_cancel_right_lemma: - assumes cnz: "c \ (0::'a::division_ring)" - and eq: "a*c = b*c" - shows "a=b" -proof - - have "(a * c) * inverse c = (b * c) * inverse c" - by (simp add: eq) - thus "a=b" - by (simp add: mult_assoc cnz) -qed - -lemma field_mult_cancel_right [simp]: - "(a*c = b*c) = (c = (0::'a::division_ring) | a=b)" -by simp - -lemma field_mult_cancel_left [simp]: - "(c*a = c*b) = (c = (0::'a::division_ring) | a=b)" -by simp -*) -lemma nonzero_imp_inverse_nonzero: - "a \ 0 ==> inverse a \ (0::'a::division_ring)" -proof - assume ianz: "inverse a = 0" - assume "a \ 0" - hence "1 = a * inverse a" by simp - also have "... = 0" by (simp add: ianz) - finally have "1 = (0::'a::division_ring)" . - thus False by (simp add: eq_commute) -qed - - -subsection{*Basic Properties of @{term inverse}*} - -lemma inverse_zero_imp_zero: "inverse a = 0 ==> a = (0::'a::division_ring)" -apply (rule ccontr) -apply (blast dest: nonzero_imp_inverse_nonzero) -done - -lemma inverse_nonzero_imp_nonzero: - "inverse a = 0 ==> a = (0::'a::division_ring)" -apply (rule ccontr) -apply (blast dest: nonzero_imp_inverse_nonzero) -done +-- {* FIXME continue localization here *} lemma inverse_nonzero_iff_nonzero [simp]: "(inverse a = 0) = (a = (0::'a::{division_ring,division_by_zero}))" -by (force dest: inverse_nonzero_imp_nonzero) - -lemma nonzero_inverse_minus_eq: - assumes [simp]: "a\0" - shows "inverse(-a) = -inverse(a::'a::division_ring)" -proof - - have "-a * inverse (- a) = -a * - inverse a" - by simp - thus ?thesis - by (simp only: mult_cancel_left, simp) -qed +by (force dest: inverse_zero_imp_zero) lemma inverse_minus_eq [simp]: "inverse(-a) = -inverse(a::'a::{division_ring,division_by_zero})" @@ -993,20 +1005,6 @@ thus ?thesis by (simp add: nonzero_inverse_minus_eq) qed -lemma nonzero_inverse_eq_imp_eq: - assumes inveq: "inverse a = inverse b" - and anz: "a \ 0" - and bnz: "b \ 0" - shows "a = (b::'a::division_ring)" -proof - - have "a * inverse b = a * inverse a" - by (simp add: inveq) - hence "(a * inverse b) * b = (a * inverse a) * b" - by simp - thus "a = b" - by (simp add: mult_assoc anz bnz) -qed - lemma inverse_eq_imp_eq: "inverse a = inverse b ==> a = (b::'a::{division_ring,division_by_zero})" apply (cases "a=0 | b=0") @@ -1019,16 +1017,6 @@ "(inverse a = inverse b) = (a = (b::'a::{division_ring,division_by_zero}))" by (force dest!: inverse_eq_imp_eq) -lemma nonzero_inverse_inverse_eq: - assumes [simp]: "a \ 0" - shows "inverse(inverse (a::'a::division_ring)) = a" - proof - - have "(inverse (inverse a) * inverse a) * a = a" - by (simp add: nonzero_imp_inverse_nonzero) - thus ?thesis - by (simp add: mult_assoc) - qed - lemma inverse_inverse_eq [simp]: "inverse(inverse (a::'a::{division_ring,division_by_zero})) = a" proof cases @@ -1038,37 +1026,6 @@ thus ?thesis by (simp add: nonzero_inverse_inverse_eq) qed -lemma inverse_1 [simp]: "inverse 1 = (1::'a::division_ring)" - proof - - have "inverse 1 * 1 = (1::'a::division_ring)" - by (rule left_inverse [OF zero_neq_one [symmetric]]) - thus ?thesis by simp - qed - -lemma inverse_unique: - assumes ab: "a*b = 1" - shows "inverse a = (b::'a::division_ring)" -proof - - have "a \ 0" using ab by auto - moreover have "inverse a * (a * b) = inverse a" by (simp add: ab) - ultimately show ?thesis by (simp add: mult_assoc [symmetric]) -qed - -lemma nonzero_inverse_mult_distrib: - assumes anz: "a \ 0" - and bnz: "b \ 0" - shows "inverse(a*b) = inverse(b) * inverse(a::'a::division_ring)" - proof - - have "inverse(a*b) * (a * b) * inverse(b) = inverse(b)" - by (simp add: anz bnz) - hence "inverse(a*b) * a = inverse(b)" - by (simp add: mult_assoc bnz) - hence "inverse(a*b) * a * inverse(a) = inverse(b) * inverse(a)" - by simp - thus ?thesis - by (simp add: mult_assoc anz) - qed - text{*This version builds in division by zero while also re-orienting the right-hand side.*} lemma inverse_mult_distrib [simp]: @@ -1083,16 +1040,6 @@ by force qed -lemma division_ring_inverse_add: - "[|(a::'a::division_ring) \ 0; b \ 0|] - ==> inverse a + inverse b = inverse a * (a+b) * inverse b" -by (simp add: ring_simps) - -lemma division_ring_inverse_diff: - "[|(a::'a::division_ring) \ 0; b \ 0|] - ==> inverse a - inverse b = inverse a * (b-a) * inverse b" -by (simp add: ring_simps) - text{*There is no slick version using division by zero.*} lemma inverse_add: "[|a \ 0; b \ 0|]