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.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.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.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.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.93    hence "0 \<le> -a+b"
1.94 @@ -315,18 +315,18 @@
1.96    thus ?thesis
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.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"