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.5  by (simp add: algebra_simps)
     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.21 +by (simp add: divide_inverse)
    1.22 +
    1.23 +lemma divide_self [simp]: "a \<noteq> 0 \<Longrightarrow> a / a = 1"
    1.24 +by (simp add: divide_inverse)
    1.25 +
    1.26 +lemma divide_zero_left [simp]: "0 / a = 0"
    1.27 +by (simp add: divide_inverse)
    1.28 +
    1.29 +lemma inverse_eq_divide: "inverse a = 1 / a"
    1.30 +by (simp add: divide_inverse)
    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.54 +  by (simp add: diff_minus add_divide_distrib)
    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.206  lemma pos_add_strict:
   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.228    by (simp add: abs_if)
   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.232    by (simp add: abs_if)
   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.310    by (simp add: abs_if) 
   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.341 +  by (simp add: less_le abs_le_iff) (auto simp add: abs_if)
   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