src/HOL/Rings.thy
changeset 60562 24af00b010cf
parent 60529 24c2ef12318b
child 60570 7ed2cde6806d
     1.1 --- a/src/HOL/Rings.thy	Mon Jun 22 23:19:48 2015 +0200
     1.2 +++ b/src/HOL/Rings.thy	Tue Jun 23 16:55:28 2015 +0100
     1.3 @@ -95,7 +95,7 @@
     1.4  
     1.5  definition of_bool :: "bool \<Rightarrow> 'a"
     1.6  where
     1.7 -  "of_bool p = (if p then 1 else 0)" 
     1.8 +  "of_bool p = (if p then 1 else 0)"
     1.9  
    1.10  lemma of_bool_eq [simp, code]:
    1.11    "of_bool False = 0"
    1.12 @@ -113,8 +113,8 @@
    1.13  lemma split_of_bool_asm:
    1.14    "P (of_bool p) \<longleftrightarrow> \<not> (p \<and> \<not> P 1 \<or> \<not> p \<and> \<not> P 0)"
    1.15    by (cases p) simp_all
    1.16 -  
    1.17 -end  
    1.18 +
    1.19 +end
    1.20  
    1.21  class semiring_1 = zero_neq_one + semiring_0 + monoid_mult
    1.22  
    1.23 @@ -130,7 +130,7 @@
    1.24    unfolding dvd_def ..
    1.25  
    1.26  lemma dvdE [elim?]: "b dvd a \<Longrightarrow> (\<And>k. a = b * k \<Longrightarrow> P) \<Longrightarrow> P"
    1.27 -  unfolding dvd_def by blast 
    1.28 +  unfolding dvd_def by blast
    1.29  
    1.30  end
    1.31  
    1.32 @@ -165,7 +165,7 @@
    1.33  
    1.34  lemma dvd_mult2 [simp]:
    1.35    "a dvd b \<Longrightarrow> a dvd (b * c)"
    1.36 -  using dvd_mult [of a b c] by (simp add: ac_simps) 
    1.37 +  using dvd_mult [of a b c] by (simp add: ac_simps)
    1.38  
    1.39  lemma dvd_triv_right [simp]:
    1.40    "a dvd b * a"
    1.41 @@ -193,7 +193,7 @@
    1.42  lemma dvd_mult_right:
    1.43    "a * b dvd c \<Longrightarrow> b dvd c"
    1.44    using dvd_mult_left [of b a c] by (simp add: ac_simps)
    1.45 -  
    1.46 +
    1.47  end
    1.48  
    1.49  class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult
    1.50 @@ -237,20 +237,15 @@
    1.51  
    1.52  end
    1.53  
    1.54 -class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add
    1.55 -  + zero_neq_one + comm_monoid_mult
    1.56 +class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add +
    1.57 +                               zero_neq_one + comm_monoid_mult +
    1.58 +  assumes right_diff_distrib' [algebra_simps]: "a * (b - c) = a * b - a * c"
    1.59  begin
    1.60  
    1.61  subclass semiring_1_cancel ..
    1.62  subclass comm_semiring_0_cancel ..
    1.63  subclass comm_semiring_1 ..
    1.64  
    1.65 -end
    1.66 -
    1.67 -class comm_semiring_1_diff_distrib = comm_semiring_1_cancel +
    1.68 -  assumes right_diff_distrib' [algebra_simps]: "a * (b - c) = a * b - a * c"
    1.69 -begin
    1.70 -
    1.71  lemma left_diff_distrib' [algebra_simps]:
    1.72    "(b - c) * a = b * a - c * a"
    1.73    by (simp add: algebra_simps)
    1.74 @@ -266,7 +261,7 @@
    1.75      then obtain d where "a * c + b = a * d" ..
    1.76      then have "a * c + b - a * c = a * d - a * c" by simp
    1.77      then have "b = a * d - a * c" by simp
    1.78 -    then have "b = a * (d - c)" by (simp add: algebra_simps) 
    1.79 +    then have "b = a * (d - c)" by (simp add: algebra_simps)
    1.80      then show ?Q ..
    1.81    qed
    1.82    then show "a dvd c * a + b \<longleftrightarrow> a dvd b" by (simp add: ac_simps)
    1.83 @@ -314,10 +309,10 @@
    1.84  text {* Distribution rules *}
    1.85  
    1.86  lemma minus_mult_left: "- (a * b) = - a * b"
    1.87 -by (rule minus_unique) (simp add: distrib_right [symmetric]) 
    1.88 +by (rule minus_unique) (simp add: distrib_right [symmetric])
    1.89  
    1.90  lemma minus_mult_right: "- (a * b) = a * - b"
    1.91 -by (rule minus_unique) (simp add: distrib_left [symmetric]) 
    1.92 +by (rule minus_unique) (simp add: distrib_left [symmetric])
    1.93  
    1.94  text{*Extract signs from products*}
    1.95  lemmas mult_minus_left [simp] = minus_mult_left [symmetric]
    1.96 @@ -380,9 +375,7 @@
    1.97  begin
    1.98  
    1.99  subclass ring_1 ..
   1.100 -subclass comm_semiring_1_cancel ..
   1.101 -
   1.102 -subclass comm_semiring_1_diff_distrib
   1.103 +subclass comm_semiring_1_cancel
   1.104    by unfold_locales (simp add: algebra_simps)
   1.105  
   1.106  lemma dvd_minus_iff [simp]: "x dvd - y \<longleftrightarrow> x dvd y"
   1.107 @@ -447,11 +440,11 @@
   1.108  
   1.109  lemma mult_left_cancel:
   1.110    "c \<noteq> 0 \<Longrightarrow> c * a = c * b \<longleftrightarrow> a = b"
   1.111 -  by simp 
   1.112 +  by simp
   1.113  
   1.114  lemma mult_right_cancel:
   1.115    "c \<noteq> 0 \<Longrightarrow> a * c = b * c \<longleftrightarrow> a = b"
   1.116 -  by simp 
   1.117 +  by simp
   1.118  
   1.119  end
   1.120  
   1.121 @@ -496,7 +489,7 @@
   1.122  lemma mult_cancel_right2 [simp]:
   1.123    "a * c = c \<longleftrightarrow> c = 0 \<or> a = 1"
   1.124  by (insert mult_cancel_right [of a c 1], simp)
   1.125 - 
   1.126 +
   1.127  lemma mult_cancel_left1 [simp]:
   1.128    "c = c * b \<longleftrightarrow> c = 0 \<or> b = 1"
   1.129  by (insert mult_cancel_left [of c 1 b], force)
   1.130 @@ -507,7 +500,7 @@
   1.131  
   1.132  end
   1.133  
   1.134 -class semidom = comm_semiring_1_diff_distrib + semiring_no_zero_divisors
   1.135 +class semidom = comm_semiring_1_cancel + semiring_no_zero_divisors
   1.136  
   1.137  class idom = comm_ring_1 + semiring_no_zero_divisors
   1.138  begin
   1.139 @@ -553,10 +546,10 @@
   1.140  text {*
   1.141    The theory of partially ordered rings is taken from the books:
   1.142    \begin{itemize}
   1.143 -  \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 
   1.144 +  \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979
   1.145    \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
   1.146    \end{itemize}
   1.147 -  Most of the used notions can also be looked up in 
   1.148 +  Most of the used notions can also be looked up in
   1.149    \begin{itemize}
   1.150    \item @{url "http://www.mathworld.com"} by Eric Weisstein et. al.
   1.151    \item \emph{Algebra I} by van der Waerden, Springer.
   1.152 @@ -640,7 +633,7 @@
   1.153  lemma dvd_mult_div_cancel [simp]:
   1.154    "a dvd b \<Longrightarrow> a * (b div a) = b"
   1.155    using dvd_div_mult_self [of a b] by (simp add: ac_simps)
   1.156 -  
   1.157 +
   1.158  lemma div_mult_swap:
   1.159    assumes "c dvd b"
   1.160    shows "a * (b div c) = (a * b) div c"
   1.161 @@ -658,7 +651,7 @@
   1.162    shows "b div c * a = (b * a) div c"
   1.163    using assms div_mult_swap [of c b a] by (simp add: ac_simps)
   1.164  
   1.165 -  
   1.166 +
   1.167  text \<open>Units: invertible elements in a ring\<close>
   1.168  
   1.169  abbreviation is_unit :: "'a \<Rightarrow> bool"
   1.170 @@ -669,7 +662,7 @@
   1.171    "\<not> is_unit 0"
   1.172    by simp
   1.173  
   1.174 -lemma unit_imp_dvd [dest]: 
   1.175 +lemma unit_imp_dvd [dest]:
   1.176    "is_unit b \<Longrightarrow> b dvd a"
   1.177    by (rule dvd_trans [of _ 1]) simp_all
   1.178  
   1.179 @@ -716,8 +709,8 @@
   1.180  
   1.181  lemma unit_prod [intro]:
   1.182    "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a * b)"
   1.183 -  by (subst mult_1_left [of 1, symmetric]) (rule mult_dvd_mono) 
   1.184 -  
   1.185 +  by (subst mult_1_left [of 1, symmetric]) (rule mult_dvd_mono)
   1.186 +
   1.187  lemma unit_div [intro]:
   1.188    "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a div b)"
   1.189    by (erule is_unitE [of b a]) (simp add: ac_simps unit_prod)
   1.190 @@ -794,7 +787,7 @@
   1.191  lemma unit_mult_left_cancel:
   1.192    assumes "is_unit a"
   1.193    shows "a * b = a * c \<longleftrightarrow> b = c" (is "?P \<longleftrightarrow> ?Q")
   1.194 -  using assms mult_cancel_left [of a b c] by auto 
   1.195 +  using assms mult_cancel_left [of a b c] by auto
   1.196  
   1.197  lemma unit_mult_right_cancel:
   1.198    "is_unit a \<Longrightarrow> b * a = c * a \<longleftrightarrow> b = c"
   1.199 @@ -809,12 +802,12 @@
   1.200      by (rule unit_mult_right_cancel)
   1.201    with assms show ?thesis by simp
   1.202  qed
   1.203 -  
   1.204 +
   1.205  
   1.206  text \<open>Associated elements in a ring --- an equivalence relation induced
   1.207    by the quasi-order divisibility.\<close>
   1.208  
   1.209 -definition associated :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
   1.210 +definition associated :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   1.211  where
   1.212    "associated a b \<longleftrightarrow> a dvd b \<and> b dvd a"
   1.213  
   1.214 @@ -877,10 +870,10 @@
   1.215    then have "is_unit c" by auto
   1.216    with `a = c * b` that show thesis by blast
   1.217  qed
   1.218 -  
   1.219 -lemmas unit_simps = mult_unit_dvd_iff div_unit_dvd_iff dvd_mult_unit_iff 
   1.220 +
   1.221 +lemmas unit_simps = mult_unit_dvd_iff div_unit_dvd_iff dvd_mult_unit_iff
   1.222    dvd_div_unit_iff unit_div_mult_swap unit_div_commute
   1.223 -  unit_mult_left_cancel unit_mult_right_cancel unit_div_cancel 
   1.224 +  unit_mult_left_cancel unit_mult_right_cancel unit_div_cancel
   1.225    unit_eq_div1 unit_eq_div2
   1.226  
   1.227  end
   1.228 @@ -919,10 +912,10 @@
   1.229  using mult_right_mono [of a 0 b] by simp
   1.230  
   1.231  text {* Legacy - use @{text mult_nonpos_nonneg} *}
   1.232 -lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0" 
   1.233 +lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0"
   1.234  by (drule mult_right_mono [of b 0], auto)
   1.235  
   1.236 -lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> 0" 
   1.237 +lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> 0"
   1.238  by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)
   1.239  
   1.240  end
   1.241 @@ -937,7 +930,7 @@
   1.242  lemma mult_left_less_imp_less:
   1.243    "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
   1.244  by (force simp add: mult_left_mono not_le [symmetric])
   1.245 - 
   1.246 +
   1.247  lemma mult_right_less_imp_less:
   1.248    "a * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
   1.249  by (force simp add: mult_right_mono not_le [symmetric])
   1.250 @@ -980,7 +973,7 @@
   1.251  lemma mult_left_le_imp_le:
   1.252    "c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
   1.253  by (force simp add: mult_strict_left_mono _not_less [symmetric])
   1.254 - 
   1.255 +
   1.256  lemma mult_right_le_imp_le:
   1.257    "a * c \<le> b * c \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
   1.258  by (force simp add: mult_strict_right_mono not_less [symmetric])
   1.259 @@ -995,7 +988,7 @@
   1.260  using mult_strict_right_mono [of a 0 b] by simp
   1.261  
   1.262  text {* Legacy - use @{text mult_neg_pos} *}
   1.263 -lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0" 
   1.264 +lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0"
   1.265  by (drule mult_strict_right_mono [of b 0], auto)
   1.266  
   1.267  lemma zero_less_mult_pos:
   1.268 @@ -1072,7 +1065,7 @@
   1.269  
   1.270  end
   1.271  
   1.272 -class ordered_comm_semiring = comm_semiring_0 + ordered_ab_semigroup_add + 
   1.273 +class ordered_comm_semiring = comm_semiring_0 + ordered_ab_semigroup_add +
   1.274    assumes comm_mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
   1.275  begin
   1.276  
   1.277 @@ -1118,7 +1111,7 @@
   1.278  
   1.279  end
   1.280  
   1.281 -class ordered_ring = ring + ordered_cancel_semiring 
   1.282 +class ordered_ring = ring + ordered_cancel_semiring
   1.283  begin
   1.284  
   1.285  subclass ordered_ab_group_add ..
   1.286 @@ -1239,7 +1232,7 @@
   1.287  
   1.288  lemma mult_le_0_iff:
   1.289    "a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"
   1.290 -  apply (insert zero_le_mult_iff [of "-a" b]) 
   1.291 +  apply (insert zero_le_mult_iff [of "-a" b])
   1.292    apply force
   1.293    done
   1.294  
   1.295 @@ -1252,26 +1245,26 @@
   1.296  lemma mult_less_cancel_right_disj:
   1.297    "a * c < b * c \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
   1.298    apply (cases "c = 0")
   1.299 -  apply (auto simp add: neq_iff mult_strict_right_mono 
   1.300 +  apply (auto simp add: neq_iff mult_strict_right_mono
   1.301                        mult_strict_right_mono_neg)
   1.302 -  apply (auto simp add: not_less 
   1.303 +  apply (auto simp add: not_less
   1.304                        not_le [symmetric, of "a*c"]
   1.305                        not_le [symmetric, of a])
   1.306    apply (erule_tac [!] notE)
   1.307 -  apply (auto simp add: less_imp_le mult_right_mono 
   1.308 +  apply (auto simp add: less_imp_le mult_right_mono
   1.309                        mult_right_mono_neg)
   1.310    done
   1.311  
   1.312  lemma mult_less_cancel_left_disj:
   1.313    "c * a < c * b \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
   1.314    apply (cases "c = 0")
   1.315 -  apply (auto simp add: neq_iff mult_strict_left_mono 
   1.316 +  apply (auto simp add: neq_iff mult_strict_left_mono
   1.317                        mult_strict_left_mono_neg)
   1.318 -  apply (auto simp add: not_less 
   1.319 +  apply (auto simp add: not_less
   1.320                        not_le [symmetric, of "c*a"]
   1.321                        not_le [symmetric, of a])
   1.322    apply (erule_tac [!] notE)
   1.323 -  apply (auto simp add: less_imp_le mult_left_mono 
   1.324 +  apply (auto simp add: less_imp_le mult_left_mono
   1.325                        mult_left_mono_neg)
   1.326    done
   1.327  
   1.328 @@ -1328,26 +1321,35 @@
   1.329  
   1.330  class linordered_semidom = semidom + linordered_comm_semiring_strict +
   1.331    assumes zero_less_one [simp]: "0 < 1"
   1.332 +  assumes le_add_diff_inverse2 [simp]: "b \<le> a \<Longrightarrow> a - b + b = a"
   1.333  begin
   1.334  
   1.335 +text {* Addition is the inverse of subtraction. *}
   1.336 +
   1.337 +lemma le_add_diff_inverse [simp]: "b \<le> a \<Longrightarrow> b + (a - b) = a"
   1.338 +  by (frule le_add_diff_inverse2) (simp add: add.commute)
   1.339 +
   1.340 +lemma add_diff_inverse: "~ a<b \<Longrightarrow> b + (a - b) = a"
   1.341 +  by simp
   1.342 +  
   1.343  lemma pos_add_strict:
   1.344    shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
   1.345    using add_strict_mono [of 0 a b c] by simp
   1.346  
   1.347  lemma zero_le_one [simp]: "0 \<le> 1"
   1.348 -by (rule zero_less_one [THEN less_imp_le]) 
   1.349 +by (rule zero_less_one [THEN less_imp_le])
   1.350  
   1.351  lemma not_one_le_zero [simp]: "\<not> 1 \<le> 0"
   1.352 -by (simp add: not_le) 
   1.353 +by (simp add: not_le)
   1.354  
   1.355  lemma not_one_less_zero [simp]: "\<not> 1 < 0"
   1.356 -by (simp add: not_less) 
   1.357 +by (simp add: not_less)
   1.358  
   1.359  lemma less_1_mult:
   1.360    assumes "1 < m" and "1 < n"
   1.361    shows "1 < m * n"
   1.362    using assms mult_strict_mono [of 1 m 1 n]
   1.363 -    by (simp add:  less_trans [OF zero_less_one]) 
   1.364 +    by (simp add:  less_trans [OF zero_less_one])
   1.365  
   1.366  lemma mult_left_le: "c \<le> 1 \<Longrightarrow> 0 \<le> a \<Longrightarrow> a * c \<le> a"
   1.367    using mult_left_mono[of c 1 a] by simp
   1.368 @@ -1371,7 +1373,9 @@
   1.369  proof
   1.370    have "0 \<le> 1 * 1" by (rule zero_le_square)
   1.371    thus "0 < 1" by (simp add: le_less)
   1.372 -qed 
   1.373 +  show "\<And>b a. b \<le> a \<Longrightarrow> a - b + b = a"
   1.374 +    by simp
   1.375 +qed
   1.376  
   1.377  lemma linorder_neqE_linordered_idom:
   1.378    assumes "x \<noteq> y" obtains "x < y" | "y < x"
   1.379 @@ -1461,7 +1465,7 @@
   1.380  by(subst abs_dvd_iff[symmetric]) simp
   1.381  
   1.382  text {* The following lemmas can be proven in more general structures, but
   1.383 -are dangerous as simp rules in absence of @{thm neg_equal_zero}, 
   1.384 +are dangerous as simp rules in absence of @{thm neg_equal_zero},
   1.385  @{thm neg_less_pos}, @{thm neg_less_eq_nonneg}. *}
   1.386  
   1.387  lemma equation_minus_iff_1 [simp, no_atp]:
   1.388 @@ -1559,12 +1563,12 @@
   1.389  qed (auto simp add: abs_if not_less mult_less_0_iff)
   1.390  
   1.391  lemma abs_mult:
   1.392 -  "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>" 
   1.393 +  "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
   1.394    by (rule abs_eq_mult) auto
   1.395  
   1.396  lemma abs_mult_self:
   1.397    "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
   1.398 -  by (simp add: abs_if) 
   1.399 +  by (simp add: abs_if)
   1.400  
   1.401  lemma abs_mult_less:
   1.402    "\<bar>a\<bar> < c \<Longrightarrow> \<bar>b\<bar> < d \<Longrightarrow> \<bar>a\<bar> * \<bar>b\<bar> < c * d"
   1.403 @@ -1572,11 +1576,11 @@
   1.404    assume ac: "\<bar>a\<bar> < c"
   1.405    hence cpos: "0<c" by (blast intro: le_less_trans abs_ge_zero)
   1.406    assume "\<bar>b\<bar> < d"
   1.407 -  thus ?thesis by (simp add: ac cpos mult_strict_mono) 
   1.408 +  thus ?thesis by (simp add: ac cpos mult_strict_mono)
   1.409  qed
   1.410  
   1.411  lemma abs_less_iff:
   1.412 -  "\<bar>a\<bar> < b \<longleftrightarrow> a < b \<and> - a < b" 
   1.413 +  "\<bar>a\<bar> < b \<longleftrightarrow> a < b \<and> - a < b"
   1.414    by (simp add: less_le abs_le_iff) (auto simp add: abs_if)
   1.415  
   1.416  lemma abs_mult_pos: