diff -r f630017ed01c -r d149e3cbdb39 src/HOL/Integ/IntDiv.thy
--- a/src/HOL/Integ/IntDiv.thy	Wed Dec 10 14:29:44 2003 +0100
+++ b/src/HOL/Integ/IntDiv.thy	Wed Dec 10 15:59:34 2003 +0100
@@ -10,18 +10,18 @@
     fun posDivAlg (a,b) =
       if a<b then (0,a)
       else let val (q,r) = posDivAlg(a, 2*b)
-	       in  if 0<=r-b then (2*q+1, r-b) else (2*q, r)
+	       in  if 0\<le>r-b then (2*q+1, r-b) else (2*q, r)
 	   end
 
     fun negDivAlg (a,b) =
-      if 0<=a+b then (~1,a+b)
+      if 0\<le>a+b then (~1,a+b)
       else let val (q,r) = negDivAlg(a, 2*b)
-	       in  if 0<=r-b then (2*q+1, r-b) else (2*q, r)
+	       in  if 0\<le>r-b then (2*q+1, r-b) else (2*q, r)
 	   end;
 
     fun negateSnd (q,r:int) = (q,~r);
 
-    fun divAlg (a,b) = if 0<=a then 
+    fun divAlg (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))
@@ -40,10 +40,10 @@
   quorem :: "(int*int) * (int*int) => bool"
     "quorem == %((a,b), (q,r)).
                       a = b*q + r &
-                      (if 0 < b then 0<=r & r<b else b<r & r <= 0)"
+                      (if 0 < b then 0\<le>r & r<b else b<r & r \<le> 0)"
 
   adjust :: "[int, int*int] => int*int"
-    "adjust b == %(q,r). if 0 <= r-b then (2*q + 1, r-b)
+    "adjust b == %(q,r). if 0 \<le> r-b then (2*q + 1, r-b)
                          else (2*q, r)"
 
 (** the division algorithm **)
@@ -52,14 +52,14 @@
 consts posDivAlg :: "int*int => int*int"
 recdef posDivAlg "inv_image less_than (%(a,b). nat(a - b + 1))"
     "posDivAlg (a,b) =
-       (if (a<b | b<=0) then (0,a)
+       (if (a<b | b\<le>0) then (0,a)
         else adjust b (posDivAlg(a, 2*b)))"
 
 (*for the case a<0, b>0*)
 consts negDivAlg :: "int*int => int*int"
 recdef negDivAlg "inv_image less_than (%(a,b). nat(- a - b))"
     "negDivAlg (a,b) =
-       (if (0<=a+b | b<=0) then (-1,a+b)
+       (if (0\<le>a+b | b\<le>0) then (-1,a+b)
         else adjust b (negDivAlg(a, 2*b)))"
 
 (*for the general case b~=0*)
@@ -72,8 +72,8 @@
     including the special case a=0, b<0, because negDivAlg requires a<0*)
   divAlg :: "int*int => int*int"
     "divAlg ==
-       %(a,b). if 0<=a then
-                  if 0<=b then posDivAlg (a,b)
+       %(a,b). if 0\<le>a then
+                  if 0\<le>b then posDivAlg (a,b)
                   else if a=0 then (0,0)
                        else negateSnd (negDivAlg (-a,-b))
                else 
@@ -92,9 +92,9 @@
 subsection{*Uniqueness and Monotonicity of Quotients and Remainders*}
 
 lemma unique_quotient_lemma:
-     "[| b*q' + r'  <= b*q + r;  0 <= r';  0 < b;  r < b |]  
-      ==> q' <= (q::int)"
-apply (subgoal_tac "r' + b * (q'-q) <= r")
+     "[| b*q' + r'  \<le> b*q + r;  0 \<le> r';  0 < b;  r < b |]  
+      ==> q' \<le> (q::int)"
+apply (subgoal_tac "r' + b * (q'-q) \<le> r")
  prefer 2 apply (simp add: zdiff_zmult_distrib2)
 apply (subgoal_tac "0 < b * (1 + q - q') ")
 apply (erule_tac [2] order_le_less_trans)
@@ -105,8 +105,8 @@
 done
 
 lemma unique_quotient_lemma_neg:
-     "[| b*q' + r' <= b*q + r;  r <= 0;  b < 0;  b < r' |]  
-      ==> q <= (q'::int)"
+     "[| b*q' + r' \<le> b*q + r;  r \<le> 0;  b < 0;  b < r' |]  
+      ==> q \<le> (q'::int)"
 by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma, 
     auto)
 
@@ -136,7 +136,7 @@
 lemma adjust_eq [simp]:
      "adjust b (q,r) = 
       (let diff = r-b in  
-	if 0 <= diff then (2*q + 1, diff)   
+	if 0 \<le> diff then (2*q + 1, diff)   
                      else (2*q, r))"
 by (simp add: Let_def adjust_def)
 
@@ -150,7 +150,7 @@
 
 (*Correctness of posDivAlg: it computes quotients correctly*)
 lemma posDivAlg_correct [rule_format]:
-     "0 <= a --> 0 < b --> quorem ((a, b), posDivAlg (a, b))"
+     "0 \<le> a --> 0 < b --> quorem ((a, b), posDivAlg (a, b))"
 apply (induct_tac a b rule: posDivAlg.induct, auto)
  apply (simp_all add: quorem_def)
  (*base case: a<b*)
@@ -172,7 +172,7 @@
 lemma negDivAlg_eqn:
      "0 < b ==>  
       negDivAlg (a,b) =       
-       (if 0<=a+b then (-1,a+b) else adjust b (negDivAlg(a, 2*b)))"
+       (if 0\<le>a+b then (-1,a+b) else adjust b (negDivAlg(a, 2*b)))"
 by (rule negDivAlg.simps [THEN trans], simp)
 
 (*Correctness of negDivAlg: it computes quotients correctly
@@ -181,7 +181,7 @@
      "a < 0 --> 0 < b --> quorem ((a, b), negDivAlg (a, b))"
 apply (induct_tac a b rule: negDivAlg.induct, auto)
  apply (simp_all add: quorem_def)
- (*base case: 0<=a+b*)
+ (*base case: 0\<le>a+b*)
  apply (simp add: negDivAlg_eqn)
 (*main argument*)
 apply (subst negDivAlg_eqn, assumption)
@@ -234,7 +234,7 @@
 
 use "IntDiv_setup.ML"
 
-lemma pos_mod_conj : "(0::int) < b ==> 0 <= a mod b & a mod b < b"
+lemma pos_mod_conj : "(0::int) < b ==> 0 \<le> a mod b & a mod b < b"
 apply (cut_tac a = a and b = b in divAlg_correct)
 apply (auto simp add: quorem_def mod_def)
 done
@@ -242,7 +242,7 @@
 lemmas pos_mod_sign[simp]  = pos_mod_conj [THEN conjunct1, standard]
    and pos_mod_bound[simp] = pos_mod_conj [THEN conjunct2, standard]
 
-lemma neg_mod_conj : "b < (0::int) ==> a mod b <= 0 & b < a mod b"
+lemma neg_mod_conj : "b < (0::int) ==> a mod b \<le> 0 & b < a mod b"
 apply (cut_tac a = a and b = b in divAlg_correct)
 apply (auto simp add: quorem_def div_def mod_def)
 done
@@ -265,34 +265,34 @@
 lemma quorem_mod: "[| quorem((a,b),(q,r));  b ~= 0 |] ==> a mod b = r"
 by (simp add: quorem_div_mod [THEN unique_remainder])
 
-lemma div_pos_pos_trivial: "[| (0::int) <= a;  a < b |] ==> a div b = 0"
+lemma div_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a div b = 0"
 apply (rule quorem_div)
 apply (auto simp add: quorem_def)
 done
 
-lemma div_neg_neg_trivial: "[| a <= (0::int);  b < a |] ==> a div b = 0"
+lemma div_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a div b = 0"
 apply (rule quorem_div)
 apply (auto simp add: quorem_def)
 done
 
-lemma div_pos_neg_trivial: "[| (0::int) < a;  a+b <= 0 |] ==> a div b = -1"
+lemma div_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a div b = -1"
 apply (rule quorem_div)
 apply (auto simp add: quorem_def)
 done
 
 (*There is no div_neg_pos_trivial because  0 div b = 0 would supersede it*)
 
-lemma mod_pos_pos_trivial: "[| (0::int) <= a;  a < b |] ==> a mod b = a"
+lemma mod_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a mod b = a"
 apply (rule_tac q = 0 in quorem_mod)
 apply (auto simp add: quorem_def)
 done
 
-lemma mod_neg_neg_trivial: "[| a <= (0::int);  b < a |] ==> a mod b = a"
+lemma mod_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a mod b = a"
 apply (rule_tac q = 0 in quorem_mod)
 apply (auto simp add: quorem_def)
 done
 
-lemma mod_pos_neg_trivial: "[| (0::int) < a;  a+b <= 0 |] ==> a mod b = a+b"
+lemma mod_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a mod b = a+b"
 apply (rule_tac q = "-1" in quorem_mod)
 apply (auto simp add: quorem_def)
 done
@@ -355,13 +355,13 @@
 
 subsection{*Division of a Number by Itself*}
 
-lemma self_quotient_aux1: "[| (0::int) < a; a = r + a*q; r < a |] ==> 1 <= q"
+lemma self_quotient_aux1: "[| (0::int) < a; a = r + a*q; r < a |] ==> 1 \<le> q"
 apply (subgoal_tac "0 < a*q")
  apply (simp add: int_0_less_mult_iff, arith)
 done
 
-lemma self_quotient_aux2: "[| (0::int) < a; a = r + a*q; 0 <= r |] ==> q <= 1"
-apply (subgoal_tac "0 <= a* (1-q) ")
+lemma self_quotient_aux2: "[| (0::int) < a; a = r + a*q; 0 \<le> r |] ==> q \<le> 1"
+apply (subgoal_tac "0 \<le> a* (1-q) ")
  apply (simp add: int_0_le_mult_iff)
 apply (simp add: zdiff_zmult_distrib2)
 done
@@ -408,10 +408,10 @@
 
 (** a positive, b positive **)
 
-lemma div_pos_pos: "[| 0 < a;  0 <= b |] ==> a div b = fst (posDivAlg(a,b))"
+lemma div_pos_pos: "[| 0 < a;  0 \<le> b |] ==> a div b = fst (posDivAlg(a,b))"
 by (simp add: div_def divAlg_def)
 
-lemma mod_pos_pos: "[| 0 < a;  0 <= b |] ==> a mod b = snd (posDivAlg(a,b))"
+lemma mod_pos_pos: "[| 0 < a;  0 \<le> b |] ==> a mod b = snd (posDivAlg(a,b))"
 by (simp add: mod_def divAlg_def)
 
 (** a negative, b positive **)
@@ -435,11 +435,11 @@
 (** a negative, b negative **)
 
 lemma div_neg_neg:
-     "[| a < 0;  b <= 0 |] ==> a div b = fst (negateSnd(posDivAlg(-a,-b)))"
+     "[| a < 0;  b \<le> 0 |] ==> a div b = fst (negateSnd(posDivAlg(-a,-b)))"
 by (simp add: div_def divAlg_def)
 
 lemma mod_neg_neg:
-     "[| a < 0;  b <= 0 |] ==> a mod b = snd (negateSnd(posDivAlg(-a,-b)))"
+     "[| a < 0;  b \<le> 0 |] ==> a mod b = snd (negateSnd(posDivAlg(-a,-b)))"
 by (simp add: mod_def divAlg_def)
 
 text {*Simplify expresions in which div and mod combine numerical constants*}
@@ -492,7 +492,7 @@
 
 subsection{*Monotonicity in the First Argument (Dividend)*}
 
-lemma zdiv_mono1: "[| a <= a';  0 < (b::int) |] ==> a div b <= a' div b"
+lemma zdiv_mono1: "[| a \<le> a';  0 < (b::int) |] ==> a div b \<le> a' div b"
 apply (cut_tac a = a and b = b in zmod_zdiv_equality)
 apply (cut_tac a = a' and b = b in zmod_zdiv_equality)
 apply (rule unique_quotient_lemma)
@@ -501,7 +501,7 @@
 apply (simp_all)
 done
 
-lemma zdiv_mono1_neg: "[| a <= a';  (b::int) < 0 |] ==> a' div b <= a div b"
+lemma zdiv_mono1_neg: "[| a \<le> a';  (b::int) < 0 |] ==> a' div b \<le> a div b"
 apply (cut_tac a = a and b = b in zmod_zdiv_equality)
 apply (cut_tac a = a' and b = b in zmod_zdiv_equality)
 apply (rule unique_quotient_lemma_neg)
@@ -514,16 +514,16 @@
 subsection{*Monotonicity in the Second Argument (Divisor)*}
 
 lemma q_pos_lemma:
-     "[| 0 <= b'*q' + r'; r' < b';  0 < b' |] ==> 0 <= (q'::int)"
+     "[| 0 \<le> b'*q' + r'; r' < b';  0 < b' |] ==> 0 \<le> (q'::int)"
 apply (subgoal_tac "0 < b'* (q' + 1) ")
  apply (simp add: int_0_less_mult_iff)
 apply (simp add: zadd_zmult_distrib2)
 done
 
 lemma zdiv_mono2_lemma:
-     "[| b*q + r = b'*q' + r';  0 <= b'*q' + r';   
-         r' < b';  0 <= r;  0 < b';  b' <= b |]   
-      ==> q <= (q'::int)"
+     "[| 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 (subgoal_tac "b*q < b* (q' + 1) ")
  apply (simp add: zmult_zless_cancel1)
@@ -535,7 +535,7 @@
 done
 
 lemma zdiv_mono2:
-     "[| (0::int) <= a;  0 < b';  b' <= b |] ==> a div b <= a div b'"
+     "[| (0::int) \<le> a;  0 < b';  b' \<le> b |] ==> a div b \<le> a div b'"
 apply (subgoal_tac "b ~= 0")
  prefer 2 apply arith
 apply (cut_tac a = a and b = b in zmod_zdiv_equality)
@@ -547,20 +547,20 @@
 done
 
 lemma q_neg_lemma:
-     "[| b'*q' + r' < 0;  0 <= r';  0 < b' |] ==> q' <= (0::int)"
+     "[| b'*q' + r' < 0;  0 \<le> r';  0 < b' |] ==> q' \<le> (0::int)"
 apply (subgoal_tac "b'*q' < 0")
  apply (simp add: zmult_less_0_iff, arith)
 done
 
 lemma zdiv_mono2_neg_lemma:
      "[| b*q + r = b'*q' + r';  b'*q' + r' < 0;   
-         r < b;  0 <= r';  0 < b';  b' <= b |]   
-      ==> q' <= (q::int)"
+         r < b;  0 \<le> r';  0 < b';  b' \<le> b |]   
+      ==> q' \<le> (q::int)"
 apply (frule q_neg_lemma, assumption+) 
 apply (subgoal_tac "b*q' < b* (q + 1) ")
  apply (simp add: zmult_zless_cancel1)
 apply (simp add: zadd_zmult_distrib2)
-apply (subgoal_tac "b*q' <= b'*q'")
+apply (subgoal_tac "b*q' \<le> b'*q'")
  prefer 2 apply (simp add: zmult_zle_mono1_neg)
 apply (subgoal_tac "b'*q' < b + b*q")
  apply arith
@@ -568,7 +568,7 @@
 done
 
 lemma zdiv_mono2_neg:
-     "[| a < (0::int);  0 < b';  b' <= b |] ==> a div b' <= a div b"
+     "[| a < (0::int);  0 < b';  b' \<le> b |] ==> a div b' \<le> a div b"
 apply (cut_tac a = a and b = b in zmod_zdiv_equality)
 apply (cut_tac a = a and b = b' in zmod_zdiv_equality)
 apply (rule zdiv_mono2_neg_lemma)
@@ -698,7 +698,7 @@
 
 (** first, four lemmas to bound the remainder for the cases b<0 and b>0 **)
 
-lemma zmult2_lemma_aux1: "[| (0::int) < c;  b < r;  r <= 0 |] ==> b*c < b*(q mod c) + r"
+lemma zmult2_lemma_aux1: "[| (0::int) < c;  b < r;  r \<le> 0 |] ==> b*c < b*(q mod c) + r"
 apply (subgoal_tac "b * (c - q mod c) < r * 1")
 apply (simp add: zdiff_zmult_distrib2)
 apply (rule order_le_less_trans)
@@ -708,19 +708,19 @@
                       add1_zle_eq pos_mod_bound)
 done
 
-lemma zmult2_lemma_aux2: "[| (0::int) < c;   b < r;  r <= 0 |] ==> b * (q mod c) + r <= 0"
-apply (subgoal_tac "b * (q mod c) <= 0")
+lemma zmult2_lemma_aux2: "[| (0::int) < c;   b < r;  r \<le> 0 |] ==> b * (q mod c) + r \<le> 0"
+apply (subgoal_tac "b * (q mod c) \<le> 0")
  apply arith
 apply (simp add: zmult_le_0_iff)
 done
 
-lemma zmult2_lemma_aux3: "[| (0::int) < c;  0 <= r;  r < b |] ==> 0 <= b * (q mod c) + r"
-apply (subgoal_tac "0 <= b * (q mod c) ")
+lemma zmult2_lemma_aux3: "[| (0::int) < c;  0 \<le> r;  r < b |] ==> 0 \<le> b * (q mod c) + r"
+apply (subgoal_tac "0 \<le> b * (q mod c) ")
 apply arith
 apply (simp add: int_0_le_mult_iff)
 done
 
-lemma zmult2_lemma_aux4: "[| (0::int) < c; 0 <= r; r < b |] ==> b * (q mod c) + r < b * c"
+lemma zmult2_lemma_aux4: "[| (0::int) < c; 0 \<le> r; r < b |] ==> b * (q mod c) + r < b * c"
 apply (subgoal_tac "r * 1 < b * (c - q mod c) ")
 apply (simp add: zdiff_zmult_distrib2)
 apply (rule order_less_le_trans)
@@ -798,7 +798,7 @@
 
 lemma split_pos_lemma:
  "0<k ==> 
-    P(n div k :: int)(n mod k) = (\<forall>i j. 0<=j & j<k & n = k*i + j --> P i j)"
+    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)
  apply clarify
  apply (erule_tac P="P ?x ?y" in rev_mp)  
@@ -813,7 +813,7 @@
 
 lemma split_neg_lemma:
  "k<0 ==>
-    P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j<=0 & n = k*i + j --> P i j)"
+    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)
  apply clarify
  apply (erule_tac P="P ?x ?y" in rev_mp)  
@@ -829,8 +829,8 @@
 lemma split_zdiv:
  "P(n div k :: int) =
   ((k = 0 --> P 0) & 
-   (0<k --> (\<forall>i j. 0<=j & j<k & n = k*i + j --> P i)) & 
-   (k<0 --> (\<forall>i j. k<j & j<=0 & n = k*i + j --> P i)))"
+   (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")
  apply (simp add: DIVISION_BY_ZERO)
 apply (simp only: linorder_neq_iff)
@@ -842,8 +842,8 @@
 lemma split_zmod:
  "P(n mod k :: int) =
   ((k = 0 --> P n) & 
-   (0<k --> (\<forall>i j. 0<=j & j<k & n = k*i + j --> P j)) & 
-   (k<0 --> (\<forall>i j. k<j & j<=0 & n = k*i + j --> P j)))"
+   (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")
  apply (simp add: DIVISION_BY_ZERO)
 apply (simp only: linorder_neq_iff)
@@ -861,29 +861,33 @@
 
 (** computing div by shifting **)
 
-lemma pos_zdiv_mult_2: "(0::int) <= a ==> (1 + 2*b) div (2*a) = b div a"
-apply (case_tac "a = 0", simp add: DIVISION_BY_ZERO)
-apply (subgoal_tac "1 <= a")
- prefer 2 apply arith
-apply (subgoal_tac "1 < a * 2")
- prefer 2 apply arith
-apply (subgoal_tac "2* (1 + b mod a) <= 2*a")
- apply (rule_tac [2] zmult_zle_mono2)
-apply (auto simp add: zadd_commute [of 1] zmult_commute add1_zle_eq 
-                      pos_mod_bound)
-apply (subst zdiv_zadd1_eq)
-apply (simp add: zdiv_zmult_zmult2 zmod_zmult_zmult2 div_pos_pos_trivial)
-apply (subst div_pos_pos_trivial)
-apply (auto simp add: mod_pos_pos_trivial)
-apply (subgoal_tac "0 <= b mod a", arith)
-apply (simp)
-done
+lemma pos_zdiv_mult_2: "(0::int) \<le> a ==> (1 + 2*b) div (2*a) = b div a"
+proof cases
+  assume "a=0"
+    thus ?thesis by simp
+next
+  assume "a\<noteq>0" and le_a: "0\<le>a"   
+  hence a_pos: "1 \<le> a" by arith
+  hence one_less_a2: "1 < 2*a" by arith
+  hence le_2a: "2 * (1 + b mod a) \<le> 2 * a"
+    by (simp add: mult_le_cancel_left zadd_commute [of 1] add1_zle_eq)
+  with a_pos have "0 \<le> b mod a" by simp
+  hence le_addm: "0 \<le> 1 mod (2*a) + 2*(b mod a)"
+    by (simp add: mod_pos_pos_trivial one_less_a2)
+  with  le_2a
+  have "(1 mod (2*a) + 2*(b mod a)) div (2*a) = 0"
+    by (simp add: div_pos_pos_trivial le_addm mod_pos_pos_trivial one_less_a2
+                  right_distrib) 
+  thus ?thesis
+    by (subst zdiv_zadd1_eq,
+        simp add: zdiv_zmult_zmult1 zmod_zmult_zmult1 one_less_a2
+                  div_pos_pos_trivial)
+qed
 
-
-lemma neg_zdiv_mult_2: "a <= (0::int) ==> (1 + 2*b) div (2*a) = (b+1) div a"
+lemma neg_zdiv_mult_2: "a \<le> (0::int) ==> (1 + 2*b) div (2*a) = (b+1) div a"
 apply (subgoal_tac " (1 + 2* (-b - 1)) div (2 * (-a)) = (-b - 1) div (-a) ")
 apply (rule_tac [2] pos_zdiv_mult_2)
-apply (auto simp add: zmult_zminus_right)
+apply (auto simp add: zmult_zminus_right right_diff_distrib)
 apply (subgoal_tac " (-1 - (2 * b)) = - (1 + (2 * b))")
 apply (simp only: zdiv_zminus_zminus zdiff_def zminus_zadd_distrib [symmetric],
        simp) 
@@ -892,12 +896,12 @@
 
 (*Not clear why this must be proved separately; probably number_of causes
   simplification problems*)
-lemma not_0_le_lemma: "~ 0 <= x ==> x <= (0::int)"
+lemma not_0_le_lemma: "~ 0 \<le> x ==> x \<le> (0::int)"
 by auto
 
 lemma zdiv_number_of_BIT[simp]:
      "number_of (v BIT b) div number_of (w BIT False) =  
-          (if ~b | (0::int) <= number_of w                    
+          (if ~b | (0::int) \<le> number_of w                    
            then number_of v div (number_of w)     
            else (number_of v + (1::int)) div (number_of w))"
 apply (simp only: zadd_assoc number_of_BIT)
@@ -911,31 +915,31 @@
 (** computing mod by shifting (proofs resemble those for div) **)
 
 lemma pos_zmod_mult_2:
-     "(0::int) <= a ==> (1 + 2*b) mod (2*a) = 1 + 2 * (b mod a)"
+     "(0::int) \<le> a ==> (1 + 2*b) mod (2*a) = 1 + 2 * (b mod a)"
 apply (case_tac "a = 0", simp add: DIVISION_BY_ZERO)
-apply (subgoal_tac "1 <= a")
+apply (subgoal_tac "1 \<le> a")
  prefer 2 apply arith
 apply (subgoal_tac "1 < a * 2")
  prefer 2 apply arith
-apply (subgoal_tac "2* (1 + b mod a) <= 2*a")
+apply (subgoal_tac "2* (1 + b mod a) \<le> 2*a")
  apply (rule_tac [2] zmult_zle_mono2)
 apply (auto simp add: zadd_commute [of 1] zmult_commute add1_zle_eq 
                       pos_mod_bound)
 apply (subst zmod_zadd1_eq)
 apply (simp add: zmod_zmult_zmult2 mod_pos_pos_trivial)
 apply (rule mod_pos_pos_trivial)
-apply (auto simp add: mod_pos_pos_trivial)
-apply (subgoal_tac "0 <= b mod a", arith)
+apply (auto simp add: mod_pos_pos_trivial left_distrib)
+apply (subgoal_tac "0 \<le> b mod a", arith)
 apply (simp)
 done
 
 
 lemma neg_zmod_mult_2:
-     "a <= (0::int) ==> (1 + 2*b) mod (2*a) = 2 * ((b+1) mod a) - 1"
+     "a \<le> (0::int) ==> (1 + 2*b) mod (2*a) = 2 * ((b+1) mod a) - 1"
 apply (subgoal_tac "(1 + 2* (-b - 1)) mod (2* (-a)) = 
                     1 + 2* ((-b - 1) mod (-a))")
 apply (rule_tac [2] pos_zmod_mult_2)
-apply (auto simp add: zmult_zminus_right)
+apply (auto simp add: zmult_zminus_right right_diff_distrib)
 apply (subgoal_tac " (-1 - (2 * b)) = - (1 + (2 * b))")
  prefer 2 apply simp 
 apply (simp only: zmod_zminus_zminus zdiff_def zminus_zadd_distrib [symmetric])
@@ -944,7 +948,7 @@
 lemma zmod_number_of_BIT [simp]:
      "number_of (v BIT b) mod number_of (w BIT False) =  
           (if b then  
-                if (0::int) <= number_of w  
+                if (0::int) \<le> number_of w  
                 then 2 * (number_of v mod number_of w) + 1     
                 else 2 * ((number_of v + (1::int)) mod number_of w) - 1   
            else 2 * (number_of v mod number_of w))"
@@ -958,16 +962,16 @@
 (** Quotients of signs **)
 
 lemma div_neg_pos_less0: "[| a < (0::int);  0 < b |] ==> a div b < 0"
-apply (subgoal_tac "a div b <= -1", force)
+apply (subgoal_tac "a div b \<le> -1", force)
 apply (rule order_trans)
 apply (rule_tac a' = "-1" in zdiv_mono1)
 apply (auto simp add: zdiv_minus1)
 done
 
-lemma div_nonneg_neg_le0: "[| (0::int) <= a;  b < 0 |] ==> a div b <= 0"
+lemma div_nonneg_neg_le0: "[| (0::int) \<le> a;  b < 0 |] ==> a div b \<le> 0"
 by (drule zdiv_mono1_neg, auto)
 
-lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 <= a div b) = (0 <= a)"
+lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 \<le> a div b) = (0 \<le> a)"
 apply auto
 apply (drule_tac [2] zdiv_mono1)
 apply (auto simp add: linorder_neq_iff)
@@ -976,16 +980,16 @@
 done
 
 lemma neg_imp_zdiv_nonneg_iff:
-     "b < (0::int) ==> (0 <= a div b) = (a <= (0::int))"
+     "b < (0::int) ==> (0 \<le> a div b) = (a \<le> (0::int))"
 apply (subst zdiv_zminus_zminus [symmetric])
 apply (subst pos_imp_zdiv_nonneg_iff, auto)
 done
 
-(*But not (a div b <= 0 iff a<=0); consider a=1, b=2 when a div b = 0.*)
+(*But not (a div b \<le> 0 iff a\<le>0); consider a=1, b=2 when a div b = 0.*)
 lemma pos_imp_zdiv_neg_iff: "(0::int) < b ==> (a div b < 0) = (a < 0)"
 by (simp add: linorder_not_le [symmetric] pos_imp_zdiv_nonneg_iff)
 
-(*Again the law fails for <=: consider a = -1, b = -2 when a div b = 0*)
+(*Again the law fails for \<le>: consider a = -1, b = -2 when a div b = 0*)
 lemma neg_imp_zdiv_neg_iff: "b < (0::int) ==> (a div b < 0) = (0 < a)"
 by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff)
 
@@ -1150,7 +1154,7 @@
    apply (rule_tac [!] x = "-k" in exI, auto)
   done
 
-lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z <= (n::int)"
+lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
   apply (rule_tac z=n in int_cases)
   apply (auto simp add: dvd_int_iff) 
   apply (rule_tac z=z in int_cases)