instance division_ring < no_zero_divisors; clean up field instance proofs
authorhuffman
Thu May 17 08:42:51 2007 +0200 (2007-05-17)
changeset 22987550709aa8e66
parent 22986 d21d3539f6bb
child 22988 f6b8184f5b4a
instance division_ring < no_zero_divisors; clean up field instance proofs
src/HOL/Ring_and_Field.thy
     1.1 --- a/src/HOL/Ring_and_Field.thy	Thu May 17 08:41:23 2007 +0200
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Thu May 17 08:42:51 2007 +0200
     1.3 @@ -128,36 +128,37 @@
     1.4    assumes left_inverse [simp]:  "a \<noteq> \<^loc>0 \<Longrightarrow> inverse a \<^loc>* a = \<^loc>1"
     1.5    assumes right_inverse [simp]: "a \<noteq> \<^loc>0 \<Longrightarrow> a \<^loc>* inverse a = \<^loc>1"
     1.6  
     1.7 -class field = comm_ring_1 + inverse +
     1.8 -  assumes field_left_inverse: "a \<noteq> 0 \<Longrightarrow> inverse a \<^loc>* a = \<^loc>1"
     1.9 -  assumes divide_inverse:     "a \<^loc>/ b = a \<^loc>* inverse b"
    1.10 +instance division_ring \<subseteq> no_zero_divisors
    1.11 +proof
    1.12 +  fix a b :: 'a
    1.13 +  assume a: "a \<noteq> 0" and b: "b \<noteq> 0"
    1.14 +  show "a * b \<noteq> 0"
    1.15 +  proof
    1.16 +    assume ab: "a * b = 0"
    1.17 +    hence "0 = inverse a * (a * b) * inverse b"
    1.18 +      by simp
    1.19 +    also have "\<dots> = (inverse a * a) * (b * inverse b)"
    1.20 +      by (simp only: mult_assoc)
    1.21 +    also have "\<dots> = 1"
    1.22 +      using a b by simp
    1.23 +    finally show False
    1.24 +      by simp
    1.25 +  qed
    1.26 +qed
    1.27  
    1.28 -lemma field_right_inverse:
    1.29 -  assumes not0: "a \<noteq> 0"
    1.30 -  shows "a * inverse (a::'a::field) = 1"
    1.31 -proof -
    1.32 -  have "a * inverse a = inverse a * a" by (rule mult_commute)
    1.33 -  also have "... = 1" using not0 by (rule field_left_inverse)
    1.34 -  finally show ?thesis .
    1.35 -qed
    1.36 +class field = comm_ring_1 + inverse +
    1.37 +  assumes field_inverse:  "a \<noteq> 0 \<Longrightarrow> inverse a \<^loc>* a = \<^loc>1"
    1.38 +  assumes divide_inverse: "a \<^loc>/ b = a \<^loc>* inverse b"
    1.39  
    1.40  instance field \<subseteq> division_ring
    1.41 -by (intro_classes, erule field_left_inverse, erule field_right_inverse)
    1.42 -
    1.43 -lemma field_mult_eq_0_iff [simp]:
    1.44 -  "(a*b = (0::'a::division_ring)) = (a = 0 | b = 0)"
    1.45 -proof cases
    1.46 -  assume "a=0" thus ?thesis by simp
    1.47 -next
    1.48 -  assume anz [simp]: "a\<noteq>0"
    1.49 -  { assume "a * b = 0"
    1.50 -    hence "inverse a * (a * b) = 0" by simp
    1.51 -    hence "b = 0"  by (simp (no_asm_use) add: mult_assoc [symmetric])}
    1.52 -  thus ?thesis by force
    1.53 +proof
    1.54 +  fix a :: 'a
    1.55 +  assume "a \<noteq> 0"
    1.56 +  thus "inverse a * a = 1" by (rule field_inverse)
    1.57 +  thus "a * inverse a = 1" by (simp only: mult_commute)
    1.58  qed
    1.59  
    1.60 -instance field \<subseteq> idom
    1.61 -by (intro_classes, simp)
    1.62 +instance field \<subseteq> idom ..
    1.63  
    1.64  class division_by_zero = zero + inverse +
    1.65    assumes inverse_zero [simp]: "inverse \<^loc>0 = \<^loc>0"
    1.66 @@ -202,8 +203,7 @@
    1.67  class pordered_semiring = mult_mono + semiring_0 + pordered_ab_semigroup_add 
    1.68  
    1.69  class pordered_cancel_semiring = mult_mono + pordered_ab_semigroup_add
    1.70 -  + semiring + comm_monoid_add + pordered_ab_semigroup_add
    1.71 -  + cancel_ab_semigroup_add
    1.72 +  + semiring + comm_monoid_add + cancel_ab_semigroup_add
    1.73  
    1.74  instance pordered_cancel_semiring \<subseteq> semiring_0_cancel ..
    1.75