src/ZF/Integ/IntDiv.thy
 changeset 23146 0bc590051d95 parent 23145 5d8faadf3ecf child 23147 a5db2f7d7654
```     1.1 --- a/src/ZF/Integ/IntDiv.thy	Thu May 31 11:00:06 2007 +0200
1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,1925 +0,0 @@
1.4 -(*  Title:      ZF/IntDiv.thy
1.5 -    ID:         \$Id\$
1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1.7 -    Copyright   1999  University of Cambridge
1.8 -
1.9 -Here is the division algorithm in ML:
1.10 -
1.11 -    fun posDivAlg (a,b) =
1.12 -      if a<b then (0,a)
1.13 -      else let val (q,r) = posDivAlg(a, 2*b)
1.14 -	       in  if 0<=r-b then (2*q+1, r-b) else (2*q, r)
1.15 -	   end
1.16 -
1.17 -    fun negDivAlg (a,b) =
1.18 -      if 0<=a+b then (~1,a+b)
1.19 -      else let val (q,r) = negDivAlg(a, 2*b)
1.20 -	       in  if 0<=r-b then (2*q+1, r-b) else (2*q, r)
1.21 -	   end;
1.22 -
1.23 -    fun negateSnd (q,r:int) = (q,~r);
1.24 -
1.25 -    fun divAlg (a,b) = if 0<=a then
1.26 -			  if b>0 then posDivAlg (a,b)
1.27 -			   else if a=0 then (0,0)
1.28 -				else negateSnd (negDivAlg (~a,~b))
1.29 -		       else
1.30 -			  if 0<b then negDivAlg (a,b)
1.31 -			  else        negateSnd (posDivAlg (~a,~b));
1.32 -
1.33 -*)
1.34 -
1.35 -header{*The Division Operators Div and Mod*}
1.36 -
1.37 -theory IntDiv imports IntArith OrderArith begin
1.38 -
1.39 -constdefs
1.40 -  quorem :: "[i,i] => o"
1.41 -    "quorem == %<a,b> <q,r>.
1.42 -                      a = b\$*q \$+ r &
1.43 -                      (#0\$<b & #0\$<=r & r\$<b | ~(#0\$<b) & b\$<r & r \$<= #0)"
1.44 -
1.45 -  adjust :: "[i,i] => i"
1.46 -    "adjust(b) == %<q,r>. if #0 \$<= r\$-b then <#2\$*q \$+ #1,r\$-b>
1.47 -                          else <#2\$*q,r>"
1.48 -
1.49 -
1.50 -(** the division algorithm **)
1.51 -
1.52 -constdefs posDivAlg :: "i => i"
1.53 -(*for the case a>=0, b>0*)
1.54 -(*recdef posDivAlg "inv_image less_than (%(a,b). nat_of(a \$- b \$+ #1))"*)
1.55 -    "posDivAlg(ab) ==
1.56 -       wfrec(measure(int*int, %<a,b>. nat_of (a \$- b \$+ #1)),
1.57 -	     ab,
1.58 -	     %<a,b> f. if (a\$<b | b\$<=#0) then <#0,a>
1.59 -                       else adjust(b, f ` <a,#2\$*b>))"
1.60 -
1.61 -
1.62 -(*for the case a<0, b>0*)
1.63 -constdefs negDivAlg :: "i => i"
1.64 -(*recdef negDivAlg "inv_image less_than (%(a,b). nat_of(- a \$- b))"*)
1.65 -    "negDivAlg(ab) ==
1.66 -       wfrec(measure(int*int, %<a,b>. nat_of (\$- a \$- b)),
1.67 -	     ab,
1.68 -	     %<a,b> f. if (#0 \$<= a\$+b | b\$<=#0) then <#-1,a\$+b>
1.69 -                       else adjust(b, f ` <a,#2\$*b>))"
1.70 -
1.71 -(*for the general case b\<noteq>0*)
1.72 -
1.73 -constdefs
1.74 -  negateSnd :: "i => i"
1.75 -    "negateSnd == %<q,r>. <q, \$-r>"
1.76 -
1.77 -  (*The full division algorithm considers all possible signs for a, b
1.78 -    including the special case a=0, b<0, because negDivAlg requires a<0*)
1.79 -  divAlg :: "i => i"
1.80 -    "divAlg ==
1.81 -       %<a,b>. if #0 \$<= a then
1.82 -                  if #0 \$<= b then posDivAlg (<a,b>)
1.83 -                  else if a=#0 then <#0,#0>
1.84 -                       else negateSnd (negDivAlg (<\$-a,\$-b>))
1.85 -               else
1.86 -                  if #0\$<b then negDivAlg (<a,b>)
1.87 -                  else         negateSnd (posDivAlg (<\$-a,\$-b>))"
1.88 -
1.89 -  zdiv  :: "[i,i]=>i"                    (infixl "zdiv" 70)
1.90 -    "a zdiv b == fst (divAlg (<intify(a), intify(b)>))"
1.91 -
1.92 -  zmod  :: "[i,i]=>i"                    (infixl "zmod" 70)
1.93 -    "a zmod b == snd (divAlg (<intify(a), intify(b)>))"
1.94 -
1.95 -
1.96 -(** Some basic laws by Sidi Ehmety (need linear arithmetic!) **)
1.97 -
1.98 -lemma zspos_add_zspos_imp_zspos: "[| #0 \$< x;  #0 \$< y |] ==> #0 \$< x \$+ y"
1.99 -apply (rule_tac y = "y" in zless_trans)
1.100 -apply (rule_tac [2] zdiff_zless_iff [THEN iffD1])
1.101 -apply auto
1.102 -done
1.103 -
1.104 -lemma zpos_add_zpos_imp_zpos: "[| #0 \$<= x;  #0 \$<= y |] ==> #0 \$<= x \$+ y"
1.105 -apply (rule_tac y = "y" in zle_trans)
1.106 -apply (rule_tac [2] zdiff_zle_iff [THEN iffD1])
1.107 -apply auto
1.108 -done
1.109 -
1.110 -lemma zneg_add_zneg_imp_zneg: "[| x \$< #0;  y \$< #0 |] ==> x \$+ y \$< #0"
1.111 -apply (rule_tac y = "y" in zless_trans)
1.112 -apply (rule zless_zdiff_iff [THEN iffD1])
1.113 -apply auto
1.114 -done
1.115 -
1.116 -(* this theorem is used below *)
1.118 -     "[| x \$<= #0;  y \$<= #0 |] ==> x \$+ y \$<= #0"
1.119 -apply (rule_tac y = "y" in zle_trans)
1.120 -apply (rule zle_zdiff_iff [THEN iffD1])
1.121 -apply auto
1.122 -done
1.123 -
1.124 -lemma zero_lt_zmagnitude: "[| #0 \$< k; k \<in> int |] ==> 0 < zmagnitude(k)"
1.125 -apply (drule zero_zless_imp_znegative_zminus)
1.126 -apply (drule_tac [2] zneg_int_of)
1.127 -apply (auto simp add: zminus_equation [of k])
1.128 -apply (subgoal_tac "0 < zmagnitude (\$# succ (n))")
1.129 - apply simp
1.130 -apply (simp only: zmagnitude_int_of)
1.131 -apply simp
1.132 -done
1.133 -
1.134 -
1.135 -(*** Inequality lemmas involving \$#succ(m) ***)
1.136 -
1.138 -     "(w \$< z \$+ \$# succ(m)) <-> (w \$< z \$+ \$#m | intify(w) = z \$+ \$#m)"
1.140 -apply (rule_tac [3] x = "0" in bexI)
1.141 -apply (cut_tac m = "m" in int_succ_int_1)
1.142 -apply (cut_tac m = "n" in int_succ_int_1)
1.143 -apply simp
1.144 -apply (erule natE)
1.145 -apply auto
1.146 -apply (rule_tac x = "succ (n) " in bexI)
1.147 -apply auto
1.148 -done
1.149 -
1.151 -     "z \<in> int ==> (w \$+ \$# succ(m) \$<= z) <-> (w \$+ \$#m \$< z)"
1.152 -apply (simp only: not_zless_iff_zle [THEN iff_sym] zless_add_succ_iff)
1.153 -apply (auto intro: zle_anti_sym elim: zless_asym
1.154 -            simp add: zless_imp_zle not_zless_iff_zle)
1.155 -done
1.156 -
1.157 -lemma zadd_succ_zle_iff: "(w \$+ \$# succ(m) \$<= z) <-> (w \$+ \$#m \$< z)"
1.158 -apply (cut_tac z = "intify (z)" in zadd_succ_lemma)
1.159 -apply auto
1.160 -done
1.161 -
1.162 -(** Inequality reasoning **)
1.163 -
1.164 -lemma zless_add1_iff_zle: "(w \$< z \$+ #1) <-> (w\$<=z)"
1.165 -apply (subgoal_tac "#1 = \$# 1")
1.166 -apply (simp only: zless_add_succ_iff zle_def)
1.167 -apply auto
1.168 -done
1.169 -
1.170 -lemma add1_zle_iff: "(w \$+ #1 \$<= z) <-> (w \$< z)"
1.171 -apply (subgoal_tac "#1 = \$# 1")
1.173 -apply auto
1.174 -done
1.175 -
1.176 -lemma add1_left_zle_iff: "(#1 \$+ w \$<= z) <-> (w \$< z)"
1.179 -done
1.180 -
1.181 -
1.182 -(*** Monotonicity of Multiplication ***)
1.183 -
1.184 -lemma zmult_mono_lemma: "k \<in> nat ==> i \$<= j ==> i \$* \$#k \$<= j \$* \$#k"
1.185 -apply (induct_tac "k")
1.186 - prefer 2 apply (subst int_succ_int_1)
1.188 -done
1.189 -
1.190 -lemma zmult_zle_mono1: "[| i \$<= j;  #0 \$<= k |] ==> i\$*k \$<= j\$*k"
1.191 -apply (subgoal_tac "i \$* intify (k) \$<= j \$* intify (k) ")
1.192 -apply (simp (no_asm_use))
1.193 -apply (rule_tac b = "intify (k)" in not_zneg_mag [THEN subst])
1.194 -apply (rule_tac [3] zmult_mono_lemma)
1.195 -apply auto
1.196 -apply (simp add: znegative_iff_zless_0 not_zless_iff_zle [THEN iff_sym])
1.197 -done
1.198 -
1.199 -lemma zmult_zle_mono1_neg: "[| i \$<= j;  k \$<= #0 |] ==> j\$*k \$<= i\$*k"
1.200 -apply (rule zminus_zle_zminus [THEN iffD1])
1.201 -apply (simp del: zmult_zminus_right
1.202 -            add: zmult_zminus_right [symmetric] zmult_zle_mono1 zle_zminus)
1.203 -done
1.204 -
1.205 -lemma zmult_zle_mono2: "[| i \$<= j;  #0 \$<= k |] ==> k\$*i \$<= k\$*j"
1.206 -apply (drule zmult_zle_mono1)
1.208 -done
1.209 -
1.210 -lemma zmult_zle_mono2_neg: "[| i \$<= j;  k \$<= #0 |] ==> k\$*j \$<= k\$*i"
1.211 -apply (drule zmult_zle_mono1_neg)
1.213 -done
1.214 -
1.215 -(* \$<= monotonicity, BOTH arguments*)
1.216 -lemma zmult_zle_mono:
1.217 -     "[| i \$<= j;  k \$<= l;  #0 \$<= j;  #0 \$<= k |] ==> i\$*k \$<= j\$*l"
1.218 -apply (erule zmult_zle_mono1 [THEN zle_trans])
1.219 -apply assumption
1.220 -apply (erule zmult_zle_mono2)
1.221 -apply assumption
1.222 -done
1.223 -
1.224 -
1.225 -(** strict, in 1st argument; proof is by induction on k>0 **)
1.226 -
1.227 -lemma zmult_zless_mono2_lemma [rule_format]:
1.228 -     "[| i\$<j; k \<in> nat |] ==> 0<k --> \$#k \$* i \$< \$#k \$* j"
1.229 -apply (induct_tac "k")
1.230 - prefer 2
1.231 - apply (subst int_succ_int_1)
1.232 - apply (erule natE)
1.234 -apply (frule nat_0_le)
1.235 -apply (subgoal_tac "i \$+ (i \$+ \$# xa \$* i) \$< j \$+ (j \$+ \$# xa \$* j) ")
1.236 -apply (simp (no_asm_use))
1.238 -apply (simp_all (no_asm_simp) add: zle_def)
1.239 -done
1.240 -
1.241 -lemma zmult_zless_mono2: "[| i\$<j;  #0 \$< k |] ==> k\$*i \$< k\$*j"
1.242 -apply (subgoal_tac "intify (k) \$* i \$< intify (k) \$* j")
1.243 -apply (simp (no_asm_use))
1.244 -apply (rule_tac b = "intify (k)" in not_zneg_mag [THEN subst])
1.245 -apply (rule_tac [3] zmult_zless_mono2_lemma)
1.246 -apply auto
1.248 -apply (drule zless_trans, assumption)
1.249 -apply (auto simp add: zero_lt_zmagnitude)
1.250 -done
1.251 -
1.252 -lemma zmult_zless_mono1: "[| i\$<j;  #0 \$< k |] ==> i\$*k \$< j\$*k"
1.253 -apply (drule zmult_zless_mono2)
1.255 -done
1.256 -
1.257 -(* < monotonicity, BOTH arguments*)
1.258 -lemma zmult_zless_mono:
1.259 -     "[| i \$< j;  k \$< l;  #0 \$< j;  #0 \$< k |] ==> i\$*k \$< j\$*l"
1.260 -apply (erule zmult_zless_mono1 [THEN zless_trans])
1.261 -apply assumption
1.262 -apply (erule zmult_zless_mono2)
1.263 -apply assumption
1.264 -done
1.265 -
1.266 -lemma zmult_zless_mono1_neg: "[| i \$< j;  k \$< #0 |] ==> j\$*k \$< i\$*k"
1.267 -apply (rule zminus_zless_zminus [THEN iffD1])
1.268 -apply (simp del: zmult_zminus_right
1.269 -            add: zmult_zminus_right [symmetric] zmult_zless_mono1 zless_zminus)
1.270 -done
1.271 -
1.272 -lemma zmult_zless_mono2_neg: "[| i \$< j;  k \$< #0 |] ==> k\$*j \$< k\$*i"
1.273 -apply (rule zminus_zless_zminus [THEN iffD1])
1.274 -apply (simp del: zmult_zminus
1.275 -            add: zmult_zminus [symmetric] zmult_zless_mono2 zless_zminus)
1.276 -done
1.277 -
1.278 -
1.279 -(** Products of zeroes **)
1.280 -
1.281 -lemma zmult_eq_lemma:
1.282 -     "[| m \<in> int; n \<in> int |] ==> (m = #0 | n = #0) <-> (m\$*n = #0)"
1.283 -apply (case_tac "m \$< #0")
1.284 -apply (auto simp add: not_zless_iff_zle zle_def neq_iff_zless)
1.285 -apply (force dest: zmult_zless_mono1_neg zmult_zless_mono1)+
1.286 -done
1.287 -
1.288 -lemma zmult_eq_0_iff [iff]: "(m\$*n = #0) <-> (intify(m) = #0 | intify(n) = #0)"
1.290 -done
1.291 -
1.292 -
1.293 -(** Cancellation laws for k*m < k*n and m*k < n*k, also for <= and =,
1.294 -    but not (yet?) for k*m < n*k. **)
1.295 -
1.296 -lemma zmult_zless_lemma:
1.297 -     "[| k \<in> int; m \<in> int; n \<in> int |]
1.298 -      ==> (m\$*k \$< n\$*k) <-> ((#0 \$< k & m\$<n) | (k \$< #0 & n\$<m))"
1.299 -apply (case_tac "k = #0")
1.300 -apply (auto simp add: neq_iff_zless zmult_zless_mono1 zmult_zless_mono1_neg)
1.301 -apply (auto simp add: not_zless_iff_zle
1.302 -                      not_zle_iff_zless [THEN iff_sym, of "m\$*k"]
1.303 -                      not_zle_iff_zless [THEN iff_sym, of m])
1.304 -apply (auto elim: notE
1.305 -            simp add: zless_imp_zle zmult_zle_mono1 zmult_zle_mono1_neg)
1.306 -done
1.307 -
1.308 -lemma zmult_zless_cancel2:
1.309 -     "(m\$*k \$< n\$*k) <-> ((#0 \$< k & m\$<n) | (k \$< #0 & n\$<m))"
1.310 -apply (cut_tac k = "intify (k)" and m = "intify (m)" and n = "intify (n)"
1.311 -       in zmult_zless_lemma)
1.312 -apply auto
1.313 -done
1.314 -
1.315 -lemma zmult_zless_cancel1:
1.316 -     "(k\$*m \$< k\$*n) <-> ((#0 \$< k & m\$<n) | (k \$< #0 & n\$<m))"
1.317 -by (simp add: zmult_commute [of k] zmult_zless_cancel2)
1.318 -
1.319 -lemma zmult_zle_cancel2:
1.320 -     "(m\$*k \$<= n\$*k) <-> ((#0 \$< k --> m\$<=n) & (k \$< #0 --> n\$<=m))"
1.321 -by (auto simp add: not_zless_iff_zle [THEN iff_sym] zmult_zless_cancel2)
1.322 -
1.323 -lemma zmult_zle_cancel1:
1.324 -     "(k\$*m \$<= k\$*n) <-> ((#0 \$< k --> m\$<=n) & (k \$< #0 --> n\$<=m))"
1.325 -by (auto simp add: not_zless_iff_zle [THEN iff_sym] zmult_zless_cancel1)
1.326 -
1.327 -lemma int_eq_iff_zle: "[| m \<in> int; n \<in> int |] ==> m=n <-> (m \$<= n & n \$<= m)"
1.328 -apply (blast intro: zle_refl zle_anti_sym)
1.329 -done
1.330 -
1.331 -lemma zmult_cancel2_lemma:
1.332 -     "[| k \<in> int; m \<in> int; n \<in> int |] ==> (m\$*k = n\$*k) <-> (k=#0 | m=n)"
1.333 -apply (simp add: int_eq_iff_zle [of "m\$*k"] int_eq_iff_zle [of m])
1.334 -apply (auto simp add: zmult_zle_cancel2 neq_iff_zless)
1.335 -done
1.336 -
1.337 -lemma zmult_cancel2 [simp]:
1.338 -     "(m\$*k = n\$*k) <-> (intify(k) = #0 | intify(m) = intify(n))"
1.339 -apply (rule iff_trans)
1.340 -apply (rule_tac [2] zmult_cancel2_lemma)
1.341 -apply auto
1.342 -done
1.343 -
1.344 -lemma zmult_cancel1 [simp]:
1.345 -     "(k\$*m = k\$*n) <-> (intify(k) = #0 | intify(m) = intify(n))"
1.346 -by (simp add: zmult_commute [of k] zmult_cancel2)
1.347 -
1.348 -
1.349 -subsection{* Uniqueness and monotonicity of quotients and remainders *}
1.350 -
1.351 -lemma unique_quotient_lemma:
1.352 -     "[| b\$*q' \$+ r' \$<= b\$*q \$+ r;  #0 \$<= r';  #0 \$< b;  r \$< b |]
1.353 -      ==> q' \$<= q"
1.354 -apply (subgoal_tac "r' \$+ b \$* (q'\$-q) \$<= r")
1.356 -apply (subgoal_tac "#0 \$< b \$* (#1 \$+ q \$- q') ")
1.357 - prefer 2
1.358 - apply (erule zle_zless_trans)
1.360 - apply (erule zle_zless_trans)
1.361 - apply (simp add: );
1.362 -apply (subgoal_tac "b \$* q' \$< b \$* (#1 \$+ q)")
1.363 - prefer 2
1.365 -apply (auto elim: zless_asym
1.367 -done
1.368 -
1.369 -lemma unique_quotient_lemma_neg:
1.370 -     "[| b\$*q' \$+ r' \$<= b\$*q \$+ r;  r \$<= #0;  b \$< #0;  b \$< r' |]
1.371 -      ==> q \$<= q'"
1.372 -apply (rule_tac b = "\$-b" and r = "\$-r'" and r' = "\$-r"
1.373 -       in unique_quotient_lemma)
1.374 -apply (auto simp del: zminus_zadd_distrib
1.376 -done
1.377 -
1.378 -
1.379 -lemma unique_quotient:
1.380 -     "[| quorem (<a,b>, <q,r>);  quorem (<a,b>, <q',r'>);  b \<in> int; b ~= #0;
1.381 -         q \<in> int; q' \<in> int |] ==> q = q'"
1.382 -apply (simp add: split_ifs quorem_def neq_iff_zless)
1.383 -apply safe
1.384 -apply simp_all
1.385 -apply (blast intro: zle_anti_sym
1.386 -             dest: zle_eq_refl [THEN unique_quotient_lemma]
1.387 -                   zle_eq_refl [THEN unique_quotient_lemma_neg] sym)+
1.388 -done
1.389 -
1.390 -lemma unique_remainder:
1.391 -     "[| quorem (<a,b>, <q,r>);  quorem (<a,b>, <q',r'>);  b \<in> int; b ~= #0;
1.392 -         q \<in> int; q' \<in> int;
1.393 -         r \<in> int; r' \<in> int |] ==> r = r'"
1.394 -apply (subgoal_tac "q = q'")
1.395 - prefer 2 apply (blast intro: unique_quotient)
1.397 -done
1.398 -
1.399 -
1.400 -subsection{*Correctness of posDivAlg,
1.401 -           the Division Algorithm for @{text "a\<ge>0"} and @{text "b>0"} *}
1.402 -
1.404 -     "adjust(b, <q,r>) = (let diff = r\$-b in
1.405 -                          if #0 \$<= diff then <#2\$*q \$+ #1,diff>
1.406 -                                         else <#2\$*q,r>)"
1.408 -
1.409 -
1.410 -lemma posDivAlg_termination:
1.411 -     "[| #0 \$< b; ~ a \$< b |]
1.412 -      ==> nat_of(a \$- #2 \$\<times> b \$+ #1) < nat_of(a \$- b \$+ #1)"
1.413 -apply (simp (no_asm) add: zless_nat_conj)
1.415 -done
1.416 -
1.417 -lemmas posDivAlg_unfold = def_wfrec [OF posDivAlg_def wf_measure]
1.418 -
1.419 -lemma posDivAlg_eqn:
1.420 -     "[| #0 \$< b; a \<in> int; b \<in> int |] ==>
1.421 -      posDivAlg(<a,b>) =
1.422 -       (if a\$<b then <#0,a> else adjust(b, posDivAlg (<a, #2\$*b>)))"
1.423 -apply (rule posDivAlg_unfold [THEN trans])
1.424 -apply (simp add: vimage_iff not_zless_iff_zle [THEN iff_sym])
1.425 -apply (blast intro: posDivAlg_termination)
1.426 -done
1.427 -
1.428 -lemma posDivAlg_induct_lemma [rule_format]:
1.429 -  assumes prem:
1.430 -        "!!a b. [| a \<in> int; b \<in> int;
1.431 -                   ~ (a \$< b | b \$<= #0) --> P(<a, #2 \$* b>) |] ==> P(<a,b>)"
1.432 -  shows "<u,v> \<in> int*int --> P(<u,v>)"
1.433 -apply (rule_tac a = "<u,v>" in wf_induct)
1.434 -apply (rule_tac A = "int*int" and f = "%<a,b>.nat_of (a \$- b \$+ #1)"
1.435 -       in wf_measure)
1.436 -apply clarify
1.437 -apply (rule prem)
1.438 -apply (drule_tac [3] x = "<xa, #2 \$\<times> y>" in spec)
1.439 -apply auto
1.440 -apply (simp add: not_zle_iff_zless posDivAlg_termination)
1.441 -done
1.442 -
1.443 -
1.444 -lemma posDivAlg_induct [consumes 2]:
1.445 -  assumes u_int: "u \<in> int"
1.446 -      and v_int: "v \<in> int"
1.447 -      and ih: "!!a b. [| a \<in> int; b \<in> int;
1.448 -                     ~ (a \$< b | b \$<= #0) --> P(a, #2 \$* b) |] ==> P(a,b)"
1.449 -  shows "P(u,v)"
1.450 -apply (subgoal_tac "(%<x,y>. P (x,y)) (<u,v>)")
1.451 -apply simp
1.452 -apply (rule posDivAlg_induct_lemma)
1.453 -apply (simp (no_asm_use))
1.454 -apply (rule ih)
1.455 -apply (auto simp add: u_int v_int)
1.456 -done
1.457 -
1.458 -(*FIXME: use intify in integ_of so that we always have integ_of w \<in> int.
1.459 -    then this rewrite can work for ALL constants!!*)
1.460 -lemma intify_eq_0_iff_zle: "intify(m) = #0 <-> (m \$<= #0 & #0 \$<= m)"
1.461 -apply (simp (no_asm) add: int_eq_iff_zle)
1.462 -done
1.463 -
1.464 -
1.465 -subsection{* Some convenient biconditionals for products of signs *}
1.466 -
1.467 -lemma zmult_pos: "[| #0 \$< i; #0 \$< j |] ==> #0 \$< i \$* j"
1.468 -apply (drule zmult_zless_mono1)
1.469 -apply auto
1.470 -done
1.471 -
1.472 -lemma zmult_neg: "[| i \$< #0; j \$< #0 |] ==> #0 \$< i \$* j"
1.473 -apply (drule zmult_zless_mono1_neg)
1.474 -apply auto
1.475 -done
1.476 -
1.477 -lemma zmult_pos_neg: "[| #0 \$< i; j \$< #0 |] ==> i \$* j \$< #0"
1.478 -apply (drule zmult_zless_mono1_neg)
1.479 -apply auto
1.480 -done
1.481 -
1.482 -(** Inequality reasoning **)
1.483 -
1.484 -lemma int_0_less_lemma:
1.485 -     "[| x \<in> int; y \<in> int |]
1.486 -      ==> (#0 \$< x \$* y) <-> (#0 \$< x & #0 \$< y | x \$< #0 & y \$< #0)"
1.487 -apply (auto simp add: zle_def not_zless_iff_zle zmult_pos zmult_neg)
1.488 -apply (rule ccontr)
1.489 -apply (rule_tac [2] ccontr)
1.490 -apply (auto simp add: zle_def not_zless_iff_zle)
1.491 -apply (erule_tac P = "#0\$< x\$* y" in rev_mp)
1.492 -apply (erule_tac [2] P = "#0\$< x\$* y" in rev_mp)
1.493 -apply (drule zmult_pos_neg, assumption)
1.494 - prefer 2
1.495 - apply (drule zmult_pos_neg, assumption)
1.496 -apply (auto dest: zless_not_sym simp add: zmult_commute)
1.497 -done
1.498 -
1.499 -lemma int_0_less_mult_iff:
1.500 -     "(#0 \$< x \$* y) <-> (#0 \$< x & #0 \$< y | x \$< #0 & y \$< #0)"
1.501 -apply (cut_tac x = "intify (x)" and y = "intify (y)" in int_0_less_lemma)
1.502 -apply auto
1.503 -done
1.504 -
1.505 -lemma int_0_le_lemma:
1.506 -     "[| x \<in> int; y \<in> int |]
1.507 -      ==> (#0 \$<= x \$* y) <-> (#0 \$<= x & #0 \$<= y | x \$<= #0 & y \$<= #0)"
1.508 -by (auto simp add: zle_def not_zless_iff_zle int_0_less_mult_iff)
1.509 -
1.510 -lemma int_0_le_mult_iff:
1.511 -     "(#0 \$<= x \$* y) <-> ((#0 \$<= x & #0 \$<= y) | (x \$<= #0 & y \$<= #0))"
1.512 -apply (cut_tac x = "intify (x)" and y = "intify (y)" in int_0_le_lemma)
1.513 -apply auto
1.514 -done
1.515 -
1.516 -lemma zmult_less_0_iff:
1.517 -     "(x \$* y \$< #0) <-> (#0 \$< x & y \$< #0 | x \$< #0 & #0 \$< y)"
1.518 -apply (auto simp add: int_0_le_mult_iff not_zle_iff_zless [THEN iff_sym])
1.519 -apply (auto dest: zless_not_sym simp add: not_zle_iff_zless)
1.520 -done
1.521 -
1.522 -lemma zmult_le_0_iff:
1.523 -     "(x \$* y \$<= #0) <-> (#0 \$<= x & y \$<= #0 | x \$<= #0 & #0 \$<= y)"
1.524 -by (auto dest: zless_not_sym
1.525 -         simp add: int_0_less_mult_iff not_zless_iff_zle [THEN iff_sym])
1.526 -
1.527 -
1.528 -(*Typechecking for posDivAlg*)
1.529 -lemma posDivAlg_type [rule_format]:
1.530 -     "[| a \<in> int; b \<in> int |] ==> posDivAlg(<a,b>) \<in> int * int"
1.531 -apply (rule_tac u = "a" and v = "b" in posDivAlg_induct)
1.532 -apply assumption+
1.533 -apply (case_tac "#0 \$< ba")
1.536 - apply clarify
1.537 - apply (simp add: int_0_less_mult_iff not_zle_iff_zless)
1.539 -apply (subst posDivAlg_unfold)
1.540 -apply simp
1.541 -done
1.542 -
1.543 -(*Correctness of posDivAlg: it computes quotients correctly*)
1.544 -lemma posDivAlg_correct [rule_format]:
1.545 -     "[| a \<in> int; b \<in> int |]
1.546 -      ==> #0 \$<= a --> #0 \$< b --> quorem (<a,b>, posDivAlg(<a,b>))"
1.547 -apply (rule_tac u = "a" and v = "b" in posDivAlg_induct)
1.548 -apply auto
1.549 -   apply (simp_all add: quorem_def)
1.550 -   txt{*base case: a<b*}
1.551 -   apply (simp add: posDivAlg_eqn)
1.552 -  apply (simp add: not_zless_iff_zle [THEN iff_sym])
1.553 - apply (simp add: int_0_less_mult_iff)
1.554 -txt{*main argument*}
1.555 -apply (subst posDivAlg_eqn)
1.556 -apply (simp_all (no_asm_simp))
1.557 -apply (erule splitE)
1.558 -apply (rule posDivAlg_type)
1.561 -txt{*now just linear arithmetic*}
1.562 -apply (simp add: not_zle_iff_zless zdiff_zless_iff)
1.563 -done
1.564 -
1.565 -
1.566 -subsection{*Correctness of negDivAlg, the division algorithm for a<0 and b>0*}
1.567 -
1.568 -lemma negDivAlg_termination:
1.569 -     "[| #0 \$< b; a \$+ b \$< #0 |]
1.570 -      ==> nat_of(\$- a \$- #2 \$* b) < nat_of(\$- a \$- b)"
1.571 -apply (simp (no_asm) add: zless_nat_conj)
1.572 -apply (simp add: zcompare_rls not_zle_iff_zless zless_zdiff_iff [THEN iff_sym]
1.573 -                 zless_zminus)
1.574 -done
1.575 -
1.576 -lemmas negDivAlg_unfold = def_wfrec [OF negDivAlg_def wf_measure]
1.577 -
1.578 -lemma negDivAlg_eqn:
1.579 -     "[| #0 \$< b; a : int; b : int |] ==>
1.580 -      negDivAlg(<a,b>) =
1.581 -       (if #0 \$<= a\$+b then <#-1,a\$+b>
1.582 -                       else adjust(b, negDivAlg (<a, #2\$*b>)))"
1.583 -apply (rule negDivAlg_unfold [THEN trans])
1.584 -apply (simp (no_asm_simp) add: vimage_iff not_zless_iff_zle [THEN iff_sym])
1.585 -apply (blast intro: negDivAlg_termination)
1.586 -done
1.587 -
1.588 -lemma negDivAlg_induct_lemma [rule_format]:
1.589 -  assumes prem:
1.590 -        "!!a b. [| a \<in> int; b \<in> int;
1.591 -                   ~ (#0 \$<= a \$+ b | b \$<= #0) --> P(<a, #2 \$* b>) |]
1.592 -                ==> P(<a,b>)"
1.593 -  shows "<u,v> \<in> int*int --> P(<u,v>)"
1.594 -apply (rule_tac a = "<u,v>" in wf_induct)
1.595 -apply (rule_tac A = "int*int" and f = "%<a,b>.nat_of (\$- a \$- b)"
1.596 -       in wf_measure)
1.597 -apply clarify
1.598 -apply (rule prem)
1.599 -apply (drule_tac [3] x = "<xa, #2 \$\<times> y>" in spec)
1.600 -apply auto
1.601 -apply (simp add: not_zle_iff_zless negDivAlg_termination)
1.602 -done
1.603 -
1.604 -lemma negDivAlg_induct [consumes 2]:
1.605 -  assumes u_int: "u \<in> int"
1.606 -      and v_int: "v \<in> int"
1.607 -      and ih: "!!a b. [| a \<in> int; b \<in> int;
1.608 -                         ~ (#0 \$<= a \$+ b | b \$<= #0) --> P(a, #2 \$* b) |]
1.609 -                      ==> P(a,b)"
1.610 -  shows "P(u,v)"
1.611 -apply (subgoal_tac " (%<x,y>. P (x,y)) (<u,v>)")
1.612 -apply simp
1.613 -apply (rule negDivAlg_induct_lemma)
1.614 -apply (simp (no_asm_use))
1.615 -apply (rule ih)
1.616 -apply (auto simp add: u_int v_int)
1.617 -done
1.618 -
1.619 -
1.620 -(*Typechecking for negDivAlg*)
1.621 -lemma negDivAlg_type:
1.622 -     "[| a \<in> int; b \<in> int |] ==> negDivAlg(<a,b>) \<in> int * int"
1.623 -apply (rule_tac u = "a" and v = "b" in negDivAlg_induct)
1.624 -apply assumption+
1.625 -apply (case_tac "#0 \$< ba")
1.628 - apply clarify
1.629 - apply (simp add: int_0_less_mult_iff not_zle_iff_zless)
1.631 -apply (subst negDivAlg_unfold)
1.632 -apply simp
1.633 -done
1.634 -
1.635 -
1.636 -(*Correctness of negDivAlg: it computes quotients correctly
1.637 -  It doesn't work if a=0 because the 0/b=0 rather than -1*)
1.638 -lemma negDivAlg_correct [rule_format]:
1.639 -     "[| a \<in> int; b \<in> int |]
1.640 -      ==> a \$< #0 --> #0 \$< b --> quorem (<a,b>, negDivAlg(<a,b>))"
1.641 -apply (rule_tac u = "a" and v = "b" in negDivAlg_induct)
1.642 -  apply auto
1.643 -   apply (simp_all add: quorem_def)
1.644 -   txt{*base case: @{term "0\$<=a\$+b"}*}
1.645 -   apply (simp add: negDivAlg_eqn)
1.646 -  apply (simp add: not_zless_iff_zle [THEN iff_sym])
1.647 - apply (simp add: int_0_less_mult_iff)
1.648 -txt{*main argument*}
1.649 -apply (subst negDivAlg_eqn)
1.650 -apply (simp_all (no_asm_simp))
1.651 -apply (erule splitE)
1.652 -apply (rule negDivAlg_type)
1.655 -txt{*now just linear arithmetic*}
1.656 -apply (simp add: not_zle_iff_zless zdiff_zless_iff)
1.657 -done
1.658 -
1.659 -
1.660 -subsection{* Existence shown by proving the division algorithm to be correct *}
1.661 -
1.662 -(*the case a=0*)
1.663 -lemma quorem_0: "[|b \<noteq> #0;  b \<in> int|] ==> quorem (<#0,b>, <#0,#0>)"
1.664 -by (force simp add: quorem_def neq_iff_zless)
1.665 -
1.666 -lemma posDivAlg_zero_divisor: "posDivAlg(<a,#0>) = <#0,a>"
1.667 -apply (subst posDivAlg_unfold)
1.668 -apply simp
1.669 -done
1.670 -
1.671 -lemma posDivAlg_0 [simp]: "posDivAlg (<#0,b>) = <#0,#0>"
1.672 -apply (subst posDivAlg_unfold)
1.674 -done
1.675 -
1.676 -
1.677 -(*Needed below.  Actually it's an equivalence.*)
1.678 -lemma linear_arith_lemma: "~ (#0 \$<= #-1 \$+ b) ==> (b \$<= #0)"
1.680 -apply (drule zminus_zless_zminus [THEN iffD2])
1.682 -done
1.683 -
1.684 -lemma negDivAlg_minus1 [simp]: "negDivAlg (<#-1,b>) = <#-1, b\$-#1>"
1.685 -apply (subst negDivAlg_unfold)
1.686 -apply (simp add: linear_arith_lemma integ_of_type vimage_iff)
1.687 -done
1.688 -
1.689 -lemma negateSnd_eq [simp]: "negateSnd (<q,r>) = <q, \$-r>"
1.690 -apply (unfold negateSnd_def)
1.691 -apply auto
1.692 -done
1.693 -
1.694 -lemma negateSnd_type: "qr \<in> int * int ==> negateSnd (qr) \<in> int * int"
1.695 -apply (unfold negateSnd_def)
1.696 -apply auto
1.697 -done
1.698 -
1.699 -lemma quorem_neg:
1.700 -     "[|quorem (<\$-a,\$-b>, qr);  a \<in> int;  b \<in> int;  qr \<in> int * int|]
1.701 -      ==> quorem (<a,b>, negateSnd(qr))"
1.702 -apply clarify
1.703 -apply (auto elim: zless_asym simp add: quorem_def zless_zminus)
1.704 -txt{*linear arithmetic from here on*}
1.705 -apply (simp_all add: zminus_equation [of a] zminus_zless)
1.706 -apply (cut_tac [2] z = "b" and w = "#0" in zless_linear)
1.707 -apply (cut_tac [1] z = "b" and w = "#0" in zless_linear)
1.708 -apply auto
1.709 -apply (blast dest: zle_zless_trans)+
1.710 -done
1.711 -
1.712 -lemma divAlg_correct:
1.713 -     "[|b \<noteq> #0;  a \<in> int;  b \<in> int|] ==> quorem (<a,b>, divAlg(<a,b>))"
1.714 -apply (auto simp add: quorem_0 divAlg_def)
1.715 -apply (safe intro!: quorem_neg posDivAlg_correct negDivAlg_correct
1.716 -                    posDivAlg_type negDivAlg_type)
1.717 -apply (auto simp add: quorem_def neq_iff_zless)
1.718 -txt{*linear arithmetic from here on*}
1.719 -apply (auto simp add: zle_def)
1.720 -done
1.721 -
1.722 -lemma divAlg_type: "[|a \<in> int;  b \<in> int|] ==> divAlg(<a,b>) \<in> int * int"
1.723 -apply (auto simp add: divAlg_def)
1.724 -apply (auto simp add: posDivAlg_type negDivAlg_type negateSnd_type)
1.725 -done
1.726 -
1.727 -
1.728 -(** intify cancellation **)
1.729 -
1.730 -lemma zdiv_intify1 [simp]: "intify(x) zdiv y = x zdiv y"
1.731 -apply (simp (no_asm) add: zdiv_def)
1.732 -done
1.733 -
1.734 -lemma zdiv_intify2 [simp]: "x zdiv intify(y) = x zdiv y"
1.735 -apply (simp (no_asm) add: zdiv_def)
1.736 -done
1.737 -
1.738 -lemma zdiv_type [iff,TC]: "z zdiv w \<in> int"
1.739 -apply (unfold zdiv_def)
1.740 -apply (blast intro: fst_type divAlg_type)
1.741 -done
1.742 -
1.743 -lemma zmod_intify1 [simp]: "intify(x) zmod y = x zmod y"
1.744 -apply (simp (no_asm) add: zmod_def)
1.745 -done
1.746 -
1.747 -lemma zmod_intify2 [simp]: "x zmod intify(y) = x zmod y"
1.748 -apply (simp (no_asm) add: zmod_def)
1.749 -done
1.750 -
1.751 -lemma zmod_type [iff,TC]: "z zmod w \<in> int"
1.752 -apply (unfold zmod_def)
1.753 -apply (rule snd_type)
1.754 -apply (blast intro: divAlg_type)
1.755 -done
1.756 -
1.757 -
1.758 -(** Arbitrary definitions for division by zero.  Useful to simplify
1.759 -    certain equations **)
1.760 -
1.761 -lemma DIVISION_BY_ZERO_ZDIV: "a zdiv #0 = #0"
1.762 -apply (simp (no_asm) add: zdiv_def divAlg_def posDivAlg_zero_divisor)
1.763 -done  (*NOT for adding to default simpset*)
1.764 -
1.765 -lemma DIVISION_BY_ZERO_ZMOD: "a zmod #0 = intify(a)"
1.766 -apply (simp (no_asm) add: zmod_def divAlg_def posDivAlg_zero_divisor)
1.767 -done  (*NOT for adding to default simpset*)
1.768 -
1.769 -
1.770 -
1.771 -(** Basic laws about division and remainder **)
1.772 -
1.773 -lemma raw_zmod_zdiv_equality:
1.774 -     "[| a \<in> int; b \<in> int |] ==> a = b \$* (a zdiv b) \$+ (a zmod b)"
1.775 -apply (case_tac "b = #0")
1.776 - apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.777 -apply (cut_tac a = "a" and b = "b" in divAlg_correct)
1.778 -apply (auto simp add: quorem_def zdiv_def zmod_def split_def)
1.779 -done
1.780 -
1.781 -lemma zmod_zdiv_equality: "intify(a) = b \$* (a zdiv b) \$+ (a zmod b)"
1.782 -apply (rule trans)
1.783 -apply (rule_tac b = "intify (b)" in raw_zmod_zdiv_equality)
1.784 -apply auto
1.785 -done
1.786 -
1.787 -lemma pos_mod: "#0 \$< b ==> #0 \$<= a zmod b & a zmod b \$< b"
1.788 -apply (cut_tac a = "intify (a)" and b = "intify (b)" in divAlg_correct)
1.789 -apply (auto simp add: intify_eq_0_iff_zle quorem_def zmod_def split_def)
1.790 -apply (blast dest: zle_zless_trans)+
1.791 -done
1.792 -
1.793 -lemmas pos_mod_sign = pos_mod [THEN conjunct1, standard]
1.794 -and    pos_mod_bound = pos_mod [THEN conjunct2, standard]
1.795 -
1.796 -lemma neg_mod: "b \$< #0 ==> a zmod b \$<= #0 & b \$< a zmod b"
1.797 -apply (cut_tac a = "intify (a)" and b = "intify (b)" in divAlg_correct)
1.798 -apply (auto simp add: intify_eq_0_iff_zle quorem_def zmod_def split_def)
1.799 -apply (blast dest: zle_zless_trans)
1.800 -apply (blast dest: zless_trans)+
1.801 -done
1.802 -
1.803 -lemmas neg_mod_sign = neg_mod [THEN conjunct1, standard]
1.804 -and    neg_mod_bound = neg_mod [THEN conjunct2, standard]
1.805 -
1.806 -
1.807 -(** proving general properties of zdiv and zmod **)
1.808 -
1.809 -lemma quorem_div_mod:
1.810 -     "[|b \<noteq> #0;  a \<in> int;  b \<in> int |]
1.811 -      ==> quorem (<a,b>, <a zdiv b, a zmod b>)"
1.812 -apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality)
1.813 -apply (auto simp add: quorem_def neq_iff_zless pos_mod_sign pos_mod_bound
1.814 -                      neg_mod_sign neg_mod_bound)
1.815 -done
1.816 -
1.817 -(*Surely quorem(<a,b>,<q,r>) implies a \<in> int, but it doesn't matter*)
1.818 -lemma quorem_div:
1.819 -     "[| quorem(<a,b>,<q,r>);  b \<noteq> #0;  a \<in> int;  b \<in> int;  q \<in> int |]
1.820 -      ==> a zdiv b = q"
1.821 -by (blast intro: quorem_div_mod [THEN unique_quotient])
1.822 -
1.823 -lemma quorem_mod:
1.824 -     "[| quorem(<a,b>,<q,r>); b \<noteq> #0; a \<in> int; b \<in> int; q \<in> int; r \<in> int |]
1.825 -      ==> a zmod b = r"
1.826 -by (blast intro: quorem_div_mod [THEN unique_remainder])
1.827 -
1.828 -lemma zdiv_pos_pos_trivial_raw:
1.829 -     "[| a \<in> int;  b \<in> int;  #0 \$<= a;  a \$< b |] ==> a zdiv b = #0"
1.830 -apply (rule quorem_div)
1.831 -apply (auto simp add: quorem_def)
1.832 -(*linear arithmetic*)
1.833 -apply (blast dest: zle_zless_trans)+
1.834 -done
1.835 -
1.836 -lemma zdiv_pos_pos_trivial: "[| #0 \$<= a;  a \$< b |] ==> a zdiv b = #0"
1.837 -apply (cut_tac a = "intify (a)" and b = "intify (b)"
1.838 -       in zdiv_pos_pos_trivial_raw)
1.839 -apply auto
1.840 -done
1.841 -
1.842 -lemma zdiv_neg_neg_trivial_raw:
1.843 -     "[| a \<in> int;  b \<in> int;  a \$<= #0;  b \$< a |] ==> a zdiv b = #0"
1.844 -apply (rule_tac r = "a" in quorem_div)
1.845 -apply (auto simp add: quorem_def)
1.846 -(*linear arithmetic*)
1.847 -apply (blast dest: zle_zless_trans zless_trans)+
1.848 -done
1.849 -
1.850 -lemma zdiv_neg_neg_trivial: "[| a \$<= #0;  b \$< a |] ==> a zdiv b = #0"
1.851 -apply (cut_tac a = "intify (a)" and b = "intify (b)"
1.852 -       in zdiv_neg_neg_trivial_raw)
1.853 -apply auto
1.854 -done
1.855 -
1.856 -lemma zadd_le_0_lemma: "[| a\$+b \$<= #0;  #0 \$< a;  #0 \$< b |] ==> False"
1.857 -apply (drule_tac z' = "#0" and z = "b" in zadd_zless_mono)
1.858 -apply (auto simp add: zle_def)
1.859 -apply (blast dest: zless_trans)
1.860 -done
1.861 -
1.862 -lemma zdiv_pos_neg_trivial_raw:
1.863 -     "[| a \<in> int;  b \<in> int;  #0 \$< a;  a\$+b \$<= #0 |] ==> a zdiv b = #-1"
1.864 -apply (rule_tac r = "a \$+ b" in quorem_div)
1.865 -apply (auto simp add: quorem_def)
1.866 -(*linear arithmetic*)
1.867 -apply (blast dest: zadd_le_0_lemma zle_zless_trans)+
1.868 -done
1.869 -
1.870 -lemma zdiv_pos_neg_trivial: "[| #0 \$< a;  a\$+b \$<= #0 |] ==> a zdiv b = #-1"
1.871 -apply (cut_tac a = "intify (a)" and b = "intify (b)"
1.872 -       in zdiv_pos_neg_trivial_raw)
1.873 -apply auto
1.874 -done
1.875 -
1.876 -(*There is no zdiv_neg_pos_trivial because  #0 zdiv b = #0 would supersede it*)
1.877 -
1.878 -
1.879 -lemma zmod_pos_pos_trivial_raw:
1.880 -     "[| a \<in> int;  b \<in> int;  #0 \$<= a;  a \$< b |] ==> a zmod b = a"
1.881 -apply (rule_tac q = "#0" in quorem_mod)
1.882 -apply (auto simp add: quorem_def)
1.883 -(*linear arithmetic*)
1.884 -apply (blast dest: zle_zless_trans)+
1.885 -done
1.886 -
1.887 -lemma zmod_pos_pos_trivial: "[| #0 \$<= a;  a \$< b |] ==> a zmod b = intify(a)"
1.888 -apply (cut_tac a = "intify (a)" and b = "intify (b)"
1.889 -       in zmod_pos_pos_trivial_raw)
1.890 -apply auto
1.891 -done
1.892 -
1.893 -lemma zmod_neg_neg_trivial_raw:
1.894 -     "[| a \<in> int;  b \<in> int;  a \$<= #0;  b \$< a |] ==> a zmod b = a"
1.895 -apply (rule_tac q = "#0" in quorem_mod)
1.896 -apply (auto simp add: quorem_def)
1.897 -(*linear arithmetic*)
1.898 -apply (blast dest: zle_zless_trans zless_trans)+
1.899 -done
1.900 -
1.901 -lemma zmod_neg_neg_trivial: "[| a \$<= #0;  b \$< a |] ==> a zmod b = intify(a)"
1.902 -apply (cut_tac a = "intify (a)" and b = "intify (b)"
1.903 -       in zmod_neg_neg_trivial_raw)
1.904 -apply auto
1.905 -done
1.906 -
1.907 -lemma zmod_pos_neg_trivial_raw:
1.908 -     "[| a \<in> int;  b \<in> int;  #0 \$< a;  a\$+b \$<= #0 |] ==> a zmod b = a\$+b"
1.909 -apply (rule_tac q = "#-1" in quorem_mod)
1.910 -apply (auto simp add: quorem_def)
1.911 -(*linear arithmetic*)
1.912 -apply (blast dest: zadd_le_0_lemma zle_zless_trans)+
1.913 -done
1.914 -
1.915 -lemma zmod_pos_neg_trivial: "[| #0 \$< a;  a\$+b \$<= #0 |] ==> a zmod b = a\$+b"
1.916 -apply (cut_tac a = "intify (a)" and b = "intify (b)"
1.917 -       in zmod_pos_neg_trivial_raw)
1.918 -apply auto
1.919 -done
1.920 -
1.921 -(*There is no zmod_neg_pos_trivial...*)
1.922 -
1.923 -
1.924 -(*Simpler laws such as -a zdiv b = -(a zdiv b) FAIL*)
1.925 -
1.926 -lemma zdiv_zminus_zminus_raw:
1.927 -     "[|a \<in> int;  b \<in> int|] ==> (\$-a) zdiv (\$-b) = a zdiv b"
1.928 -apply (case_tac "b = #0")
1.929 - apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.930 -apply (subst quorem_div_mod [THEN quorem_neg, simplified, THEN quorem_div])
1.931 -apply auto
1.932 -done
1.933 -
1.934 -lemma zdiv_zminus_zminus [simp]: "(\$-a) zdiv (\$-b) = a zdiv b"
1.935 -apply (cut_tac a = "intify (a)" and b = "intify (b)" in zdiv_zminus_zminus_raw)
1.936 -apply auto
1.937 -done
1.938 -
1.939 -(*Simpler laws such as -a zmod b = -(a zmod b) FAIL*)
1.940 -lemma zmod_zminus_zminus_raw:
1.941 -     "[|a \<in> int;  b \<in> int|] ==> (\$-a) zmod (\$-b) = \$- (a zmod b)"
1.942 -apply (case_tac "b = #0")
1.943 - apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.944 -apply (subst quorem_div_mod [THEN quorem_neg, simplified, THEN quorem_mod])
1.945 -apply auto
1.946 -done
1.947 -
1.948 -lemma zmod_zminus_zminus [simp]: "(\$-a) zmod (\$-b) = \$- (a zmod b)"
1.949 -apply (cut_tac a = "intify (a)" and b = "intify (b)" in zmod_zminus_zminus_raw)
1.950 -apply auto
1.951 -done
1.952 -
1.953 -
1.954 -subsection{* division of a number by itself *}
1.955 -
1.956 -lemma self_quotient_aux1: "[| #0 \$< a; a = r \$+ a\$*q; r \$< a |] ==> #1 \$<= q"
1.957 -apply (subgoal_tac "#0 \$< a\$*q")
1.958 -apply (cut_tac w = "#0" and z = "q" in add1_zle_iff)
1.960 -apply (blast dest: zless_trans)
1.961 -(*linear arithmetic...*)
1.962 -apply (drule_tac t = "%x. x \$- r" in subst_context)
1.963 -apply (drule sym)
1.965 -done
1.966 -
1.967 -lemma self_quotient_aux2: "[| #0 \$< a; a = r \$+ a\$*q; #0 \$<= r |] ==> q \$<= #1"
1.968 -apply (subgoal_tac "#0 \$<= a\$* (#1\$-q)")
1.969 - apply (simp add: int_0_le_mult_iff zcompare_rls)
1.970 - apply (blast dest: zle_zless_trans)
1.972 -apply (drule_tac t = "%x. x \$- a \$* q" in subst_context)
1.974 -done
1.975 -
1.976 -lemma self_quotient:
1.977 -     "[| quorem(<a,a>,<q,r>);  a \<in> int;  q \<in> int;  a \<noteq> #0|] ==> q = #1"
1.978 -apply (simp add: split_ifs quorem_def neq_iff_zless)
1.979 -apply (rule zle_anti_sym)
1.980 -apply safe
1.981 -apply auto
1.982 -prefer 4 apply (blast dest: zless_trans)
1.983 -apply (blast dest: zless_trans)
1.984 -apply (rule_tac [3] a = "\$-a" and r = "\$-r" in self_quotient_aux1)
1.985 -apply (rule_tac a = "\$-a" and r = "\$-r" in self_quotient_aux2)
1.986 -apply (rule_tac [6] zminus_equation [THEN iffD1])
1.987 -apply (rule_tac [2] zminus_equation [THEN iffD1])
1.988 -apply (force intro: self_quotient_aux1 self_quotient_aux2
1.990 -done
1.991 -
1.992 -lemma self_remainder:
1.993 -     "[|quorem(<a,a>,<q,r>); a \<in> int; q \<in> int; r \<in> int; a \<noteq> #0|] ==> r = #0"
1.994 -apply (frule self_quotient)
1.995 -apply (auto simp add: quorem_def)
1.996 -done
1.997 -
1.998 -lemma zdiv_self_raw: "[|a \<noteq> #0; a \<in> int|] ==> a zdiv a = #1"
1.999 -apply (blast intro: quorem_div_mod [THEN self_quotient])
1.1000 -done
1.1001 -
1.1002 -lemma zdiv_self [simp]: "intify(a) \<noteq> #0 ==> a zdiv a = #1"
1.1003 -apply (drule zdiv_self_raw)
1.1004 -apply auto
1.1005 -done
1.1006 -
1.1007 -(*Here we have 0 zmod 0 = 0, also assumed by Knuth (who puts m zmod 0 = 0) *)
1.1008 -lemma zmod_self_raw: "a \<in> int ==> a zmod a = #0"
1.1009 -apply (case_tac "a = #0")
1.1010 - apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.1011 -apply (blast intro: quorem_div_mod [THEN self_remainder])
1.1012 -done
1.1013 -
1.1014 -lemma zmod_self [simp]: "a zmod a = #0"
1.1015 -apply (cut_tac a = "intify (a)" in zmod_self_raw)
1.1016 -apply auto
1.1017 -done
1.1018 -
1.1019 -
1.1020 -subsection{* Computation of division and remainder *}
1.1021 -
1.1022 -lemma zdiv_zero [simp]: "#0 zdiv b = #0"
1.1023 -apply (simp (no_asm) add: zdiv_def divAlg_def)
1.1024 -done
1.1025 -
1.1026 -lemma zdiv_eq_minus1: "#0 \$< b ==> #-1 zdiv b = #-1"
1.1027 -apply (simp (no_asm_simp) add: zdiv_def divAlg_def)
1.1028 -done
1.1029 -
1.1030 -lemma zmod_zero [simp]: "#0 zmod b = #0"
1.1031 -apply (simp (no_asm) add: zmod_def divAlg_def)
1.1032 -done
1.1033 -
1.1034 -lemma zdiv_minus1: "#0 \$< b ==> #-1 zdiv b = #-1"
1.1035 -apply (simp (no_asm_simp) add: zdiv_def divAlg_def)
1.1036 -done
1.1037 -
1.1038 -lemma zmod_minus1: "#0 \$< b ==> #-1 zmod b = b \$- #1"
1.1039 -apply (simp (no_asm_simp) add: zmod_def divAlg_def)
1.1040 -done
1.1041 -
1.1042 -(** a positive, b positive **)
1.1043 -
1.1044 -lemma zdiv_pos_pos: "[| #0 \$< a;  #0 \$<= b |]
1.1045 -      ==> a zdiv b = fst (posDivAlg(<intify(a), intify(b)>))"
1.1046 -apply (simp (no_asm_simp) add: zdiv_def divAlg_def)
1.1047 -apply (auto simp add: zle_def)
1.1048 -done
1.1049 -
1.1050 -lemma zmod_pos_pos:
1.1051 -     "[| #0 \$< a;  #0 \$<= b |]
1.1052 -      ==> a zmod b = snd (posDivAlg(<intify(a), intify(b)>))"
1.1053 -apply (simp (no_asm_simp) add: zmod_def divAlg_def)
1.1054 -apply (auto simp add: zle_def)
1.1055 -done
1.1056 -
1.1057 -(** a negative, b positive **)
1.1058 -
1.1059 -lemma zdiv_neg_pos:
1.1060 -     "[| a \$< #0;  #0 \$< b |]
1.1061 -      ==> a zdiv b = fst (negDivAlg(<intify(a), intify(b)>))"
1.1062 -apply (simp (no_asm_simp) add: zdiv_def divAlg_def)
1.1063 -apply (blast dest: zle_zless_trans)
1.1064 -done
1.1065 -
1.1066 -lemma zmod_neg_pos:
1.1067 -     "[| a \$< #0;  #0 \$< b |]
1.1068 -      ==> a zmod b = snd (negDivAlg(<intify(a), intify(b)>))"
1.1069 -apply (simp (no_asm_simp) add: zmod_def divAlg_def)
1.1070 -apply (blast dest: zle_zless_trans)
1.1071 -done
1.1072 -
1.1073 -(** a positive, b negative **)
1.1074 -
1.1075 -lemma zdiv_pos_neg:
1.1076 -     "[| #0 \$< a;  b \$< #0 |]
1.1077 -      ==> a zdiv b = fst (negateSnd(negDivAlg (<\$-a, \$-b>)))"
1.1078 -apply (simp (no_asm_simp) add: zdiv_def divAlg_def intify_eq_0_iff_zle)
1.1079 -apply auto
1.1080 -apply (blast dest: zle_zless_trans)+
1.1081 -apply (blast dest: zless_trans)
1.1082 -apply (blast intro: zless_imp_zle)
1.1083 -done
1.1084 -
1.1085 -lemma zmod_pos_neg:
1.1086 -     "[| #0 \$< a;  b \$< #0 |]
1.1087 -      ==> a zmod b = snd (negateSnd(negDivAlg (<\$-a, \$-b>)))"
1.1088 -apply (simp (no_asm_simp) add: zmod_def divAlg_def intify_eq_0_iff_zle)
1.1089 -apply auto
1.1090 -apply (blast dest: zle_zless_trans)+
1.1091 -apply (blast dest: zless_trans)
1.1092 -apply (blast intro: zless_imp_zle)
1.1093 -done
1.1094 -
1.1095 -(** a negative, b negative **)
1.1096 -
1.1097 -lemma zdiv_neg_neg:
1.1098 -     "[| a \$< #0;  b \$<= #0 |]
1.1099 -      ==> a zdiv b = fst (negateSnd(posDivAlg(<\$-a, \$-b>)))"
1.1100 -apply (simp (no_asm_simp) add: zdiv_def divAlg_def)
1.1101 -apply auto
1.1102 -apply (blast dest!: zle_zless_trans)+
1.1103 -done
1.1104 -
1.1105 -lemma zmod_neg_neg:
1.1106 -     "[| a \$< #0;  b \$<= #0 |]
1.1107 -      ==> a zmod b = snd (negateSnd(posDivAlg(<\$-a, \$-b>)))"
1.1108 -apply (simp (no_asm_simp) add: zmod_def divAlg_def)
1.1109 -apply auto
1.1110 -apply (blast dest!: zle_zless_trans)+
1.1111 -done
1.1112 -
1.1113 -declare zdiv_pos_pos [of "integ_of (v)" "integ_of (w)", standard, simp]
1.1114 -declare zdiv_neg_pos [of "integ_of (v)" "integ_of (w)", standard, simp]
1.1115 -declare zdiv_pos_neg [of "integ_of (v)" "integ_of (w)", standard, simp]
1.1116 -declare zdiv_neg_neg [of "integ_of (v)" "integ_of (w)", standard, simp]
1.1117 -declare zmod_pos_pos [of "integ_of (v)" "integ_of (w)", standard, simp]
1.1118 -declare zmod_neg_pos [of "integ_of (v)" "integ_of (w)", standard, simp]
1.1119 -declare zmod_pos_neg [of "integ_of (v)" "integ_of (w)", standard, simp]
1.1120 -declare zmod_neg_neg [of "integ_of (v)" "integ_of (w)", standard, simp]
1.1121 -declare posDivAlg_eqn [of concl: "integ_of (v)" "integ_of (w)", standard, simp]
1.1122 -declare negDivAlg_eqn [of concl: "integ_of (v)" "integ_of (w)", standard, simp]
1.1123 -
1.1124 -
1.1125 -(** Special-case simplification **)
1.1126 -
1.1127 -lemma zmod_1 [simp]: "a zmod #1 = #0"
1.1128 -apply (cut_tac a = "a" and b = "#1" in pos_mod_sign)
1.1129 -apply (cut_tac [2] a = "a" and b = "#1" in pos_mod_bound)
1.1130 -apply auto
1.1131 -(*arithmetic*)
1.1132 -apply (drule add1_zle_iff [THEN iffD2])
1.1133 -apply (rule zle_anti_sym)
1.1134 -apply auto
1.1135 -done
1.1136 -
1.1137 -lemma zdiv_1 [simp]: "a zdiv #1 = intify(a)"
1.1138 -apply (cut_tac a = "a" and b = "#1" in zmod_zdiv_equality)
1.1139 -apply auto
1.1140 -done
1.1141 -
1.1142 -lemma zmod_minus1_right [simp]: "a zmod #-1 = #0"
1.1143 -apply (cut_tac a = "a" and b = "#-1" in neg_mod_sign)
1.1144 -apply (cut_tac [2] a = "a" and b = "#-1" in neg_mod_bound)
1.1145 -apply auto
1.1146 -(*arithmetic*)
1.1147 -apply (drule add1_zle_iff [THEN iffD2])
1.1148 -apply (rule zle_anti_sym)
1.1149 -apply auto
1.1150 -done
1.1151 -
1.1152 -lemma zdiv_minus1_right_raw: "a \<in> int ==> a zdiv #-1 = \$-a"
1.1153 -apply (cut_tac a = "a" and b = "#-1" in zmod_zdiv_equality)
1.1154 -apply auto
1.1155 -apply (rule equation_zminus [THEN iffD2])
1.1156 -apply auto
1.1157 -done
1.1158 -
1.1159 -lemma zdiv_minus1_right: "a zdiv #-1 = \$-a"
1.1160 -apply (cut_tac a = "intify (a)" in zdiv_minus1_right_raw)
1.1161 -apply auto
1.1162 -done
1.1163 -declare zdiv_minus1_right [simp]
1.1164 -
1.1165 -
1.1166 -subsection{* Monotonicity in the first argument (divisor) *}
1.1167 -
1.1168 -lemma zdiv_mono1: "[| a \$<= a';  #0 \$< b |] ==> a zdiv b \$<= a' zdiv b"
1.1169 -apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality)
1.1170 -apply (cut_tac a = "a'" and b = "b" in zmod_zdiv_equality)
1.1171 -apply (rule unique_quotient_lemma)
1.1172 -apply (erule subst)
1.1173 -apply (erule subst)
1.1174 -apply (simp_all (no_asm_simp) add: pos_mod_sign pos_mod_bound)
1.1175 -done
1.1176 -
1.1177 -lemma zdiv_mono1_neg: "[| a \$<= a';  b \$< #0 |] ==> a' zdiv b \$<= a zdiv b"
1.1178 -apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality)
1.1179 -apply (cut_tac a = "a'" and b = "b" in zmod_zdiv_equality)
1.1180 -apply (rule unique_quotient_lemma_neg)
1.1181 -apply (erule subst)
1.1182 -apply (erule subst)
1.1183 -apply (simp_all (no_asm_simp) add: neg_mod_sign neg_mod_bound)
1.1184 -done
1.1185 -
1.1186 -
1.1187 -subsection{* Monotonicity in the second argument (dividend) *}
1.1188 -
1.1189 -lemma q_pos_lemma:
1.1190 -     "[| #0 \$<= b'\$*q' \$+ r'; r' \$< b';  #0 \$< b' |] ==> #0 \$<= q'"
1.1191 -apply (subgoal_tac "#0 \$< b'\$* (q' \$+ #1)")
1.1192 - apply (simp add: int_0_less_mult_iff)
1.1193 - apply (blast dest: zless_trans intro: zless_add1_iff_zle [THEN iffD1])
1.1195 -apply (erule zle_zless_trans)
1.1197 -done
1.1198 -
1.1199 -lemma zdiv_mono2_lemma:
1.1200 -     "[| b\$*q \$+ r = b'\$*q' \$+ r';  #0 \$<= b'\$*q' \$+ r';
1.1201 -         r' \$< b';  #0 \$<= r;  #0 \$< b';  b' \$<= b |]
1.1202 -      ==> q \$<= q'"
1.1203 -apply (frule q_pos_lemma, assumption+)
1.1204 -apply (subgoal_tac "b\$*q \$< b\$* (q' \$+ #1)")
1.1205 - apply (simp add: zmult_zless_cancel1)
1.1206 - apply (force dest: zless_add1_iff_zle [THEN iffD1] zless_trans zless_zle_trans)
1.1207 -apply (subgoal_tac "b\$*q = r' \$- r \$+ b'\$*q'")
1.1208 - prefer 2 apply (simp add: zcompare_rls)
1.1211 - prefer 2 apply (blast intro: zmult_zle_mono1)
1.1212 -apply (subgoal_tac "r' \$+ #0 \$< b \$+ r")
1.1213 - apply (simp add: zcompare_rls)
1.1215 - apply auto
1.1216 -apply (blast dest: zless_zle_trans)
1.1217 -done
1.1218 -
1.1219 -
1.1220 -lemma zdiv_mono2_raw:
1.1221 -     "[| #0 \$<= a;  #0 \$< b';  b' \$<= b;  a \<in> int |]
1.1222 -      ==> a zdiv b \$<= a zdiv b'"
1.1223 -apply (subgoal_tac "#0 \$< b")
1.1224 - prefer 2 apply (blast dest: zless_zle_trans)
1.1225 -apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality)
1.1226 -apply (cut_tac a = "a" and b = "b'" in zmod_zdiv_equality)
1.1227 -apply (rule zdiv_mono2_lemma)
1.1228 -apply (erule subst)
1.1229 -apply (erule subst)
1.1230 -apply (simp_all add: pos_mod_sign pos_mod_bound)
1.1231 -done
1.1232 -
1.1233 -lemma zdiv_mono2:
1.1234 -     "[| #0 \$<= a;  #0 \$< b';  b' \$<= b |]
1.1235 -      ==> a zdiv b \$<= a zdiv b'"
1.1236 -apply (cut_tac a = "intify (a)" in zdiv_mono2_raw)
1.1237 -apply auto
1.1238 -done
1.1239 -
1.1240 -lemma q_neg_lemma:
1.1241 -     "[| b'\$*q' \$+ r' \$< #0;  #0 \$<= r';  #0 \$< b' |] ==> q' \$< #0"
1.1242 -apply (subgoal_tac "b'\$*q' \$< #0")
1.1243 - prefer 2 apply (force intro: zle_zless_trans)
1.1245 -apply (blast dest: zless_trans)
1.1246 -done
1.1247 -
1.1248 -
1.1249 -
1.1250 -lemma zdiv_mono2_neg_lemma:
1.1251 -     "[| b\$*q \$+ r = b'\$*q' \$+ r';  b'\$*q' \$+ r' \$< #0;
1.1252 -         r \$< b;  #0 \$<= r';  #0 \$< b';  b' \$<= b |]
1.1253 -      ==> q' \$<= q"
1.1254 -apply (subgoal_tac "#0 \$< b")
1.1255 - prefer 2 apply (blast dest: zless_zle_trans)
1.1256 -apply (frule q_neg_lemma, assumption+)
1.1257 -apply (subgoal_tac "b\$*q' \$< b\$* (q \$+ #1)")
1.1258 - apply (simp add: zmult_zless_cancel1)
1.1259 - apply (blast dest: zless_trans zless_add1_iff_zle [THEN iffD1])
1.1261 -apply (subgoal_tac "b\$*q' \$<= b'\$*q'")
1.1262 - prefer 2
1.1263 - apply (simp add: zmult_zle_cancel2)
1.1264 - apply (blast dest: zless_trans)
1.1265 -apply (subgoal_tac "b'\$*q' \$+ r \$< b \$+ (b\$*q \$+ r)")
1.1266 - prefer 2
1.1267 - apply (erule ssubst)
1.1268 - apply simp
1.1269 - apply (drule_tac w' = "r" and z' = "#0" in zadd_zless_mono)
1.1270 -  apply (assumption)
1.1271 - apply simp
1.1273 -apply (rule zle_zless_trans)
1.1274 - prefer 2 apply (assumption)
1.1275 -apply (simp (no_asm_simp) add: zmult_zle_cancel2)
1.1276 -apply (blast dest: zless_trans)
1.1277 -done
1.1278 -
1.1279 -lemma zdiv_mono2_neg_raw:
1.1280 -     "[| a \$< #0;  #0 \$< b';  b' \$<= b;  a \<in> int |]
1.1281 -      ==> a zdiv b' \$<= a zdiv b"
1.1282 -apply (subgoal_tac "#0 \$< b")
1.1283 - prefer 2 apply (blast dest: zless_zle_trans)
1.1284 -apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality)
1.1285 -apply (cut_tac a = "a" and b = "b'" in zmod_zdiv_equality)
1.1286 -apply (rule zdiv_mono2_neg_lemma)
1.1287 -apply (erule subst)
1.1288 -apply (erule subst)
1.1289 -apply (simp_all add: pos_mod_sign pos_mod_bound)
1.1290 -done
1.1291 -
1.1292 -lemma zdiv_mono2_neg: "[| a \$< #0;  #0 \$< b';  b' \$<= b |]
1.1293 -      ==> a zdiv b' \$<= a zdiv b"
1.1294 -apply (cut_tac a = "intify (a)" in zdiv_mono2_neg_raw)
1.1295 -apply auto
1.1296 -done
1.1297 -
1.1298 -
1.1299 -
1.1300 -subsection{* More algebraic laws for zdiv and zmod *}
1.1301 -
1.1302 -(** proving (a*b) zdiv c = a \$* (b zdiv c) \$+ a * (b zmod c) **)
1.1303 -
1.1304 -lemma zmult1_lemma:
1.1305 -     "[| quorem(<b,c>, <q,r>);  c \<in> int;  c \<noteq> #0 |]
1.1306 -      ==> quorem (<a\$*b, c>, <a\$*q \$+ (a\$*r) zdiv c, (a\$*r) zmod c>)"
1.1308 -                      pos_mod_sign pos_mod_bound neg_mod_sign neg_mod_bound)
1.1309 -apply (auto intro: raw_zmod_zdiv_equality)
1.1310 -done
1.1311 -
1.1312 -lemma zdiv_zmult1_eq_raw:
1.1313 -     "[|b \<in> int;  c \<in> int|]
1.1314 -      ==> (a\$*b) zdiv c = a\$*(b zdiv c) \$+ a\$*(b zmod c) zdiv c"
1.1315 -apply (case_tac "c = #0")
1.1316 - apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.1317 -apply (rule quorem_div_mod [THEN zmult1_lemma, THEN quorem_div])
1.1318 -apply auto
1.1319 -done
1.1320 -
1.1321 -lemma zdiv_zmult1_eq: "(a\$*b) zdiv c = a\$*(b zdiv c) \$+ a\$*(b zmod c) zdiv c"
1.1322 -apply (cut_tac b = "intify (b)" and c = "intify (c)" in zdiv_zmult1_eq_raw)
1.1323 -apply auto
1.1324 -done
1.1325 -
1.1326 -lemma zmod_zmult1_eq_raw:
1.1327 -     "[|b \<in> int;  c \<in> int|] ==> (a\$*b) zmod c = a\$*(b zmod c) zmod c"
1.1328 -apply (case_tac "c = #0")
1.1329 - apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.1330 -apply (rule quorem_div_mod [THEN zmult1_lemma, THEN quorem_mod])
1.1331 -apply auto
1.1332 -done
1.1333 -
1.1334 -lemma zmod_zmult1_eq: "(a\$*b) zmod c = a\$*(b zmod c) zmod c"
1.1335 -apply (cut_tac b = "intify (b)" and c = "intify (c)" in zmod_zmult1_eq_raw)
1.1336 -apply auto
1.1337 -done
1.1338 -
1.1339 -lemma zmod_zmult1_eq': "(a\$*b) zmod c = ((a zmod c) \$* b) zmod c"
1.1340 -apply (rule trans)
1.1341 -apply (rule_tac b = " (b \$* a) zmod c" in trans)
1.1342 -apply (rule_tac [2] zmod_zmult1_eq)
1.1343 -apply (simp_all (no_asm) add: zmult_commute)
1.1344 -done
1.1345 -
1.1346 -lemma zmod_zmult_distrib: "(a\$*b) zmod c = ((a zmod c) \$* (b zmod c)) zmod c"
1.1347 -apply (rule zmod_zmult1_eq' [THEN trans])
1.1348 -apply (rule zmod_zmult1_eq)
1.1349 -done
1.1350 -
1.1351 -lemma zdiv_zmult_self1 [simp]: "intify(b) \<noteq> #0 ==> (a\$*b) zdiv b = intify(a)"
1.1352 -apply (simp (no_asm_simp) add: zdiv_zmult1_eq)
1.1353 -done
1.1354 -
1.1355 -lemma zdiv_zmult_self2 [simp]: "intify(b) \<noteq> #0 ==> (b\$*a) zdiv b = intify(a)"
1.1356 -apply (subst zmult_commute , erule zdiv_zmult_self1)
1.1357 -done
1.1358 -
1.1359 -lemma zmod_zmult_self1 [simp]: "(a\$*b) zmod b = #0"
1.1360 -apply (simp (no_asm) add: zmod_zmult1_eq)
1.1361 -done
1.1362 -
1.1363 -lemma zmod_zmult_self2 [simp]: "(b\$*a) zmod b = #0"
1.1364 -apply (simp (no_asm) add: zmult_commute zmod_zmult1_eq)
1.1365 -done
1.1366 -
1.1367 -
1.1368 -(** proving (a\$+b) zdiv c =
1.1369 -            a zdiv c \$+ b zdiv c \$+ ((a zmod c \$+ b zmod c) zdiv c) **)
1.1370 -
1.1372 -     "[| quorem(<a,c>, <aq,ar>);  quorem(<b,c>, <bq,br>);
1.1373 -         c \<in> int;  c \<noteq> #0 |]
1.1374 -      ==> quorem (<a\$+b, c>, <aq \$+ bq \$+ (ar\$+br) zdiv c, (ar\$+br) zmod c>)"
1.1376 -                      pos_mod_sign pos_mod_bound neg_mod_sign neg_mod_bound)
1.1377 -apply (auto intro: raw_zmod_zdiv_equality)
1.1378 -done
1.1379 -
1.1380 -(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
1.1382 -     "[|a \<in> int; b \<in> int; c \<in> int|] ==>
1.1383 -      (a\$+b) zdiv c = a zdiv c \$+ b zdiv c \$+ ((a zmod c \$+ b zmod c) zdiv c)"
1.1384 -apply (case_tac "c = #0")
1.1385 - apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.1386 -apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod,
1.1387 -                                 THEN quorem_div])
1.1388 -done
1.1389 -
1.1391 -     "(a\$+b) zdiv c = a zdiv c \$+ b zdiv c \$+ ((a zmod c \$+ b zmod c) zdiv c)"
1.1392 -apply (cut_tac a = "intify (a)" and b = "intify (b)" and c = "intify (c)"
1.1394 -apply auto
1.1395 -done
1.1396 -
1.1398 -     "[|a \<in> int; b \<in> int; c \<in> int|]
1.1399 -      ==> (a\$+b) zmod c = (a zmod c \$+ b zmod c) zmod c"
1.1400 -apply (case_tac "c = #0")
1.1401 - apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.1402 -apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod,
1.1403 -                                 THEN quorem_mod])
1.1404 -done
1.1405 -
1.1406 -lemma zmod_zadd1_eq: "(a\$+b) zmod c = (a zmod c \$+ b zmod c) zmod c"
1.1407 -apply (cut_tac a = "intify (a)" and b = "intify (b)" and c = "intify (c)"
1.1409 -apply auto
1.1410 -done
1.1411 -
1.1412 -lemma zmod_div_trivial_raw:
1.1413 -     "[|a \<in> int; b \<in> int|] ==> (a zmod b) zdiv b = #0"
1.1414 -apply (case_tac "b = #0")
1.1415 - apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.1416 -apply (auto simp add: neq_iff_zless pos_mod_sign pos_mod_bound
1.1417 -         zdiv_pos_pos_trivial neg_mod_sign neg_mod_bound zdiv_neg_neg_trivial)
1.1418 -done
1.1419 -
1.1420 -lemma zmod_div_trivial [simp]: "(a zmod b) zdiv b = #0"
1.1421 -apply (cut_tac a = "intify (a)" and b = "intify (b)" in zmod_div_trivial_raw)
1.1422 -apply auto
1.1423 -done
1.1424 -
1.1425 -lemma zmod_mod_trivial_raw:
1.1426 -     "[|a \<in> int; b \<in> int|] ==> (a zmod b) zmod b = a zmod b"
1.1427 -apply (case_tac "b = #0")
1.1428 - apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.1429 -apply (auto simp add: neq_iff_zless pos_mod_sign pos_mod_bound
1.1430 -       zmod_pos_pos_trivial neg_mod_sign neg_mod_bound zmod_neg_neg_trivial)
1.1431 -done
1.1432 -
1.1433 -lemma zmod_mod_trivial [simp]: "(a zmod b) zmod b = a zmod b"
1.1434 -apply (cut_tac a = "intify (a)" and b = "intify (b)" in zmod_mod_trivial_raw)
1.1435 -apply auto
1.1436 -done
1.1437 -
1.1438 -lemma zmod_zadd_left_eq: "(a\$+b) zmod c = ((a zmod c) \$+ b) zmod c"
1.1439 -apply (rule trans [symmetric])
1.1441 -apply (simp (no_asm))
1.1443 -done
1.1444 -
1.1445 -lemma zmod_zadd_right_eq: "(a\$+b) zmod c = (a \$+ (b zmod c)) zmod c"
1.1446 -apply (rule trans [symmetric])
1.1448 -apply (simp (no_asm))
1.1450 -done
1.1451 -
1.1452 -
1.1454 -     "intify(a) \<noteq> #0 ==> (a\$+b) zdiv a = b zdiv a \$+ #1"
1.1456 -
1.1458 -     "intify(a) \<noteq> #0 ==> (b\$+a) zdiv a = b zdiv a \$+ #1"
1.1460 -
1.1461 -lemma zmod_zadd_self1 [simp]: "(a\$+b) zmod a = b zmod a"
1.1462 -apply (case_tac "a = #0")
1.1463 - apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.1465 -done
1.1466 -
1.1467 -lemma zmod_zadd_self2 [simp]: "(b\$+a) zmod a = b zmod a"
1.1468 -apply (case_tac "a = #0")
1.1469 - apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.1471 -done
1.1472 -
1.1473 -
1.1474 -subsection{* proving  a zdiv (b*c) = (a zdiv b) zdiv c *}
1.1475 -
1.1476 -(*The condition c>0 seems necessary.  Consider that 7 zdiv ~6 = ~2 but
1.1477 -  7 zdiv 2 zdiv ~3 = 3 zdiv ~3 = ~1.  The subcase (a zdiv b) zmod c = 0 seems
1.1478 -  to cause particular problems.*)
1.1479 -
1.1480 -(** first, four lemmas to bound the remainder for the cases b<0 and b>0 **)
1.1481 -
1.1482 -lemma zdiv_zmult2_aux1:
1.1483 -     "[| #0 \$< c;  b \$< r;  r \$<= #0 |] ==> b\$*c \$< b\$*(q zmod c) \$+ r"
1.1484 -apply (subgoal_tac "b \$* (c \$- q zmod c) \$< r \$* #1")
1.1486 -apply (rule zle_zless_trans)
1.1487 -apply (erule_tac [2] zmult_zless_mono1)
1.1488 -apply (rule zmult_zle_mono2_neg)
1.1490 -apply (blast intro: zless_imp_zle dest: zless_zle_trans)
1.1491 -done
1.1492 -
1.1493 -lemma zdiv_zmult2_aux2:
1.1494 -     "[| #0 \$< c;   b \$< r;  r \$<= #0 |] ==> b \$* (q zmod c) \$+ r \$<= #0"
1.1495 -apply (subgoal_tac "b \$* (q zmod c) \$<= #0")
1.1496 - prefer 2
1.1497 - apply (simp add: zmult_le_0_iff pos_mod_sign)
1.1498 - apply (blast intro: zless_imp_zle dest: zless_zle_trans)
1.1499 -(*arithmetic*)
1.1501 -apply assumption
1.1503 -done
1.1504 -
1.1505 -lemma zdiv_zmult2_aux3:
1.1506 -     "[| #0 \$< c;  #0 \$<= r;  r \$< b |] ==> #0 \$<= b \$* (q zmod c) \$+ r"
1.1507 -apply (subgoal_tac "#0 \$<= b \$* (q zmod c)")
1.1508 - prefer 2
1.1509 - apply (simp add: int_0_le_mult_iff pos_mod_sign)
1.1510 - apply (blast intro: zless_imp_zle dest: zle_zless_trans)
1.1511 -(*arithmetic*)
1.1513 -apply assumption
1.1515 -done
1.1516 -
1.1517 -lemma zdiv_zmult2_aux4:
1.1518 -     "[| #0 \$< c; #0 \$<= r; r \$< b |] ==> b \$* (q zmod c) \$+ r \$< b \$* c"
1.1519 -apply (subgoal_tac "r \$* #1 \$< b \$* (c \$- q zmod c)")
1.1521 -apply (rule zless_zle_trans)
1.1522 -apply (erule zmult_zless_mono1)
1.1523 -apply (rule_tac [2] zmult_zle_mono2)
1.1525 -apply (blast intro: zless_imp_zle dest: zle_zless_trans)
1.1526 -done
1.1527 -
1.1528 -lemma zdiv_zmult2_lemma:
1.1529 -     "[| quorem (<a,b>, <q,r>);  a \<in> int;  b \<in> int;  b \<noteq> #0;  #0 \$< c |]
1.1530 -      ==> quorem (<a,b\$*c>, <q zdiv c, b\$*(q zmod c) \$+ r>)"
1.1531 -apply (auto simp add: zmult_ac zmod_zdiv_equality [symmetric] quorem_def
1.1532 -               neq_iff_zless int_0_less_mult_iff
1.1533 -               zadd_zmult_distrib2 [symmetric] zdiv_zmult2_aux1 zdiv_zmult2_aux2
1.1534 -               zdiv_zmult2_aux3 zdiv_zmult2_aux4)
1.1535 -apply (blast dest: zless_trans)+
1.1536 -done
1.1537 -
1.1538 -lemma zdiv_zmult2_eq_raw:
1.1539 -     "[|#0 \$< c;  a \<in> int;  b \<in> int|] ==> a zdiv (b\$*c) = (a zdiv b) zdiv c"
1.1540 -apply (case_tac "b = #0")
1.1541 - apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.1542 -apply (rule quorem_div_mod [THEN zdiv_zmult2_lemma, THEN quorem_div])
1.1543 -apply (auto simp add: intify_eq_0_iff_zle)
1.1544 -apply (blast dest: zle_zless_trans)
1.1545 -done
1.1546 -
1.1547 -lemma zdiv_zmult2_eq: "#0 \$< c ==> a zdiv (b\$*c) = (a zdiv b) zdiv c"
1.1548 -apply (cut_tac a = "intify (a)" and b = "intify (b)" in zdiv_zmult2_eq_raw)
1.1549 -apply auto
1.1550 -done
1.1551 -
1.1552 -lemma zmod_zmult2_eq_raw:
1.1553 -     "[|#0 \$< c;  a \<in> int;  b \<in> int|]
1.1554 -      ==> a zmod (b\$*c) = b\$*(a zdiv b zmod c) \$+ a zmod b"
1.1555 -apply (case_tac "b = #0")
1.1556 - apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.1557 -apply (rule quorem_div_mod [THEN zdiv_zmult2_lemma, THEN quorem_mod])
1.1558 -apply (auto simp add: intify_eq_0_iff_zle)
1.1559 -apply (blast dest: zle_zless_trans)
1.1560 -done
1.1561 -
1.1562 -lemma zmod_zmult2_eq:
1.1563 -     "#0 \$< c ==> a zmod (b\$*c) = b\$*(a zdiv b zmod c) \$+ a zmod b"
1.1564 -apply (cut_tac a = "intify (a)" and b = "intify (b)" in zmod_zmult2_eq_raw)
1.1565 -apply auto
1.1566 -done
1.1567 -
1.1568 -subsection{* Cancellation of common factors in "zdiv" *}
1.1569 -
1.1570 -lemma zdiv_zmult_zmult1_aux1:
1.1571 -     "[| #0 \$< b;  intify(c) \<noteq> #0 |] ==> (c\$*a) zdiv (c\$*b) = a zdiv b"
1.1572 -apply (subst zdiv_zmult2_eq)
1.1573 -apply auto
1.1574 -done
1.1575 -
1.1576 -lemma zdiv_zmult_zmult1_aux2:
1.1577 -     "[| b \$< #0;  intify(c) \<noteq> #0 |] ==> (c\$*a) zdiv (c\$*b) = a zdiv b"
1.1578 -apply (subgoal_tac " (c \$* (\$-a)) zdiv (c \$* (\$-b)) = (\$-a) zdiv (\$-b)")
1.1579 -apply (rule_tac [2] zdiv_zmult_zmult1_aux1)
1.1580 -apply auto
1.1581 -done
1.1582 -
1.1583 -lemma zdiv_zmult_zmult1_raw:
1.1584 -     "[|intify(c) \<noteq> #0; b \<in> int|] ==> (c\$*a) zdiv (c\$*b) = a zdiv b"
1.1585 -apply (case_tac "b = #0")
1.1586 - apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.1587 -apply (auto simp add: neq_iff_zless [of b]
1.1588 -  zdiv_zmult_zmult1_aux1 zdiv_zmult_zmult1_aux2)
1.1589 -done
1.1590 -
1.1591 -lemma zdiv_zmult_zmult1: "intify(c) \<noteq> #0 ==> (c\$*a) zdiv (c\$*b) = a zdiv b"
1.1592 -apply (cut_tac b = "intify (b)" in zdiv_zmult_zmult1_raw)
1.1593 -apply auto
1.1594 -done
1.1595 -
1.1596 -lemma zdiv_zmult_zmult2: "intify(c) \<noteq> #0 ==> (a\$*c) zdiv (b\$*c) = a zdiv b"
1.1597 -apply (drule zdiv_zmult_zmult1)
1.1598 -apply (auto simp add: zmult_commute)
1.1599 -done
1.1600 -
1.1601 -
1.1602 -subsection{* Distribution of factors over "zmod" *}
1.1603 -
1.1604 -lemma zmod_zmult_zmult1_aux1:
1.1605 -     "[| #0 \$< b;  intify(c) \<noteq> #0 |]
1.1606 -      ==> (c\$*a) zmod (c\$*b) = c \$* (a zmod b)"
1.1607 -apply (subst zmod_zmult2_eq)
1.1608 -apply auto
1.1609 -done
1.1610 -
1.1611 -lemma zmod_zmult_zmult1_aux2:
1.1612 -     "[| b \$< #0;  intify(c) \<noteq> #0 |]
1.1613 -      ==> (c\$*a) zmod (c\$*b) = c \$* (a zmod b)"
1.1614 -apply (subgoal_tac " (c \$* (\$-a)) zmod (c \$* (\$-b)) = c \$* ((\$-a) zmod (\$-b))")
1.1615 -apply (rule_tac [2] zmod_zmult_zmult1_aux1)
1.1616 -apply auto
1.1617 -done
1.1618 -
1.1619 -lemma zmod_zmult_zmult1_raw:
1.1620 -     "[|b \<in> int; c \<in> int|] ==> (c\$*a) zmod (c\$*b) = c \$* (a zmod b)"
1.1621 -apply (case_tac "b = #0")
1.1622 - apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.1623 -apply (case_tac "c = #0")
1.1624 - apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
1.1625 -apply (auto simp add: neq_iff_zless [of b]
1.1626 -  zmod_zmult_zmult1_aux1 zmod_zmult_zmult1_aux2)
1.1627 -done
1.1628 -
1.1629 -lemma zmod_zmult_zmult1: "(c\$*a) zmod (c\$*b) = c \$* (a zmod b)"
1.1630 -apply (cut_tac b = "intify (b)" and c = "intify (c)" in zmod_zmult_zmult1_raw)
1.1631 -apply auto
1.1632 -done
1.1633 -
1.1634 -lemma zmod_zmult_zmult2: "(a\$*c) zmod (b\$*c) = (a zmod b) \$* c"
1.1635 -apply (cut_tac c = "c" in zmod_zmult_zmult1)
1.1636 -apply (auto simp add: zmult_commute)
1.1637 -done
1.1638 -
1.1639 -
1.1640 -(** Quotients of signs **)
1.1641 -
1.1642 -lemma zdiv_neg_pos_less0: "[| a \$< #0;  #0 \$< b |] ==> a zdiv b \$< #0"
1.1643 -apply (subgoal_tac "a zdiv b \$<= #-1")
1.1644 -apply (erule zle_zless_trans)
1.1645 -apply (simp (no_asm))
1.1646 -apply (rule zle_trans)
1.1647 -apply (rule_tac a' = "#-1" in zdiv_mono1)
1.1648 -apply (rule zless_add1_iff_zle [THEN iffD1])
1.1649 -apply (simp (no_asm))
1.1650 -apply (auto simp add: zdiv_minus1)
1.1651 -done
1.1652 -
1.1653 -lemma zdiv_nonneg_neg_le0: "[| #0 \$<= a;  b \$< #0 |] ==> a zdiv b \$<= #0"
1.1654 -apply (drule zdiv_mono1_neg)
1.1655 -apply auto
1.1656 -done
1.1657 -
1.1658 -lemma pos_imp_zdiv_nonneg_iff: "#0 \$< b ==> (#0 \$<= a zdiv b) <-> (#0 \$<= a)"
1.1659 -apply auto
1.1660 -apply (drule_tac [2] zdiv_mono1)
1.1661 -apply (auto simp add: neq_iff_zless)
1.1662 -apply (simp (no_asm_use) add: not_zless_iff_zle [THEN iff_sym])
1.1663 -apply (blast intro: zdiv_neg_pos_less0)
1.1664 -done
1.1665 -
1.1666 -lemma neg_imp_zdiv_nonneg_iff: "b \$< #0 ==> (#0 \$<= a zdiv b) <-> (a \$<= #0)"
1.1667 -apply (subst zdiv_zminus_zminus [symmetric])
1.1668 -apply (rule iff_trans)
1.1669 -apply (rule pos_imp_zdiv_nonneg_iff)
1.1670 -apply auto
1.1671 -done
1.1672 -
1.1673 -(*But not (a zdiv b \$<= 0 iff a\$<=0); consider a=1, b=2 when a zdiv b = 0.*)
1.1674 -lemma pos_imp_zdiv_neg_iff: "#0 \$< b ==> (a zdiv b \$< #0) <-> (a \$< #0)"
1.1675 -apply (simp (no_asm_simp) add: not_zle_iff_zless [THEN iff_sym])
1.1676 -apply (erule pos_imp_zdiv_nonneg_iff)
1.1677 -done
1.1678 -
1.1679 -(*Again the law fails for \$<=: consider a = -1, b = -2 when a zdiv b = 0*)
1.1680 -lemma neg_imp_zdiv_neg_iff: "b \$< #0 ==> (a zdiv b \$< #0) <-> (#0 \$< a)"
1.1681 -apply (simp (no_asm_simp) add: not_zle_iff_zless [THEN iff_sym])
1.1682 -apply (erule neg_imp_zdiv_nonneg_iff)
1.1683 -done
1.1684 -
1.1685 -(*
1.1686 - THESE REMAIN TO BE CONVERTED -- but aren't that useful!
1.1687 -
1.1688 - subsection{* Speeding up the division algorithm with shifting *}
1.1689 -
1.1690 - (** computing "zdiv" by shifting **)
1.1691 -
1.1692 - lemma pos_zdiv_mult_2: "#0 \$<= a ==> (#1 \$+ #2\$*b) zdiv (#2\$*a) = b zdiv a"
1.1693 - apply (case_tac "a = #0")
1.1694 - apply (subgoal_tac "#1 \$<= a")
1.1695 -  apply (arith_tac 2)
1.1696 - apply (subgoal_tac "#1 \$< a \$* #2")
1.1697 -  apply (arith_tac 2)
1.1698 - apply (subgoal_tac "#2\$* (#1 \$+ b zmod a) \$<= #2\$*a")
1.1699 -  apply (rule_tac [2] zmult_zle_mono2)
1.1702 - apply (simp (no_asm_simp) add: zdiv_zmult_zmult2 zmod_zmult_zmult2 zdiv_pos_pos_trivial)
1.1703 - apply (subst zdiv_pos_pos_trivial)
1.1704 - apply (simp (no_asm_simp) add: [zmod_pos_pos_trivial pos_mod_sign [THEN zadd_zle_mono1] RSN (2,zle_trans) ])
1.1705 - apply (auto simp add: zmod_pos_pos_trivial)
1.1706 - apply (subgoal_tac "#0 \$<= b zmod a")
1.1707 -  apply (asm_simp_tac (simpset () add: pos_mod_sign) 2)
1.1708 - apply arith
1.1709 - done
1.1710 -
1.1711 -
1.1712 - lemma neg_zdiv_mult_2: "a \$<= #0 ==> (#1 \$+ #2\$*b) zdiv (#2\$*a) <-> (b\$+#1) zdiv a"
1.1713 - apply (subgoal_tac " (#1 \$+ #2\$* (\$-b-#1)) zdiv (#2 \$* (\$-a)) <-> (\$-b-#1) zdiv (\$-a)")
1.1714 - apply (rule_tac [2] pos_zdiv_mult_2)
1.1715 - apply (auto simp add: zmult_zminus_right)
1.1716 - apply (subgoal_tac " (#-1 - (#2 \$* b)) = - (#1 \$+ (#2 \$* b))")
1.1717 - apply (Simp_tac 2)
1.1719 - done
1.1720 -
1.1721 -
1.1722 - (*Not clear why this must be proved separately; probably integ_of causes
1.1723 -   simplification problems*)
1.1724 - lemma lemma: "~ #0 \$<= x ==> x \$<= #0"
1.1725 - apply auto
1.1726 - done
1.1727 -
1.1728 - lemma zdiv_integ_of_BIT: "integ_of (v BIT b) zdiv integ_of (w BIT False) =
1.1729 -           (if ~b | #0 \$<= integ_of w
1.1730 -            then integ_of v zdiv (integ_of w)
1.1731 -            else (integ_of v \$+ #1) zdiv (integ_of w))"
1.1733 - apply (simp (no_asm_simp) del: bin_arith_extra_simps@bin_rel_simps add: zdiv_zmult_zmult1 pos_zdiv_mult_2 lemma neg_zdiv_mult_2)
1.1734 - done
1.1735 -
1.1736 - declare zdiv_integ_of_BIT [simp]
1.1737 -
1.1738 -
1.1739 - (** computing "zmod" by shifting (proofs resemble those for "zdiv") **)
1.1740 -
1.1741 - lemma pos_zmod_mult_2: "#0 \$<= a ==> (#1 \$+ #2\$*b) zmod (#2\$*a) = #1 \$+ #2 \$* (b zmod a)"
1.1742 - apply (case_tac "a = #0")
1.1743 - apply (subgoal_tac "#1 \$<= a")
1.1744 -  apply (arith_tac 2)
1.1745 - apply (subgoal_tac "#1 \$< a \$* #2")
1.1746 -  apply (arith_tac 2)
1.1747 - apply (subgoal_tac "#2\$* (#1 \$+ b zmod a) \$<= #2\$*a")
1.1748 -  apply (rule_tac [2] zmult_zle_mono2)
1.1751 - apply (simp (no_asm_simp) add: zmod_zmult_zmult2 zmod_pos_pos_trivial)
1.1752 - apply (rule zmod_pos_pos_trivial)
1.1753 - apply (simp (no_asm_simp) # add: [zmod_pos_pos_trivial pos_mod_sign [THEN zadd_zle_mono1] RSN (2,zle_trans) ])
1.1754 - apply (auto simp add: zmod_pos_pos_trivial)
1.1755 - apply (subgoal_tac "#0 \$<= b zmod a")
1.1756 -  apply (asm_simp_tac (simpset () add: pos_mod_sign) 2)
1.1757 - apply arith
1.1758 - done
1.1759 -
1.1760 -
1.1761 - lemma neg_zmod_mult_2: "a \$<= #0 ==> (#1 \$+ #2\$*b) zmod (#2\$*a) = #2 \$* ((b\$+#1) zmod a) - #1"
1.1762 - apply (subgoal_tac " (#1 \$+ #2\$* (\$-b-#1)) zmod (#2\$* (\$-a)) = #1 \$+ #2\$* ((\$-b-#1) zmod (\$-a))")
1.1763 - apply (rule_tac [2] pos_zmod_mult_2)
1.1764 - apply (auto simp add: zmult_zminus_right)
1.1765 - apply (subgoal_tac " (#-1 - (#2 \$* b)) = - (#1 \$+ (#2 \$* b))")
1.1766 - apply (Simp_tac 2)
1.1768 - apply (dtac (zminus_equation [THEN iffD1, symmetric])
1.1769 - apply auto
1.1770 - done
1.1771 -
1.1772 - lemma zmod_integ_of_BIT: "integ_of (v BIT b) zmod integ_of (w BIT False) =
1.1773 -           (if b then
1.1774 -                 if #0 \$<= integ_of w
1.1775 -                 then #2 \$* (integ_of v zmod integ_of w) \$+ #1
1.1776 -                 else #2 \$* ((integ_of v \$+ #1) zmod integ_of w) - #1
1.1777 -            else #2 \$* (integ_of v zmod integ_of w))"
1.1779 - apply (simp (no_asm_simp) del: bin_arith_extra_simps@bin_rel_simps add: zmod_zmult_zmult1 pos_zmod_mult_2 lemma neg_zmod_mult_2)
1.1780 - done
1.1781 -
1.1782 - declare zmod_integ_of_BIT [simp]
1.1783 -*)
1.1784 -
1.1785 -ML{*
1.1790 -val zero_lt_zmagnitude = thm "zero_lt_zmagnitude";
1.1796 -val zmult_zle_mono1 = thm "zmult_zle_mono1";
1.1797 -val zmult_zle_mono1_neg = thm "zmult_zle_mono1_neg";
1.1798 -val zmult_zle_mono2 = thm "zmult_zle_mono2";
1.1799 -val zmult_zle_mono2_neg = thm "zmult_zle_mono2_neg";
1.1800 -val zmult_zle_mono = thm "zmult_zle_mono";
1.1801 -val zmult_zless_mono2 = thm "zmult_zless_mono2";
1.1802 -val zmult_zless_mono1 = thm "zmult_zless_mono1";
1.1803 -val zmult_zless_mono = thm "zmult_zless_mono";
1.1804 -val zmult_zless_mono1_neg = thm "zmult_zless_mono1_neg";
1.1805 -val zmult_zless_mono2_neg = thm "zmult_zless_mono2_neg";
1.1806 -val zmult_eq_0_iff = thm "zmult_eq_0_iff";
1.1807 -val zmult_zless_cancel2 = thm "zmult_zless_cancel2";
1.1808 -val zmult_zless_cancel1 = thm "zmult_zless_cancel1";
1.1809 -val zmult_zle_cancel2 = thm "zmult_zle_cancel2";
1.1810 -val zmult_zle_cancel1 = thm "zmult_zle_cancel1";
1.1811 -val int_eq_iff_zle = thm "int_eq_iff_zle";
1.1812 -val zmult_cancel2 = thm "zmult_cancel2";
1.1813 -val zmult_cancel1 = thm "zmult_cancel1";
1.1814 -val unique_quotient = thm "unique_quotient";
1.1815 -val unique_remainder = thm "unique_remainder";
1.1817 -val posDivAlg_termination = thm "posDivAlg_termination";
1.1818 -val posDivAlg_unfold = thm "posDivAlg_unfold";
1.1819 -val posDivAlg_eqn = thm "posDivAlg_eqn";
1.1820 -val posDivAlg_induct = thm "posDivAlg_induct";
1.1821 -val intify_eq_0_iff_zle = thm "intify_eq_0_iff_zle";
1.1822 -val zmult_pos = thm "zmult_pos";
1.1823 -val zmult_neg = thm "zmult_neg";
1.1824 -val zmult_pos_neg = thm "zmult_pos_neg";
1.1825 -val int_0_less_mult_iff = thm "int_0_less_mult_iff";
1.1826 -val int_0_le_mult_iff = thm "int_0_le_mult_iff";
1.1827 -val zmult_less_0_iff = thm "zmult_less_0_iff";
1.1828 -val zmult_le_0_iff = thm "zmult_le_0_iff";
1.1829 -val posDivAlg_type = thm "posDivAlg_type";
1.1830 -val posDivAlg_correct = thm "posDivAlg_correct";
1.1831 -val negDivAlg_termination = thm "negDivAlg_termination";
1.1832 -val negDivAlg_unfold = thm "negDivAlg_unfold";
1.1833 -val negDivAlg_eqn = thm "negDivAlg_eqn";
1.1834 -val negDivAlg_induct = thm "negDivAlg_induct";
1.1835 -val negDivAlg_type = thm "negDivAlg_type";
1.1836 -val negDivAlg_correct = thm "negDivAlg_correct";
1.1837 -val quorem_0 = thm "quorem_0";
1.1838 -val posDivAlg_zero_divisor = thm "posDivAlg_zero_divisor";
1.1839 -val posDivAlg_0 = thm "posDivAlg_0";
1.1840 -val negDivAlg_minus1 = thm "negDivAlg_minus1";
1.1841 -val negateSnd_eq = thm "negateSnd_eq";
1.1842 -val negateSnd_type = thm "negateSnd_type";
1.1843 -val quorem_neg = thm "quorem_neg";
1.1844 -val divAlg_correct = thm "divAlg_correct";
1.1845 -val divAlg_type = thm "divAlg_type";
1.1846 -val zdiv_intify1 = thm "zdiv_intify1";
1.1847 -val zdiv_intify2 = thm "zdiv_intify2";
1.1848 -val zdiv_type = thm "zdiv_type";
1.1849 -val zmod_intify1 = thm "zmod_intify1";
1.1850 -val zmod_intify2 = thm "zmod_intify2";
1.1851 -val zmod_type = thm "zmod_type";
1.1852 -val DIVISION_BY_ZERO_ZDIV = thm "DIVISION_BY_ZERO_ZDIV";
1.1853 -val DIVISION_BY_ZERO_ZMOD = thm "DIVISION_BY_ZERO_ZMOD";
1.1854 -val zmod_zdiv_equality = thm "zmod_zdiv_equality";
1.1855 -val pos_mod = thm "pos_mod";
1.1856 -val pos_mod_sign = thm "pos_mod_sign";
1.1857 -val neg_mod = thm "neg_mod";
1.1858 -val neg_mod_sign = thm "neg_mod_sign";
1.1859 -val quorem_div_mod = thm "quorem_div_mod";
1.1860 -val quorem_div = thm "quorem_div";
1.1861 -val quorem_mod = thm "quorem_mod";
1.1862 -val zdiv_pos_pos_trivial = thm "zdiv_pos_pos_trivial";
1.1863 -val zdiv_neg_neg_trivial = thm "zdiv_neg_neg_trivial";
1.1864 -val zdiv_pos_neg_trivial = thm "zdiv_pos_neg_trivial";
1.1865 -val zmod_pos_pos_trivial = thm "zmod_pos_pos_trivial";
1.1866 -val zmod_neg_neg_trivial = thm "zmod_neg_neg_trivial";
1.1867 -val zmod_pos_neg_trivial = thm "zmod_pos_neg_trivial";
1.1868 -val zdiv_zminus_zminus = thm "zdiv_zminus_zminus";
1.1869 -val zmod_zminus_zminus = thm "zmod_zminus_zminus";
1.1870 -val self_quotient = thm "self_quotient";
1.1871 -val self_remainder = thm "self_remainder";
1.1872 -val zdiv_self = thm "zdiv_self";
1.1873 -val zmod_self = thm "zmod_self";
1.1874 -val zdiv_zero = thm "zdiv_zero";
1.1875 -val zdiv_eq_minus1 = thm "zdiv_eq_minus1";
1.1876 -val zmod_zero = thm "zmod_zero";
1.1877 -val zdiv_minus1 = thm "zdiv_minus1";
1.1878 -val zmod_minus1 = thm "zmod_minus1";
1.1879 -val zdiv_pos_pos = thm "zdiv_pos_pos";
1.1880 -val zmod_pos_pos = thm "zmod_pos_pos";
1.1881 -val zdiv_neg_pos = thm "zdiv_neg_pos";
1.1882 -val zmod_neg_pos = thm "zmod_neg_pos";
1.1883 -val zdiv_pos_neg = thm "zdiv_pos_neg";
1.1884 -val zmod_pos_neg = thm "zmod_pos_neg";
1.1885 -val zdiv_neg_neg = thm "zdiv_neg_neg";
1.1886 -val zmod_neg_neg = thm "zmod_neg_neg";
1.1887 -val zmod_1 = thm "zmod_1";
1.1888 -val zdiv_1 = thm "zdiv_1";
1.1889 -val zmod_minus1_right = thm "zmod_minus1_right";
1.1890 -val zdiv_minus1_right = thm "zdiv_minus1_right";
1.1891 -val zdiv_mono1 = thm "zdiv_mono1";
1.1892 -val zdiv_mono1_neg = thm "zdiv_mono1_neg";
1.1893 -val zdiv_mono2 = thm "zdiv_mono2";
1.1894 -val zdiv_mono2_neg = thm "zdiv_mono2_neg";
1.1895 -val zdiv_zmult1_eq = thm "zdiv_zmult1_eq";
1.1896 -val zmod_zmult1_eq = thm "zmod_zmult1_eq";
1.1897 -val zmod_zmult1_eq' = thm "zmod_zmult1_eq'";
1.1898 -val zmod_zmult_distrib = thm "zmod_zmult_distrib";
1.1899 -val zdiv_zmult_self1 = thm "zdiv_zmult_self1";
1.1900 -val zdiv_zmult_self2 = thm "zdiv_zmult_self2";
1.1901 -val zmod_zmult_self1 = thm "zmod_zmult_self1";
1.1902 -val zmod_zmult_self2 = thm "zmod_zmult_self2";
1.1905 -val zmod_div_trivial = thm "zmod_div_trivial";
1.1906 -val zmod_mod_trivial = thm "zmod_mod_trivial";
1.1913 -val zdiv_zmult2_eq = thm "zdiv_zmult2_eq";
1.1914 -val zmod_zmult2_eq = thm "zmod_zmult2_eq";
1.1915 -val zdiv_zmult_zmult1 = thm "zdiv_zmult_zmult1";
1.1916 -val zdiv_zmult_zmult2 = thm "zdiv_zmult_zmult2";
1.1917 -val zmod_zmult_zmult1 = thm "zmod_zmult_zmult1";
1.1918 -val zmod_zmult_zmult2 = thm "zmod_zmult_zmult2";
1.1919 -val zdiv_neg_pos_less0 = thm "zdiv_neg_pos_less0";
1.1920 -val zdiv_nonneg_neg_le0 = thm "zdiv_nonneg_neg_le0";
1.1921 -val pos_imp_zdiv_nonneg_iff = thm "pos_imp_zdiv_nonneg_iff";
1.1922 -val neg_imp_zdiv_nonneg_iff = thm "neg_imp_zdiv_nonneg_iff";
1.1923 -val pos_imp_zdiv_neg_iff = thm "pos_imp_zdiv_neg_iff";
1.1924 -val neg_imp_zdiv_neg_iff = thm "neg_imp_zdiv_neg_iff";
1.1925 -*}
1.1926 -
1.1927 -end
1.1928 -
```