# HG changeset patch # User huffman # Date 1179384171 -7200 # Node ID 550709aa8e66d4d36020ffcbb4a46e55a1251bec # Parent d21d3539f6bb7f51cba4ec70e5702407bedfd870 instance division_ring < no_zero_divisors; clean up field instance proofs diff -r d21d3539f6bb -r 550709aa8e66 src/HOL/Ring_and_Field.thy --- a/src/HOL/Ring_and_Field.thy Thu May 17 08:41:23 2007 +0200 +++ b/src/HOL/Ring_and_Field.thy Thu May 17 08:42:51 2007 +0200 @@ -128,36 +128,37 @@ assumes left_inverse [simp]: "a \ \<^loc>0 \ inverse a \<^loc>* a = \<^loc>1" assumes right_inverse [simp]: "a \ \<^loc>0 \ a \<^loc>* inverse a = \<^loc>1" -class field = comm_ring_1 + inverse + - assumes field_left_inverse: "a \ 0 \ inverse a \<^loc>* a = \<^loc>1" - assumes divide_inverse: "a \<^loc>/ b = a \<^loc>* inverse b" +instance division_ring \ no_zero_divisors +proof + fix a b :: 'a + assume a: "a \ 0" and b: "b \ 0" + show "a * b \ 0" + proof + assume ab: "a * b = 0" + hence "0 = inverse a * (a * b) * inverse b" + by simp + also have "\ = (inverse a * a) * (b * inverse b)" + by (simp only: mult_assoc) + also have "\ = 1" + using a b by simp + finally show False + by simp + qed +qed -lemma field_right_inverse: - assumes not0: "a \ 0" - shows "a * inverse (a::'a::field) = 1" -proof - - have "a * inverse a = inverse a * a" by (rule mult_commute) - also have "... = 1" using not0 by (rule field_left_inverse) - finally show ?thesis . -qed +class field = comm_ring_1 + inverse + + assumes field_inverse: "a \ 0 \ inverse a \<^loc>* a = \<^loc>1" + assumes divide_inverse: "a \<^loc>/ b = a \<^loc>* inverse b" instance field \ division_ring -by (intro_classes, erule field_left_inverse, erule field_right_inverse) - -lemma field_mult_eq_0_iff [simp]: - "(a*b = (0::'a::division_ring)) = (a = 0 | b = 0)" -proof cases - assume "a=0" thus ?thesis by simp -next - assume anz [simp]: "a\0" - { assume "a * b = 0" - hence "inverse a * (a * b) = 0" by simp - hence "b = 0" by (simp (no_asm_use) add: mult_assoc [symmetric])} - thus ?thesis by force +proof + fix a :: 'a + assume "a \ 0" + thus "inverse a * a = 1" by (rule field_inverse) + thus "a * inverse a = 1" by (simp only: mult_commute) qed -instance field \ idom -by (intro_classes, simp) +instance field \ idom .. class division_by_zero = zero + inverse + assumes inverse_zero [simp]: "inverse \<^loc>0 = \<^loc>0" @@ -202,8 +203,7 @@ class pordered_semiring = mult_mono + semiring_0 + pordered_ab_semigroup_add class pordered_cancel_semiring = mult_mono + pordered_ab_semigroup_add - + semiring + comm_monoid_add + pordered_ab_semigroup_add - + cancel_ab_semigroup_add + + semiring + comm_monoid_add + cancel_ab_semigroup_add instance pordered_cancel_semiring \ semiring_0_cancel ..