src/HOL/Ring_and_Field.thy
changeset 20496 23eb6034c06d
parent 19404 9bf2cdc9e8e8
child 20609 5681da8c12ef
     1.1 --- a/src/HOL/Ring_and_Field.thy	Sat Sep 09 18:28:42 2006 +0200
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Sun Sep 10 05:34:24 2006 +0200
     1.3 @@ -96,9 +96,24 @@
     1.4  
     1.5  axclass idom \<subseteq> comm_ring_1, axclass_no_zero_divisors
     1.6  
     1.7 +axclass division_ring \<subseteq> ring_1, inverse
     1.8 +  left_inverse [simp]:  "a \<noteq> 0 ==> inverse a * a = 1"
     1.9 +  right_inverse [simp]: "a \<noteq> 0 ==> a * inverse a = 1"
    1.10 +
    1.11  axclass field \<subseteq> comm_ring_1, inverse
    1.12 -  left_inverse [simp]: "a \<noteq> 0 ==> inverse a * a = 1"
    1.13 -  divide_inverse:      "a / b = a * inverse b"
    1.14 +  field_left_inverse: "a \<noteq> 0 ==> inverse a * a = 1"
    1.15 +  divide_inverse:     "a / b = a * inverse b"
    1.16 +
    1.17 +lemma field_right_inverse:
    1.18 +      assumes not0: "a \<noteq> 0" shows "a * inverse (a::'a::field) = 1"
    1.19 +proof -
    1.20 +  have "a * inverse a = inverse a * a" by (rule mult_commute)
    1.21 +  also have "... = 1" using not0 by (rule field_left_inverse)
    1.22 +  finally show ?thesis .
    1.23 +qed
    1.24 +
    1.25 +instance field \<subseteq> division_ring
    1.26 +by (intro_classes, erule field_left_inverse, erule field_right_inverse)
    1.27  
    1.28  lemma mult_zero_left [simp]: "0 * a = (0::'a::semiring_0_cancel)"
    1.29  proof -
    1.30 @@ -116,7 +131,8 @@
    1.31      by (simp only: add_left_cancel)
    1.32  qed
    1.33  
    1.34 -lemma field_mult_eq_0_iff [simp]: "(a*b = (0::'a::field)) = (a = 0 | b = 0)"
    1.35 +lemma field_mult_eq_0_iff [simp]:
    1.36 +  "(a*b = (0::'a::division_ring)) = (a = 0 | b = 0)"
    1.37  proof cases
    1.38    assume "a=0" thus ?thesis by simp
    1.39  next
    1.40 @@ -129,7 +145,7 @@
    1.41  
    1.42  instance field \<subseteq> idom
    1.43  by (intro_classes, simp)
    1.44 -  
    1.45 +
    1.46  axclass division_by_zero \<subseteq> zero, inverse
    1.47    inverse_zero [simp]: "inverse 0 = 0"
    1.48  
    1.49 @@ -677,14 +693,6 @@
    1.50      
    1.51  subsection {* Fields *}
    1.52  
    1.53 -lemma right_inverse [simp]:
    1.54 -      assumes not0: "a \<noteq> 0" shows "a * inverse (a::'a::field) = 1"
    1.55 -proof -
    1.56 -  have "a * inverse a = inverse a * a" by (simp add: mult_ac)
    1.57 -  also have "... = 1" using not0 by simp
    1.58 -  finally show ?thesis .
    1.59 -qed
    1.60 -
    1.61  lemma right_inverse_eq: "b \<noteq> 0 ==> (a / b = 1) = (a = (b::'a::field))"
    1.62  proof
    1.63    assume neq: "b \<noteq> 0"
    1.64 @@ -723,7 +731,8 @@
    1.65  
    1.66  text{*Compared with @{text mult_eq_0_iff}, this version removes the requirement
    1.67        of an ordering.*}
    1.68 -lemma field_mult_eq_0_iff [simp]: "(a*b = (0::'a::field)) = (a = 0 | b = 0)"
    1.69 +lemma field_mult_eq_0_iff [simp]:
    1.70 +  "(a*b = (0::'a::division_ring)) = (a = 0 | b = 0)"
    1.71  proof cases
    1.72    assume "a=0" thus ?thesis by simp
    1.73  next
    1.74 @@ -736,9 +745,9 @@
    1.75  
    1.76  text{*Cancellation of equalities with a common factor*}
    1.77  lemma field_mult_cancel_right_lemma:
    1.78 -      assumes cnz: "c \<noteq> (0::'a::field)"
    1.79 -	  and eq:  "a*c = b*c"
    1.80 -	 shows "a=b"
    1.81 +      assumes cnz: "c \<noteq> (0::'a::division_ring)"
    1.82 +         and eq:  "a*c = b*c"
    1.83 +        shows "a=b"
    1.84  proof -
    1.85    have "(a * c) * inverse c = (b * c) * inverse c"
    1.86      by (simp add: eq)
    1.87 @@ -747,48 +756,61 @@
    1.88  qed
    1.89  
    1.90  lemma field_mult_cancel_right [simp]:
    1.91 -     "(a*c = b*c) = (c = (0::'a::field) | a=b)"
    1.92 -proof cases
    1.93 -  assume "c=0" thus ?thesis by simp
    1.94 -next
    1.95 -  assume "c\<noteq>0" 
    1.96 -  thus ?thesis by (force dest: field_mult_cancel_right_lemma)
    1.97 +     "(a*c = b*c) = (c = (0::'a::division_ring) | a=b)"
    1.98 +proof -
    1.99 +  have "(a*c = b*c) = (a*c - b*c = 0)"
   1.100 +    by simp
   1.101 +  also have "\<dots> = ((a - b)*c = 0)"
   1.102 +     by (simp only: left_diff_distrib)
   1.103 +  also have "\<dots> = (c = 0 \<or> a = b)"
   1.104 +     by (simp add: disj_commute)
   1.105 +  finally show ?thesis .
   1.106  qed
   1.107  
   1.108  lemma field_mult_cancel_left [simp]:
   1.109 -     "(c*a = c*b) = (c = (0::'a::field) | a=b)"
   1.110 -  by (simp add: mult_commute [of c] field_mult_cancel_right) 
   1.111 +     "(c*a = c*b) = (c = (0::'a::division_ring) | a=b)"
   1.112 +proof -
   1.113 +  have "(c*a = c*b) = (c*a - c*b = 0)"
   1.114 +    by simp
   1.115 +  also have "\<dots> = (c*(a - b) = 0)"
   1.116 +     by (simp only: right_diff_distrib)
   1.117 +  also have "\<dots> = (c = 0 \<or> a = b)"
   1.118 +     by simp
   1.119 +  finally show ?thesis .
   1.120 +qed
   1.121  
   1.122 -lemma nonzero_imp_inverse_nonzero: "a \<noteq> 0 ==> inverse a \<noteq> (0::'a::field)"
   1.123 +lemma nonzero_imp_inverse_nonzero:
   1.124 +  "a \<noteq> 0 ==> inverse a \<noteq> (0::'a::division_ring)"
   1.125  proof
   1.126    assume ianz: "inverse a = 0"
   1.127    assume "a \<noteq> 0"
   1.128    hence "1 = a * inverse a" by simp
   1.129    also have "... = 0" by (simp add: ianz)
   1.130 -  finally have "1 = (0::'a::field)" .
   1.131 +  finally have "1 = (0::'a::division_ring)" .
   1.132    thus False by (simp add: eq_commute)
   1.133  qed
   1.134  
   1.135  
   1.136  subsection{*Basic Properties of @{term inverse}*}
   1.137  
   1.138 -lemma inverse_zero_imp_zero: "inverse a = 0 ==> a = (0::'a::field)"
   1.139 +lemma inverse_zero_imp_zero: "inverse a = 0 ==> a = (0::'a::division_ring)"
   1.140  apply (rule ccontr) 
   1.141  apply (blast dest: nonzero_imp_inverse_nonzero) 
   1.142  done
   1.143  
   1.144  lemma inverse_nonzero_imp_nonzero:
   1.145 -   "inverse a = 0 ==> a = (0::'a::field)"
   1.146 +   "inverse a = 0 ==> a = (0::'a::division_ring)"
   1.147  apply (rule ccontr) 
   1.148  apply (blast dest: nonzero_imp_inverse_nonzero) 
   1.149  done
   1.150  
   1.151  lemma inverse_nonzero_iff_nonzero [simp]:
   1.152 -   "(inverse a = 0) = (a = (0::'a::{field,division_by_zero}))"
   1.153 +   "(inverse a = 0) = (a = (0::'a::{division_ring,division_by_zero}))"
   1.154  by (force dest: inverse_nonzero_imp_nonzero) 
   1.155  
   1.156  lemma nonzero_inverse_minus_eq:
   1.157 -      assumes [simp]: "a\<noteq>0"  shows "inverse(-a) = -inverse(a::'a::field)"
   1.158 +      assumes [simp]: "a\<noteq>0"
   1.159 +      shows "inverse(-a) = -inverse(a::'a::division_ring)"
   1.160  proof -
   1.161    have "-a * inverse (- a) = -a * - inverse a"
   1.162      by simp
   1.163 @@ -797,7 +819,7 @@
   1.164  qed
   1.165  
   1.166  lemma inverse_minus_eq [simp]:
   1.167 -   "inverse(-a) = -inverse(a::'a::{field,division_by_zero})"
   1.168 +   "inverse(-a) = -inverse(a::'a::{division_ring,division_by_zero})"
   1.169  proof cases
   1.170    assume "a=0" thus ?thesis by (simp add: inverse_zero)
   1.171  next
   1.172 @@ -809,7 +831,7 @@
   1.173        assumes inveq: "inverse a = inverse b"
   1.174  	  and anz:  "a \<noteq> 0"
   1.175  	  and bnz:  "b \<noteq> 0"
   1.176 -	 shows "a = (b::'a::field)"
   1.177 +	 shows "a = (b::'a::division_ring)"
   1.178  proof -
   1.179    have "a * inverse b = a * inverse a"
   1.180      by (simp add: inveq)
   1.181 @@ -820,7 +842,7 @@
   1.182  qed
   1.183  
   1.184  lemma inverse_eq_imp_eq:
   1.185 -     "inverse a = inverse b ==> a = (b::'a::{field,division_by_zero})"
   1.186 +  "inverse a = inverse b ==> a = (b::'a::{division_ring,division_by_zero})"
   1.187  apply (case_tac "a=0 | b=0") 
   1.188   apply (force dest!: inverse_zero_imp_zero
   1.189                simp add: eq_commute [of "0::'a"])
   1.190 @@ -828,11 +850,12 @@
   1.191  done
   1.192  
   1.193  lemma inverse_eq_iff_eq [simp]:
   1.194 -     "(inverse a = inverse b) = (a = (b::'a::{field,division_by_zero}))"
   1.195 -by (force dest!: inverse_eq_imp_eq) 
   1.196 +  "(inverse a = inverse b) = (a = (b::'a::{division_ring,division_by_zero}))"
   1.197 +by (force dest!: inverse_eq_imp_eq)
   1.198  
   1.199  lemma nonzero_inverse_inverse_eq:
   1.200 -      assumes [simp]: "a \<noteq> 0"  shows "inverse(inverse (a::'a::field)) = a"
   1.201 +      assumes [simp]: "a \<noteq> 0"
   1.202 +      shows "inverse(inverse (a::'a::division_ring)) = a"
   1.203    proof -
   1.204    have "(inverse (inverse a) * inverse a) * a = a" 
   1.205      by (simp add: nonzero_imp_inverse_nonzero)
   1.206 @@ -841,7 +864,7 @@
   1.207    qed
   1.208  
   1.209  lemma inverse_inverse_eq [simp]:
   1.210 -     "inverse(inverse (a::'a::{field,division_by_zero})) = a"
   1.211 +     "inverse(inverse (a::'a::{division_ring,division_by_zero})) = a"
   1.212    proof cases
   1.213      assume "a=0" thus ?thesis by simp
   1.214    next
   1.215 @@ -849,16 +872,16 @@
   1.216      thus ?thesis by (simp add: nonzero_inverse_inverse_eq)
   1.217    qed
   1.218  
   1.219 -lemma inverse_1 [simp]: "inverse 1 = (1::'a::field)"
   1.220 +lemma inverse_1 [simp]: "inverse 1 = (1::'a::division_ring)"
   1.221    proof -
   1.222 -  have "inverse 1 * 1 = (1::'a::field)" 
   1.223 +  have "inverse 1 * 1 = (1::'a::division_ring)" 
   1.224      by (rule left_inverse [OF zero_neq_one [symmetric]])
   1.225    thus ?thesis  by simp
   1.226    qed
   1.227  
   1.228  lemma inverse_unique: 
   1.229    assumes ab: "a*b = 1"
   1.230 -  shows "inverse a = (b::'a::field)"
   1.231 +  shows "inverse a = (b::'a::division_ring)"
   1.232  proof -
   1.233    have "a \<noteq> 0" using ab by auto
   1.234    moreover have "inverse a * (a * b) = inverse a" by (simp add: ab) 
   1.235 @@ -868,7 +891,7 @@
   1.236  lemma nonzero_inverse_mult_distrib: 
   1.237        assumes anz: "a \<noteq> 0"
   1.238            and bnz: "b \<noteq> 0"
   1.239 -      shows "inverse(a*b) = inverse(b) * inverse(a::'a::field)"
   1.240 +      shows "inverse(a*b) = inverse(b) * inverse(a::'a::division_ring)"
   1.241    proof -
   1.242    have "inverse(a*b) * (a * b) * inverse(b) = inverse(b)" 
   1.243      by (simp add: field_mult_eq_0_iff anz bnz)
   1.244 @@ -892,14 +915,21 @@
   1.245      thus ?thesis  by force
   1.246    qed
   1.247  
   1.248 +lemma division_ring_inverse_add:
   1.249 +  "[|(a::'a::division_ring) \<noteq> 0; b \<noteq> 0|]
   1.250 +   ==> inverse a + inverse b = inverse a * (a+b) * inverse b"
   1.251 +by (simp add: right_distrib left_distrib mult_assoc)
   1.252 +
   1.253 +lemma division_ring_inverse_diff:
   1.254 +  "[|(a::'a::division_ring) \<noteq> 0; b \<noteq> 0|]
   1.255 +   ==> inverse a - inverse b = inverse a * (b-a) * inverse b"
   1.256 +by (simp add: right_diff_distrib left_diff_distrib mult_assoc)
   1.257 +
   1.258  text{*There is no slick version using division by zero.*}
   1.259  lemma inverse_add:
   1.260       "[|a \<noteq> 0;  b \<noteq> 0|]
   1.261        ==> inverse a + inverse b = (a+b) * inverse a * inverse (b::'a::field)"
   1.262 -apply (simp add: left_distrib mult_assoc)
   1.263 -apply (simp add: mult_commute [of "inverse a"]) 
   1.264 -apply (simp add: mult_assoc [symmetric] add_commute)
   1.265 -done
   1.266 +by (simp add: division_ring_inverse_add mult_ac)
   1.267  
   1.268  lemma inverse_divide [simp]:
   1.269        "inverse (a/b) = b / (a::'a::{field,division_by_zero})"