Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
authorpaulson <lp15@cam.ac.uk>
Tue Jun 23 16:55:28 2015 +0100 (2015-06-23)
changeset 6056224af00b010cf
parent 60560 ce7030d9191d
child 60563 b28677f33eaa
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
src/HOL/Code_Numeral.thy
src/HOL/Divides.thy
src/HOL/Library/Function_Algebras.thy
src/HOL/Library/Polynomial.thy
src/HOL/NSA/StarDef.thy
src/HOL/Nat.thy
src/HOL/Parity.thy
src/HOL/Rings.thy
     1.1 --- a/src/HOL/Code_Numeral.thy	Mon Jun 22 23:19:48 2015 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Tue Jun 23 16:55:28 2015 +0100
     1.3 @@ -217,7 +217,7 @@
     1.4  
     1.5  instance integer :: semiring_numeral_div
     1.6    by intro_classes (transfer,
     1.7 -    fact semiring_numeral_div_class.le_add_diff_inverse2
     1.8 +    fact le_add_diff_inverse2
     1.9      semiring_numeral_div_class.div_less
    1.10      semiring_numeral_div_class.mod_less
    1.11      semiring_numeral_div_class.div_positive
     2.1 --- a/src/HOL/Divides.thy	Mon Jun 22 23:19:48 2015 +0200
     2.2 +++ b/src/HOL/Divides.thy	Tue Jun 23 16:55:28 2015 +0100
     2.3 @@ -92,7 +92,7 @@
     2.4    then show ?thesis by simp
     2.5  qed
     2.6  
     2.7 -lemma mod_mult_self2 [simp]: 
     2.8 +lemma mod_mult_self2 [simp]:
     2.9    "(a + b * c) mod b = a mod b"
    2.10    by (simp add: mult.commute [of b])
    2.11  
    2.12 @@ -365,9 +365,9 @@
    2.13    have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" .
    2.14    with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b)
    2.15      = c * a + c * (a mod b)" by (simp add: algebra_simps)
    2.16 -  with mod_div_equality show ?thesis by simp 
    2.17 +  with mod_div_equality show ?thesis by simp
    2.18  qed
    2.19 -  
    2.20 +
    2.21  lemma mod_mult_mult2:
    2.22    "(a * c) mod (b * c) = (a mod b) * c"
    2.23    using mod_mult_mult1 [of c a b] by (simp add: mult.commute)
    2.24 @@ -406,7 +406,7 @@
    2.25  done
    2.26  
    2.27  lemma dvd_div_eq_mult:
    2.28 -  assumes "a \<noteq> 0" and "a dvd b"  
    2.29 +  assumes "a \<noteq> 0" and "a dvd b"
    2.30    shows "b div a = c \<longleftrightarrow> b = c * a"
    2.31  proof
    2.32    assume "b = c * a"
    2.33 @@ -417,7 +417,7 @@
    2.34    moreover from `a dvd b` have "b div a * a = b" by simp
    2.35    ultimately show "b = c * a" by simp
    2.36  qed
    2.37 -   
    2.38 +
    2.39  lemma dvd_div_div_eq_mult:
    2.40    assumes "a \<noteq> 0" "c \<noteq> 0" and "a dvd b" "c dvd d"
    2.41    shows "b div a = d div c \<longleftrightarrow> b * c = a * d"
    2.42 @@ -515,11 +515,11 @@
    2.43  lemma mod_minus1_right [simp]: "a mod (-1) = 0"
    2.44    using mod_minus_right [of a 1] by simp
    2.45  
    2.46 -lemma minus_mod_self2 [simp]: 
    2.47 +lemma minus_mod_self2 [simp]:
    2.48    "(a - b) mod b = a mod b"
    2.49    by (simp add: mod_diff_right_eq)
    2.50  
    2.51 -lemma minus_mod_self1 [simp]: 
    2.52 +lemma minus_mod_self1 [simp]:
    2.53    "(b - a) mod b = - a mod b"
    2.54    using mod_add_self2 [of "- a" b] by simp
    2.55  
    2.56 @@ -528,7 +528,7 @@
    2.57  
    2.58  subsubsection {* Parity and division *}
    2.59  
    2.60 -class semiring_div_parity = semiring_div + comm_semiring_1_diff_distrib + numeral + 
    2.61 +class semiring_div_parity = semiring_div + comm_semiring_1_cancel + numeral +
    2.62    assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
    2.63    assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1"
    2.64    assumes zero_not_eq_two: "0 \<noteq> 2"
    2.65 @@ -618,8 +618,7 @@
    2.66    and less technical class hierarchy.
    2.67  *}
    2.68  
    2.69 -class semiring_numeral_div = semiring_div + comm_semiring_1_diff_distrib + linordered_semidom +
    2.70 -  assumes le_add_diff_inverse2: "b \<le> a \<Longrightarrow> a - b + b = a"
    2.71 +class semiring_numeral_div = semiring_div + comm_semiring_1_cancel + linordered_semidom +
    2.72    assumes div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
    2.73      and mod_less: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"
    2.74      and div_positive: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0"
    2.75 @@ -794,7 +793,7 @@
    2.76    then have "divmod m n =
    2.77      divmod_step n (numeral m div numeral (Num.Bit0 n),
    2.78        numeral m mod numeral (Num.Bit0 n))"
    2.79 -    by (simp only: numeral.simps distrib mult_1) 
    2.80 +    by (simp only: numeral.simps distrib mult_1)
    2.81    then have "divmod m n = divmod_step n (divmod m (Num.Bit0 n))"
    2.82      by (simp add: divmod_def)
    2.83    with False show ?thesis by simp
    2.84 @@ -834,10 +833,7 @@
    2.85  
    2.86  end
    2.87  
    2.88 -hide_fact (open) le_add_diff_inverse2
    2.89 -  -- {* restore simple accesses for more general variants of theorems *}
    2.90 -
    2.91 -  
    2.92 +
    2.93  subsection {* Division on @{typ nat} *}
    2.94  
    2.95  text {*
    2.96 @@ -927,7 +923,7 @@
    2.97  qed
    2.98  
    2.99  lemma divmod_nat_unique:
   2.100 -  assumes "divmod_nat_rel m n qr" 
   2.101 +  assumes "divmod_nat_rel m n qr"
   2.102    shows "divmod_nat m n = qr"
   2.103    using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)
   2.104  
   2.105 @@ -953,12 +949,12 @@
   2.106    by (simp add: prod_eq_iff)
   2.107  
   2.108  lemma div_nat_unique:
   2.109 -  assumes "divmod_nat_rel m n (q, r)" 
   2.110 +  assumes "divmod_nat_rel m n (q, r)"
   2.111    shows "m div n = q"
   2.112    using assms by (auto dest!: divmod_nat_unique simp add: prod_eq_iff)
   2.113  
   2.114  lemma mod_nat_unique:
   2.115 -  assumes "divmod_nat_rel m n (q, r)" 
   2.116 +  assumes "divmod_nat_rel m n (q, r)"
   2.117    shows "m mod n = r"
   2.118    using assms by (auto dest!: divmod_nat_unique simp add: prod_eq_iff)
   2.119  
   2.120 @@ -1168,7 +1164,7 @@
   2.121    assumes "divmod_nat_rel a b (q, r)"
   2.122    shows "divmod_nat_rel a (b * c) (q div c, b *(q mod c) + r)"
   2.123  proof -
   2.124 -  { assume "r < b" and "0 < c" 
   2.125 +  { assume "r < b" and "0 < c"
   2.126      then have "b * (q mod c) + r < b * c"
   2.127        apply (cut_tac m = q and n = c in mod_less_divisor)
   2.128        apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
   2.129 @@ -1180,7 +1176,7 @@
   2.130    } with assms show ?thesis
   2.131      by (auto simp add: divmod_nat_rel_def algebra_simps add_mult_distrib2 [symmetric])
   2.132  qed
   2.133 -    
   2.134 +
   2.135  lemma div_mult2_eq: "a div (b * c) = (a div b) div (c::nat)"
   2.136  by (force simp add: divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN div_nat_unique])
   2.137  
   2.138 @@ -1523,7 +1519,7 @@
   2.139  lemmas Suc_div_eq_add3_div_numeral [simp] = Suc_div_eq_add3_div [of _ "numeral v"] for v
   2.140  lemmas Suc_mod_eq_add3_mod_numeral [simp] = Suc_mod_eq_add3_mod [of _ "numeral v"] for v
   2.141  
   2.142 -lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1" 
   2.143 +lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1"
   2.144  apply (induct "m")
   2.145  apply (simp_all add: mod_Suc)
   2.146  done
   2.147 @@ -1539,30 +1535,30 @@
   2.148  lemma div_2_gt_zero [simp]: assumes A: "(1::nat) < n" shows "0 < n div 2"
   2.149  proof -
   2.150    from A have B: "0 < n - 1" and C: "n - 1 + 1 = n" by simp_all
   2.151 -  from Suc_n_div_2_gt_zero [OF B] C show ?thesis by simp 
   2.152 +  from Suc_n_div_2_gt_zero [OF B] C show ?thesis by simp
   2.153  qed
   2.154  
   2.155  lemma mod_mult_self4 [simp]: "Suc (k*n + m) mod n = Suc m mod n"
   2.156  proof -
   2.157    have "Suc (k * n + m) mod n = (k * n + Suc m) mod n" by simp
   2.158 -  also have "... = Suc m mod n" by (rule mod_mult_self3) 
   2.159 +  also have "... = Suc m mod n" by (rule mod_mult_self3)
   2.160    finally show ?thesis .
   2.161  qed
   2.162  
   2.163  lemma mod_Suc_eq_Suc_mod: "Suc m mod n = Suc (m mod n) mod n"
   2.164 -apply (subst mod_Suc [of m]) 
   2.165 -apply (subst mod_Suc [of "m mod n"], simp) 
   2.166 +apply (subst mod_Suc [of m])
   2.167 +apply (subst mod_Suc [of "m mod n"], simp)
   2.168  done
   2.169  
   2.170  lemma mod_2_not_eq_zero_eq_one_nat:
   2.171    fixes n :: nat
   2.172    shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
   2.173    by (fact not_mod_2_eq_0_eq_1)
   2.174 -  
   2.175 +
   2.176  lemma even_Suc_div_two [simp]:
   2.177    "even n \<Longrightarrow> Suc n div 2 = n div 2"
   2.178    using even_succ_div_two [of n] by simp
   2.179 -  
   2.180 +
   2.181  lemma odd_Suc_div_two [simp]:
   2.182    "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)"
   2.183    using odd_succ_div_two [of n] by simp
   2.184 @@ -1603,7 +1599,7 @@
   2.185          by simp
   2.186      next
   2.187        case False
   2.188 -      with hyp odd [of "n div 2"] show ?thesis 
   2.189 +      with hyp odd [of "n div 2"] show ?thesis
   2.190          by simp
   2.191      qed
   2.192    qed
   2.193 @@ -1650,12 +1646,12 @@
   2.194  
   2.195  definition divmod_int :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
   2.196      --{*The full division algorithm considers all possible signs for a, b
   2.197 -       including the special case @{text "a=0, b<0"} because 
   2.198 +       including the special case @{text "a=0, b<0"} because
   2.199         @{term negDivAlg} requires @{term "a<0"}.*}
   2.200    "divmod_int a b = (if 0 \<le> a then if 0 \<le> b then posDivAlg a b
   2.201                    else if a = 0 then (0, 0)
   2.202                         else apsnd uminus (negDivAlg (-a) (-b))
   2.203 -               else 
   2.204 +               else
   2.205                    if 0 < b then negDivAlg a b
   2.206                    else apsnd uminus (posDivAlg (-a) (-b)))"
   2.207  
   2.208 @@ -1698,11 +1694,11 @@
   2.209  
   2.210      fun negateSnd (q,r:int) = (q,~r);
   2.211  
   2.212 -    fun divmod (a,b) = if 0\<le>a then 
   2.213 -                          if b>0 then posDivAlg (a,b) 
   2.214 +    fun divmod (a,b) = if 0\<le>a then
   2.215 +                          if b>0 then posDivAlg (a,b)
   2.216                             else if a=0 then (0,0)
   2.217                                  else negateSnd (negDivAlg (~a,~b))
   2.218 -                       else 
   2.219 +                       else
   2.220                            if 0<b then negDivAlg (a,b)
   2.221                            else        negateSnd (posDivAlg (~a,~b));
   2.222  \end{verbatim}
   2.223 @@ -1712,7 +1708,7 @@
   2.224  subsubsection {* Uniqueness and Monotonicity of Quotients and Remainders *}
   2.225  
   2.226  lemma unique_quotient_lemma:
   2.227 -     "[| b*q' + r'  \<le> b*q + r;  0 \<le> r';  r' < b;  r < b |]  
   2.228 +     "[| b*q' + r'  \<le> b*q + r;  0 \<le> r';  r' < b;  r < b |]
   2.229        ==> q' \<le> (q::int)"
   2.230  apply (subgoal_tac "r' + b * (q'-q) \<le> r")
   2.231   prefer 2 apply (simp add: right_diff_distrib)
   2.232 @@ -1725,23 +1721,23 @@
   2.233  done
   2.234  
   2.235  lemma unique_quotient_lemma_neg:
   2.236 -     "[| b*q' + r' \<le> b*q + r;  r \<le> 0;  b < r;  b < r' |]  
   2.237 +     "[| b*q' + r' \<le> b*q + r;  r \<le> 0;  b < r;  b < r' |]
   2.238        ==> q \<le> (q'::int)"
   2.239 -by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma, 
   2.240 +by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma,
   2.241      auto)
   2.242  
   2.243  lemma unique_quotient:
   2.244 -     "[| divmod_int_rel a b (q, r); divmod_int_rel a b (q', r') |]  
   2.245 +     "[| divmod_int_rel a b (q, r); divmod_int_rel a b (q', r') |]
   2.246        ==> q = q'"
   2.247  apply (simp add: divmod_int_rel_def linorder_neq_iff split: split_if_asm)
   2.248  apply (blast intro: order_antisym
   2.249 -             dest: order_eq_refl [THEN unique_quotient_lemma] 
   2.250 +             dest: order_eq_refl [THEN unique_quotient_lemma]
   2.251               order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
   2.252  done
   2.253  
   2.254  
   2.255  lemma unique_remainder:
   2.256 -     "[| divmod_int_rel a b (q, r); divmod_int_rel a b (q', r') |]  
   2.257 +     "[| divmod_int_rel a b (q, r); divmod_int_rel a b (q', r') |]
   2.258        ==> r = r'"
   2.259  apply (subgoal_tac "q = q'")
   2.260   apply (simp add: divmod_int_rel_def)
   2.261 @@ -1754,9 +1750,9 @@
   2.262  text{*And positive divisors*}
   2.263  
   2.264  lemma adjust_eq [simp]:
   2.265 -     "adjust b (q, r) = 
   2.266 -      (let diff = r - b in  
   2.267 -        if 0 \<le> diff then (2 * q + 1, diff)   
   2.268 +     "adjust b (q, r) =
   2.269 +      (let diff = r - b in
   2.270 +        if 0 \<le> diff then (2 * q + 1, diff)
   2.271                       else (2*q, r))"
   2.272    by (simp add: Let_def adjust_def)
   2.273  
   2.274 @@ -1764,7 +1760,7 @@
   2.275  
   2.276  text{*use with a simproc to avoid repeatedly proving the premise*}
   2.277  lemma posDivAlg_eqn:
   2.278 -     "0 < b ==>  
   2.279 +     "0 < b ==>
   2.280        posDivAlg a b = (if a<b then (0,a) else adjust b (posDivAlg a (2*b)))"
   2.281  by (rule posDivAlg.simps [THEN trans], simp)
   2.282  
   2.283 @@ -1792,8 +1788,8 @@
   2.284  
   2.285  text{*use with a simproc to avoid repeatedly proving the premise*}
   2.286  lemma negDivAlg_eqn:
   2.287 -     "0 < b ==>  
   2.288 -      negDivAlg a b =       
   2.289 +     "0 < b ==>
   2.290 +      negDivAlg a b =
   2.291         (if 0\<le>a+b then (-1,a+b) else adjust b (negDivAlg a (2*b)))"
   2.292  by (rule negDivAlg.simps [THEN trans], simp)
   2.293  
   2.294 @@ -1838,7 +1834,7 @@
   2.295                      posDivAlg_correct negDivAlg_correct)
   2.296  
   2.297  lemma divmod_int_unique:
   2.298 -  assumes "divmod_int_rel a b qr" 
   2.299 +  assumes "divmod_int_rel a b qr"
   2.300    shows "divmod_int a b = qr"
   2.301    using assms divmod_int_correct [of a b]
   2.302    using unique_quotient [of a b] unique_remainder [of a b]
   2.303 @@ -1912,7 +1908,7 @@
   2.304  
   2.305    val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
   2.306  
   2.307 -  val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac 
   2.308 +  val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
   2.309      (@{thm diff_conv_add_uminus} :: @{thms add_0_left add_0_right} @ @{thms ac_simps}))
   2.310  )
   2.311  *}
   2.312 @@ -1975,14 +1971,14 @@
   2.313  
   2.314  lemma zminus1_lemma:
   2.315       "divmod_int_rel a b (q, r) ==> b \<noteq> 0
   2.316 -      ==> divmod_int_rel (-a) b (if r=0 then -q else -q - 1,  
   2.317 +      ==> divmod_int_rel (-a) b (if r=0 then -q else -q - 1,
   2.318                            if r=0 then 0 else b-r)"
   2.319  by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff right_diff_distrib)
   2.320  
   2.321  
   2.322  lemma zdiv_zminus1_eq_if:
   2.323 -     "b \<noteq> (0::int)  
   2.324 -      ==> (-a) div b =  
   2.325 +     "b \<noteq> (0::int)
   2.326 +      ==> (-a) div b =
   2.327            (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
   2.328  by (blast intro: divmod_int_rel_div_mod [THEN zminus1_lemma, THEN div_int_unique])
   2.329  
   2.330 @@ -1998,8 +1994,8 @@
   2.331    unfolding zmod_zminus1_eq_if by auto
   2.332  
   2.333  lemma zdiv_zminus2_eq_if:
   2.334 -     "b \<noteq> (0::int)  
   2.335 -      ==> a div (-b) =  
   2.336 +     "b \<noteq> (0::int)
   2.337 +      ==> a div (-b) =
   2.338            (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
   2.339  by (simp add: zdiv_zminus1_eq_if div_minus_right)
   2.340  
   2.341 @@ -2010,7 +2006,7 @@
   2.342  lemma zmod_zminus2_not_zero:
   2.343    fixes k l :: int
   2.344    shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
   2.345 -  unfolding zmod_zminus2_eq_if by auto 
   2.346 +  unfolding zmod_zminus2_eq_if by auto
   2.347  
   2.348  
   2.349  subsubsection {* Computation of Division and Remainder *}
   2.350 @@ -2185,10 +2181,10 @@
   2.351  done
   2.352  
   2.353  lemma zdiv_mono2_lemma:
   2.354 -     "[| b*q + r = b'*q' + r';  0 \<le> b'*q' + r';   
   2.355 -         r' < b';  0 \<le> r;  0 < b';  b' \<le> b |]   
   2.356 +     "[| b*q + r = b'*q' + r';  0 \<le> b'*q' + r';
   2.357 +         r' < b';  0 \<le> r;  0 < b';  b' \<le> b |]
   2.358        ==> q \<le> (q'::int)"
   2.359 -apply (frule q_pos_lemma, assumption+) 
   2.360 +apply (frule q_pos_lemma, assumption+)
   2.361  apply (subgoal_tac "b*q < b* (q' + 1) ")
   2.362   apply (simp add: mult_less_cancel_left)
   2.363  apply (subgoal_tac "b*q = r' - r + b'*q'")
   2.364 @@ -2216,10 +2212,10 @@
   2.365  done
   2.366  
   2.367  lemma zdiv_mono2_neg_lemma:
   2.368 -     "[| b*q + r = b'*q' + r';  b'*q' + r' < 0;   
   2.369 -         r < b;  0 \<le> r';  0 < b';  b' \<le> b |]   
   2.370 +     "[| b*q + r = b'*q' + r';  b'*q' + r' < 0;
   2.371 +         r < b;  0 \<le> r';  0 < b';  b' \<le> b |]
   2.372        ==> q' \<le> (q::int)"
   2.373 -apply (frule q_neg_lemma, assumption+) 
   2.374 +apply (frule q_neg_lemma, assumption+)
   2.375  apply (subgoal_tac "b*q' < b* (q + 1) ")
   2.376   apply (simp add: mult_less_cancel_left)
   2.377  apply (simp add: distrib_left)
   2.378 @@ -2242,7 +2238,7 @@
   2.379  text{*proving (a*b) div c = a * (b div c) + a * (b mod c) *}
   2.380  
   2.381  lemma zmult1_lemma:
   2.382 -     "[| divmod_int_rel b c (q, r) |]  
   2.383 +     "[| divmod_int_rel b c (q, r) |]
   2.384        ==> divmod_int_rel (a * b) c (a*q + a*r div c, a*r mod c)"
   2.385  by (auto simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left ac_simps)
   2.386  
   2.387 @@ -2254,7 +2250,7 @@
   2.388  text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}
   2.389  
   2.390  lemma zadd1_lemma:
   2.391 -     "[| divmod_int_rel a c (aq, ar);  divmod_int_rel b c (bq, br) |]  
   2.392 +     "[| divmod_int_rel a c (aq, ar);  divmod_int_rel b c (bq, br) |]
   2.393        ==> divmod_int_rel (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)"
   2.394  by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left)
   2.395  
   2.396 @@ -2346,10 +2342,10 @@
   2.397  apply simp
   2.398  done
   2.399  
   2.400 -lemma zmult2_lemma: "[| divmod_int_rel a b (q, r); 0 < c |]  
   2.401 +lemma zmult2_lemma: "[| divmod_int_rel a b (q, r); 0 < c |]
   2.402        ==> divmod_int_rel a (b * c) (q div c, b*(q mod c) + r)"
   2.403  by (auto simp add: mult.assoc divmod_int_rel_def linorder_neq_iff
   2.404 -                   zero_less_mult_iff distrib_left [symmetric] 
   2.405 +                   zero_less_mult_iff distrib_left [symmetric]
   2.406                     zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: split_if_asm)
   2.407  
   2.408  lemma zdiv_zmult2_eq:
   2.409 @@ -2392,15 +2388,15 @@
   2.410  text{*The proofs of the two lemmas below are essentially identical*}
   2.411  
   2.412  lemma split_pos_lemma:
   2.413 - "0<k ==> 
   2.414 + "0<k ==>
   2.415      P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i j)"
   2.416  apply (rule iffI, clarify)
   2.417 - apply (erule_tac P="P x y" for x y in rev_mp)  
   2.418 - apply (subst mod_add_eq) 
   2.419 - apply (subst zdiv_zadd1_eq) 
   2.420 - apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial)  
   2.421 + apply (erule_tac P="P x y" for x y in rev_mp)
   2.422 + apply (subst mod_add_eq)
   2.423 + apply (subst zdiv_zadd1_eq)
   2.424 + apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial)
   2.425  txt{*converse direction*}
   2.426 -apply (drule_tac x = "n div k" in spec) 
   2.427 +apply (drule_tac x = "n div k" in spec)
   2.428  apply (drule_tac x = "n mod k" in spec, simp)
   2.429  done
   2.430  
   2.431 @@ -2408,36 +2404,36 @@
   2.432   "k<0 ==>
   2.433      P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i j)"
   2.434  apply (rule iffI, clarify)
   2.435 - apply (erule_tac P="P x y" for x y in rev_mp)  
   2.436 - apply (subst mod_add_eq) 
   2.437 - apply (subst zdiv_zadd1_eq) 
   2.438 - apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial)  
   2.439 + apply (erule_tac P="P x y" for x y in rev_mp)
   2.440 + apply (subst mod_add_eq)
   2.441 + apply (subst zdiv_zadd1_eq)
   2.442 + apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial)
   2.443  txt{*converse direction*}
   2.444 -apply (drule_tac x = "n div k" in spec) 
   2.445 +apply (drule_tac x = "n div k" in spec)
   2.446  apply (drule_tac x = "n mod k" in spec, simp)
   2.447  done
   2.448  
   2.449  lemma split_zdiv:
   2.450   "P(n div k :: int) =
   2.451 -  ((k = 0 --> P 0) & 
   2.452 -   (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i)) & 
   2.453 +  ((k = 0 --> P 0) &
   2.454 +   (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i)) &
   2.455     (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i)))"
   2.456  apply (case_tac "k=0", simp)
   2.457  apply (simp only: linorder_neq_iff)
   2.458 -apply (erule disjE) 
   2.459 - apply (simp_all add: split_pos_lemma [of concl: "%x y. P x"] 
   2.460 +apply (erule disjE)
   2.461 + apply (simp_all add: split_pos_lemma [of concl: "%x y. P x"]
   2.462                        split_neg_lemma [of concl: "%x y. P x"])
   2.463  done
   2.464  
   2.465  lemma split_zmod:
   2.466   "P(n mod k :: int) =
   2.467 -  ((k = 0 --> P n) & 
   2.468 -   (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P j)) & 
   2.469 +  ((k = 0 --> P n) &
   2.470 +   (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P j)) &
   2.471     (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P j)))"
   2.472  apply (case_tac "k=0", simp)
   2.473  apply (simp only: linorder_neq_iff)
   2.474 -apply (erule disjE) 
   2.475 - apply (simp_all add: split_pos_lemma [of concl: "%x y. P y"] 
   2.476 +apply (erule disjE)
   2.477 + apply (simp_all add: split_pos_lemma [of concl: "%x y. P y"]
   2.478                        split_neg_lemma [of concl: "%x y. P y"])
   2.479  done
   2.480  
   2.481 @@ -2470,7 +2466,7 @@
   2.482    using pos_divmod_int_rel_mult_2 [OF _ divmod_int_rel_div_mod]
   2.483    by (rule div_int_unique)
   2.484  
   2.485 -lemma neg_zdiv_mult_2: 
   2.486 +lemma neg_zdiv_mult_2:
   2.487    assumes A: "a \<le> (0::int)" shows "(1 + 2*b) div (2*a) = (b+1) div a"
   2.488    using neg_divmod_int_rel_mult_2 [OF A divmod_int_rel_div_mod]
   2.489    by (rule div_int_unique)
   2.490 @@ -2483,7 +2479,7 @@
   2.491    by (rule div_mult_mult1, simp)
   2.492  
   2.493  lemma zdiv_numeral_Bit1 [simp]:
   2.494 -  "numeral (Num.Bit1 v) div numeral (Num.Bit0 w) =  
   2.495 +  "numeral (Num.Bit1 v) div numeral (Num.Bit0 w) =
   2.496      (numeral v div (numeral w :: int))"
   2.497    unfolding numeral.simps
   2.498    unfolding mult_2 [symmetric] add.commute [of _ 1]
   2.499 @@ -2505,7 +2501,7 @@
   2.500  
   2.501  (* FIXME: add rules for negative numerals *)
   2.502  lemma zmod_numeral_Bit0 [simp]:
   2.503 -  "numeral (Num.Bit0 v) mod numeral (Num.Bit0 w) =  
   2.504 +  "numeral (Num.Bit0 v) mod numeral (Num.Bit0 w) =
   2.505      (2::int) * (numeral v mod numeral w)"
   2.506    unfolding numeral_Bit0 [of v] numeral_Bit0 [of w]
   2.507    unfolding mult_2 [symmetric] by (rule mod_mult_mult1)
   2.508 @@ -2609,7 +2605,7 @@
   2.509      simp add: zmult_div_cancel
   2.510      pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial
   2.511      zmod_zmult2_eq zdiv_zmult2_eq)
   2.512 -  
   2.513 +
   2.514  lemma zdiv_int: "int (a div b) = (int a) div (int b)"
   2.515  apply (subst split_div, auto)
   2.516  apply (subst split_zdiv, auto)
   2.517 @@ -2620,7 +2616,7 @@
   2.518  lemma zmod_int: "int (a mod b) = (int a) mod (int b)"
   2.519  apply (subst split_mod, auto)
   2.520  apply (subst split_zmod, auto)
   2.521 -apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia 
   2.522 +apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia
   2.523         in unique_remainder)
   2.524  apply (auto simp add: divmod_int_rel_def of_nat_mult)
   2.525  done
   2.526 @@ -2718,7 +2714,7 @@
   2.527  proof
   2.528    assume H: "x mod n = y mod n"
   2.529    hence "x mod n - y mod n = 0" by simp
   2.530 -  hence "(x mod n - y mod n) mod n = 0" by simp 
   2.531 +  hence "(x mod n - y mod n) mod n = 0" by simp
   2.532    hence "(x - y) mod n = 0" by (simp add: mod_diff_eq[symmetric])
   2.533    thus "n dvd x - y" by (simp add: dvd_eq_mod_eq_0)
   2.534  next
   2.535 @@ -2732,27 +2728,27 @@
   2.536  lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y  mod n" and xy:"y \<le> x"
   2.537    shows "\<exists>q. x = y + n * q"
   2.538  proof-
   2.539 -  from xy have th: "int x - int y = int (x - y)" by simp 
   2.540 -  from xyn have "int x mod int n = int y mod int n" 
   2.541 +  from xy have th: "int x - int y = int (x - y)" by simp
   2.542 +  from xyn have "int x mod int n = int y mod int n"
   2.543      by (simp add: zmod_int [symmetric])
   2.544 -  hence "int n dvd int x - int y" by (simp only: zmod_eq_dvd_iff[symmetric]) 
   2.545 +  hence "int n dvd int x - int y" by (simp only: zmod_eq_dvd_iff[symmetric])
   2.546    hence "n dvd x - y" by (simp add: th zdvd_int)
   2.547    then show ?thesis using xy unfolding dvd_def apply clarsimp apply (rule_tac x="k" in exI) by arith
   2.548  qed
   2.549  
   2.550 -lemma nat_mod_eq_iff: "(x::nat) mod n = y mod n \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)" 
   2.551 +lemma nat_mod_eq_iff: "(x::nat) mod n = y mod n \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)"
   2.552    (is "?lhs = ?rhs")
   2.553  proof
   2.554    assume H: "x mod n = y mod n"
   2.555    {assume xy: "x \<le> y"
   2.556      from H have th: "y mod n = x mod n" by simp
   2.557 -    from nat_mod_eq_lemma[OF th xy] have ?rhs 
   2.558 +    from nat_mod_eq_lemma[OF th xy] have ?rhs
   2.559        apply clarify  apply (rule_tac x="q" in exI) by (rule exI[where x="0"], simp)}
   2.560    moreover
   2.561    {assume xy: "y \<le> x"
   2.562 -    from nat_mod_eq_lemma[OF H xy] have ?rhs 
   2.563 +    from nat_mod_eq_lemma[OF H xy] have ?rhs
   2.564        apply clarify  apply (rule_tac x="0" in exI) by (rule_tac x="q" in exI, simp)}
   2.565 -  ultimately  show ?rhs using linear[of x y] by blast  
   2.566 +  ultimately  show ?rhs using linear[of x y] by blast
   2.567  next
   2.568    assume ?rhs then obtain q1 q2 where q12: "x + n * q1 = y + n * q2" by blast
   2.569    hence "(x + n * q1) mod n = (y + n * q2) mod n" by simp
   2.570 @@ -2762,7 +2758,7 @@
   2.571  text {*
   2.572    This re-embedding of natural division on integers goes back to the
   2.573    time when numerals had been signed numerals.  It should
   2.574 -  now be replaced by the algorithm developed in @{class semiring_numeral_div}.  
   2.575 +  now be replaced by the algorithm developed in @{class semiring_numeral_div}.
   2.576  *}
   2.577  
   2.578  lemma div_nat_numeral [simp]:
     3.1 --- a/src/HOL/Library/Function_Algebras.thy	Mon Jun 22 23:19:48 2015 +0200
     3.2 +++ b/src/HOL/Library/Function_Algebras.thy	Tue Jun 23 16:55:28 2015 +0100
     3.3 @@ -154,7 +154,8 @@
     3.4  
     3.5  instance "fun" :: (type, semiring_1_cancel) semiring_1_cancel ..
     3.6  
     3.7 -instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel ..
     3.8 +instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel 
     3.9 +  by default (auto simp add: times_fun_def algebra_simps)
    3.10  
    3.11  instance "fun" :: (type, semiring_char_0) semiring_char_0
    3.12  proof
     4.1 --- a/src/HOL/Library/Polynomial.thy	Mon Jun 22 23:19:48 2015 +0200
     4.2 +++ b/src/HOL/Library/Polynomial.thy	Tue Jun 23 16:55:28 2015 +0100
     4.3 @@ -868,8 +868,6 @@
     4.4  
     4.5  end
     4.6  
     4.7 -instance poly :: (comm_semiring_1_cancel) comm_semiring_1_cancel ..
     4.8 -
     4.9  instance poly :: (comm_ring) comm_ring ..
    4.10  
    4.11  instance poly :: (comm_ring_1) comm_ring_1 ..
     5.1 --- a/src/HOL/NSA/StarDef.thy	Mon Jun 22 23:19:48 2015 +0200
     5.2 +++ b/src/HOL/NSA/StarDef.thy	Tue Jun 23 16:55:28 2015 +0100
     5.3 @@ -837,7 +837,7 @@
     5.4  
     5.5  declare dvd_def [transfer_refold]
     5.6  
     5.7 -instance star :: (comm_semiring_1_diff_distrib) comm_semiring_1_diff_distrib
     5.8 +instance star :: (comm_semiring_1_cancel) comm_semiring_1_cancel
     5.9    by (intro_classes; transfer) (fact right_diff_distrib')
    5.10  
    5.11  instance star :: (semiring_no_zero_divisors) semiring_no_zero_divisors
    5.12 @@ -847,7 +847,6 @@
    5.13    by (intro_classes; transfer) simp_all
    5.14  
    5.15  instance star :: (semiring_1_cancel) semiring_1_cancel ..
    5.16 -instance star :: (comm_semiring_1_cancel) comm_semiring_1_cancel ..
    5.17  instance star :: (ring) ring ..
    5.18  instance star :: (comm_ring) comm_ring ..
    5.19  instance star :: (ring_1) ring_1 ..
    5.20 @@ -902,7 +901,10 @@
    5.21  instance star :: (ordered_comm_ring) ordered_comm_ring ..
    5.22  
    5.23  instance star :: (linordered_semidom) linordered_semidom
    5.24 -  by (intro_classes; transfer) (fact zero_less_one)
    5.25 +  apply intro_classes
    5.26 +  apply(transfer, fact zero_less_one)
    5.27 +  apply(transfer, fact le_add_diff_inverse2)
    5.28 +  done
    5.29  
    5.30  instance star :: (linordered_idom) linordered_idom ..
    5.31  instance star :: (linordered_field) linordered_field ..
    5.32 @@ -1005,7 +1007,6 @@
    5.33  
    5.34  instance star :: (semiring_numeral_div) semiring_numeral_div
    5.35  apply intro_classes
    5.36 -apply(transfer, fact semiring_numeral_div_class.le_add_diff_inverse2)
    5.37  apply(transfer, fact semiring_numeral_div_class.div_less)
    5.38  apply(transfer, fact semiring_numeral_div_class.mod_less)
    5.39  apply(transfer, fact semiring_numeral_div_class.div_positive)
     6.1 --- a/src/HOL/Nat.thy	Mon Jun 22 23:19:48 2015 +0200
     6.2 +++ b/src/HOL/Nat.thy	Tue Jun 23 16:55:28 2015 +0100
     6.3 @@ -282,10 +282,25 @@
     6.4    show "n * m = m * n" by (induct n) simp_all
     6.5    show "(n * m) * q = n * (m * q)" by (induct n) (simp_all add: add_mult_distrib)
     6.6    show "(n + m) * q = n * q + m * q" by (rule add_mult_distrib)
     6.7 +next
     6.8 +  fix k m n :: nat
     6.9 +  show "k * ((m::nat) - n) = (k * m) - (k * n)"
    6.10 +    by (induct m n rule: diff_induct) simp_all
    6.11  qed
    6.12  
    6.13  end
    6.14  
    6.15 +text {* Difference distributes over multiplication *}
    6.16 +
    6.17 +lemma diff_mult_distrib:
    6.18 +  "((m::nat) - n) * k = (m * k) - (n * k)"
    6.19 +  by (fact left_diff_distrib')
    6.20 +
    6.21 +lemma diff_mult_distrib2:
    6.22 +  "k * ((m::nat) - n) = (k * m) - (k * n)"
    6.23 +  by (fact right_diff_distrib')
    6.24 +
    6.25 +
    6.26  subsubsection {* Addition *}
    6.27  
    6.28  lemma nat_add_left_cancel:
    6.29 @@ -364,24 +379,6 @@
    6.30  lemma diff_Suc_1 [simp]: "Suc n - 1 = n"
    6.31    unfolding One_nat_def by simp
    6.32  
    6.33 -text {* Difference distributes over multiplication *}
    6.34 -
    6.35 -instance nat :: comm_semiring_1_diff_distrib
    6.36 -proof
    6.37 -  fix k m n :: nat
    6.38 -  show "k * ((m::nat) - n) = (k * m) - (k * n)"
    6.39 -    by (induct m n rule: diff_induct) simp_all
    6.40 -qed
    6.41 -
    6.42 -lemma diff_mult_distrib:
    6.43 -  "((m::nat) - n) * k = (m * k) - (n * k)"
    6.44 -  by (fact left_diff_distrib')
    6.45 -  
    6.46 -lemma diff_mult_distrib2:
    6.47 -  "k * ((m::nat) - n) = (k * m) - (k * n)"
    6.48 -  by (fact right_diff_distrib')
    6.49 -
    6.50 -
    6.51  subsubsection {* Multiplication *}
    6.52  
    6.53  lemma add_mult_distrib2: "k * (m + n) = (k * m) + ((k * n)::nat)"
    6.54 @@ -488,7 +485,7 @@
    6.55  instance
    6.56  proof
    6.57    fix n m :: nat
    6.58 -  show "n < m \<longleftrightarrow> n \<le> m \<and> \<not> m \<le> n" 
    6.59 +  show "n < m \<longleftrightarrow> n \<le> m \<and> \<not> m \<le> n"
    6.60    proof (induct n arbitrary: m)
    6.61      case 0 then show ?case by (cases m) (simp_all add: less_eq_Suc_le)
    6.62    next
    6.63 @@ -550,7 +547,7 @@
    6.64    by (rule order_less_irrefl)
    6.65  
    6.66  lemma less_not_refl2: "n < m ==> m \<noteq> (n::nat)"
    6.67 -  by (rule not_sym) (rule less_imp_neq) 
    6.68 +  by (rule not_sym) (rule less_imp_neq)
    6.69  
    6.70  lemma less_not_refl3: "(s::nat) < t ==> s \<noteq> t"
    6.71    by (rule less_imp_neq)
    6.72 @@ -594,7 +591,7 @@
    6.73  subsubsection {* Inductive (?) properties *}
    6.74  
    6.75  lemma Suc_lessI: "m < n ==> Suc m \<noteq> n ==> Suc m < n"
    6.76 -  unfolding less_eq_Suc_le [of m] le_less by simp 
    6.77 +  unfolding less_eq_Suc_le [of m] le_less by simp
    6.78  
    6.79  lemma lessE:
    6.80    assumes major: "i < k"
    6.81 @@ -783,6 +780,12 @@
    6.82  apply (simp_all add: add_less_mono)
    6.83  done
    6.84  
    6.85 +text {* Addition is the inverse of subtraction:
    6.86 +  if @{term "n \<le> m"} then @{term "n + (m - n) = m"}. *}
    6.87 +lemma add_diff_inverse_nat: "~  m < n ==> n + (m - n) = (m::nat)"
    6.88 +by (induct m n rule: diff_induct) simp_all
    6.89 +
    6.90 +
    6.91  text{*The naturals form an ordered @{text semidom}*}
    6.92  instance nat :: linordered_semidom
    6.93  proof
    6.94 @@ -790,7 +793,9 @@
    6.95    show "\<And>m n q :: nat. m \<le> n \<Longrightarrow> q + m \<le> q + n" by simp
    6.96    show "\<And>m n q :: nat. m < n \<Longrightarrow> 0 < q \<Longrightarrow> q * m < q * n" by (simp add: mult_less_mono2)
    6.97    show "\<And>m n :: nat. m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> m * n \<noteq> 0" by simp
    6.98 -qed
    6.99 +  show "\<And>m n :: nat. n \<le> m ==> (m - n) + n = (m::nat)"
   6.100 +    by (simp add: add_diff_inverse_nat add.commute linorder_not_less)
   6.101 +qed 
   6.102  
   6.103  
   6.104  subsubsection {* @{term min} and @{term max} *}
   6.105 @@ -989,7 +994,7 @@
   6.106    "\<lbrakk> !!n::nat. \<not> P n \<Longrightarrow>  \<exists>m<n. \<not>  P m \<rbrakk> \<Longrightarrow>  P n"
   6.107  by (induct n rule: less_induct) auto
   6.108  
   6.109 -lemma infinite_descent0[case_names 0 smaller]: 
   6.110 +lemma infinite_descent0[case_names 0 smaller]:
   6.111    "\<lbrakk> P 0; !!n. n>0 \<Longrightarrow> \<not> P n \<Longrightarrow> (\<exists>m::nat. m < n \<and> \<not>P m) \<rbrakk> \<Longrightarrow> P n"
   6.112  by (rule infinite_descent) (case_tac "n>0", auto)
   6.113  
   6.114 @@ -1112,17 +1117,6 @@
   6.115  
   6.116  subsubsection {* More results about difference *}
   6.117  
   6.118 -text {* Addition is the inverse of subtraction:
   6.119 -  if @{term "n \<le> m"} then @{term "n + (m - n) = m"}. *}
   6.120 -lemma add_diff_inverse: "~  m < n ==> n + (m - n) = (m::nat)"
   6.121 -by (induct m n rule: diff_induct) simp_all
   6.122 -
   6.123 -lemma le_add_diff_inverse [simp]: "n \<le> m ==> n + (m - n) = (m::nat)"
   6.124 -by (simp add: add_diff_inverse linorder_not_less)
   6.125 -
   6.126 -lemma le_add_diff_inverse2 [simp]: "n \<le> m ==> (m - n) + n = (m::nat)"
   6.127 -by (simp add: add.commute)
   6.128 -
   6.129  lemma Suc_diff_le: "n \<le> m ==> Suc m - n = Suc (m - n)"
   6.130  by (induct m n rule: diff_induct) simp_all
   6.131  
   6.132 @@ -1490,8 +1484,8 @@
   6.133  
   6.134  lemma of_nat_0_neq [simp]:
   6.135    "0 \<noteq> of_nat (Suc n)"
   6.136 -  unfolding of_nat_0_eq_iff by simp  
   6.137 -  
   6.138 +  unfolding of_nat_0_eq_iff by simp
   6.139 +
   6.140  end
   6.141  
   6.142  context linordered_semidom
   6.143 @@ -1770,7 +1764,7 @@
   6.144  lemma min_diff: "min (m - (i::nat)) (n - i) = min m n - i"
   6.145  by auto
   6.146  
   6.147 -lemma inj_on_diff_nat: 
   6.148 +lemma inj_on_diff_nat:
   6.149    assumes k_le_n: "\<forall>n \<in> N. k \<le> (n::nat)"
   6.150    shows "inj_on (\<lambda>n. n - k) N"
   6.151  proof (rule inj_onI)
   6.152 @@ -1980,7 +1974,7 @@
   6.153  
   6.154  lemma nat_mult_1: "(1::nat) * n = n"
   6.155    by (fact mult_1_left)
   6.156 - 
   6.157 +
   6.158  lemma nat_mult_1_right: "n * (1::nat) = n"
   6.159    by (fact mult_1_right)
   6.160  
     7.1 --- a/src/HOL/Parity.thy	Mon Jun 22 23:19:48 2015 +0200
     7.2 +++ b/src/HOL/Parity.thy	Tue Jun 23 16:55:28 2015 +0100
     7.3 @@ -11,7 +11,7 @@
     7.4  
     7.5  subsection {* Ring structures with parity and @{text even}/@{text odd} predicates *}
     7.6  
     7.7 -class semiring_parity = comm_semiring_1_diff_distrib + numeral +
     7.8 +class semiring_parity = comm_semiring_1_cancel + numeral +
     7.9    assumes odd_one [simp]: "\<not> 2 dvd 1"
    7.10    assumes odd_even_add: "\<not> 2 dvd a \<Longrightarrow> \<not> 2 dvd b \<Longrightarrow> 2 dvd a + b"
    7.11    assumes even_multD: "2 dvd a * b \<Longrightarrow> 2 dvd a \<or> 2 dvd b"
     8.1 --- a/src/HOL/Rings.thy	Mon Jun 22 23:19:48 2015 +0200
     8.2 +++ b/src/HOL/Rings.thy	Tue Jun 23 16:55:28 2015 +0100
     8.3 @@ -95,7 +95,7 @@
     8.4  
     8.5  definition of_bool :: "bool \<Rightarrow> 'a"
     8.6  where
     8.7 -  "of_bool p = (if p then 1 else 0)" 
     8.8 +  "of_bool p = (if p then 1 else 0)"
     8.9  
    8.10  lemma of_bool_eq [simp, code]:
    8.11    "of_bool False = 0"
    8.12 @@ -113,8 +113,8 @@
    8.13  lemma split_of_bool_asm:
    8.14    "P (of_bool p) \<longleftrightarrow> \<not> (p \<and> \<not> P 1 \<or> \<not> p \<and> \<not> P 0)"
    8.15    by (cases p) simp_all
    8.16 -  
    8.17 -end  
    8.18 +
    8.19 +end
    8.20  
    8.21  class semiring_1 = zero_neq_one + semiring_0 + monoid_mult
    8.22  
    8.23 @@ -130,7 +130,7 @@
    8.24    unfolding dvd_def ..
    8.25  
    8.26  lemma dvdE [elim?]: "b dvd a \<Longrightarrow> (\<And>k. a = b * k \<Longrightarrow> P) \<Longrightarrow> P"
    8.27 -  unfolding dvd_def by blast 
    8.28 +  unfolding dvd_def by blast
    8.29  
    8.30  end
    8.31  
    8.32 @@ -165,7 +165,7 @@
    8.33  
    8.34  lemma dvd_mult2 [simp]:
    8.35    "a dvd b \<Longrightarrow> a dvd (b * c)"
    8.36 -  using dvd_mult [of a b c] by (simp add: ac_simps) 
    8.37 +  using dvd_mult [of a b c] by (simp add: ac_simps)
    8.38  
    8.39  lemma dvd_triv_right [simp]:
    8.40    "a dvd b * a"
    8.41 @@ -193,7 +193,7 @@
    8.42  lemma dvd_mult_right:
    8.43    "a * b dvd c \<Longrightarrow> b dvd c"
    8.44    using dvd_mult_left [of b a c] by (simp add: ac_simps)
    8.45 -  
    8.46 +
    8.47  end
    8.48  
    8.49  class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult
    8.50 @@ -237,20 +237,15 @@
    8.51  
    8.52  end
    8.53  
    8.54 -class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add
    8.55 -  + zero_neq_one + comm_monoid_mult
    8.56 +class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add +
    8.57 +                               zero_neq_one + comm_monoid_mult +
    8.58 +  assumes right_diff_distrib' [algebra_simps]: "a * (b - c) = a * b - a * c"
    8.59  begin
    8.60  
    8.61  subclass semiring_1_cancel ..
    8.62  subclass comm_semiring_0_cancel ..
    8.63  subclass comm_semiring_1 ..
    8.64  
    8.65 -end
    8.66 -
    8.67 -class comm_semiring_1_diff_distrib = comm_semiring_1_cancel +
    8.68 -  assumes right_diff_distrib' [algebra_simps]: "a * (b - c) = a * b - a * c"
    8.69 -begin
    8.70 -
    8.71  lemma left_diff_distrib' [algebra_simps]:
    8.72    "(b - c) * a = b * a - c * a"
    8.73    by (simp add: algebra_simps)
    8.74 @@ -266,7 +261,7 @@
    8.75      then obtain d where "a * c + b = a * d" ..
    8.76      then have "a * c + b - a * c = a * d - a * c" by simp
    8.77      then have "b = a * d - a * c" by simp
    8.78 -    then have "b = a * (d - c)" by (simp add: algebra_simps) 
    8.79 +    then have "b = a * (d - c)" by (simp add: algebra_simps)
    8.80      then show ?Q ..
    8.81    qed
    8.82    then show "a dvd c * a + b \<longleftrightarrow> a dvd b" by (simp add: ac_simps)
    8.83 @@ -314,10 +309,10 @@
    8.84  text {* Distribution rules *}
    8.85  
    8.86  lemma minus_mult_left: "- (a * b) = - a * b"
    8.87 -by (rule minus_unique) (simp add: distrib_right [symmetric]) 
    8.88 +by (rule minus_unique) (simp add: distrib_right [symmetric])
    8.89  
    8.90  lemma minus_mult_right: "- (a * b) = a * - b"
    8.91 -by (rule minus_unique) (simp add: distrib_left [symmetric]) 
    8.92 +by (rule minus_unique) (simp add: distrib_left [symmetric])
    8.93  
    8.94  text{*Extract signs from products*}
    8.95  lemmas mult_minus_left [simp] = minus_mult_left [symmetric]
    8.96 @@ -380,9 +375,7 @@
    8.97  begin
    8.98  
    8.99  subclass ring_1 ..
   8.100 -subclass comm_semiring_1_cancel ..
   8.101 -
   8.102 -subclass comm_semiring_1_diff_distrib
   8.103 +subclass comm_semiring_1_cancel
   8.104    by unfold_locales (simp add: algebra_simps)
   8.105  
   8.106  lemma dvd_minus_iff [simp]: "x dvd - y \<longleftrightarrow> x dvd y"
   8.107 @@ -447,11 +440,11 @@
   8.108  
   8.109  lemma mult_left_cancel:
   8.110    "c \<noteq> 0 \<Longrightarrow> c * a = c * b \<longleftrightarrow> a = b"
   8.111 -  by simp 
   8.112 +  by simp
   8.113  
   8.114  lemma mult_right_cancel:
   8.115    "c \<noteq> 0 \<Longrightarrow> a * c = b * c \<longleftrightarrow> a = b"
   8.116 -  by simp 
   8.117 +  by simp
   8.118  
   8.119  end
   8.120  
   8.121 @@ -496,7 +489,7 @@
   8.122  lemma mult_cancel_right2 [simp]:
   8.123    "a * c = c \<longleftrightarrow> c = 0 \<or> a = 1"
   8.124  by (insert mult_cancel_right [of a c 1], simp)
   8.125 - 
   8.126 +
   8.127  lemma mult_cancel_left1 [simp]:
   8.128    "c = c * b \<longleftrightarrow> c = 0 \<or> b = 1"
   8.129  by (insert mult_cancel_left [of c 1 b], force)
   8.130 @@ -507,7 +500,7 @@
   8.131  
   8.132  end
   8.133  
   8.134 -class semidom = comm_semiring_1_diff_distrib + semiring_no_zero_divisors
   8.135 +class semidom = comm_semiring_1_cancel + semiring_no_zero_divisors
   8.136  
   8.137  class idom = comm_ring_1 + semiring_no_zero_divisors
   8.138  begin
   8.139 @@ -553,10 +546,10 @@
   8.140  text {*
   8.141    The theory of partially ordered rings is taken from the books:
   8.142    \begin{itemize}
   8.143 -  \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 
   8.144 +  \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979
   8.145    \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
   8.146    \end{itemize}
   8.147 -  Most of the used notions can also be looked up in 
   8.148 +  Most of the used notions can also be looked up in
   8.149    \begin{itemize}
   8.150    \item @{url "http://www.mathworld.com"} by Eric Weisstein et. al.
   8.151    \item \emph{Algebra I} by van der Waerden, Springer.
   8.152 @@ -640,7 +633,7 @@
   8.153  lemma dvd_mult_div_cancel [simp]:
   8.154    "a dvd b \<Longrightarrow> a * (b div a) = b"
   8.155    using dvd_div_mult_self [of a b] by (simp add: ac_simps)
   8.156 -  
   8.157 +
   8.158  lemma div_mult_swap:
   8.159    assumes "c dvd b"
   8.160    shows "a * (b div c) = (a * b) div c"
   8.161 @@ -658,7 +651,7 @@
   8.162    shows "b div c * a = (b * a) div c"
   8.163    using assms div_mult_swap [of c b a] by (simp add: ac_simps)
   8.164  
   8.165 -  
   8.166 +
   8.167  text \<open>Units: invertible elements in a ring\<close>
   8.168  
   8.169  abbreviation is_unit :: "'a \<Rightarrow> bool"
   8.170 @@ -669,7 +662,7 @@
   8.171    "\<not> is_unit 0"
   8.172    by simp
   8.173  
   8.174 -lemma unit_imp_dvd [dest]: 
   8.175 +lemma unit_imp_dvd [dest]:
   8.176    "is_unit b \<Longrightarrow> b dvd a"
   8.177    by (rule dvd_trans [of _ 1]) simp_all
   8.178  
   8.179 @@ -716,8 +709,8 @@
   8.180  
   8.181  lemma unit_prod [intro]:
   8.182    "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a * b)"
   8.183 -  by (subst mult_1_left [of 1, symmetric]) (rule mult_dvd_mono) 
   8.184 -  
   8.185 +  by (subst mult_1_left [of 1, symmetric]) (rule mult_dvd_mono)
   8.186 +
   8.187  lemma unit_div [intro]:
   8.188    "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a div b)"
   8.189    by (erule is_unitE [of b a]) (simp add: ac_simps unit_prod)
   8.190 @@ -794,7 +787,7 @@
   8.191  lemma unit_mult_left_cancel:
   8.192    assumes "is_unit a"
   8.193    shows "a * b = a * c \<longleftrightarrow> b = c" (is "?P \<longleftrightarrow> ?Q")
   8.194 -  using assms mult_cancel_left [of a b c] by auto 
   8.195 +  using assms mult_cancel_left [of a b c] by auto
   8.196  
   8.197  lemma unit_mult_right_cancel:
   8.198    "is_unit a \<Longrightarrow> b * a = c * a \<longleftrightarrow> b = c"
   8.199 @@ -809,12 +802,12 @@
   8.200      by (rule unit_mult_right_cancel)
   8.201    with assms show ?thesis by simp
   8.202  qed
   8.203 -  
   8.204 +
   8.205  
   8.206  text \<open>Associated elements in a ring --- an equivalence relation induced
   8.207    by the quasi-order divisibility.\<close>
   8.208  
   8.209 -definition associated :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
   8.210 +definition associated :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   8.211  where
   8.212    "associated a b \<longleftrightarrow> a dvd b \<and> b dvd a"
   8.213  
   8.214 @@ -877,10 +870,10 @@
   8.215    then have "is_unit c" by auto
   8.216    with `a = c * b` that show thesis by blast
   8.217  qed
   8.218 -  
   8.219 -lemmas unit_simps = mult_unit_dvd_iff div_unit_dvd_iff dvd_mult_unit_iff 
   8.220 +
   8.221 +lemmas unit_simps = mult_unit_dvd_iff div_unit_dvd_iff dvd_mult_unit_iff
   8.222    dvd_div_unit_iff unit_div_mult_swap unit_div_commute
   8.223 -  unit_mult_left_cancel unit_mult_right_cancel unit_div_cancel 
   8.224 +  unit_mult_left_cancel unit_mult_right_cancel unit_div_cancel
   8.225    unit_eq_div1 unit_eq_div2
   8.226  
   8.227  end
   8.228 @@ -919,10 +912,10 @@
   8.229  using mult_right_mono [of a 0 b] by simp
   8.230  
   8.231  text {* Legacy - use @{text mult_nonpos_nonneg} *}
   8.232 -lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0" 
   8.233 +lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0"
   8.234  by (drule mult_right_mono [of b 0], auto)
   8.235  
   8.236 -lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> 0" 
   8.237 +lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> 0"
   8.238  by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)
   8.239  
   8.240  end
   8.241 @@ -937,7 +930,7 @@
   8.242  lemma mult_left_less_imp_less:
   8.243    "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
   8.244  by (force simp add: mult_left_mono not_le [symmetric])
   8.245 - 
   8.246 +
   8.247  lemma mult_right_less_imp_less:
   8.248    "a * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
   8.249  by (force simp add: mult_right_mono not_le [symmetric])
   8.250 @@ -980,7 +973,7 @@
   8.251  lemma mult_left_le_imp_le:
   8.252    "c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
   8.253  by (force simp add: mult_strict_left_mono _not_less [symmetric])
   8.254 - 
   8.255 +
   8.256  lemma mult_right_le_imp_le:
   8.257    "a * c \<le> b * c \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
   8.258  by (force simp add: mult_strict_right_mono not_less [symmetric])
   8.259 @@ -995,7 +988,7 @@
   8.260  using mult_strict_right_mono [of a 0 b] by simp
   8.261  
   8.262  text {* Legacy - use @{text mult_neg_pos} *}
   8.263 -lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0" 
   8.264 +lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0"
   8.265  by (drule mult_strict_right_mono [of b 0], auto)
   8.266  
   8.267  lemma zero_less_mult_pos:
   8.268 @@ -1072,7 +1065,7 @@
   8.269  
   8.270  end
   8.271  
   8.272 -class ordered_comm_semiring = comm_semiring_0 + ordered_ab_semigroup_add + 
   8.273 +class ordered_comm_semiring = comm_semiring_0 + ordered_ab_semigroup_add +
   8.274    assumes comm_mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
   8.275  begin
   8.276  
   8.277 @@ -1118,7 +1111,7 @@
   8.278  
   8.279  end
   8.280  
   8.281 -class ordered_ring = ring + ordered_cancel_semiring 
   8.282 +class ordered_ring = ring + ordered_cancel_semiring
   8.283  begin
   8.284  
   8.285  subclass ordered_ab_group_add ..
   8.286 @@ -1239,7 +1232,7 @@
   8.287  
   8.288  lemma mult_le_0_iff:
   8.289    "a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"
   8.290 -  apply (insert zero_le_mult_iff [of "-a" b]) 
   8.291 +  apply (insert zero_le_mult_iff [of "-a" b])
   8.292    apply force
   8.293    done
   8.294  
   8.295 @@ -1252,26 +1245,26 @@
   8.296  lemma mult_less_cancel_right_disj:
   8.297    "a * c < b * c \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
   8.298    apply (cases "c = 0")
   8.299 -  apply (auto simp add: neq_iff mult_strict_right_mono 
   8.300 +  apply (auto simp add: neq_iff mult_strict_right_mono
   8.301                        mult_strict_right_mono_neg)
   8.302 -  apply (auto simp add: not_less 
   8.303 +  apply (auto simp add: not_less
   8.304                        not_le [symmetric, of "a*c"]
   8.305                        not_le [symmetric, of a])
   8.306    apply (erule_tac [!] notE)
   8.307 -  apply (auto simp add: less_imp_le mult_right_mono 
   8.308 +  apply (auto simp add: less_imp_le mult_right_mono
   8.309                        mult_right_mono_neg)
   8.310    done
   8.311  
   8.312  lemma mult_less_cancel_left_disj:
   8.313    "c * a < c * b \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
   8.314    apply (cases "c = 0")
   8.315 -  apply (auto simp add: neq_iff mult_strict_left_mono 
   8.316 +  apply (auto simp add: neq_iff mult_strict_left_mono
   8.317                        mult_strict_left_mono_neg)
   8.318 -  apply (auto simp add: not_less 
   8.319 +  apply (auto simp add: not_less
   8.320                        not_le [symmetric, of "c*a"]
   8.321                        not_le [symmetric, of a])
   8.322    apply (erule_tac [!] notE)
   8.323 -  apply (auto simp add: less_imp_le mult_left_mono 
   8.324 +  apply (auto simp add: less_imp_le mult_left_mono
   8.325                        mult_left_mono_neg)
   8.326    done
   8.327  
   8.328 @@ -1328,26 +1321,35 @@
   8.329  
   8.330  class linordered_semidom = semidom + linordered_comm_semiring_strict +
   8.331    assumes zero_less_one [simp]: "0 < 1"
   8.332 +  assumes le_add_diff_inverse2 [simp]: "b \<le> a \<Longrightarrow> a - b + b = a"
   8.333  begin
   8.334  
   8.335 +text {* Addition is the inverse of subtraction. *}
   8.336 +
   8.337 +lemma le_add_diff_inverse [simp]: "b \<le> a \<Longrightarrow> b + (a - b) = a"
   8.338 +  by (frule le_add_diff_inverse2) (simp add: add.commute)
   8.339 +
   8.340 +lemma add_diff_inverse: "~ a<b \<Longrightarrow> b + (a - b) = a"
   8.341 +  by simp
   8.342 +  
   8.343  lemma pos_add_strict:
   8.344    shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
   8.345    using add_strict_mono [of 0 a b c] by simp
   8.346  
   8.347  lemma zero_le_one [simp]: "0 \<le> 1"
   8.348 -by (rule zero_less_one [THEN less_imp_le]) 
   8.349 +by (rule zero_less_one [THEN less_imp_le])
   8.350  
   8.351  lemma not_one_le_zero [simp]: "\<not> 1 \<le> 0"
   8.352 -by (simp add: not_le) 
   8.353 +by (simp add: not_le)
   8.354  
   8.355  lemma not_one_less_zero [simp]: "\<not> 1 < 0"
   8.356 -by (simp add: not_less) 
   8.357 +by (simp add: not_less)
   8.358  
   8.359  lemma less_1_mult:
   8.360    assumes "1 < m" and "1 < n"
   8.361    shows "1 < m * n"
   8.362    using assms mult_strict_mono [of 1 m 1 n]
   8.363 -    by (simp add:  less_trans [OF zero_less_one]) 
   8.364 +    by (simp add:  less_trans [OF zero_less_one])
   8.365  
   8.366  lemma mult_left_le: "c \<le> 1 \<Longrightarrow> 0 \<le> a \<Longrightarrow> a * c \<le> a"
   8.367    using mult_left_mono[of c 1 a] by simp
   8.368 @@ -1371,7 +1373,9 @@
   8.369  proof
   8.370    have "0 \<le> 1 * 1" by (rule zero_le_square)
   8.371    thus "0 < 1" by (simp add: le_less)
   8.372 -qed 
   8.373 +  show "\<And>b a. b \<le> a \<Longrightarrow> a - b + b = a"
   8.374 +    by simp
   8.375 +qed
   8.376  
   8.377  lemma linorder_neqE_linordered_idom:
   8.378    assumes "x \<noteq> y" obtains "x < y" | "y < x"
   8.379 @@ -1461,7 +1465,7 @@
   8.380  by(subst abs_dvd_iff[symmetric]) simp
   8.381  
   8.382  text {* The following lemmas can be proven in more general structures, but
   8.383 -are dangerous as simp rules in absence of @{thm neg_equal_zero}, 
   8.384 +are dangerous as simp rules in absence of @{thm neg_equal_zero},
   8.385  @{thm neg_less_pos}, @{thm neg_less_eq_nonneg}. *}
   8.386  
   8.387  lemma equation_minus_iff_1 [simp, no_atp]:
   8.388 @@ -1559,12 +1563,12 @@
   8.389  qed (auto simp add: abs_if not_less mult_less_0_iff)
   8.390  
   8.391  lemma abs_mult:
   8.392 -  "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>" 
   8.393 +  "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
   8.394    by (rule abs_eq_mult) auto
   8.395  
   8.396  lemma abs_mult_self:
   8.397    "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
   8.398 -  by (simp add: abs_if) 
   8.399 +  by (simp add: abs_if)
   8.400  
   8.401  lemma abs_mult_less:
   8.402    "\<bar>a\<bar> < c \<Longrightarrow> \<bar>b\<bar> < d \<Longrightarrow> \<bar>a\<bar> * \<bar>b\<bar> < c * d"
   8.403 @@ -1572,11 +1576,11 @@
   8.404    assume ac: "\<bar>a\<bar> < c"
   8.405    hence cpos: "0<c" by (blast intro: le_less_trans abs_ge_zero)
   8.406    assume "\<bar>b\<bar> < d"
   8.407 -  thus ?thesis by (simp add: ac cpos mult_strict_mono) 
   8.408 +  thus ?thesis by (simp add: ac cpos mult_strict_mono)
   8.409  qed
   8.410  
   8.411  lemma abs_less_iff:
   8.412 -  "\<bar>a\<bar> < b \<longleftrightarrow> a < b \<and> - a < b" 
   8.413 +  "\<bar>a\<bar> < b \<longleftrightarrow> a < b \<and> - a < b"
   8.414    by (simp add: less_le abs_le_iff) (auto simp add: abs_if)
   8.415  
   8.416  lemma abs_mult_pos: