src/HOL/Rings.thy
 changeset 36301 72f4d079ebf8 parent 35828 46cfc4b8112e child 36304 6984744e6b34
```     1.1 --- a/src/HOL/Rings.thy	Fri Apr 23 13:58:14 2010 +0200
1.2 +++ b/src/HOL/Rings.thy	Fri Apr 23 13:58:14 2010 +0200
1.3 @@ -487,6 +487,125 @@
1.4    "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a - inverse b = inverse a * (b - a) * inverse b"
1.6
1.7 +lemma right_inverse_eq: "b \<noteq> 0 \<Longrightarrow> a / b = 1 \<longleftrightarrow> a = b"
1.8 +proof
1.9 +  assume neq: "b \<noteq> 0"
1.10 +  {
1.11 +    hence "a = (a / b) * b" by (simp add: divide_inverse mult_assoc)
1.12 +    also assume "a / b = 1"
1.13 +    finally show "a = b" by simp
1.14 +  next
1.15 +    assume "a = b"
1.16 +    with neq show "a / b = 1" by (simp add: divide_inverse)
1.17 +  }
1.18 +qed
1.19 +
1.20 +lemma nonzero_inverse_eq_divide: "a \<noteq> 0 \<Longrightarrow> inverse a = 1 / a"
1.22 +
1.23 +lemma divide_self [simp]: "a \<noteq> 0 \<Longrightarrow> a / a = 1"
1.25 +
1.26 +lemma divide_zero_left [simp]: "0 / a = 0"
1.28 +
1.29 +lemma inverse_eq_divide: "inverse a = 1 / a"
1.31 +
1.32 +lemma add_divide_distrib: "(a+b) / c = a/c + b/c"
1.33 +by (simp add: divide_inverse algebra_simps)
1.34 +
1.35 +lemma divide_1 [simp]: "a / 1 = a"
1.36 +  by (simp add: divide_inverse)
1.37 +
1.38 +lemma times_divide_eq_right: "a * (b / c) = (a * b) / c"
1.39 +  by (simp add: divide_inverse mult_assoc)
1.40 +
1.41 +lemma minus_divide_left: "- (a / b) = (-a) / b"
1.42 +  by (simp add: divide_inverse)
1.43 +
1.44 +lemma nonzero_minus_divide_right: "b \<noteq> 0 ==> - (a / b) = a / (- b)"
1.45 +  by (simp add: divide_inverse nonzero_inverse_minus_eq)
1.46 +
1.47 +lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a) / (-b) = a / b"
1.48 +  by (simp add: divide_inverse nonzero_inverse_minus_eq)
1.49 +
1.50 +lemma divide_minus_left [simp, no_atp]: "(-a) / b = - (a / b)"
1.51 +  by (simp add: divide_inverse)
1.52 +
1.53 +lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"
1.55 +
1.56 +lemma nonzero_eq_divide_eq: "c \<noteq> 0 \<Longrightarrow> a = b / c \<longleftrightarrow> a * c = b"
1.57 +proof -
1.58 +  assume [simp]: "c \<noteq> 0"
1.59 +  have "a = b / c \<longleftrightarrow> a * c = (b / c) * c" by simp
1.60 +  also have "... \<longleftrightarrow> a * c = b" by (simp add: divide_inverse mult_assoc)
1.61 +  finally show ?thesis .
1.62 +qed
1.63 +
1.64 +lemma nonzero_divide_eq_eq: "c \<noteq> 0 \<Longrightarrow> b / c = a \<longleftrightarrow> b = a * c"
1.65 +proof -
1.66 +  assume [simp]: "c \<noteq> 0"
1.67 +  have "b / c = a \<longleftrightarrow> (b / c) * c = a * c" by simp
1.68 +  also have "... \<longleftrightarrow> b = a * c" by (simp add: divide_inverse mult_assoc)
1.69 +  finally show ?thesis .
1.70 +qed
1.71 +
1.72 +lemma divide_eq_imp: "c \<noteq> 0 \<Longrightarrow> b = a * c \<Longrightarrow> b / c = a"
1.73 +  by (simp add: divide_inverse mult_assoc)
1.74 +
1.75 +lemma eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c"
1.76 +  by (drule sym) (simp add: divide_inverse mult_assoc)
1.77 +
1.78 +end
1.79 +
1.80 +class division_by_zero = division_ring +
1.81 +  assumes inverse_zero [simp]: "inverse 0 = 0"
1.82 +begin
1.83 +
1.84 +lemma divide_zero [simp]:
1.85 +  "a / 0 = 0"
1.86 +  by (simp add: divide_inverse)
1.87 +
1.88 +lemma divide_self_if [simp]:
1.89 +  "a / a = (if a = 0 then 0 else 1)"
1.90 +  by simp
1.91 +
1.92 +lemma inverse_nonzero_iff_nonzero [simp]:
1.93 +  "inverse a = 0 \<longleftrightarrow> a = 0"
1.94 +  by rule (fact inverse_zero_imp_zero, simp)
1.95 +
1.96 +lemma inverse_minus_eq [simp]:
1.97 +  "inverse (- a) = - inverse a"
1.98 +proof cases
1.99 +  assume "a=0" thus ?thesis by simp
1.100 +next
1.101 +  assume "a\<noteq>0"
1.102 +  thus ?thesis by (simp add: nonzero_inverse_minus_eq)
1.103 +qed
1.104 +
1.105 +lemma inverse_eq_imp_eq:
1.106 +  "inverse a = inverse b \<Longrightarrow> a = b"
1.107 +apply (cases "a=0 | b=0")
1.108 + apply (force dest!: inverse_zero_imp_zero
1.109 +              simp add: eq_commute [of "0::'a"])
1.110 +apply (force dest!: nonzero_inverse_eq_imp_eq)
1.111 +done
1.112 +
1.113 +lemma inverse_eq_iff_eq [simp]:
1.114 +  "inverse a = inverse b \<longleftrightarrow> a = b"
1.115 +  by (force dest!: inverse_eq_imp_eq)
1.116 +
1.117 +lemma inverse_inverse_eq [simp]:
1.118 +  "inverse (inverse a) = a"
1.119 +proof cases
1.120 +  assume "a=0" thus ?thesis by simp
1.121 +next
1.122 +  assume "a\<noteq>0"
1.123 +  thus ?thesis by (simp add: nonzero_inverse_inverse_eq)
1.124 +qed
1.125 +
1.126  end
1.127
1.128  class mult_mono = times + zero + ord +
1.129 @@ -533,17 +652,17 @@
1.130  subclass ordered_semiring ..
1.131
1.132  lemma mult_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
1.133 -using mult_left_mono [of zero b a] by simp
1.134 +using mult_left_mono [of 0 b a] by simp
1.135
1.136  lemma mult_nonneg_nonpos: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> a * b \<le> 0"
1.137 -using mult_left_mono [of b zero a] by simp
1.138 +using mult_left_mono [of b 0 a] by simp
1.139
1.140  lemma mult_nonpos_nonneg: "a \<le> 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a * b \<le> 0"
1.141 -using mult_right_mono [of a zero b] by simp
1.142 +using mult_right_mono [of a 0 b] by simp
1.143
1.144  text {* Legacy - use @{text mult_nonpos_nonneg} *}
1.145  lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0"
1.146 -by (drule mult_right_mono [of b zero], auto)
1.147 +by (drule mult_right_mono [of b 0], auto)
1.148
1.149  lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> 0"
1.150  by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)
1.151 @@ -597,17 +716,17 @@
1.152  by (force simp add: mult_strict_right_mono not_less [symmetric])
1.153
1.154  lemma mult_pos_pos: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"
1.155 -using mult_strict_left_mono [of zero b a] by simp
1.156 +using mult_strict_left_mono [of 0 b a] by simp
1.157
1.158  lemma mult_pos_neg: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0"
1.159 -using mult_strict_left_mono [of b zero a] by simp
1.160 +using mult_strict_left_mono [of b 0 a] by simp
1.161
1.162  lemma mult_neg_pos: "a < 0 \<Longrightarrow> 0 < b \<Longrightarrow> a * b < 0"
1.163 -using mult_strict_right_mono [of a zero b] by simp
1.164 +using mult_strict_right_mono [of a 0 b] by simp
1.165
1.166  text {* Legacy - use @{text mult_neg_pos} *}
1.167  lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0"
1.168 -by (drule mult_strict_right_mono [of b zero], auto)
1.169 +by (drule mult_strict_right_mono [of b 0], auto)
1.170
1.171  lemma zero_less_mult_pos:
1.172    "0 < a * b \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
1.173 @@ -763,18 +882,18 @@
1.174
1.175  lemma mult_left_mono_neg:
1.176    "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> c * b"
1.177 -  apply (drule mult_left_mono [of _ _ "uminus c"])
1.178 +  apply (drule mult_left_mono [of _ _ "- c"])
1.179    apply simp_all
1.180    done
1.181
1.182  lemma mult_right_mono_neg:
1.183    "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> b * c"
1.184 -  apply (drule mult_right_mono [of _ _ "uminus c"])
1.185 +  apply (drule mult_right_mono [of _ _ "- c"])
1.186    apply simp_all
1.187    done
1.188
1.189  lemma mult_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"
1.190 -using mult_right_mono_neg [of a zero b] by simp
1.191 +using mult_right_mono_neg [of a 0 b] by simp
1.192
1.193  lemma split_mult_pos_le:
1.194    "(0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0) \<Longrightarrow> 0 \<le> a * b"
1.195 @@ -821,7 +940,7 @@
1.196  using mult_strict_right_mono [of b a "- c"] by simp
1.197
1.198  lemma mult_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b"
1.199 -using mult_strict_right_mono_neg [of a zero b] by simp
1.200 +using mult_strict_right_mono_neg [of a 0 b] by simp
1.201
1.202  subclass ring_no_zero_divisors
1.203  proof
1.204 @@ -973,7 +1092,7 @@
1.205
1.207    shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
1.208 -  using add_strict_mono [of zero a b c] by simp
1.209 +  using add_strict_mono [of 0 a b c] by simp
1.210
1.211  lemma zero_le_one [simp]: "0 \<le> 1"
1.212  by (rule zero_less_one [THEN less_imp_le])
1.213 @@ -1074,7 +1193,7 @@
1.214    "sgn (a * b) = sgn a * sgn b"
1.215  by (auto simp add: sgn_if zero_less_mult_iff)
1.216
1.217 -lemma abs_sgn: "abs k = k * sgn k"
1.218 +lemma abs_sgn: "\<bar>k\<bar> = k * sgn k"
1.219  unfolding sgn_if abs_if by auto
1.220
1.221  lemma sgn_greater [simp]:
1.222 @@ -1085,14 +1204,14 @@
1.223    "sgn a < 0 \<longleftrightarrow> a < 0"
1.224    unfolding sgn_if by auto
1.225
1.226 -lemma abs_dvd_iff [simp]: "(abs m) dvd k \<longleftrightarrow> m dvd k"
1.227 +lemma abs_dvd_iff [simp]: "\<bar>m\<bar> dvd k \<longleftrightarrow> m dvd k"
1.229
1.230 -lemma dvd_abs_iff [simp]: "m dvd (abs k) \<longleftrightarrow> m dvd k"
1.231 +lemma dvd_abs_iff [simp]: "m dvd \<bar>k\<bar> \<longleftrightarrow> m dvd k"
1.233
1.234  lemma dvd_if_abs_eq:
1.235 -  "abs l = abs (k) \<Longrightarrow> l dvd k"
1.236 +  "\<bar>l\<bar> = \<bar>k\<bar> \<Longrightarrow> l dvd k"
1.237  by(subst abs_dvd_iff[symmetric]) simp
1.238
1.239  end
1.240 @@ -1110,17 +1229,7 @@
1.241      mult_cancel_right1 mult_cancel_right2
1.242      mult_cancel_left1 mult_cancel_left2
1.243
1.244 --- {* FIXME continue localization here *}
1.245 -
1.246 -subsection {* Reasoning about inequalities with division *}
1.247 -
1.248 -lemma mult_right_le_one_le: "0 <= (x::'a::linordered_idom) ==> 0 <= y ==> y <= 1
1.249 -    ==> x * y <= x"
1.250 -by (auto simp add: mult_le_cancel_left2)
1.251 -
1.252 -lemma mult_left_le_one_le: "0 <= (x::'a::linordered_idom) ==> 0 <= y ==> y <= 1
1.253 -    ==> y * x <= x"
1.254 -by (auto simp add: mult_le_cancel_right2)
1.255 +text {* Reasoning about inequalities with division *}
1.256
1.257  context linordered_semidom
1.258  begin
1.259 @@ -1137,20 +1246,34 @@
1.260
1.261  end
1.262
1.263 +context linordered_idom
1.264 +begin
1.265
1.266 -subsection {* Absolute Value *}
1.267 +lemma mult_right_le_one_le:
1.268 +  "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> x * y \<le> x"
1.269 +  by (auto simp add: mult_le_cancel_left2)
1.270 +
1.271 +lemma mult_left_le_one_le:
1.272 +  "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> y * x \<le> x"
1.273 +  by (auto simp add: mult_le_cancel_right2)
1.274 +
1.275 +end
1.276 +
1.277 +text {* Absolute Value *}
1.278
1.279  context linordered_idom
1.280  begin
1.281
1.282 -lemma mult_sgn_abs: "sgn x * abs x = x"
1.283 +lemma mult_sgn_abs:
1.284 +  "sgn x * \<bar>x\<bar> = x"
1.285    unfolding abs_if sgn_if by auto
1.286
1.287 +lemma abs_one [simp]:
1.288 +  "\<bar>1\<bar> = 1"
1.289 +  by (simp add: abs_if zero_less_one [THEN less_not_sym])
1.290 +
1.291  end
1.292
1.293 -lemma abs_one [simp]: "abs 1 = (1::'a::linordered_idom)"
1.294 -by (simp add: abs_if zero_less_one [THEN order_less_not_sym])
1.295 -
1.296  class ordered_ring_abs = ordered_ring + ordered_ab_group_add_abs +
1.297    assumes abs_eq_mult:
1.298      "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0) \<Longrightarrow> \<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
1.299 @@ -1162,39 +1285,35 @@
1.300  qed (auto simp add: abs_if not_less mult_less_0_iff)
1.301
1.302  lemma abs_mult:
1.303 -  "abs (a * b) = abs a * abs b"
1.304 +  "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
1.305    by (rule abs_eq_mult) auto
1.306
1.307  lemma abs_mult_self:
1.308 -  "abs a * abs a = a * a"
1.309 +  "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
1.311
1.312 -end
1.313 -
1.314  lemma abs_mult_less:
1.315 -     "[| abs a < c; abs b < d |] ==> abs a * abs b < c*(d::'a::linordered_idom)"
1.316 +  "\<bar>a\<bar> < c \<Longrightarrow> \<bar>b\<bar> < d \<Longrightarrow> \<bar>a\<bar> * \<bar>b\<bar> < c * d"
1.317  proof -
1.318 -  assume ac: "abs a < c"
1.319 -  hence cpos: "0<c" by (blast intro: order_le_less_trans abs_ge_zero)
1.320 -  assume "abs b < d"
1.321 +  assume ac: "\<bar>a\<bar> < c"
1.322 +  hence cpos: "0<c" by (blast intro: le_less_trans abs_ge_zero)
1.323 +  assume "\<bar>b\<bar> < d"
1.324    thus ?thesis by (simp add: ac cpos mult_strict_mono)
1.325  qed
1.326
1.327 -lemmas eq_minus_self_iff[no_atp] = equal_neg_zero
1.328 -
1.329 -lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::linordered_idom))"
1.330 -  unfolding order_less_le less_eq_neg_nonpos equal_neg_zero ..
1.331 +lemma less_minus_self_iff:
1.332 +  "a < - a \<longleftrightarrow> a < 0"
1.333 +  by (simp only: less_le less_eq_neg_nonpos equal_neg_zero)
1.334
1.335 -lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::linordered_idom))"
1.336 -apply (simp add: order_less_le abs_le_iff)
1.337 -apply (auto simp add: abs_if)
1.338 -done
1.339 +lemma abs_less_iff:
1.340 +  "\<bar>a\<bar> < b \<longleftrightarrow> a < b \<and> - a < b"
1.342
1.343 -lemma abs_mult_pos: "(0::'a::linordered_idom) <= x ==>
1.344 -    (abs y) * x = abs (y * x)"
1.345 -  apply (subst abs_mult)
1.346 -  apply simp
1.347 -done
1.348 +lemma abs_mult_pos:
1.349 +  "0 \<le> x \<Longrightarrow> \<bar>y\<bar> * x = \<bar>y * x\<bar>"
1.350 +  by (simp add: abs_mult)
1.351 +
1.352 +end
1.353
1.354  code_modulename SML
1.355    Rings Arith
```