src/ZF/IntDiv_ZF.thy
changeset 61395 4f8c2c4a0a8c
parent 60770 240563fbf41d
child 61798 27f3c10b0b50
     1.1 --- a/src/ZF/IntDiv_ZF.thy	Sat Oct 10 22:14:44 2015 +0200
     1.2 +++ b/src/ZF/IntDiv_ZF.thy	Sat Oct 10 22:19:06 2015 +0200
     1.3 @@ -37,11 +37,11 @@
     1.4    quorem :: "[i,i] => o"  where
     1.5      "quorem == %<a,b> <q,r>.
     1.6                        a = b$*q $+ r &
     1.7 -                      (#0$<b & #0$<=r & r$<b | ~(#0$<b) & b$<r & r $<= #0)"
     1.8 +                      (#0$<b & #0$\<le>r & r$<b | ~(#0$<b) & b$<r & r $\<le> #0)"
     1.9  
    1.10  definition
    1.11    adjust :: "[i,i] => i"  where
    1.12 -    "adjust(b) == %<q,r>. if #0 $<= r$-b then <#2$*q $+ #1,r$-b>
    1.13 +    "adjust(b) == %<q,r>. if #0 $\<le> r$-b then <#2$*q $+ #1,r$-b>
    1.14                            else <#2$*q,r>"
    1.15  
    1.16  
    1.17 @@ -54,7 +54,7 @@
    1.18      "posDivAlg(ab) ==
    1.19         wfrec(measure(int*int, %<a,b>. nat_of (a $- b $+ #1)),
    1.20               ab,
    1.21 -             %<a,b> f. if (a$<b | b$<=#0) then <#0,a>
    1.22 +             %<a,b> f. if (a$<b | b$\<le>#0) then <#0,a>
    1.23                         else adjust(b, f ` <a,#2$*b>))"
    1.24  
    1.25  
    1.26 @@ -65,7 +65,7 @@
    1.27      "negDivAlg(ab) ==
    1.28         wfrec(measure(int*int, %<a,b>. nat_of ($- a $- b)),
    1.29               ab,
    1.30 -             %<a,b> f. if (#0 $<= a$+b | b$<=#0) then <#-1,a$+b>
    1.31 +             %<a,b> f. if (#0 $\<le> a$+b | b$\<le>#0) then <#-1,a$+b>
    1.32                         else adjust(b, f ` <a,#2$*b>))"
    1.33  
    1.34  (*for the general case @{term"b\<noteq>0"}*)
    1.35 @@ -79,8 +79,8 @@
    1.36  definition
    1.37    divAlg :: "i => i"  where
    1.38      "divAlg ==
    1.39 -       %<a,b>. if #0 $<= a then
    1.40 -                  if #0 $<= b then posDivAlg (<a,b>)
    1.41 +       %<a,b>. if #0 $\<le> a then
    1.42 +                  if #0 $\<le> b then posDivAlg (<a,b>)
    1.43                    else if a=#0 then <#0,#0>
    1.44                         else negateSnd (negDivAlg (<$-a,$-b>))
    1.45                 else
    1.46 @@ -104,7 +104,7 @@
    1.47  apply auto
    1.48  done
    1.49  
    1.50 -lemma zpos_add_zpos_imp_zpos: "[| #0 $<= x;  #0 $<= y |] ==> #0 $<= x $+ y"
    1.51 +lemma zpos_add_zpos_imp_zpos: "[| #0 $\<le> x;  #0 $\<le> y |] ==> #0 $\<le> x $+ y"
    1.52  apply (rule_tac y = "y" in zle_trans)
    1.53  apply (rule_tac [2] zdiff_zle_iff [THEN iffD1])
    1.54  apply auto
    1.55 @@ -118,7 +118,7 @@
    1.56  
    1.57  (* this theorem is used below *)
    1.58  lemma zneg_or_0_add_zneg_or_0_imp_zneg_or_0:
    1.59 -     "[| x $<= #0;  y $<= #0 |] ==> x $+ y $<= #0"
    1.60 +     "[| x $\<le> #0;  y $\<le> #0 |] ==> x $+ y $\<le> #0"
    1.61  apply (rule_tac y = "y" in zle_trans)
    1.62  apply (rule zle_zdiff_iff [THEN iffD1])
    1.63  apply auto
    1.64 @@ -151,32 +151,32 @@
    1.65  done
    1.66  
    1.67  lemma zadd_succ_lemma:
    1.68 -     "z \<in> int ==> (w $+ $# succ(m) $<= z) \<longleftrightarrow> (w $+ $#m $< z)"
    1.69 +     "z \<in> int ==> (w $+ $# succ(m) $\<le> z) \<longleftrightarrow> (w $+ $#m $< z)"
    1.70  apply (simp only: not_zless_iff_zle [THEN iff_sym] zless_add_succ_iff)
    1.71  apply (auto intro: zle_anti_sym elim: zless_asym
    1.72              simp add: zless_imp_zle not_zless_iff_zle)
    1.73  done
    1.74  
    1.75 -lemma zadd_succ_zle_iff: "(w $+ $# succ(m) $<= z) \<longleftrightarrow> (w $+ $#m $< z)"
    1.76 +lemma zadd_succ_zle_iff: "(w $+ $# succ(m) $\<le> z) \<longleftrightarrow> (w $+ $#m $< z)"
    1.77  apply (cut_tac z = "intify (z)" in zadd_succ_lemma)
    1.78  apply auto
    1.79  done
    1.80  
    1.81  (** Inequality reasoning **)
    1.82  
    1.83 -lemma zless_add1_iff_zle: "(w $< z $+ #1) \<longleftrightarrow> (w$<=z)"
    1.84 +lemma zless_add1_iff_zle: "(w $< z $+ #1) \<longleftrightarrow> (w$\<le>z)"
    1.85  apply (subgoal_tac "#1 = $# 1")
    1.86  apply (simp only: zless_add_succ_iff zle_def)
    1.87  apply auto
    1.88  done
    1.89  
    1.90 -lemma add1_zle_iff: "(w $+ #1 $<= z) \<longleftrightarrow> (w $< z)"
    1.91 +lemma add1_zle_iff: "(w $+ #1 $\<le> z) \<longleftrightarrow> (w $< z)"
    1.92  apply (subgoal_tac "#1 = $# 1")
    1.93  apply (simp only: zadd_succ_zle_iff)
    1.94  apply auto
    1.95  done
    1.96  
    1.97 -lemma add1_left_zle_iff: "(#1 $+ w $<= z) \<longleftrightarrow> (w $< z)"
    1.98 +lemma add1_left_zle_iff: "(#1 $+ w $\<le> z) \<longleftrightarrow> (w $< z)"
    1.99  apply (subst zadd_commute)
   1.100  apply (rule add1_zle_iff)
   1.101  done
   1.102 @@ -184,14 +184,14 @@
   1.103  
   1.104  (*** Monotonicity of Multiplication ***)
   1.105  
   1.106 -lemma zmult_mono_lemma: "k \<in> nat ==> i $<= j ==> i $* $#k $<= j $* $#k"
   1.107 +lemma zmult_mono_lemma: "k \<in> nat ==> i $\<le> j ==> i $* $#k $\<le> j $* $#k"
   1.108  apply (induct_tac "k")
   1.109   prefer 2 apply (subst int_succ_int_1)
   1.110  apply (simp_all (no_asm_simp) add: zadd_zmult_distrib2 zadd_zle_mono)
   1.111  done
   1.112  
   1.113 -lemma zmult_zle_mono1: "[| i $<= j;  #0 $<= k |] ==> i$*k $<= j$*k"
   1.114 -apply (subgoal_tac "i $* intify (k) $<= j $* intify (k) ")
   1.115 +lemma zmult_zle_mono1: "[| i $\<le> j;  #0 $\<le> k |] ==> i$*k $\<le> j$*k"
   1.116 +apply (subgoal_tac "i $* intify (k) $\<le> j $* intify (k) ")
   1.117  apply (simp (no_asm_use))
   1.118  apply (rule_tac b = "intify (k)" in not_zneg_mag [THEN subst])
   1.119  apply (rule_tac [3] zmult_mono_lemma)
   1.120 @@ -199,25 +199,25 @@
   1.121  apply (simp add: znegative_iff_zless_0 not_zless_iff_zle [THEN iff_sym])
   1.122  done
   1.123  
   1.124 -lemma zmult_zle_mono1_neg: "[| i $<= j;  k $<= #0 |] ==> j$*k $<= i$*k"
   1.125 +lemma zmult_zle_mono1_neg: "[| i $\<le> j;  k $\<le> #0 |] ==> j$*k $\<le> i$*k"
   1.126  apply (rule zminus_zle_zminus [THEN iffD1])
   1.127  apply (simp del: zmult_zminus_right
   1.128              add: zmult_zminus_right [symmetric] zmult_zle_mono1 zle_zminus)
   1.129  done
   1.130  
   1.131 -lemma zmult_zle_mono2: "[| i $<= j;  #0 $<= k |] ==> k$*i $<= k$*j"
   1.132 +lemma zmult_zle_mono2: "[| i $\<le> j;  #0 $\<le> k |] ==> k$*i $\<le> k$*j"
   1.133  apply (drule zmult_zle_mono1)
   1.134  apply (simp_all add: zmult_commute)
   1.135  done
   1.136  
   1.137 -lemma zmult_zle_mono2_neg: "[| i $<= j;  k $<= #0 |] ==> k$*j $<= k$*i"
   1.138 +lemma zmult_zle_mono2_neg: "[| i $\<le> j;  k $\<le> #0 |] ==> k$*j $\<le> k$*i"
   1.139  apply (drule zmult_zle_mono1_neg)
   1.140  apply (simp_all add: zmult_commute)
   1.141  done
   1.142  
   1.143 -(* $<= monotonicity, BOTH arguments*)
   1.144 +(* $\<le> monotonicity, BOTH arguments*)
   1.145  lemma zmult_zle_mono:
   1.146 -     "[| i $<= j;  k $<= l;  #0 $<= j;  #0 $<= k |] ==> i$*k $<= j$*l"
   1.147 +     "[| i $\<le> j;  k $\<le> l;  #0 $\<le> j;  #0 $\<le> k |] ==> i$*k $\<le> j$*l"
   1.148  apply (erule zmult_zle_mono1 [THEN zle_trans])
   1.149  apply assumption
   1.150  apply (erule zmult_zle_mono2)
   1.151 @@ -320,14 +320,14 @@
   1.152  by (simp add: zmult_commute [of k] zmult_zless_cancel2)
   1.153  
   1.154  lemma zmult_zle_cancel2:
   1.155 -     "(m$*k $<= n$*k) \<longleftrightarrow> ((#0 $< k \<longrightarrow> m$<=n) & (k $< #0 \<longrightarrow> n$<=m))"
   1.156 +     "(m$*k $\<le> n$*k) \<longleftrightarrow> ((#0 $< k \<longrightarrow> m$\<le>n) & (k $< #0 \<longrightarrow> n$\<le>m))"
   1.157  by (auto simp add: not_zless_iff_zle [THEN iff_sym] zmult_zless_cancel2)
   1.158  
   1.159  lemma zmult_zle_cancel1:
   1.160 -     "(k$*m $<= k$*n) \<longleftrightarrow> ((#0 $< k \<longrightarrow> m$<=n) & (k $< #0 \<longrightarrow> n$<=m))"
   1.161 +     "(k$*m $\<le> k$*n) \<longleftrightarrow> ((#0 $< k \<longrightarrow> m$\<le>n) & (k $< #0 \<longrightarrow> n$\<le>m))"
   1.162  by (auto simp add: not_zless_iff_zle [THEN iff_sym] zmult_zless_cancel1)
   1.163  
   1.164 -lemma int_eq_iff_zle: "[| m \<in> int; n \<in> int |] ==> m=n \<longleftrightarrow> (m $<= n & n $<= m)"
   1.165 +lemma int_eq_iff_zle: "[| m \<in> int; n \<in> int |] ==> m=n \<longleftrightarrow> (m $\<le> n & n $\<le> m)"
   1.166  apply (blast intro: zle_refl zle_anti_sym)
   1.167  done
   1.168  
   1.169 @@ -352,9 +352,9 @@
   1.170  subsection\<open>Uniqueness and monotonicity of quotients and remainders\<close>
   1.171  
   1.172  lemma unique_quotient_lemma:
   1.173 -     "[| b$*q' $+ r' $<= b$*q $+ r;  #0 $<= r';  #0 $< b;  r $< b |]
   1.174 -      ==> q' $<= q"
   1.175 -apply (subgoal_tac "r' $+ b $* (q'$-q) $<= r")
   1.176 +     "[| b$*q' $+ r' $\<le> b$*q $+ r;  #0 $\<le> r';  #0 $< b;  r $< b |]
   1.177 +      ==> q' $\<le> q"
   1.178 +apply (subgoal_tac "r' $+ b $* (q'$-q) $\<le> r")
   1.179   prefer 2 apply (simp add: zdiff_zmult_distrib2 zadd_ac zcompare_rls)
   1.180  apply (subgoal_tac "#0 $< b $* (#1 $+ q $- q') ")
   1.181   prefer 2
   1.182 @@ -370,8 +370,8 @@
   1.183  done
   1.184  
   1.185  lemma unique_quotient_lemma_neg:
   1.186 -     "[| b$*q' $+ r' $<= b$*q $+ r;  r $<= #0;  b $< #0;  b $< r' |]
   1.187 -      ==> q $<= q'"
   1.188 +     "[| b$*q' $+ r' $\<le> b$*q $+ r;  r $\<le> #0;  b $< #0;  b $< r' |]
   1.189 +      ==> q $\<le> q'"
   1.190  apply (rule_tac b = "$-b" and r = "$-r'" and r' = "$-r"
   1.191         in unique_quotient_lemma)
   1.192  apply (auto simp del: zminus_zadd_distrib
   1.193 @@ -405,14 +405,14 @@
   1.194  
   1.195  lemma adjust_eq [simp]:
   1.196       "adjust(b, <q,r>) = (let diff = r$-b in
   1.197 -                          if #0 $<= diff then <#2$*q $+ #1,diff>
   1.198 +                          if #0 $\<le> diff then <#2$*q $+ #1,diff>
   1.199                                           else <#2$*q,r>)"
   1.200  by (simp add: Let_def adjust_def)
   1.201  
   1.202  
   1.203  lemma posDivAlg_termination:
   1.204       "[| #0 $< b; ~ a $< b |]
   1.205 -      ==> nat_of(a $- #2 $\<times> b $+ #1) < nat_of(a $- b $+ #1)"
   1.206 +      ==> nat_of(a $- #2 $* b $+ #1) < nat_of(a $- b $+ #1)"
   1.207  apply (simp (no_asm) add: zless_nat_conj)
   1.208  apply (simp add: not_zless_iff_zle zless_add1_iff_zle zcompare_rls)
   1.209  done
   1.210 @@ -431,7 +431,7 @@
   1.211  lemma posDivAlg_induct_lemma [rule_format]:
   1.212    assumes prem:
   1.213          "!!a b. [| a \<in> int; b \<in> int;
   1.214 -                   ~ (a $< b | b $<= #0) \<longrightarrow> P(<a, #2 $* b>) |] ==> P(<a,b>)"
   1.215 +                   ~ (a $< b | b $\<le> #0) \<longrightarrow> P(<a, #2 $* b>) |] ==> P(<a,b>)"
   1.216    shows "<u,v> \<in> int*int \<Longrightarrow> P(<u,v>)"
   1.217  using wf_measure [where A = "int*int" and f = "%<a,b>.nat_of (a $- b $+ #1)"]
   1.218  proof (induct "<u,v>" arbitrary: u v rule: wf_induct)
   1.219 @@ -450,7 +450,7 @@
   1.220    assumes u_int: "u \<in> int"
   1.221        and v_int: "v \<in> int"
   1.222        and ih: "!!a b. [| a \<in> int; b \<in> int;
   1.223 -                     ~ (a $< b | b $<= #0) \<longrightarrow> P(a, #2 $* b) |] ==> P(a,b)"
   1.224 +                     ~ (a $< b | b $\<le> #0) \<longrightarrow> P(a, #2 $* b) |] ==> P(a,b)"
   1.225    shows "P(u,v)"
   1.226  apply (subgoal_tac "(%<x,y>. P (x,y)) (<u,v>)")
   1.227  apply simp
   1.228 @@ -462,7 +462,7 @@
   1.229  
   1.230  (*FIXME: use intify in integ_of so that we always have @{term"integ_of w \<in> int"}.
   1.231      then this rewrite can work for all constants!!*)
   1.232 -lemma intify_eq_0_iff_zle: "intify(m) = #0 \<longleftrightarrow> (m $<= #0 & #0 $<= m)"
   1.233 +lemma intify_eq_0_iff_zle: "intify(m) = #0 \<longleftrightarrow> (m $\<le> #0 & #0 $\<le> m)"
   1.234    by (simp add: int_eq_iff_zle)
   1.235  
   1.236  
   1.237 @@ -503,11 +503,11 @@
   1.238  
   1.239  lemma int_0_le_lemma:
   1.240       "[| x \<in> int; y \<in> int |]
   1.241 -      ==> (#0 $<= x $* y) \<longleftrightarrow> (#0 $<= x & #0 $<= y | x $<= #0 & y $<= #0)"
   1.242 +      ==> (#0 $\<le> x $* y) \<longleftrightarrow> (#0 $\<le> x & #0 $\<le> y | x $\<le> #0 & y $\<le> #0)"
   1.243  by (auto simp add: zle_def not_zless_iff_zle int_0_less_mult_iff)
   1.244  
   1.245  lemma int_0_le_mult_iff:
   1.246 -     "(#0 $<= x $* y) \<longleftrightarrow> ((#0 $<= x & #0 $<= y) | (x $<= #0 & y $<= #0))"
   1.247 +     "(#0 $\<le> x $* y) \<longleftrightarrow> ((#0 $\<le> x & #0 $\<le> y) | (x $\<le> #0 & y $\<le> #0))"
   1.248  apply (cut_tac x = "intify (x)" and y = "intify (y)" in int_0_le_lemma)
   1.249  apply auto
   1.250  done
   1.251 @@ -519,7 +519,7 @@
   1.252  done
   1.253  
   1.254  lemma zmult_le_0_iff:
   1.255 -     "(x $* y $<= #0) \<longleftrightarrow> (#0 $<= x & y $<= #0 | x $<= #0 & #0 $<= y)"
   1.256 +     "(x $* y $\<le> #0) \<longleftrightarrow> (#0 $\<le> x & y $\<le> #0 | x $\<le> #0 & #0 $\<le> y)"
   1.257  by (auto dest: zless_not_sym
   1.258           simp add: int_0_less_mult_iff not_zless_iff_zle [THEN iff_sym])
   1.259  
   1.260 @@ -542,7 +542,7 @@
   1.261  (*Correctness of posDivAlg: it computes quotients correctly*)
   1.262  lemma posDivAlg_correct [rule_format]:
   1.263       "[| a \<in> int; b \<in> int |]
   1.264 -      ==> #0 $<= a \<longrightarrow> #0 $< b \<longrightarrow> quorem (<a,b>, posDivAlg(<a,b>))"
   1.265 +      ==> #0 $\<le> a \<longrightarrow> #0 $< b \<longrightarrow> quorem (<a,b>, posDivAlg(<a,b>))"
   1.266  apply (rule_tac u = "a" and v = "b" in posDivAlg_induct)
   1.267  apply auto
   1.268     apply (simp_all add: quorem_def)
   1.269 @@ -577,7 +577,7 @@
   1.270  lemma negDivAlg_eqn:
   1.271       "[| #0 $< b; a \<in> int; b \<in> int |] ==>
   1.272        negDivAlg(<a,b>) =
   1.273 -       (if #0 $<= a$+b then <#-1,a$+b>
   1.274 +       (if #0 $\<le> a$+b then <#-1,a$+b>
   1.275                         else adjust(b, negDivAlg (<a, #2$*b>)))"
   1.276  apply (rule negDivAlg_unfold [THEN trans])
   1.277  apply (simp (no_asm_simp) add: vimage_iff not_zless_iff_zle [THEN iff_sym])
   1.278 @@ -587,7 +587,7 @@
   1.279  lemma negDivAlg_induct_lemma [rule_format]:
   1.280    assumes prem:
   1.281          "!!a b. [| a \<in> int; b \<in> int;
   1.282 -                   ~ (#0 $<= a $+ b | b $<= #0) \<longrightarrow> P(<a, #2 $* b>) |]
   1.283 +                   ~ (#0 $\<le> a $+ b | b $\<le> #0) \<longrightarrow> P(<a, #2 $* b>) |]
   1.284                  ==> P(<a,b>)"
   1.285    shows "<u,v> \<in> int*int \<Longrightarrow> P(<u,v>)"
   1.286  using wf_measure [where A = "int*int" and f = "%<a,b>.nat_of ($- a $- b)"]
   1.287 @@ -606,7 +606,7 @@
   1.288    assumes u_int: "u \<in> int"
   1.289        and v_int: "v \<in> int"
   1.290        and ih: "!!a b. [| a \<in> int; b \<in> int;
   1.291 -                         ~ (#0 $<= a $+ b | b $<= #0) \<longrightarrow> P(a, #2 $* b) |]
   1.292 +                         ~ (#0 $\<le> a $+ b | b $\<le> #0) \<longrightarrow> P(a, #2 $* b) |]
   1.293                        ==> P(a,b)"
   1.294    shows "P(u,v)"
   1.295  apply (subgoal_tac " (%<x,y>. P (x,y)) (<u,v>)")
   1.296 @@ -642,7 +642,7 @@
   1.297  apply (rule_tac u = "a" and v = "b" in negDivAlg_induct)
   1.298    apply auto
   1.299     apply (simp_all add: quorem_def)
   1.300 -   txt\<open>base case: @{term "0$<=a$+b"}\<close>
   1.301 +   txt\<open>base case: @{term "0$\<le>a$+b"}\<close>
   1.302     apply (simp add: negDivAlg_eqn)
   1.303    apply (simp add: not_zless_iff_zle [THEN iff_sym])
   1.304   apply (simp add: int_0_less_mult_iff)
   1.305 @@ -676,7 +676,7 @@
   1.306  
   1.307  
   1.308  (*Needed below.  Actually it's an equivalence.*)
   1.309 -lemma linear_arith_lemma: "~ (#0 $<= #-1 $+ b) ==> (b $<= #0)"
   1.310 +lemma linear_arith_lemma: "~ (#0 $\<le> #-1 $+ b) ==> (b $\<le> #0)"
   1.311  apply (simp add: not_zle_iff_zless)
   1.312  apply (drule zminus_zless_zminus [THEN iffD2])
   1.313  apply (simp add: zadd_commute zless_add1_iff_zle zle_zminus)
   1.314 @@ -778,7 +778,7 @@
   1.315  apply auto
   1.316  done
   1.317  
   1.318 -lemma pos_mod: "#0 $< b ==> #0 $<= a zmod b & a zmod b $< b"
   1.319 +lemma pos_mod: "#0 $< b ==> #0 $\<le> a zmod b & a zmod b $< b"
   1.320  apply (cut_tac a = "intify (a)" and b = "intify (b)" in divAlg_correct)
   1.321  apply (auto simp add: intify_eq_0_iff_zle quorem_def zmod_def split_def)
   1.322  apply (blast dest: zle_zless_trans)+
   1.323 @@ -787,7 +787,7 @@
   1.324  lemmas pos_mod_sign = pos_mod [THEN conjunct1]
   1.325    and pos_mod_bound = pos_mod [THEN conjunct2]
   1.326  
   1.327 -lemma neg_mod: "b $< #0 ==> a zmod b $<= #0 & b $< a zmod b"
   1.328 +lemma neg_mod: "b $< #0 ==> a zmod b $\<le> #0 & b $< a zmod b"
   1.329  apply (cut_tac a = "intify (a)" and b = "intify (b)" in divAlg_correct)
   1.330  apply (auto simp add: intify_eq_0_iff_zle quorem_def zmod_def split_def)
   1.331  apply (blast dest: zle_zless_trans)
   1.332 @@ -820,48 +820,48 @@
   1.333  by (blast intro: quorem_div_mod [THEN unique_remainder])
   1.334  
   1.335  lemma zdiv_pos_pos_trivial_raw:
   1.336 -     "[| a \<in> int;  b \<in> int;  #0 $<= a;  a $< b |] ==> a zdiv b = #0"
   1.337 +     "[| a \<in> int;  b \<in> int;  #0 $\<le> a;  a $< b |] ==> a zdiv b = #0"
   1.338  apply (rule quorem_div)
   1.339  apply (auto simp add: quorem_def)
   1.340  (*linear arithmetic*)
   1.341  apply (blast dest: zle_zless_trans)+
   1.342  done
   1.343  
   1.344 -lemma zdiv_pos_pos_trivial: "[| #0 $<= a;  a $< b |] ==> a zdiv b = #0"
   1.345 +lemma zdiv_pos_pos_trivial: "[| #0 $\<le> a;  a $< b |] ==> a zdiv b = #0"
   1.346  apply (cut_tac a = "intify (a)" and b = "intify (b)"
   1.347         in zdiv_pos_pos_trivial_raw)
   1.348  apply auto
   1.349  done
   1.350  
   1.351  lemma zdiv_neg_neg_trivial_raw:
   1.352 -     "[| a \<in> int;  b \<in> int;  a $<= #0;  b $< a |] ==> a zdiv b = #0"
   1.353 +     "[| a \<in> int;  b \<in> int;  a $\<le> #0;  b $< a |] ==> a zdiv b = #0"
   1.354  apply (rule_tac r = "a" in quorem_div)
   1.355  apply (auto simp add: quorem_def)
   1.356  (*linear arithmetic*)
   1.357  apply (blast dest: zle_zless_trans zless_trans)+
   1.358  done
   1.359  
   1.360 -lemma zdiv_neg_neg_trivial: "[| a $<= #0;  b $< a |] ==> a zdiv b = #0"
   1.361 +lemma zdiv_neg_neg_trivial: "[| a $\<le> #0;  b $< a |] ==> a zdiv b = #0"
   1.362  apply (cut_tac a = "intify (a)" and b = "intify (b)"
   1.363         in zdiv_neg_neg_trivial_raw)
   1.364  apply auto
   1.365  done
   1.366  
   1.367 -lemma zadd_le_0_lemma: "[| a$+b $<= #0;  #0 $< a;  #0 $< b |] ==> False"
   1.368 +lemma zadd_le_0_lemma: "[| a$+b $\<le> #0;  #0 $< a;  #0 $< b |] ==> False"
   1.369  apply (drule_tac z' = "#0" and z = "b" in zadd_zless_mono)
   1.370  apply (auto simp add: zle_def)
   1.371  apply (blast dest: zless_trans)
   1.372  done
   1.373  
   1.374  lemma zdiv_pos_neg_trivial_raw:
   1.375 -     "[| a \<in> int;  b \<in> int;  #0 $< a;  a$+b $<= #0 |] ==> a zdiv b = #-1"
   1.376 +     "[| a \<in> int;  b \<in> int;  #0 $< a;  a$+b $\<le> #0 |] ==> a zdiv b = #-1"
   1.377  apply (rule_tac r = "a $+ b" in quorem_div)
   1.378  apply (auto simp add: quorem_def)
   1.379  (*linear arithmetic*)
   1.380  apply (blast dest: zadd_le_0_lemma zle_zless_trans)+
   1.381  done
   1.382  
   1.383 -lemma zdiv_pos_neg_trivial: "[| #0 $< a;  a$+b $<= #0 |] ==> a zdiv b = #-1"
   1.384 +lemma zdiv_pos_neg_trivial: "[| #0 $< a;  a$+b $\<le> #0 |] ==> a zdiv b = #-1"
   1.385  apply (cut_tac a = "intify (a)" and b = "intify (b)"
   1.386         in zdiv_pos_neg_trivial_raw)
   1.387  apply auto
   1.388 @@ -871,42 +871,42 @@
   1.389  
   1.390  
   1.391  lemma zmod_pos_pos_trivial_raw:
   1.392 -     "[| a \<in> int;  b \<in> int;  #0 $<= a;  a $< b |] ==> a zmod b = a"
   1.393 +     "[| a \<in> int;  b \<in> int;  #0 $\<le> a;  a $< b |] ==> a zmod b = a"
   1.394  apply (rule_tac q = "#0" in quorem_mod)
   1.395  apply (auto simp add: quorem_def)
   1.396  (*linear arithmetic*)
   1.397  apply (blast dest: zle_zless_trans)+
   1.398  done
   1.399  
   1.400 -lemma zmod_pos_pos_trivial: "[| #0 $<= a;  a $< b |] ==> a zmod b = intify(a)"
   1.401 +lemma zmod_pos_pos_trivial: "[| #0 $\<le> a;  a $< b |] ==> a zmod b = intify(a)"
   1.402  apply (cut_tac a = "intify (a)" and b = "intify (b)"
   1.403         in zmod_pos_pos_trivial_raw)
   1.404  apply auto
   1.405  done
   1.406  
   1.407  lemma zmod_neg_neg_trivial_raw:
   1.408 -     "[| a \<in> int;  b \<in> int;  a $<= #0;  b $< a |] ==> a zmod b = a"
   1.409 +     "[| a \<in> int;  b \<in> int;  a $\<le> #0;  b $< a |] ==> a zmod b = a"
   1.410  apply (rule_tac q = "#0" in quorem_mod)
   1.411  apply (auto simp add: quorem_def)
   1.412  (*linear arithmetic*)
   1.413  apply (blast dest: zle_zless_trans zless_trans)+
   1.414  done
   1.415  
   1.416 -lemma zmod_neg_neg_trivial: "[| a $<= #0;  b $< a |] ==> a zmod b = intify(a)"
   1.417 +lemma zmod_neg_neg_trivial: "[| a $\<le> #0;  b $< a |] ==> a zmod b = intify(a)"
   1.418  apply (cut_tac a = "intify (a)" and b = "intify (b)"
   1.419         in zmod_neg_neg_trivial_raw)
   1.420  apply auto
   1.421  done
   1.422  
   1.423  lemma zmod_pos_neg_trivial_raw:
   1.424 -     "[| a \<in> int;  b \<in> int;  #0 $< a;  a$+b $<= #0 |] ==> a zmod b = a$+b"
   1.425 +     "[| a \<in> int;  b \<in> int;  #0 $< a;  a$+b $\<le> #0 |] ==> a zmod b = a$+b"
   1.426  apply (rule_tac q = "#-1" in quorem_mod)
   1.427  apply (auto simp add: quorem_def)
   1.428  (*linear arithmetic*)
   1.429  apply (blast dest: zadd_le_0_lemma zle_zless_trans)+
   1.430  done
   1.431  
   1.432 -lemma zmod_pos_neg_trivial: "[| #0 $< a;  a$+b $<= #0 |] ==> a zmod b = a$+b"
   1.433 +lemma zmod_pos_neg_trivial: "[| #0 $< a;  a$+b $\<le> #0 |] ==> a zmod b = a$+b"
   1.434  apply (cut_tac a = "intify (a)" and b = "intify (b)"
   1.435         in zmod_pos_neg_trivial_raw)
   1.436  apply auto
   1.437 @@ -947,7 +947,7 @@
   1.438  
   1.439  subsection\<open>division of a number by itself\<close>
   1.440  
   1.441 -lemma self_quotient_aux1: "[| #0 $< a; a = r $+ a$*q; r $< a |] ==> #1 $<= q"
   1.442 +lemma self_quotient_aux1: "[| #0 $< a; a = r $+ a$*q; r $< a |] ==> #1 $\<le> q"
   1.443  apply (subgoal_tac "#0 $< a$*q")
   1.444  apply (cut_tac w = "#0" and z = "q" in add1_zle_iff)
   1.445  apply (simp add: int_0_less_mult_iff)
   1.446 @@ -958,8 +958,8 @@
   1.447  apply (simp add: zcompare_rls)
   1.448  done
   1.449  
   1.450 -lemma self_quotient_aux2: "[| #0 $< a; a = r $+ a$*q; #0 $<= r |] ==> q $<= #1"
   1.451 -apply (subgoal_tac "#0 $<= a$* (#1$-q)")
   1.452 +lemma self_quotient_aux2: "[| #0 $< a; a = r $+ a$*q; #0 $\<le> r |] ==> q $\<le> #1"
   1.453 +apply (subgoal_tac "#0 $\<le> a$* (#1$-q)")
   1.454   apply (simp add: int_0_le_mult_iff zcompare_rls)
   1.455   apply (blast dest: zle_zless_trans)
   1.456  apply (simp add: zdiff_zmult_distrib2)
   1.457 @@ -1030,14 +1030,14 @@
   1.458  
   1.459  (** a positive, b positive **)
   1.460  
   1.461 -lemma zdiv_pos_pos: "[| #0 $< a;  #0 $<= b |]
   1.462 +lemma zdiv_pos_pos: "[| #0 $< a;  #0 $\<le> b |]
   1.463        ==> a zdiv b = fst (posDivAlg(<intify(a), intify(b)>))"
   1.464  apply (simp (no_asm_simp) add: zdiv_def divAlg_def)
   1.465  apply (auto simp add: zle_def)
   1.466  done
   1.467  
   1.468  lemma zmod_pos_pos:
   1.469 -     "[| #0 $< a;  #0 $<= b |]
   1.470 +     "[| #0 $< a;  #0 $\<le> b |]
   1.471        ==> a zmod b = snd (posDivAlg(<intify(a), intify(b)>))"
   1.472  apply (simp (no_asm_simp) add: zmod_def divAlg_def)
   1.473  apply (auto simp add: zle_def)
   1.474 @@ -1084,7 +1084,7 @@
   1.475  (** a negative, b negative **)
   1.476  
   1.477  lemma zdiv_neg_neg:
   1.478 -     "[| a $< #0;  b $<= #0 |]
   1.479 +     "[| a $< #0;  b $\<le> #0 |]
   1.480        ==> a zdiv b = fst (negateSnd(posDivAlg(<$-a, $-b>)))"
   1.481  apply (simp (no_asm_simp) add: zdiv_def divAlg_def)
   1.482  apply auto
   1.483 @@ -1092,7 +1092,7 @@
   1.484  done
   1.485  
   1.486  lemma zmod_neg_neg:
   1.487 -     "[| a $< #0;  b $<= #0 |]
   1.488 +     "[| a $< #0;  b $\<le> #0 |]
   1.489        ==> a zmod b = snd (negateSnd(posDivAlg(<$-a, $-b>)))"
   1.490  apply (simp (no_asm_simp) add: zmod_def divAlg_def)
   1.491  apply auto
   1.492 @@ -1154,7 +1154,7 @@
   1.493  
   1.494  subsection\<open>Monotonicity in the first argument (divisor)\<close>
   1.495  
   1.496 -lemma zdiv_mono1: "[| a $<= a';  #0 $< b |] ==> a zdiv b $<= a' zdiv b"
   1.497 +lemma zdiv_mono1: "[| a $\<le> a';  #0 $< b |] ==> a zdiv b $\<le> a' zdiv b"
   1.498  apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality)
   1.499  apply (cut_tac a = "a'" and b = "b" in zmod_zdiv_equality)
   1.500  apply (rule unique_quotient_lemma)
   1.501 @@ -1163,7 +1163,7 @@
   1.502  apply (simp_all (no_asm_simp) add: pos_mod_sign pos_mod_bound)
   1.503  done
   1.504  
   1.505 -lemma zdiv_mono1_neg: "[| a $<= a';  b $< #0 |] ==> a' zdiv b $<= a zdiv b"
   1.506 +lemma zdiv_mono1_neg: "[| a $\<le> a';  b $< #0 |] ==> a' zdiv b $\<le> a zdiv b"
   1.507  apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality)
   1.508  apply (cut_tac a = "a'" and b = "b" in zmod_zdiv_equality)
   1.509  apply (rule unique_quotient_lemma_neg)
   1.510 @@ -1176,7 +1176,7 @@
   1.511  subsection\<open>Monotonicity in the second argument (dividend)\<close>
   1.512  
   1.513  lemma q_pos_lemma:
   1.514 -     "[| #0 $<= b'$*q' $+ r'; r' $< b';  #0 $< b' |] ==> #0 $<= q'"
   1.515 +     "[| #0 $\<le> b'$*q' $+ r'; r' $< b';  #0 $< b' |] ==> #0 $\<le> q'"
   1.516  apply (subgoal_tac "#0 $< b'$* (q' $+ #1)")
   1.517   apply (simp add: int_0_less_mult_iff)
   1.518   apply (blast dest: zless_trans intro: zless_add1_iff_zle [THEN iffD1])
   1.519 @@ -1186,9 +1186,9 @@
   1.520  done
   1.521  
   1.522  lemma zdiv_mono2_lemma:
   1.523 -     "[| b$*q $+ r = b'$*q' $+ r';  #0 $<= b'$*q' $+ r';
   1.524 -         r' $< b';  #0 $<= r;  #0 $< b';  b' $<= b |]
   1.525 -      ==> q $<= q'"
   1.526 +     "[| b$*q $+ r = b'$*q' $+ r';  #0 $\<le> b'$*q' $+ r';
   1.527 +         r' $< b';  #0 $\<le> r;  #0 $< b';  b' $\<le> b |]
   1.528 +      ==> q $\<le> q'"
   1.529  apply (frule q_pos_lemma, assumption+)
   1.530  apply (subgoal_tac "b$*q $< b$* (q' $+ #1)")
   1.531   apply (simp add: zmult_zless_cancel1)
   1.532 @@ -1196,7 +1196,7 @@
   1.533  apply (subgoal_tac "b$*q = r' $- r $+ b'$*q'")
   1.534   prefer 2 apply (simp add: zcompare_rls)
   1.535  apply (simp (no_asm_simp) add: zadd_zmult_distrib2)
   1.536 -apply (subst zadd_commute [of "b $\<times> q'"], rule zadd_zless_mono)
   1.537 +apply (subst zadd_commute [of "b $* q'"], rule zadd_zless_mono)
   1.538   prefer 2 apply (blast intro: zmult_zle_mono1)
   1.539  apply (subgoal_tac "r' $+ #0 $< b $+ r")
   1.540   apply (simp add: zcompare_rls)
   1.541 @@ -1207,8 +1207,8 @@
   1.542  
   1.543  
   1.544  lemma zdiv_mono2_raw:
   1.545 -     "[| #0 $<= a;  #0 $< b';  b' $<= b;  a \<in> int |]
   1.546 -      ==> a zdiv b $<= a zdiv b'"
   1.547 +     "[| #0 $\<le> a;  #0 $< b';  b' $\<le> b;  a \<in> int |]
   1.548 +      ==> a zdiv b $\<le> a zdiv b'"
   1.549  apply (subgoal_tac "#0 $< b")
   1.550   prefer 2 apply (blast dest: zless_zle_trans)
   1.551  apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality)
   1.552 @@ -1220,14 +1220,14 @@
   1.553  done
   1.554  
   1.555  lemma zdiv_mono2:
   1.556 -     "[| #0 $<= a;  #0 $< b';  b' $<= b |]
   1.557 -      ==> a zdiv b $<= a zdiv b'"
   1.558 +     "[| #0 $\<le> a;  #0 $< b';  b' $\<le> b |]
   1.559 +      ==> a zdiv b $\<le> a zdiv b'"
   1.560  apply (cut_tac a = "intify (a)" in zdiv_mono2_raw)
   1.561  apply auto
   1.562  done
   1.563  
   1.564  lemma q_neg_lemma:
   1.565 -     "[| b'$*q' $+ r' $< #0;  #0 $<= r';  #0 $< b' |] ==> q' $< #0"
   1.566 +     "[| b'$*q' $+ r' $< #0;  #0 $\<le> r';  #0 $< b' |] ==> q' $< #0"
   1.567  apply (subgoal_tac "b'$*q' $< #0")
   1.568   prefer 2 apply (force intro: zle_zless_trans)
   1.569  apply (simp add: zmult_less_0_iff)
   1.570 @@ -1238,8 +1238,8 @@
   1.571  
   1.572  lemma zdiv_mono2_neg_lemma:
   1.573       "[| b$*q $+ r = b'$*q' $+ r';  b'$*q' $+ r' $< #0;
   1.574 -         r $< b;  #0 $<= r';  #0 $< b';  b' $<= b |]
   1.575 -      ==> q' $<= q"
   1.576 +         r $< b;  #0 $\<le> r';  #0 $< b';  b' $\<le> b |]
   1.577 +      ==> q' $\<le> q"
   1.578  apply (subgoal_tac "#0 $< b")
   1.579   prefer 2 apply (blast dest: zless_zle_trans)
   1.580  apply (frule q_neg_lemma, assumption+)
   1.581 @@ -1247,7 +1247,7 @@
   1.582   apply (simp add: zmult_zless_cancel1)
   1.583   apply (blast dest: zless_trans zless_add1_iff_zle [THEN iffD1])
   1.584  apply (simp (no_asm_simp) add: zadd_zmult_distrib2)
   1.585 -apply (subgoal_tac "b$*q' $<= b'$*q'")
   1.586 +apply (subgoal_tac "b$*q' $\<le> b'$*q'")
   1.587   prefer 2
   1.588   apply (simp add: zmult_zle_cancel2)
   1.589   apply (blast dest: zless_trans)
   1.590 @@ -1266,8 +1266,8 @@
   1.591  done
   1.592  
   1.593  lemma zdiv_mono2_neg_raw:
   1.594 -     "[| a $< #0;  #0 $< b';  b' $<= b;  a \<in> int |]
   1.595 -      ==> a zdiv b' $<= a zdiv b"
   1.596 +     "[| a $< #0;  #0 $< b';  b' $\<le> b;  a \<in> int |]
   1.597 +      ==> a zdiv b' $\<le> a zdiv b"
   1.598  apply (subgoal_tac "#0 $< b")
   1.599   prefer 2 apply (blast dest: zless_zle_trans)
   1.600  apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality)
   1.601 @@ -1278,8 +1278,8 @@
   1.602  apply (simp_all add: pos_mod_sign pos_mod_bound)
   1.603  done
   1.604  
   1.605 -lemma zdiv_mono2_neg: "[| a $< #0;  #0 $< b';  b' $<= b |]
   1.606 -      ==> a zdiv b' $<= a zdiv b"
   1.607 +lemma zdiv_mono2_neg: "[| a $< #0;  #0 $< b';  b' $\<le> b |]
   1.608 +      ==> a zdiv b' $\<le> a zdiv b"
   1.609  apply (cut_tac a = "intify (a)" in zdiv_mono2_neg_raw)
   1.610  apply auto
   1.611  done
   1.612 @@ -1465,7 +1465,7 @@
   1.613  (** first, four lemmas to bound the remainder for the cases b<0 and b>0 **)
   1.614  
   1.615  lemma zdiv_zmult2_aux1:
   1.616 -     "[| #0 $< c;  b $< r;  r $<= #0 |] ==> b$*c $< b$*(q zmod c) $+ r"
   1.617 +     "[| #0 $< c;  b $< r;  r $\<le> #0 |] ==> b$*c $< b$*(q zmod c) $+ r"
   1.618  apply (subgoal_tac "b $* (c $- q zmod c) $< r $* #1")
   1.619  apply (simp add: zdiff_zmult_distrib2 zadd_commute zcompare_rls)
   1.620  apply (rule zle_zless_trans)
   1.621 @@ -1476,8 +1476,8 @@
   1.622  done
   1.623  
   1.624  lemma zdiv_zmult2_aux2:
   1.625 -     "[| #0 $< c;   b $< r;  r $<= #0 |] ==> b $* (q zmod c) $+ r $<= #0"
   1.626 -apply (subgoal_tac "b $* (q zmod c) $<= #0")
   1.627 +     "[| #0 $< c;   b $< r;  r $\<le> #0 |] ==> b $* (q zmod c) $+ r $\<le> #0"
   1.628 +apply (subgoal_tac "b $* (q zmod c) $\<le> #0")
   1.629   prefer 2
   1.630   apply (simp add: zmult_le_0_iff pos_mod_sign)
   1.631   apply (blast intro: zless_imp_zle dest: zless_zle_trans)
   1.632 @@ -1488,8 +1488,8 @@
   1.633  done
   1.634  
   1.635  lemma zdiv_zmult2_aux3:
   1.636 -     "[| #0 $< c;  #0 $<= r;  r $< b |] ==> #0 $<= b $* (q zmod c) $+ r"
   1.637 -apply (subgoal_tac "#0 $<= b $* (q zmod c)")
   1.638 +     "[| #0 $< c;  #0 $\<le> r;  r $< b |] ==> #0 $\<le> b $* (q zmod c) $+ r"
   1.639 +apply (subgoal_tac "#0 $\<le> b $* (q zmod c)")
   1.640   prefer 2
   1.641   apply (simp add: int_0_le_mult_iff pos_mod_sign)
   1.642   apply (blast intro: zless_imp_zle dest: zle_zless_trans)
   1.643 @@ -1500,7 +1500,7 @@
   1.644  done
   1.645  
   1.646  lemma zdiv_zmult2_aux4:
   1.647 -     "[| #0 $< c; #0 $<= r; r $< b |] ==> b $* (q zmod c) $+ r $< b $* c"
   1.648 +     "[| #0 $< c; #0 $\<le> r; r $< b |] ==> b $* (q zmod c) $+ r $< b $* c"
   1.649  apply (subgoal_tac "r $* #1 $< b $* (c $- q zmod c)")
   1.650  apply (simp add: zdiff_zmult_distrib2 zadd_commute zcompare_rls)
   1.651  apply (rule zless_zle_trans)
   1.652 @@ -1625,7 +1625,7 @@
   1.653  (** Quotients of signs **)
   1.654  
   1.655  lemma zdiv_neg_pos_less0: "[| a $< #0;  #0 $< b |] ==> a zdiv b $< #0"
   1.656 -apply (subgoal_tac "a zdiv b $<= #-1")
   1.657 +apply (subgoal_tac "a zdiv b $\<le> #-1")
   1.658  apply (erule zle_zless_trans)
   1.659  apply (simp (no_asm))
   1.660  apply (rule zle_trans)
   1.661 @@ -1635,12 +1635,12 @@
   1.662  apply (auto simp add: zdiv_minus1)
   1.663  done
   1.664  
   1.665 -lemma zdiv_nonneg_neg_le0: "[| #0 $<= a;  b $< #0 |] ==> a zdiv b $<= #0"
   1.666 +lemma zdiv_nonneg_neg_le0: "[| #0 $\<le> a;  b $< #0 |] ==> a zdiv b $\<le> #0"
   1.667  apply (drule zdiv_mono1_neg)
   1.668  apply auto
   1.669  done
   1.670  
   1.671 -lemma pos_imp_zdiv_nonneg_iff: "#0 $< b ==> (#0 $<= a zdiv b) \<longleftrightarrow> (#0 $<= a)"
   1.672 +lemma pos_imp_zdiv_nonneg_iff: "#0 $< b ==> (#0 $\<le> a zdiv b) \<longleftrightarrow> (#0 $\<le> a)"
   1.673  apply auto
   1.674  apply (drule_tac [2] zdiv_mono1)
   1.675  apply (auto simp add: neq_iff_zless)
   1.676 @@ -1648,20 +1648,20 @@
   1.677  apply (blast intro: zdiv_neg_pos_less0)
   1.678  done
   1.679  
   1.680 -lemma neg_imp_zdiv_nonneg_iff: "b $< #0 ==> (#0 $<= a zdiv b) \<longleftrightarrow> (a $<= #0)"
   1.681 +lemma neg_imp_zdiv_nonneg_iff: "b $< #0 ==> (#0 $\<le> a zdiv b) \<longleftrightarrow> (a $\<le> #0)"
   1.682  apply (subst zdiv_zminus_zminus [symmetric])
   1.683  apply (rule iff_trans)
   1.684  apply (rule pos_imp_zdiv_nonneg_iff)
   1.685  apply auto
   1.686  done
   1.687  
   1.688 -(*But not (a zdiv b $<= 0 iff a$<=0); consider a=1, b=2 when a zdiv b = 0.*)
   1.689 +(*But not (a zdiv b $\<le> 0 iff a$\<le>0); consider a=1, b=2 when a zdiv b = 0.*)
   1.690  lemma pos_imp_zdiv_neg_iff: "#0 $< b ==> (a zdiv b $< #0) \<longleftrightarrow> (a $< #0)"
   1.691  apply (simp (no_asm_simp) add: not_zle_iff_zless [THEN iff_sym])
   1.692  apply (erule pos_imp_zdiv_nonneg_iff)
   1.693  done
   1.694  
   1.695 -(*Again the law fails for $<=: consider a = -1, b = -2 when a zdiv b = 0*)
   1.696 +(*Again the law fails for $\<le>: consider a = -1, b = -2 when a zdiv b = 0*)
   1.697  lemma neg_imp_zdiv_neg_iff: "b $< #0 ==> (a zdiv b $< #0) \<longleftrightarrow> (#0 $< a)"
   1.698  apply (simp (no_asm_simp) add: not_zle_iff_zless [THEN iff_sym])
   1.699  apply (erule neg_imp_zdiv_nonneg_iff)
   1.700 @@ -1674,13 +1674,13 @@
   1.701  
   1.702   (** computing "zdiv" by shifting **)
   1.703  
   1.704 - lemma pos_zdiv_mult_2: "#0 $<= a ==> (#1 $+ #2$*b) zdiv (#2$*a) = b zdiv a"
   1.705 + lemma pos_zdiv_mult_2: "#0 $\<le> a ==> (#1 $+ #2$*b) zdiv (#2$*a) = b zdiv a"
   1.706   apply (case_tac "a = #0")
   1.707 - apply (subgoal_tac "#1 $<= a")
   1.708 + apply (subgoal_tac "#1 $\<le> a")
   1.709    apply (arith_tac 2)
   1.710   apply (subgoal_tac "#1 $< a $* #2")
   1.711    apply (arith_tac 2)
   1.712 - apply (subgoal_tac "#2$* (#1 $+ b zmod a) $<= #2$*a")
   1.713 + apply (subgoal_tac "#2$* (#1 $+ b zmod a) $\<le> #2$*a")
   1.714    apply (rule_tac [2] zmult_zle_mono2)
   1.715   apply (auto simp add: zadd_commute zmult_commute add1_zle_iff pos_mod_bound)
   1.716   apply (subst zdiv_zadd1_eq)
   1.717 @@ -1688,13 +1688,13 @@
   1.718   apply (subst zdiv_pos_pos_trivial)
   1.719   apply (simp (no_asm_simp) add: [zmod_pos_pos_trivial pos_mod_sign [THEN zadd_zle_mono1] RSN (2,zle_trans) ])
   1.720   apply (auto simp add: zmod_pos_pos_trivial)
   1.721 - apply (subgoal_tac "#0 $<= b zmod a")
   1.722 + apply (subgoal_tac "#0 $\<le> b zmod a")
   1.723    apply (asm_simp_tac (simpset () add: pos_mod_sign) 2)
   1.724   apply arith
   1.725   done
   1.726  
   1.727  
   1.728 - lemma neg_zdiv_mult_2: "a $<= #0 ==> (#1 $+ #2$*b) zdiv (#2$*a) \<longleftrightarrow> (b$+#1) zdiv a"
   1.729 + lemma neg_zdiv_mult_2: "a $\<le> #0 ==> (#1 $+ #2$*b) zdiv (#2$*a) \<longleftrightarrow> (b$+#1) zdiv a"
   1.730   apply (subgoal_tac " (#1 $+ #2$* ($-b-#1)) zdiv (#2 $* ($-a)) \<longleftrightarrow> ($-b-#1) zdiv ($-a)")
   1.731   apply (rule_tac [2] pos_zdiv_mult_2)
   1.732   apply (auto simp add: zmult_zminus_right)
   1.733 @@ -1706,12 +1706,12 @@
   1.734  
   1.735   (*Not clear why this must be proved separately; probably integ_of causes
   1.736     simplification problems*)
   1.737 - lemma lemma: "~ #0 $<= x ==> x $<= #0"
   1.738 + lemma lemma: "~ #0 $\<le> x ==> x $\<le> #0"
   1.739   apply auto
   1.740   done
   1.741  
   1.742   lemma zdiv_integ_of_BIT: "integ_of (v BIT b) zdiv integ_of (w BIT False) =
   1.743 -           (if ~b | #0 $<= integ_of w
   1.744 +           (if ~b | #0 $\<le> integ_of w
   1.745              then integ_of v zdiv (integ_of w)
   1.746              else (integ_of v $+ #1) zdiv (integ_of w))"
   1.747   apply (simp_tac (simpset_of @{theory_context Int} add: zadd_assoc integ_of_BIT)
   1.748 @@ -1723,13 +1723,13 @@
   1.749  
   1.750   (** computing "zmod" by shifting (proofs resemble those for "zdiv") **)
   1.751  
   1.752 - lemma pos_zmod_mult_2: "#0 $<= a ==> (#1 $+ #2$*b) zmod (#2$*a) = #1 $+ #2 $* (b zmod a)"
   1.753 + lemma pos_zmod_mult_2: "#0 $\<le> a ==> (#1 $+ #2$*b) zmod (#2$*a) = #1 $+ #2 $* (b zmod a)"
   1.754   apply (case_tac "a = #0")
   1.755 - apply (subgoal_tac "#1 $<= a")
   1.756 + apply (subgoal_tac "#1 $\<le> a")
   1.757    apply (arith_tac 2)
   1.758   apply (subgoal_tac "#1 $< a $* #2")
   1.759    apply (arith_tac 2)
   1.760 - apply (subgoal_tac "#2$* (#1 $+ b zmod a) $<= #2$*a")
   1.761 + apply (subgoal_tac "#2$* (#1 $+ b zmod a) $\<le> #2$*a")
   1.762    apply (rule_tac [2] zmult_zle_mono2)
   1.763   apply (auto simp add: zadd_commute zmult_commute add1_zle_iff pos_mod_bound)
   1.764   apply (subst zmod_zadd1_eq)
   1.765 @@ -1737,13 +1737,13 @@
   1.766   apply (rule zmod_pos_pos_trivial)
   1.767   apply (simp (no_asm_simp) # add: [zmod_pos_pos_trivial pos_mod_sign [THEN zadd_zle_mono1] RSN (2,zle_trans) ])
   1.768   apply (auto simp add: zmod_pos_pos_trivial)
   1.769 - apply (subgoal_tac "#0 $<= b zmod a")
   1.770 + apply (subgoal_tac "#0 $\<le> b zmod a")
   1.771    apply (asm_simp_tac (simpset () add: pos_mod_sign) 2)
   1.772   apply arith
   1.773   done
   1.774  
   1.775  
   1.776 - lemma neg_zmod_mult_2: "a $<= #0 ==> (#1 $+ #2$*b) zmod (#2$*a) = #2 $* ((b$+#1) zmod a) - #1"
   1.777 + lemma neg_zmod_mult_2: "a $\<le> #0 ==> (#1 $+ #2$*b) zmod (#2$*a) = #2 $* ((b$+#1) zmod a) - #1"
   1.778   apply (subgoal_tac " (#1 $+ #2$* ($-b-#1)) zmod (#2$* ($-a)) = #1 $+ #2$* (($-b-#1) zmod ($-a))")
   1.779   apply (rule_tac [2] pos_zmod_mult_2)
   1.780   apply (auto simp add: zmult_zminus_right)
   1.781 @@ -1756,7 +1756,7 @@
   1.782  
   1.783   lemma zmod_integ_of_BIT: "integ_of (v BIT b) zmod integ_of (w BIT False) =
   1.784             (if b then
   1.785 -                 if #0 $<= integ_of w
   1.786 +                 if #0 $\<le> integ_of w
   1.787                   then #2 $* (integ_of v zmod integ_of w) $+ #1
   1.788                   else #2 $* ((integ_of v $+ #1) zmod integ_of w) - #1
   1.789              else #2 $* (integ_of v zmod integ_of w))"