src/HOL/Ring_and_Field.thy
changeset 14377 f454b3004f8f
parent 14370 b0064703967b
child 14387 e96d5c42c4b0
     1.1 --- a/src/HOL/Ring_and_Field.thy	Thu Feb 05 04:30:38 2004 +0100
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Thu Feb 05 10:45:28 2004 +0100
     1.3 @@ -94,10 +94,10 @@
     1.4    by (simp add: add_commute)
     1.5  
     1.6  lemma minus_minus [simp]: "- (- (a::'a::ring)) = a"
     1.7 -  proof (rule add_left_cancel [of "-a", THEN iffD1])
     1.8 -    show "(-a + -(-a) = -a + a)"
     1.9 -    by simp
    1.10 -  qed
    1.11 +proof (rule add_left_cancel [of "-a", THEN iffD1])
    1.12 +  show "(-a + -(-a) = -a + a)"
    1.13 +  by simp
    1.14 +qed
    1.15  
    1.16  lemma equals_zero_I: "a+b = 0 ==> -a = (b::'a::ring)"
    1.17  apply (rule right_minus_eq [THEN iffD1, symmetric])
    1.18 @@ -120,15 +120,15 @@
    1.19  by (simp add: diff_minus)
    1.20  
    1.21  lemma neg_equal_iff_equal [simp]: "(-a = -b) = (a = (b::'a::ring))" 
    1.22 -  proof 
    1.23 -    assume "- a = - b"
    1.24 -    hence "- (- a) = - (- b)"
    1.25 -      by simp
    1.26 -    thus "a=b" by simp
    1.27 -  next
    1.28 -    assume "a=b"
    1.29 -    thus "-a = -b" by simp
    1.30 -  qed
    1.31 +proof 
    1.32 +  assume "- a = - b"
    1.33 +  hence "- (- a) = - (- b)"
    1.34 +    by simp
    1.35 +  thus "a=b" by simp
    1.36 +next
    1.37 +  assume "a=b"
    1.38 +  thus "-a = -b" by simp
    1.39 +qed
    1.40  
    1.41  lemma neg_equal_0_iff_equal [simp]: "(-a = 0) = (a = (0::'a::ring))"
    1.42  by (subst neg_equal_iff_equal [symmetric], simp)
    1.43 @@ -139,16 +139,16 @@
    1.44  text{*The next two equations can make the simplifier loop!*}
    1.45  
    1.46  lemma equation_minus_iff: "(a = - b) = (b = - (a::'a::ring))"
    1.47 -  proof -
    1.48 +proof -
    1.49    have "(- (-a) = - b) = (- a = b)" by (rule neg_equal_iff_equal)
    1.50    thus ?thesis by (simp add: eq_commute)
    1.51 -  qed
    1.52 +qed
    1.53  
    1.54  lemma minus_equation_iff: "(- a = b) = (- (b::'a::ring) = a)"
    1.55 -  proof -
    1.56 +proof -
    1.57    have "(- a = - (-b)) = (a = -b)" by (rule neg_equal_iff_equal)
    1.58    thus ?thesis by (simp add: eq_commute)
    1.59 -  qed
    1.60 +qed
    1.61  
    1.62  
    1.63  subsection {* Derived rules for multiplication *}
    1.64 @@ -263,13 +263,13 @@
    1.65  
    1.66  lemma add_less_imp_less_left:
    1.67        assumes less: "c + a < c + b"  shows "a < (b::'a::ordered_semiring)"
    1.68 -  proof (rule ccontr)
    1.69 -    assume "~ a < b"
    1.70 -    hence "b \<le> a" by (simp add: linorder_not_less)
    1.71 -    hence "c+b \<le> c+a" by (rule add_left_mono)
    1.72 -    with this and less show False 
    1.73 -      by (simp add: linorder_not_less [symmetric])
    1.74 -  qed
    1.75 +proof (rule ccontr)
    1.76 +  assume "~ a < b"
    1.77 +  hence "b \<le> a" by (simp add: linorder_not_less)
    1.78 +  hence "c+b \<le> c+a" by (rule add_left_mono)
    1.79 +  with this and less show False 
    1.80 +    by (simp add: linorder_not_less [symmetric])
    1.81 +qed
    1.82  
    1.83  lemma add_less_imp_less_right:
    1.84        "a + c < b + c ==> a < (b::'a::ordered_semiring)"
    1.85 @@ -306,7 +306,7 @@
    1.86  
    1.87  lemma le_imp_neg_le:
    1.88        assumes "a \<le> (b::'a::ordered_ring)" shows "-b \<le> -a"
    1.89 -  proof -
    1.90 +proof -
    1.91    have "-a+a \<le> -a+b"
    1.92      by (rule add_left_mono) 
    1.93    hence "0 \<le> -a+b"
    1.94 @@ -315,18 +315,18 @@
    1.95      by (rule add_right_mono) 
    1.96    thus ?thesis
    1.97      by (simp add: add_assoc)
    1.98 -  qed
    1.99 +qed
   1.100  
   1.101  lemma neg_le_iff_le [simp]: "(-b \<le> -a) = (a \<le> (b::'a::ordered_ring))"
   1.102 -  proof 
   1.103 -    assume "- b \<le> - a"
   1.104 -    hence "- (- a) \<le> - (- b)"
   1.105 -      by (rule le_imp_neg_le)
   1.106 -    thus "a\<le>b" by simp
   1.107 -  next
   1.108 -    assume "a\<le>b"
   1.109 -    thus "-b \<le> -a" by (rule le_imp_neg_le)
   1.110 -  qed
   1.111 +proof 
   1.112 +  assume "- b \<le> - a"
   1.113 +  hence "- (- a) \<le> - (- b)"
   1.114 +    by (rule le_imp_neg_le)
   1.115 +  thus "a\<le>b" by simp
   1.116 +next
   1.117 +  assume "a\<le>b"
   1.118 +  thus "-b \<le> -a" by (rule le_imp_neg_le)
   1.119 +qed
   1.120  
   1.121  lemma neg_le_0_iff_le [simp]: "(-a \<le> 0) = (0 \<le> (a::'a::ordered_ring))"
   1.122  by (subst neg_le_iff_le [symmetric], simp)
   1.123 @@ -346,16 +346,16 @@
   1.124  text{*The next several equations can make the simplifier loop!*}
   1.125  
   1.126  lemma less_minus_iff: "(a < - b) = (b < - (a::'a::ordered_ring))"
   1.127 -  proof -
   1.128 +proof -
   1.129    have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less)
   1.130    thus ?thesis by simp
   1.131 -  qed
   1.132 +qed
   1.133  
   1.134  lemma minus_less_iff: "(- a < b) = (- b < (a::'a::ordered_ring))"
   1.135 -  proof -
   1.136 +proof -
   1.137    have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less)
   1.138    thus ?thesis by simp
   1.139 -  qed
   1.140 +qed
   1.141  
   1.142  lemma le_minus_iff: "(a \<le> - b) = (b \<le> - (a::'a::ordered_ring))"
   1.143  apply (simp add: linorder_not_less [symmetric])
   1.144 @@ -645,13 +645,13 @@
   1.145  lemma mult_less_imp_less_left:
   1.146        assumes less: "c*a < c*b" and nonneg: "0 \<le> c"
   1.147        shows "a < (b::'a::ordered_semiring)"
   1.148 -  proof (rule ccontr)
   1.149 -    assume "~ a < b"
   1.150 -    hence "b \<le> a" by (simp add: linorder_not_less)
   1.151 -    hence "c*b \<le> c*a" by (rule mult_left_mono)
   1.152 -    with this and less show False 
   1.153 -      by (simp add: linorder_not_less [symmetric])
   1.154 -  qed
   1.155 +proof (rule ccontr)
   1.156 +  assume "~ a < b"
   1.157 +  hence "b \<le> a" by (simp add: linorder_not_less)
   1.158 +  hence "c*b \<le> c*a" by (rule mult_left_mono)
   1.159 +  with this and less show False 
   1.160 +    by (simp add: linorder_not_less [symmetric])
   1.161 +qed
   1.162  
   1.163  lemma mult_less_imp_less_right:
   1.164      "[|a*c < b*c; 0 \<le> c|] ==> a < (b::'a::ordered_semiring)"
   1.165 @@ -723,52 +723,50 @@
   1.166  text{*Compared with @{text mult_eq_0_iff}, this version removes the requirement
   1.167        of an ordering.*}
   1.168  lemma field_mult_eq_0_iff [simp]: "(a*b = (0::'a::field)) = (a = 0 | b = 0)"
   1.169 -  proof cases
   1.170 -    assume "a=0" thus ?thesis by simp
   1.171 -  next
   1.172 -    assume anz [simp]: "a\<noteq>0"
   1.173 -    thus ?thesis
   1.174 -    proof auto
   1.175 -      assume "a * b = 0"
   1.176 -      hence "inverse a * (a * b) = 0" by simp
   1.177 -      thus "b = 0"  by (simp (no_asm_use) add: mult_assoc [symmetric])
   1.178 -    qed
   1.179 -  qed
   1.180 +proof cases
   1.181 +  assume "a=0" thus ?thesis by simp
   1.182 +next
   1.183 +  assume anz [simp]: "a\<noteq>0"
   1.184 +  { assume "a * b = 0"
   1.185 +    hence "inverse a * (a * b) = 0" by simp
   1.186 +    hence "b = 0"  by (simp (no_asm_use) add: mult_assoc [symmetric])}
   1.187 +  thus ?thesis by force
   1.188 +qed
   1.189  
   1.190  text{*Cancellation of equalities with a common factor*}
   1.191  lemma field_mult_cancel_right_lemma:
   1.192        assumes cnz: "c \<noteq> (0::'a::field)"
   1.193  	  and eq:  "a*c = b*c"
   1.194  	 shows "a=b"
   1.195 -  proof -
   1.196 +proof -
   1.197    have "(a * c) * inverse c = (b * c) * inverse c"
   1.198      by (simp add: eq)
   1.199    thus "a=b"
   1.200      by (simp add: mult_assoc cnz)
   1.201 -  qed
   1.202 +qed
   1.203  
   1.204  lemma field_mult_cancel_right [simp]:
   1.205       "(a*c = b*c) = (c = (0::'a::field) | a=b)"
   1.206 -  proof cases
   1.207 -    assume "c=0" thus ?thesis by simp
   1.208 -  next
   1.209 -    assume "c\<noteq>0" 
   1.210 -    thus ?thesis by (force dest: field_mult_cancel_right_lemma)
   1.211 -  qed
   1.212 +proof cases
   1.213 +  assume "c=0" thus ?thesis by simp
   1.214 +next
   1.215 +  assume "c\<noteq>0" 
   1.216 +  thus ?thesis by (force dest: field_mult_cancel_right_lemma)
   1.217 +qed
   1.218  
   1.219  lemma field_mult_cancel_left [simp]:
   1.220       "(c*a = c*b) = (c = (0::'a::field) | a=b)"
   1.221    by (simp add: mult_commute [of c] field_mult_cancel_right) 
   1.222  
   1.223  lemma nonzero_imp_inverse_nonzero: "a \<noteq> 0 ==> inverse a \<noteq> (0::'a::field)"
   1.224 -  proof
   1.225 +proof
   1.226    assume ianz: "inverse a = 0"
   1.227    assume "a \<noteq> 0"
   1.228    hence "1 = a * inverse a" by simp
   1.229    also have "... = 0" by (simp add: ianz)
   1.230    finally have "1 = (0::'a::field)" .
   1.231    thus False by (simp add: eq_commute)
   1.232 -  qed
   1.233 +qed
   1.234  
   1.235  
   1.236  subsection{*Basic Properties of @{term inverse}*}
   1.237 @@ -790,35 +788,35 @@
   1.238  
   1.239  lemma nonzero_inverse_minus_eq:
   1.240        assumes [simp]: "a\<noteq>0"  shows "inverse(-a) = -inverse(a::'a::field)"
   1.241 -  proof -
   1.242 -    have "-a * inverse (- a) = -a * - inverse a"
   1.243 -      by simp
   1.244 -    thus ?thesis 
   1.245 -      by (simp only: field_mult_cancel_left, simp)
   1.246 -  qed
   1.247 +proof -
   1.248 +  have "-a * inverse (- a) = -a * - inverse a"
   1.249 +    by simp
   1.250 +  thus ?thesis 
   1.251 +    by (simp only: field_mult_cancel_left, simp)
   1.252 +qed
   1.253  
   1.254  lemma inverse_minus_eq [simp]:
   1.255 -     "inverse(-a) = -inverse(a::'a::{field,division_by_zero})";
   1.256 -  proof cases
   1.257 -    assume "a=0" thus ?thesis by (simp add: inverse_zero)
   1.258 -  next
   1.259 -    assume "a\<noteq>0" 
   1.260 -    thus ?thesis by (simp add: nonzero_inverse_minus_eq)
   1.261 -  qed
   1.262 +   "inverse(-a) = -inverse(a::'a::{field,division_by_zero})";
   1.263 +proof cases
   1.264 +  assume "a=0" thus ?thesis by (simp add: inverse_zero)
   1.265 +next
   1.266 +  assume "a\<noteq>0" 
   1.267 +  thus ?thesis by (simp add: nonzero_inverse_minus_eq)
   1.268 +qed
   1.269  
   1.270  lemma nonzero_inverse_eq_imp_eq:
   1.271        assumes inveq: "inverse a = inverse b"
   1.272  	  and anz:  "a \<noteq> 0"
   1.273  	  and bnz:  "b \<noteq> 0"
   1.274  	 shows "a = (b::'a::field)"
   1.275 -  proof -
   1.276 +proof -
   1.277    have "a * inverse b = a * inverse a"
   1.278      by (simp add: inveq)
   1.279    hence "(a * inverse b) * b = (a * inverse a) * b"
   1.280      by simp
   1.281    thus "a = b"
   1.282      by (simp add: mult_assoc anz bnz)
   1.283 -  qed
   1.284 +qed
   1.285  
   1.286  lemma inverse_eq_imp_eq:
   1.287       "inverse a = inverse b ==> a = (b::'a::{field,division_by_zero})"