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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.300 -   txt\<open>base case: @{term "0\$<=a\$+b"}\<close>
1.301 +   txt\<open>base case: @{term "0\$\<le>a\$+b"}\<close>
1.303    apply (simp add: not_zless_iff_zle [THEN iff_sym])
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.312  apply (drule zminus_zless_zminus [THEN iffD2])
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.446 @@ -958,8 +958,8 @@
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.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.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.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.538   prefer 2 apply (blast intro: zmult_zle_mono1)
1.539  apply (subgoal_tac "r' \$+ #0 \$< b \$+ r")
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.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.583   apply (blast dest: zless_trans zless_add1_iff_zle [THEN iffD1])
1.585 -apply (subgoal_tac "b\$*q' \$<= b'\$*q'")
1.586 +apply (subgoal_tac "b\$*q' \$\<le> b'\$*q'")
1.587   prefer 2
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.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.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.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.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.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))"
```