# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1435074928 -3600
# Node ID 24af00b010cf6a8c793672eb3276ddb79ccb9c16
# Parent  ce7030d9191d023d5267b613313a17f9a641ed90
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.

diff -r ce7030d9191d -r 24af00b010cf src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Mon Jun 22 23:19:48 2015 +0200
+++ b/src/HOL/Code_Numeral.thy	Tue Jun 23 16:55:28 2015 +0100
@@ -217,7 +217,7 @@
 
 instance integer :: semiring_numeral_div
   by intro_classes (transfer,
-    fact semiring_numeral_div_class.le_add_diff_inverse2
+    fact le_add_diff_inverse2
     semiring_numeral_div_class.div_less
     semiring_numeral_div_class.mod_less
     semiring_numeral_div_class.div_positive
diff -r ce7030d9191d -r 24af00b010cf src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Mon Jun 22 23:19:48 2015 +0200
+++ b/src/HOL/Divides.thy	Tue Jun 23 16:55:28 2015 +0100
@@ -92,7 +92,7 @@
   then show ?thesis by simp
 qed
 
-lemma mod_mult_self2 [simp]: 
+lemma mod_mult_self2 [simp]:
   "(a + b * c) mod b = a mod b"
   by (simp add: mult.commute [of b])
 
@@ -365,9 +365,9 @@
   have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" .
   with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b)
     = c * a + c * (a mod b)" by (simp add: algebra_simps)
-  with mod_div_equality show ?thesis by simp 
+  with mod_div_equality show ?thesis by simp
 qed
-  
+
 lemma mod_mult_mult2:
   "(a * c) mod (b * c) = (a mod b) * c"
   using mod_mult_mult1 [of c a b] by (simp add: mult.commute)
@@ -406,7 +406,7 @@
 done
 
 lemma dvd_div_eq_mult:
-  assumes "a \<noteq> 0" and "a dvd b"  
+  assumes "a \<noteq> 0" and "a dvd b"
   shows "b div a = c \<longleftrightarrow> b = c * a"
 proof
   assume "b = c * a"
@@ -417,7 +417,7 @@
   moreover from `a dvd b` have "b div a * a = b" by simp
   ultimately show "b = c * a" by simp
 qed
-   
+
 lemma dvd_div_div_eq_mult:
   assumes "a \<noteq> 0" "c \<noteq> 0" and "a dvd b" "c dvd d"
   shows "b div a = d div c \<longleftrightarrow> b * c = a * d"
@@ -515,11 +515,11 @@
 lemma mod_minus1_right [simp]: "a mod (-1) = 0"
   using mod_minus_right [of a 1] by simp
 
-lemma minus_mod_self2 [simp]: 
+lemma minus_mod_self2 [simp]:
   "(a - b) mod b = a mod b"
   by (simp add: mod_diff_right_eq)
 
-lemma minus_mod_self1 [simp]: 
+lemma minus_mod_self1 [simp]:
   "(b - a) mod b = - a mod b"
   using mod_add_self2 [of "- a" b] by simp
 
@@ -528,7 +528,7 @@
 
 subsubsection {* Parity and division *}
 
-class semiring_div_parity = semiring_div + comm_semiring_1_diff_distrib + numeral + 
+class semiring_div_parity = semiring_div + comm_semiring_1_cancel + numeral +
   assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
   assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1"
   assumes zero_not_eq_two: "0 \<noteq> 2"
@@ -618,8 +618,7 @@
   and less technical class hierarchy.
 *}
 
-class semiring_numeral_div = semiring_div + comm_semiring_1_diff_distrib + linordered_semidom +
-  assumes le_add_diff_inverse2: "b \<le> a \<Longrightarrow> a - b + b = a"
+class semiring_numeral_div = semiring_div + comm_semiring_1_cancel + linordered_semidom +
   assumes div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
     and mod_less: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"
     and div_positive: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0"
@@ -794,7 +793,7 @@
   then have "divmod m n =
     divmod_step n (numeral m div numeral (Num.Bit0 n),
       numeral m mod numeral (Num.Bit0 n))"
-    by (simp only: numeral.simps distrib mult_1) 
+    by (simp only: numeral.simps distrib mult_1)
   then have "divmod m n = divmod_step n (divmod m (Num.Bit0 n))"
     by (simp add: divmod_def)
   with False show ?thesis by simp
@@ -834,10 +833,7 @@
 
 end
 
-hide_fact (open) le_add_diff_inverse2
-  -- {* restore simple accesses for more general variants of theorems *}
-
-  
+
 subsection {* Division on @{typ nat} *}
 
 text {*
@@ -927,7 +923,7 @@
 qed
 
 lemma divmod_nat_unique:
-  assumes "divmod_nat_rel m n qr" 
+  assumes "divmod_nat_rel m n qr"
   shows "divmod_nat m n = qr"
   using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)
 
@@ -953,12 +949,12 @@
   by (simp add: prod_eq_iff)
 
 lemma div_nat_unique:
-  assumes "divmod_nat_rel m n (q, r)" 
+  assumes "divmod_nat_rel m n (q, r)"
   shows "m div n = q"
   using assms by (auto dest!: divmod_nat_unique simp add: prod_eq_iff)
 
 lemma mod_nat_unique:
-  assumes "divmod_nat_rel m n (q, r)" 
+  assumes "divmod_nat_rel m n (q, r)"
   shows "m mod n = r"
   using assms by (auto dest!: divmod_nat_unique simp add: prod_eq_iff)
 
@@ -1168,7 +1164,7 @@
   assumes "divmod_nat_rel a b (q, r)"
   shows "divmod_nat_rel a (b * c) (q div c, b *(q mod c) + r)"
 proof -
-  { assume "r < b" and "0 < c" 
+  { assume "r < b" and "0 < c"
     then have "b * (q mod c) + r < b * c"
       apply (cut_tac m = q and n = c in mod_less_divisor)
       apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
@@ -1180,7 +1176,7 @@
   } with assms show ?thesis
     by (auto simp add: divmod_nat_rel_def algebra_simps add_mult_distrib2 [symmetric])
 qed
-    
+
 lemma div_mult2_eq: "a div (b * c) = (a div b) div (c::nat)"
 by (force simp add: divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN div_nat_unique])
 
@@ -1523,7 +1519,7 @@
 lemmas Suc_div_eq_add3_div_numeral [simp] = Suc_div_eq_add3_div [of _ "numeral v"] for v
 lemmas Suc_mod_eq_add3_mod_numeral [simp] = Suc_mod_eq_add3_mod [of _ "numeral v"] for v
 
-lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1" 
+lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1"
 apply (induct "m")
 apply (simp_all add: mod_Suc)
 done
@@ -1539,30 +1535,30 @@
 lemma div_2_gt_zero [simp]: assumes A: "(1::nat) < n" shows "0 < n div 2"
 proof -
   from A have B: "0 < n - 1" and C: "n - 1 + 1 = n" by simp_all
-  from Suc_n_div_2_gt_zero [OF B] C show ?thesis by simp 
+  from Suc_n_div_2_gt_zero [OF B] C show ?thesis by simp
 qed
 
 lemma mod_mult_self4 [simp]: "Suc (k*n + m) mod n = Suc m mod n"
 proof -
   have "Suc (k * n + m) mod n = (k * n + Suc m) mod n" by simp
-  also have "... = Suc m mod n" by (rule mod_mult_self3) 
+  also have "... = Suc m mod n" by (rule mod_mult_self3)
   finally show ?thesis .
 qed
 
 lemma mod_Suc_eq_Suc_mod: "Suc m mod n = Suc (m mod n) mod n"
-apply (subst mod_Suc [of m]) 
-apply (subst mod_Suc [of "m mod n"], simp) 
+apply (subst mod_Suc [of m])
+apply (subst mod_Suc [of "m mod n"], simp)
 done
 
 lemma mod_2_not_eq_zero_eq_one_nat:
   fixes n :: nat
   shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
   by (fact not_mod_2_eq_0_eq_1)
-  
+
 lemma even_Suc_div_two [simp]:
   "even n \<Longrightarrow> Suc n div 2 = n div 2"
   using even_succ_div_two [of n] by simp
-  
+
 lemma odd_Suc_div_two [simp]:
   "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)"
   using odd_succ_div_two [of n] by simp
@@ -1603,7 +1599,7 @@
         by simp
     next
       case False
-      with hyp odd [of "n div 2"] show ?thesis 
+      with hyp odd [of "n div 2"] show ?thesis
         by simp
     qed
   qed
@@ -1650,12 +1646,12 @@
 
 definition divmod_int :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
     --{*The full division algorithm considers all possible signs for a, b
-       including the special case @{text "a=0, b<0"} because 
+       including the special case @{text "a=0, b<0"} because
        @{term negDivAlg} requires @{term "a<0"}.*}
   "divmod_int a b = (if 0 \<le> a then if 0 \<le> b then posDivAlg a b
                   else if a = 0 then (0, 0)
                        else apsnd uminus (negDivAlg (-a) (-b))
-               else 
+               else
                   if 0 < b then negDivAlg a b
                   else apsnd uminus (posDivAlg (-a) (-b)))"
 
@@ -1698,11 +1694,11 @@
 
     fun negateSnd (q,r:int) = (q,~r);
 
-    fun divmod (a,b) = if 0\<le>a then 
-                          if b>0 then posDivAlg (a,b) 
+    fun divmod (a,b) = if 0\<le>a then
+                          if b>0 then posDivAlg (a,b)
                            else if a=0 then (0,0)
                                 else negateSnd (negDivAlg (~a,~b))
-                       else 
+                       else
                           if 0<b then negDivAlg (a,b)
                           else        negateSnd (posDivAlg (~a,~b));
 \end{verbatim}
@@ -1712,7 +1708,7 @@
 subsubsection {* Uniqueness and Monotonicity of Quotients and Remainders *}
 
 lemma unique_quotient_lemma:
-     "[| b*q' + r'  \<le> b*q + r;  0 \<le> r';  r' < b;  r < b |]  
+     "[| b*q' + r'  \<le> b*q + r;  0 \<le> r';  r' < b;  r < b |]
       ==> q' \<le> (q::int)"
 apply (subgoal_tac "r' + b * (q'-q) \<le> r")
  prefer 2 apply (simp add: right_diff_distrib)
@@ -1725,23 +1721,23 @@
 done
 
 lemma unique_quotient_lemma_neg:
-     "[| b*q' + r' \<le> b*q + r;  r \<le> 0;  b < r;  b < r' |]  
+     "[| b*q' + r' \<le> b*q + r;  r \<le> 0;  b < r;  b < r' |]
       ==> q \<le> (q'::int)"
-by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma, 
+by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma,
     auto)
 
 lemma unique_quotient:
-     "[| divmod_int_rel a b (q, r); divmod_int_rel a b (q', r') |]  
+     "[| divmod_int_rel a b (q, r); divmod_int_rel a b (q', r') |]
       ==> q = q'"
 apply (simp add: divmod_int_rel_def linorder_neq_iff split: split_if_asm)
 apply (blast intro: order_antisym
-             dest: order_eq_refl [THEN unique_quotient_lemma] 
+             dest: order_eq_refl [THEN unique_quotient_lemma]
              order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
 done
 
 
 lemma unique_remainder:
-     "[| divmod_int_rel a b (q, r); divmod_int_rel a b (q', r') |]  
+     "[| divmod_int_rel a b (q, r); divmod_int_rel a b (q', r') |]
       ==> r = r'"
 apply (subgoal_tac "q = q'")
  apply (simp add: divmod_int_rel_def)
@@ -1754,9 +1750,9 @@
 text{*And positive divisors*}
 
 lemma adjust_eq [simp]:
-     "adjust b (q, r) = 
-      (let diff = r - b in  
-        if 0 \<le> diff then (2 * q + 1, diff)   
+     "adjust b (q, r) =
+      (let diff = r - b in
+        if 0 \<le> diff then (2 * q + 1, diff)
                      else (2*q, r))"
   by (simp add: Let_def adjust_def)
 
@@ -1764,7 +1760,7 @@
 
 text{*use with a simproc to avoid repeatedly proving the premise*}
 lemma posDivAlg_eqn:
-     "0 < b ==>  
+     "0 < b ==>
       posDivAlg a b = (if a<b then (0,a) else adjust b (posDivAlg a (2*b)))"
 by (rule posDivAlg.simps [THEN trans], simp)
 
@@ -1792,8 +1788,8 @@
 
 text{*use with a simproc to avoid repeatedly proving the premise*}
 lemma negDivAlg_eqn:
-     "0 < b ==>  
-      negDivAlg a b =       
+     "0 < b ==>
+      negDivAlg a b =
        (if 0\<le>a+b then (-1,a+b) else adjust b (negDivAlg a (2*b)))"
 by (rule negDivAlg.simps [THEN trans], simp)
 
@@ -1838,7 +1834,7 @@
                     posDivAlg_correct negDivAlg_correct)
 
 lemma divmod_int_unique:
-  assumes "divmod_int_rel a b qr" 
+  assumes "divmod_int_rel a b qr"
   shows "divmod_int a b = qr"
   using assms divmod_int_correct [of a b]
   using unique_quotient [of a b] unique_remainder [of a b]
@@ -1912,7 +1908,7 @@
 
   val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
 
-  val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac 
+  val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
     (@{thm diff_conv_add_uminus} :: @{thms add_0_left add_0_right} @ @{thms ac_simps}))
 )
 *}
@@ -1975,14 +1971,14 @@
 
 lemma zminus1_lemma:
      "divmod_int_rel a b (q, r) ==> b \<noteq> 0
-      ==> divmod_int_rel (-a) b (if r=0 then -q else -q - 1,  
+      ==> divmod_int_rel (-a) b (if r=0 then -q else -q - 1,
                           if r=0 then 0 else b-r)"
 by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff right_diff_distrib)
 
 
 lemma zdiv_zminus1_eq_if:
-     "b \<noteq> (0::int)  
-      ==> (-a) div b =  
+     "b \<noteq> (0::int)
+      ==> (-a) div b =
           (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
 by (blast intro: divmod_int_rel_div_mod [THEN zminus1_lemma, THEN div_int_unique])
 
@@ -1998,8 +1994,8 @@
   unfolding zmod_zminus1_eq_if by auto
 
 lemma zdiv_zminus2_eq_if:
-     "b \<noteq> (0::int)  
-      ==> a div (-b) =  
+     "b \<noteq> (0::int)
+      ==> a div (-b) =
           (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
 by (simp add: zdiv_zminus1_eq_if div_minus_right)
 
@@ -2010,7 +2006,7 @@
 lemma zmod_zminus2_not_zero:
   fixes k l :: int
   shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
-  unfolding zmod_zminus2_eq_if by auto 
+  unfolding zmod_zminus2_eq_if by auto
 
 
 subsubsection {* Computation of Division and Remainder *}
@@ -2185,10 +2181,10 @@
 done
 
 lemma zdiv_mono2_lemma:
-     "[| b*q + r = b'*q' + r';  0 \<le> b'*q' + r';   
-         r' < b';  0 \<le> r;  0 < b';  b' \<le> b |]   
+     "[| b*q + r = b'*q' + r';  0 \<le> b'*q' + r';
+         r' < b';  0 \<le> r;  0 < b';  b' \<le> b |]
       ==> q \<le> (q'::int)"
-apply (frule q_pos_lemma, assumption+) 
+apply (frule q_pos_lemma, assumption+)
 apply (subgoal_tac "b*q < b* (q' + 1) ")
  apply (simp add: mult_less_cancel_left)
 apply (subgoal_tac "b*q = r' - r + b'*q'")
@@ -2216,10 +2212,10 @@
 done
 
 lemma zdiv_mono2_neg_lemma:
-     "[| b*q + r = b'*q' + r';  b'*q' + r' < 0;   
-         r < b;  0 \<le> r';  0 < b';  b' \<le> b |]   
+     "[| b*q + r = b'*q' + r';  b'*q' + r' < 0;
+         r < b;  0 \<le> r';  0 < b';  b' \<le> b |]
       ==> q' \<le> (q::int)"
-apply (frule q_neg_lemma, assumption+) 
+apply (frule q_neg_lemma, assumption+)
 apply (subgoal_tac "b*q' < b* (q + 1) ")
  apply (simp add: mult_less_cancel_left)
 apply (simp add: distrib_left)
@@ -2242,7 +2238,7 @@
 text{*proving (a*b) div c = a * (b div c) + a * (b mod c) *}
 
 lemma zmult1_lemma:
-     "[| divmod_int_rel b c (q, r) |]  
+     "[| divmod_int_rel b c (q, r) |]
       ==> divmod_int_rel (a * b) c (a*q + a*r div c, a*r mod c)"
 by (auto simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left ac_simps)
 
@@ -2254,7 +2250,7 @@
 text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}
 
 lemma zadd1_lemma:
-     "[| divmod_int_rel a c (aq, ar);  divmod_int_rel b c (bq, br) |]  
+     "[| divmod_int_rel a c (aq, ar);  divmod_int_rel b c (bq, br) |]
       ==> divmod_int_rel (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)"
 by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left)
 
@@ -2346,10 +2342,10 @@
 apply simp
 done
 
-lemma zmult2_lemma: "[| divmod_int_rel a b (q, r); 0 < c |]  
+lemma zmult2_lemma: "[| divmod_int_rel a b (q, r); 0 < c |]
       ==> divmod_int_rel a (b * c) (q div c, b*(q mod c) + r)"
 by (auto simp add: mult.assoc divmod_int_rel_def linorder_neq_iff
-                   zero_less_mult_iff distrib_left [symmetric] 
+                   zero_less_mult_iff distrib_left [symmetric]
                    zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: split_if_asm)
 
 lemma zdiv_zmult2_eq:
@@ -2392,15 +2388,15 @@
 text{*The proofs of the two lemmas below are essentially identical*}
 
 lemma split_pos_lemma:
- "0<k ==> 
+ "0<k ==>
     P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i j)"
 apply (rule iffI, clarify)
- apply (erule_tac P="P x y" for x y in rev_mp)  
- apply (subst mod_add_eq) 
- apply (subst zdiv_zadd1_eq) 
- apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial)  
+ apply (erule_tac P="P x y" for x y in rev_mp)
+ apply (subst mod_add_eq)
+ apply (subst zdiv_zadd1_eq)
+ apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial)
 txt{*converse direction*}
-apply (drule_tac x = "n div k" in spec) 
+apply (drule_tac x = "n div k" in spec)
 apply (drule_tac x = "n mod k" in spec, simp)
 done
 
@@ -2408,36 +2404,36 @@
  "k<0 ==>
     P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i j)"
 apply (rule iffI, clarify)
- apply (erule_tac P="P x y" for x y in rev_mp)  
- apply (subst mod_add_eq) 
- apply (subst zdiv_zadd1_eq) 
- apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial)  
+ apply (erule_tac P="P x y" for x y in rev_mp)
+ apply (subst mod_add_eq)
+ apply (subst zdiv_zadd1_eq)
+ apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial)
 txt{*converse direction*}
-apply (drule_tac x = "n div k" in spec) 
+apply (drule_tac x = "n div k" in spec)
 apply (drule_tac x = "n mod k" in spec, simp)
 done
 
 lemma split_zdiv:
  "P(n div k :: int) =
-  ((k = 0 --> P 0) & 
-   (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i)) & 
+  ((k = 0 --> P 0) &
+   (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i)) &
    (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i)))"
 apply (case_tac "k=0", simp)
 apply (simp only: linorder_neq_iff)
-apply (erule disjE) 
- apply (simp_all add: split_pos_lemma [of concl: "%x y. P x"] 
+apply (erule disjE)
+ apply (simp_all add: split_pos_lemma [of concl: "%x y. P x"]
                       split_neg_lemma [of concl: "%x y. P x"])
 done
 
 lemma split_zmod:
  "P(n mod k :: int) =
-  ((k = 0 --> P n) & 
-   (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P j)) & 
+  ((k = 0 --> P n) &
+   (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P j)) &
    (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P j)))"
 apply (case_tac "k=0", simp)
 apply (simp only: linorder_neq_iff)
-apply (erule disjE) 
- apply (simp_all add: split_pos_lemma [of concl: "%x y. P y"] 
+apply (erule disjE)
+ apply (simp_all add: split_pos_lemma [of concl: "%x y. P y"]
                       split_neg_lemma [of concl: "%x y. P y"])
 done
 
@@ -2470,7 +2466,7 @@
   using pos_divmod_int_rel_mult_2 [OF _ divmod_int_rel_div_mod]
   by (rule div_int_unique)
 
-lemma neg_zdiv_mult_2: 
+lemma neg_zdiv_mult_2:
   assumes A: "a \<le> (0::int)" shows "(1 + 2*b) div (2*a) = (b+1) div a"
   using neg_divmod_int_rel_mult_2 [OF A divmod_int_rel_div_mod]
   by (rule div_int_unique)
@@ -2483,7 +2479,7 @@
   by (rule div_mult_mult1, simp)
 
 lemma zdiv_numeral_Bit1 [simp]:
-  "numeral (Num.Bit1 v) div numeral (Num.Bit0 w) =  
+  "numeral (Num.Bit1 v) div numeral (Num.Bit0 w) =
     (numeral v div (numeral w :: int))"
   unfolding numeral.simps
   unfolding mult_2 [symmetric] add.commute [of _ 1]
@@ -2505,7 +2501,7 @@
 
 (* FIXME: add rules for negative numerals *)
 lemma zmod_numeral_Bit0 [simp]:
-  "numeral (Num.Bit0 v) mod numeral (Num.Bit0 w) =  
+  "numeral (Num.Bit0 v) mod numeral (Num.Bit0 w) =
     (2::int) * (numeral v mod numeral w)"
   unfolding numeral_Bit0 [of v] numeral_Bit0 [of w]
   unfolding mult_2 [symmetric] by (rule mod_mult_mult1)
@@ -2609,7 +2605,7 @@
     simp add: zmult_div_cancel
     pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial
     zmod_zmult2_eq zdiv_zmult2_eq)
-  
+
 lemma zdiv_int: "int (a div b) = (int a) div (int b)"
 apply (subst split_div, auto)
 apply (subst split_zdiv, auto)
@@ -2620,7 +2616,7 @@
 lemma zmod_int: "int (a mod b) = (int a) mod (int b)"
 apply (subst split_mod, auto)
 apply (subst split_zmod, auto)
-apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia 
+apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia
        in unique_remainder)
 apply (auto simp add: divmod_int_rel_def of_nat_mult)
 done
@@ -2718,7 +2714,7 @@
 proof
   assume H: "x mod n = y mod n"
   hence "x mod n - y mod n = 0" by simp
-  hence "(x mod n - y mod n) mod n = 0" by simp 
+  hence "(x mod n - y mod n) mod n = 0" by simp
   hence "(x - y) mod n = 0" by (simp add: mod_diff_eq[symmetric])
   thus "n dvd x - y" by (simp add: dvd_eq_mod_eq_0)
 next
@@ -2732,27 +2728,27 @@
 lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y  mod n" and xy:"y \<le> x"
   shows "\<exists>q. x = y + n * q"
 proof-
-  from xy have th: "int x - int y = int (x - y)" by simp 
-  from xyn have "int x mod int n = int y mod int n" 
+  from xy have th: "int x - int y = int (x - y)" by simp
+  from xyn have "int x mod int n = int y mod int n"
     by (simp add: zmod_int [symmetric])
-  hence "int n dvd int x - int y" by (simp only: zmod_eq_dvd_iff[symmetric]) 
+  hence "int n dvd int x - int y" by (simp only: zmod_eq_dvd_iff[symmetric])
   hence "n dvd x - y" by (simp add: th zdvd_int)
   then show ?thesis using xy unfolding dvd_def apply clarsimp apply (rule_tac x="k" in exI) by arith
 qed
 
-lemma nat_mod_eq_iff: "(x::nat) mod n = y mod n \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)" 
+lemma nat_mod_eq_iff: "(x::nat) mod n = y mod n \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)"
   (is "?lhs = ?rhs")
 proof
   assume H: "x mod n = y mod n"
   {assume xy: "x \<le> y"
     from H have th: "y mod n = x mod n" by simp
-    from nat_mod_eq_lemma[OF th xy] have ?rhs 
+    from nat_mod_eq_lemma[OF th xy] have ?rhs
       apply clarify  apply (rule_tac x="q" in exI) by (rule exI[where x="0"], simp)}
   moreover
   {assume xy: "y \<le> x"
-    from nat_mod_eq_lemma[OF H xy] have ?rhs 
+    from nat_mod_eq_lemma[OF H xy] have ?rhs
       apply clarify  apply (rule_tac x="0" in exI) by (rule_tac x="q" in exI, simp)}
-  ultimately  show ?rhs using linear[of x y] by blast  
+  ultimately  show ?rhs using linear[of x y] by blast
 next
   assume ?rhs then obtain q1 q2 where q12: "x + n * q1 = y + n * q2" by blast
   hence "(x + n * q1) mod n = (y + n * q2) mod n" by simp
@@ -2762,7 +2758,7 @@
 text {*
   This re-embedding of natural division on integers goes back to the
   time when numerals had been signed numerals.  It should
-  now be replaced by the algorithm developed in @{class semiring_numeral_div}.  
+  now be replaced by the algorithm developed in @{class semiring_numeral_div}.
 *}
 
 lemma div_nat_numeral [simp]:
diff -r ce7030d9191d -r 24af00b010cf src/HOL/Library/Function_Algebras.thy
--- a/src/HOL/Library/Function_Algebras.thy	Mon Jun 22 23:19:48 2015 +0200
+++ b/src/HOL/Library/Function_Algebras.thy	Tue Jun 23 16:55:28 2015 +0100
@@ -154,7 +154,8 @@
 
 instance "fun" :: (type, semiring_1_cancel) semiring_1_cancel ..
 
-instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel ..
+instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel 
+  by default (auto simp add: times_fun_def algebra_simps)
 
 instance "fun" :: (type, semiring_char_0) semiring_char_0
 proof
diff -r ce7030d9191d -r 24af00b010cf src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Mon Jun 22 23:19:48 2015 +0200
+++ b/src/HOL/Library/Polynomial.thy	Tue Jun 23 16:55:28 2015 +0100
@@ -868,8 +868,6 @@
 
 end
 
-instance poly :: (comm_semiring_1_cancel) comm_semiring_1_cancel ..
-
 instance poly :: (comm_ring) comm_ring ..
 
 instance poly :: (comm_ring_1) comm_ring_1 ..
diff -r ce7030d9191d -r 24af00b010cf src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Mon Jun 22 23:19:48 2015 +0200
+++ b/src/HOL/NSA/StarDef.thy	Tue Jun 23 16:55:28 2015 +0100
@@ -837,7 +837,7 @@
 
 declare dvd_def [transfer_refold]
 
-instance star :: (comm_semiring_1_diff_distrib) comm_semiring_1_diff_distrib
+instance star :: (comm_semiring_1_cancel) comm_semiring_1_cancel
   by (intro_classes; transfer) (fact right_diff_distrib')
 
 instance star :: (semiring_no_zero_divisors) semiring_no_zero_divisors
@@ -847,7 +847,6 @@
   by (intro_classes; transfer) simp_all
 
 instance star :: (semiring_1_cancel) semiring_1_cancel ..
-instance star :: (comm_semiring_1_cancel) comm_semiring_1_cancel ..
 instance star :: (ring) ring ..
 instance star :: (comm_ring) comm_ring ..
 instance star :: (ring_1) ring_1 ..
@@ -902,7 +901,10 @@
 instance star :: (ordered_comm_ring) ordered_comm_ring ..
 
 instance star :: (linordered_semidom) linordered_semidom
-  by (intro_classes; transfer) (fact zero_less_one)
+  apply intro_classes
+  apply(transfer, fact zero_less_one)
+  apply(transfer, fact le_add_diff_inverse2)
+  done
 
 instance star :: (linordered_idom) linordered_idom ..
 instance star :: (linordered_field) linordered_field ..
@@ -1005,7 +1007,6 @@
 
 instance star :: (semiring_numeral_div) semiring_numeral_div
 apply intro_classes
-apply(transfer, fact semiring_numeral_div_class.le_add_diff_inverse2)
 apply(transfer, fact semiring_numeral_div_class.div_less)
 apply(transfer, fact semiring_numeral_div_class.mod_less)
 apply(transfer, fact semiring_numeral_div_class.div_positive)
diff -r ce7030d9191d -r 24af00b010cf src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Mon Jun 22 23:19:48 2015 +0200
+++ b/src/HOL/Nat.thy	Tue Jun 23 16:55:28 2015 +0100
@@ -282,10 +282,25 @@
   show "n * m = m * n" by (induct n) simp_all
   show "(n * m) * q = n * (m * q)" by (induct n) (simp_all add: add_mult_distrib)
   show "(n + m) * q = n * q + m * q" by (rule add_mult_distrib)
+next
+  fix k m n :: nat
+  show "k * ((m::nat) - n) = (k * m) - (k * n)"
+    by (induct m n rule: diff_induct) simp_all
 qed
 
 end
 
+text {* Difference distributes over multiplication *}
+
+lemma diff_mult_distrib:
+  "((m::nat) - n) * k = (m * k) - (n * k)"
+  by (fact left_diff_distrib')
+
+lemma diff_mult_distrib2:
+  "k * ((m::nat) - n) = (k * m) - (k * n)"
+  by (fact right_diff_distrib')
+
+
 subsubsection {* Addition *}
 
 lemma nat_add_left_cancel:
@@ -364,24 +379,6 @@
 lemma diff_Suc_1 [simp]: "Suc n - 1 = n"
   unfolding One_nat_def by simp
 
-text {* Difference distributes over multiplication *}
-
-instance nat :: comm_semiring_1_diff_distrib
-proof
-  fix k m n :: nat
-  show "k * ((m::nat) - n) = (k * m) - (k * n)"
-    by (induct m n rule: diff_induct) simp_all
-qed
-
-lemma diff_mult_distrib:
-  "((m::nat) - n) * k = (m * k) - (n * k)"
-  by (fact left_diff_distrib')
-  
-lemma diff_mult_distrib2:
-  "k * ((m::nat) - n) = (k * m) - (k * n)"
-  by (fact right_diff_distrib')
-
-
 subsubsection {* Multiplication *}
 
 lemma add_mult_distrib2: "k * (m + n) = (k * m) + ((k * n)::nat)"
@@ -488,7 +485,7 @@
 instance
 proof
   fix n m :: nat
-  show "n < m \<longleftrightarrow> n \<le> m \<and> \<not> m \<le> n" 
+  show "n < m \<longleftrightarrow> n \<le> m \<and> \<not> m \<le> n"
   proof (induct n arbitrary: m)
     case 0 then show ?case by (cases m) (simp_all add: less_eq_Suc_le)
   next
@@ -550,7 +547,7 @@
   by (rule order_less_irrefl)
 
 lemma less_not_refl2: "n < m ==> m \<noteq> (n::nat)"
-  by (rule not_sym) (rule less_imp_neq) 
+  by (rule not_sym) (rule less_imp_neq)
 
 lemma less_not_refl3: "(s::nat) < t ==> s \<noteq> t"
   by (rule less_imp_neq)
@@ -594,7 +591,7 @@
 subsubsection {* Inductive (?) properties *}
 
 lemma Suc_lessI: "m < n ==> Suc m \<noteq> n ==> Suc m < n"
-  unfolding less_eq_Suc_le [of m] le_less by simp 
+  unfolding less_eq_Suc_le [of m] le_less by simp
 
 lemma lessE:
   assumes major: "i < k"
@@ -783,6 +780,12 @@
 apply (simp_all add: add_less_mono)
 done
 
+text {* Addition is the inverse of subtraction:
+  if @{term "n \<le> m"} then @{term "n + (m - n) = m"}. *}
+lemma add_diff_inverse_nat: "~  m < n ==> n + (m - n) = (m::nat)"
+by (induct m n rule: diff_induct) simp_all
+
+
 text{*The naturals form an ordered @{text semidom}*}
 instance nat :: linordered_semidom
 proof
@@ -790,7 +793,9 @@
   show "\<And>m n q :: nat. m \<le> n \<Longrightarrow> q + m \<le> q + n" by simp
   show "\<And>m n q :: nat. m < n \<Longrightarrow> 0 < q \<Longrightarrow> q * m < q * n" by (simp add: mult_less_mono2)
   show "\<And>m n :: nat. m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> m * n \<noteq> 0" by simp
-qed
+  show "\<And>m n :: nat. n \<le> m ==> (m - n) + n = (m::nat)"
+    by (simp add: add_diff_inverse_nat add.commute linorder_not_less)
+qed 
 
 
 subsubsection {* @{term min} and @{term max} *}
@@ -989,7 +994,7 @@
   "\<lbrakk> !!n::nat. \<not> P n \<Longrightarrow>  \<exists>m<n. \<not>  P m \<rbrakk> \<Longrightarrow>  P n"
 by (induct n rule: less_induct) auto
 
-lemma infinite_descent0[case_names 0 smaller]: 
+lemma infinite_descent0[case_names 0 smaller]:
   "\<lbrakk> P 0; !!n. n>0 \<Longrightarrow> \<not> P n \<Longrightarrow> (\<exists>m::nat. m < n \<and> \<not>P m) \<rbrakk> \<Longrightarrow> P n"
 by (rule infinite_descent) (case_tac "n>0", auto)
 
@@ -1112,17 +1117,6 @@
 
 subsubsection {* More results about difference *}
 
-text {* Addition is the inverse of subtraction:
-  if @{term "n \<le> m"} then @{term "n + (m - n) = m"}. *}
-lemma add_diff_inverse: "~  m < n ==> n + (m - n) = (m::nat)"
-by (induct m n rule: diff_induct) simp_all
-
-lemma le_add_diff_inverse [simp]: "n \<le> m ==> n + (m - n) = (m::nat)"
-by (simp add: add_diff_inverse linorder_not_less)
-
-lemma le_add_diff_inverse2 [simp]: "n \<le> m ==> (m - n) + n = (m::nat)"
-by (simp add: add.commute)
-
 lemma Suc_diff_le: "n \<le> m ==> Suc m - n = Suc (m - n)"
 by (induct m n rule: diff_induct) simp_all
 
@@ -1490,8 +1484,8 @@
 
 lemma of_nat_0_neq [simp]:
   "0 \<noteq> of_nat (Suc n)"
-  unfolding of_nat_0_eq_iff by simp  
-  
+  unfolding of_nat_0_eq_iff by simp
+
 end
 
 context linordered_semidom
@@ -1770,7 +1764,7 @@
 lemma min_diff: "min (m - (i::nat)) (n - i) = min m n - i"
 by auto
 
-lemma inj_on_diff_nat: 
+lemma inj_on_diff_nat:
   assumes k_le_n: "\<forall>n \<in> N. k \<le> (n::nat)"
   shows "inj_on (\<lambda>n. n - k) N"
 proof (rule inj_onI)
@@ -1980,7 +1974,7 @@
 
 lemma nat_mult_1: "(1::nat) * n = n"
   by (fact mult_1_left)
- 
+
 lemma nat_mult_1_right: "n * (1::nat) = n"
   by (fact mult_1_right)
 
diff -r ce7030d9191d -r 24af00b010cf src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Mon Jun 22 23:19:48 2015 +0200
+++ b/src/HOL/Parity.thy	Tue Jun 23 16:55:28 2015 +0100
@@ -11,7 +11,7 @@
 
 subsection {* Ring structures with parity and @{text even}/@{text odd} predicates *}
 
-class semiring_parity = comm_semiring_1_diff_distrib + numeral +
+class semiring_parity = comm_semiring_1_cancel + numeral +
   assumes odd_one [simp]: "\<not> 2 dvd 1"
   assumes odd_even_add: "\<not> 2 dvd a \<Longrightarrow> \<not> 2 dvd b \<Longrightarrow> 2 dvd a + b"
   assumes even_multD: "2 dvd a * b \<Longrightarrow> 2 dvd a \<or> 2 dvd b"
diff -r ce7030d9191d -r 24af00b010cf src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Mon Jun 22 23:19:48 2015 +0200
+++ b/src/HOL/Rings.thy	Tue Jun 23 16:55:28 2015 +0100
@@ -95,7 +95,7 @@
 
 definition of_bool :: "bool \<Rightarrow> 'a"
 where
-  "of_bool p = (if p then 1 else 0)" 
+  "of_bool p = (if p then 1 else 0)"
 
 lemma of_bool_eq [simp, code]:
   "of_bool False = 0"
@@ -113,8 +113,8 @@
 lemma split_of_bool_asm:
   "P (of_bool p) \<longleftrightarrow> \<not> (p \<and> \<not> P 1 \<or> \<not> p \<and> \<not> P 0)"
   by (cases p) simp_all
-  
-end  
+
+end
 
 class semiring_1 = zero_neq_one + semiring_0 + monoid_mult
 
@@ -130,7 +130,7 @@
   unfolding dvd_def ..
 
 lemma dvdE [elim?]: "b dvd a \<Longrightarrow> (\<And>k. a = b * k \<Longrightarrow> P) \<Longrightarrow> P"
-  unfolding dvd_def by blast 
+  unfolding dvd_def by blast
 
 end
 
@@ -165,7 +165,7 @@
 
 lemma dvd_mult2 [simp]:
   "a dvd b \<Longrightarrow> a dvd (b * c)"
-  using dvd_mult [of a b c] by (simp add: ac_simps) 
+  using dvd_mult [of a b c] by (simp add: ac_simps)
 
 lemma dvd_triv_right [simp]:
   "a dvd b * a"
@@ -193,7 +193,7 @@
 lemma dvd_mult_right:
   "a * b dvd c \<Longrightarrow> b dvd c"
   using dvd_mult_left [of b a c] by (simp add: ac_simps)
-  
+
 end
 
 class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult
@@ -237,20 +237,15 @@
 
 end
 
-class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add
-  + zero_neq_one + comm_monoid_mult
+class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add +
+                               zero_neq_one + comm_monoid_mult +
+  assumes right_diff_distrib' [algebra_simps]: "a * (b - c) = a * b - a * c"
 begin
 
 subclass semiring_1_cancel ..
 subclass comm_semiring_0_cancel ..
 subclass comm_semiring_1 ..
 
-end
-
-class comm_semiring_1_diff_distrib = comm_semiring_1_cancel +
-  assumes right_diff_distrib' [algebra_simps]: "a * (b - c) = a * b - a * c"
-begin
-
 lemma left_diff_distrib' [algebra_simps]:
   "(b - c) * a = b * a - c * a"
   by (simp add: algebra_simps)
@@ -266,7 +261,7 @@
     then obtain d where "a * c + b = a * d" ..
     then have "a * c + b - a * c = a * d - a * c" by simp
     then have "b = a * d - a * c" by simp
-    then have "b = a * (d - c)" by (simp add: algebra_simps) 
+    then have "b = a * (d - c)" by (simp add: algebra_simps)
     then show ?Q ..
   qed
   then show "a dvd c * a + b \<longleftrightarrow> a dvd b" by (simp add: ac_simps)
@@ -314,10 +309,10 @@
 text {* Distribution rules *}
 
 lemma minus_mult_left: "- (a * b) = - a * b"
-by (rule minus_unique) (simp add: distrib_right [symmetric]) 
+by (rule minus_unique) (simp add: distrib_right [symmetric])
 
 lemma minus_mult_right: "- (a * b) = a * - b"
-by (rule minus_unique) (simp add: distrib_left [symmetric]) 
+by (rule minus_unique) (simp add: distrib_left [symmetric])
 
 text{*Extract signs from products*}
 lemmas mult_minus_left [simp] = minus_mult_left [symmetric]
@@ -380,9 +375,7 @@
 begin
 
 subclass ring_1 ..
-subclass comm_semiring_1_cancel ..
-
-subclass comm_semiring_1_diff_distrib
+subclass comm_semiring_1_cancel
   by unfold_locales (simp add: algebra_simps)
 
 lemma dvd_minus_iff [simp]: "x dvd - y \<longleftrightarrow> x dvd y"
@@ -447,11 +440,11 @@
 
 lemma mult_left_cancel:
   "c \<noteq> 0 \<Longrightarrow> c * a = c * b \<longleftrightarrow> a = b"
-  by simp 
+  by simp
 
 lemma mult_right_cancel:
   "c \<noteq> 0 \<Longrightarrow> a * c = b * c \<longleftrightarrow> a = b"
-  by simp 
+  by simp
 
 end
 
@@ -496,7 +489,7 @@
 lemma mult_cancel_right2 [simp]:
   "a * c = c \<longleftrightarrow> c = 0 \<or> a = 1"
 by (insert mult_cancel_right [of a c 1], simp)
- 
+
 lemma mult_cancel_left1 [simp]:
   "c = c * b \<longleftrightarrow> c = 0 \<or> b = 1"
 by (insert mult_cancel_left [of c 1 b], force)
@@ -507,7 +500,7 @@
 
 end
 
-class semidom = comm_semiring_1_diff_distrib + semiring_no_zero_divisors
+class semidom = comm_semiring_1_cancel + semiring_no_zero_divisors
 
 class idom = comm_ring_1 + semiring_no_zero_divisors
 begin
@@ -553,10 +546,10 @@
 text {*
   The theory of partially ordered rings is taken from the books:
   \begin{itemize}
-  \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 
+  \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979
   \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
   \end{itemize}
-  Most of the used notions can also be looked up in 
+  Most of the used notions can also be looked up in
   \begin{itemize}
   \item @{url "http://www.mathworld.com"} by Eric Weisstein et. al.
   \item \emph{Algebra I} by van der Waerden, Springer.
@@ -640,7 +633,7 @@
 lemma dvd_mult_div_cancel [simp]:
   "a dvd b \<Longrightarrow> a * (b div a) = b"
   using dvd_div_mult_self [of a b] by (simp add: ac_simps)
-  
+
 lemma div_mult_swap:
   assumes "c dvd b"
   shows "a * (b div c) = (a * b) div c"
@@ -658,7 +651,7 @@
   shows "b div c * a = (b * a) div c"
   using assms div_mult_swap [of c b a] by (simp add: ac_simps)
 
-  
+
 text \<open>Units: invertible elements in a ring\<close>
 
 abbreviation is_unit :: "'a \<Rightarrow> bool"
@@ -669,7 +662,7 @@
   "\<not> is_unit 0"
   by simp
 
-lemma unit_imp_dvd [dest]: 
+lemma unit_imp_dvd [dest]:
   "is_unit b \<Longrightarrow> b dvd a"
   by (rule dvd_trans [of _ 1]) simp_all
 
@@ -716,8 +709,8 @@
 
 lemma unit_prod [intro]:
   "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a * b)"
-  by (subst mult_1_left [of 1, symmetric]) (rule mult_dvd_mono) 
-  
+  by (subst mult_1_left [of 1, symmetric]) (rule mult_dvd_mono)
+
 lemma unit_div [intro]:
   "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a div b)"
   by (erule is_unitE [of b a]) (simp add: ac_simps unit_prod)
@@ -794,7 +787,7 @@
 lemma unit_mult_left_cancel:
   assumes "is_unit a"
   shows "a * b = a * c \<longleftrightarrow> b = c" (is "?P \<longleftrightarrow> ?Q")
-  using assms mult_cancel_left [of a b c] by auto 
+  using assms mult_cancel_left [of a b c] by auto
 
 lemma unit_mult_right_cancel:
   "is_unit a \<Longrightarrow> b * a = c * a \<longleftrightarrow> b = c"
@@ -809,12 +802,12 @@
     by (rule unit_mult_right_cancel)
   with assms show ?thesis by simp
 qed
-  
+
 
 text \<open>Associated elements in a ring --- an equivalence relation induced
   by the quasi-order divisibility.\<close>
 
-definition associated :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
+definition associated :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 where
   "associated a b \<longleftrightarrow> a dvd b \<and> b dvd a"
 
@@ -877,10 +870,10 @@
   then have "is_unit c" by auto
   with `a = c * b` that show thesis by blast
 qed
-  
-lemmas unit_simps = mult_unit_dvd_iff div_unit_dvd_iff dvd_mult_unit_iff 
+
+lemmas unit_simps = mult_unit_dvd_iff div_unit_dvd_iff dvd_mult_unit_iff
   dvd_div_unit_iff unit_div_mult_swap unit_div_commute
-  unit_mult_left_cancel unit_mult_right_cancel unit_div_cancel 
+  unit_mult_left_cancel unit_mult_right_cancel unit_div_cancel
   unit_eq_div1 unit_eq_div2
 
 end
@@ -919,10 +912,10 @@
 using mult_right_mono [of a 0 b] by simp
 
 text {* Legacy - use @{text mult_nonpos_nonneg} *}
-lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0" 
+lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0"
 by (drule mult_right_mono [of b 0], auto)
 
-lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> 0" 
+lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> 0"
 by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)
 
 end
@@ -937,7 +930,7 @@
 lemma mult_left_less_imp_less:
   "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
 by (force simp add: mult_left_mono not_le [symmetric])
- 
+
 lemma mult_right_less_imp_less:
   "a * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
 by (force simp add: mult_right_mono not_le [symmetric])
@@ -980,7 +973,7 @@
 lemma mult_left_le_imp_le:
   "c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
 by (force simp add: mult_strict_left_mono _not_less [symmetric])
- 
+
 lemma mult_right_le_imp_le:
   "a * c \<le> b * c \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
 by (force simp add: mult_strict_right_mono not_less [symmetric])
@@ -995,7 +988,7 @@
 using mult_strict_right_mono [of a 0 b] by simp
 
 text {* Legacy - use @{text mult_neg_pos} *}
-lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0" 
+lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0"
 by (drule mult_strict_right_mono [of b 0], auto)
 
 lemma zero_less_mult_pos:
@@ -1072,7 +1065,7 @@
 
 end
 
-class ordered_comm_semiring = comm_semiring_0 + ordered_ab_semigroup_add + 
+class ordered_comm_semiring = comm_semiring_0 + ordered_ab_semigroup_add +
   assumes comm_mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
 begin
 
@@ -1118,7 +1111,7 @@
 
 end
 
-class ordered_ring = ring + ordered_cancel_semiring 
+class ordered_ring = ring + ordered_cancel_semiring
 begin
 
 subclass ordered_ab_group_add ..
@@ -1239,7 +1232,7 @@
 
 lemma mult_le_0_iff:
   "a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"
-  apply (insert zero_le_mult_iff [of "-a" b]) 
+  apply (insert zero_le_mult_iff [of "-a" b])
   apply force
   done
 
@@ -1252,26 +1245,26 @@
 lemma mult_less_cancel_right_disj:
   "a * c < b * c \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
   apply (cases "c = 0")
-  apply (auto simp add: neq_iff mult_strict_right_mono 
+  apply (auto simp add: neq_iff mult_strict_right_mono
                       mult_strict_right_mono_neg)
-  apply (auto simp add: not_less 
+  apply (auto simp add: not_less
                       not_le [symmetric, of "a*c"]
                       not_le [symmetric, of a])
   apply (erule_tac [!] notE)
-  apply (auto simp add: less_imp_le mult_right_mono 
+  apply (auto simp add: less_imp_le mult_right_mono
                       mult_right_mono_neg)
   done
 
 lemma mult_less_cancel_left_disj:
   "c * a < c * b \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and>  b < a"
   apply (cases "c = 0")
-  apply (auto simp add: neq_iff mult_strict_left_mono 
+  apply (auto simp add: neq_iff mult_strict_left_mono
                       mult_strict_left_mono_neg)
-  apply (auto simp add: not_less 
+  apply (auto simp add: not_less
                       not_le [symmetric, of "c*a"]
                       not_le [symmetric, of a])
   apply (erule_tac [!] notE)
-  apply (auto simp add: less_imp_le mult_left_mono 
+  apply (auto simp add: less_imp_le mult_left_mono
                       mult_left_mono_neg)
   done
 
@@ -1328,26 +1321,35 @@
 
 class linordered_semidom = semidom + linordered_comm_semiring_strict +
   assumes zero_less_one [simp]: "0 < 1"
+  assumes le_add_diff_inverse2 [simp]: "b \<le> a \<Longrightarrow> a - b + b = a"
 begin
 
+text {* Addition is the inverse of subtraction. *}
+
+lemma le_add_diff_inverse [simp]: "b \<le> a \<Longrightarrow> b + (a - b) = a"
+  by (frule le_add_diff_inverse2) (simp add: add.commute)
+
+lemma add_diff_inverse: "~ a<b \<Longrightarrow> b + (a - b) = a"
+  by simp
+  
 lemma pos_add_strict:
   shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
   using add_strict_mono [of 0 a b c] by simp
 
 lemma zero_le_one [simp]: "0 \<le> 1"
-by (rule zero_less_one [THEN less_imp_le]) 
+by (rule zero_less_one [THEN less_imp_le])
 
 lemma not_one_le_zero [simp]: "\<not> 1 \<le> 0"
-by (simp add: not_le) 
+by (simp add: not_le)
 
 lemma not_one_less_zero [simp]: "\<not> 1 < 0"
-by (simp add: not_less) 
+by (simp add: not_less)
 
 lemma less_1_mult:
   assumes "1 < m" and "1 < n"
   shows "1 < m * n"
   using assms mult_strict_mono [of 1 m 1 n]
-    by (simp add:  less_trans [OF zero_less_one]) 
+    by (simp add:  less_trans [OF zero_less_one])
 
 lemma mult_left_le: "c \<le> 1 \<Longrightarrow> 0 \<le> a \<Longrightarrow> a * c \<le> a"
   using mult_left_mono[of c 1 a] by simp
@@ -1371,7 +1373,9 @@
 proof
   have "0 \<le> 1 * 1" by (rule zero_le_square)
   thus "0 < 1" by (simp add: le_less)
-qed 
+  show "\<And>b a. b \<le> a \<Longrightarrow> a - b + b = a"
+    by simp
+qed
 
 lemma linorder_neqE_linordered_idom:
   assumes "x \<noteq> y" obtains "x < y" | "y < x"
@@ -1461,7 +1465,7 @@
 by(subst abs_dvd_iff[symmetric]) simp
 
 text {* The following lemmas can be proven in more general structures, but
-are dangerous as simp rules in absence of @{thm neg_equal_zero}, 
+are dangerous as simp rules in absence of @{thm neg_equal_zero},
 @{thm neg_less_pos}, @{thm neg_less_eq_nonneg}. *}
 
 lemma equation_minus_iff_1 [simp, no_atp]:
@@ -1559,12 +1563,12 @@
 qed (auto simp add: abs_if not_less mult_less_0_iff)
 
 lemma abs_mult:
-  "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>" 
+  "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
   by (rule abs_eq_mult) auto
 
 lemma abs_mult_self:
   "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
-  by (simp add: abs_if) 
+  by (simp add: abs_if)
 
 lemma abs_mult_less:
   "\<bar>a\<bar> < c \<Longrightarrow> \<bar>b\<bar> < d \<Longrightarrow> \<bar>a\<bar> * \<bar>b\<bar> < c * d"
@@ -1572,11 +1576,11 @@
   assume ac: "\<bar>a\<bar> < c"
   hence cpos: "0<c" by (blast intro: le_less_trans abs_ge_zero)
   assume "\<bar>b\<bar> < d"
-  thus ?thesis by (simp add: ac cpos mult_strict_mono) 
+  thus ?thesis by (simp add: ac cpos mult_strict_mono)
 qed
 
 lemma abs_less_iff:
-  "\<bar>a\<bar> < b \<longleftrightarrow> a < b \<and> - a < b" 
+  "\<bar>a\<bar> < b \<longleftrightarrow> a < b \<and> - a < b"
   by (simp add: less_le abs_le_iff) (auto simp add: abs_if)
 
 lemma abs_mult_pos: