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.117 -lemma zneg_or_0_add_zneg_or_0_imp_zneg_or_0:
   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.137 -lemma zless_add_succ_iff:
   1.138 -     "(w $< z $+ $# succ(m)) <-> (w $< z $+ $#m | intify(w) = z $+ $#m)"
   1.139 -apply (auto simp add: zless_iff_succ_zadd zadd_assoc int_of_add [symmetric])
   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.150 -lemma zadd_succ_lemma:
   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.172 -apply (simp only: zadd_succ_zle_iff)
   1.173 -apply auto
   1.174 -done
   1.175 -
   1.176 -lemma add1_left_zle_iff: "(#1 $+ w $<= z) <-> (w $< z)"
   1.177 -apply (subst zadd_commute)
   1.178 -apply (rule add1_zle_iff)
   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.187 -apply (simp_all (no_asm_simp) add: zadd_zmult_distrib2 zadd_zle_mono)
   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.207 -apply (simp_all add: zmult_commute)
   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.212 -apply (simp_all add: zmult_commute)
   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.233 -apply (simp_all add: zadd_zmult_distrib zadd_zless_mono zle_def)
   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.237 -apply (rule zadd_zless_mono)
   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.247 -apply (simp add: znegative_iff_zless_0)
   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.254 -apply (simp_all add: zmult_commute)
   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.289 -apply (simp add: zmult_eq_lemma)
   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.355 - prefer 2 apply (simp add: zdiff_zmult_distrib2 zadd_ac zcompare_rls)
   1.356 -apply (subgoal_tac "#0 $< b $* (#1 $+ q $- q') ")
   1.357 - prefer 2
   1.358 - apply (erule zle_zless_trans)
   1.359 - apply (simp add: zdiff_zmult_distrib2 zadd_zmult_distrib2 zadd_ac zcompare_rls)
   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.364 - apply (simp add: zdiff_zmult_distrib2 zadd_zmult_distrib2 zadd_ac zcompare_rls)
   1.365 -apply (auto elim: zless_asym
   1.366 -        simp add: zmult_zless_cancel1 zless_add1_iff_zle zadd_ac zcompare_rls)
   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.375 -            simp add: zminus_zadd_distrib [symmetric] zle_zminus zless_zminus)
   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.396 -apply (simp add: quorem_def)
   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.403 -lemma adjust_eq [simp]:
   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.407 -by (simp add: Let_def adjust_def)
   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.414 -apply (simp add: not_zless_iff_zle zless_add1_iff_zle zcompare_rls)
   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.534 - apply (simp add: posDivAlg_eqn adjust_def integ_of_type 
   1.535 -             split add: split_if_asm)
   1.536 - apply clarify
   1.537 - apply (simp add: int_0_less_mult_iff not_zle_iff_zless)
   1.538 -apply (simp add: not_zless_iff_zle)
   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.559 -apply (simp_all add: int_0_less_mult_iff)
   1.560 -apply (auto simp add: zadd_zmult_distrib2 Let_def)
   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.626 - apply (simp add: negDivAlg_eqn adjust_def integ_of_type 
   1.627 -             split add: split_if_asm)
   1.628 - apply clarify
   1.629 - apply (simp add: int_0_less_mult_iff not_zle_iff_zless)
   1.630 -apply (simp add: not_zless_iff_zle)
   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.653 -apply (simp_all add: int_0_less_mult_iff)
   1.654 -apply (auto simp add: zadd_zmult_distrib2 Let_def)
   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.673 -apply (simp add: not_zle_iff_zless)
   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.679 -apply (simp add: not_zle_iff_zless)
   1.680 -apply (drule zminus_zless_zminus [THEN iffD2])
   1.681 -apply (simp add: zadd_commute zless_add1_iff_zle zle_zminus)
   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.959 -apply (simp add: int_0_less_mult_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.964 -apply (simp add: zcompare_rls)
   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.971 -apply (simp add: zdiff_zmult_distrib2)
   1.972 -apply (drule_tac t = "%x. x $- a $* q" in subst_context)
   1.973 -apply (simp add: zcompare_rls)
   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.989 -  simp add: zadd_commute zmult_zminus)+
   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.1194 -apply (simp add: zadd_zmult_distrib2)
  1.1195 -apply (erule zle_zless_trans)
  1.1196 -apply (erule zadd_zless_mono2)
  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.1209 -apply (simp (no_asm_simp) add: zadd_zmult_distrib2)
  1.1210 -apply (subst zadd_commute [of "b $\<times> q'"], rule zadd_zless_mono)
  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.1214 -apply (rule zadd_zless_mono)
  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.1244 -apply (simp add: zmult_less_0_iff)
  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.1260 -apply (simp (no_asm_simp) add: zadd_zmult_distrib2)
  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.1272 -apply (simp (no_asm_use) add: zadd_commute)
  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.1307 -apply (auto simp add: split_ifs quorem_def neq_iff_zless zadd_zmult_distrib2
  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.1371 -lemma zadd1_lemma:
  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.1375 -apply (auto simp add: split_ifs quorem_def neq_iff_zless zadd_zmult_distrib2
  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.1381 -lemma zdiv_zadd1_eq_raw:
  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.1390 -lemma zdiv_zadd1_eq:
  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.1393 -       in zdiv_zadd1_eq_raw)
  1.1394 -apply auto
  1.1395 -done
  1.1396 -
  1.1397 -lemma zmod_zadd1_eq_raw:
  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.1408 -       in zmod_zadd1_eq_raw)
  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.1440 -apply (rule zmod_zadd1_eq)
  1.1441 -apply (simp (no_asm))
  1.1442 -apply (rule zmod_zadd1_eq [symmetric])
  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.1447 -apply (rule zmod_zadd1_eq)
  1.1448 -apply (simp (no_asm))
  1.1449 -apply (rule zmod_zadd1_eq [symmetric])
  1.1450 -done
  1.1451 -
  1.1452 -
  1.1453 -lemma zdiv_zadd_self1 [simp]:
  1.1454 -     "intify(a) \<noteq> #0 ==> (a$+b) zdiv a = b zdiv a $+ #1"
  1.1455 -by (simp (no_asm_simp) add: zdiv_zadd1_eq)
  1.1456 -
  1.1457 -lemma zdiv_zadd_self2 [simp]:
  1.1458 -     "intify(a) \<noteq> #0 ==> (b$+a) zdiv a = b zdiv a $+ #1"
  1.1459 -by (simp (no_asm_simp) add: zdiv_zadd1_eq)
  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.1464 -apply (simp (no_asm_simp) add: zmod_zadd1_eq)
  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.1470 -apply (simp (no_asm_simp) add: zmod_zadd1_eq)
  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.1485 -apply (simp add: zdiff_zmult_distrib2 zadd_commute zcompare_rls)
  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.1489 -apply (auto simp add: zcompare_rls zadd_commute add1_zle_iff pos_mod_bound)
  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.1500 -apply (drule zadd_zle_mono)
  1.1501 -apply assumption
  1.1502 -apply (simp add: zadd_commute)
  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.1512 -apply (drule zadd_zle_mono)
  1.1513 -apply assumption
  1.1514 -apply (simp add: zadd_commute)
  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.1520 -apply (simp add: zdiff_zmult_distrib2 zadd_commute zcompare_rls)
  1.1521 -apply (rule zless_zle_trans)
  1.1522 -apply (erule zmult_zless_mono1)
  1.1523 -apply (rule_tac [2] zmult_zle_mono2)
  1.1524 -apply (auto simp add: zcompare_rls zadd_commute add1_zle_iff pos_mod_bound)
  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.1700 - apply (auto simp add: zadd_commute zmult_commute add1_zle_iff pos_mod_bound)
  1.1701 - apply (subst zdiv_zadd1_eq)
  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.1718 - apply (asm_full_simp_tac (HOL_ss add: zdiv_zminus_zminus zdiff_def zminus_zadd_distrib [symmetric])
  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.1732 - apply (simp_tac (simpset_of Int.thy add: zadd_assoc integ_of_BIT)
  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.1749 - apply (auto simp add: zadd_commute zmult_commute add1_zle_iff pos_mod_bound)
  1.1750 - apply (subst zmod_zadd1_eq)
  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.1767 - apply (asm_full_simp_tac (HOL_ss add: zmod_zminus_zminus zdiff_def zminus_zadd_distrib [symmetric])
  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.1778 - apply (simp_tac (simpset_of Int.thy add: zadd_assoc integ_of_BIT)
  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.1786 -val zspos_add_zspos_imp_zspos = thm "zspos_add_zspos_imp_zspos";
  1.1787 -val zpos_add_zpos_imp_zpos = thm "zpos_add_zpos_imp_zpos";
  1.1788 -val zneg_add_zneg_imp_zneg = thm "zneg_add_zneg_imp_zneg";
  1.1789 -val zneg_or_0_add_zneg_or_0_imp_zneg_or_0 = thm "zneg_or_0_add_zneg_or_0_imp_zneg_or_0";
  1.1790 -val zero_lt_zmagnitude = thm "zero_lt_zmagnitude";
  1.1791 -val zless_add_succ_iff = thm "zless_add_succ_iff";
  1.1792 -val zadd_succ_zle_iff = thm "zadd_succ_zle_iff";
  1.1793 -val zless_add1_iff_zle = thm "zless_add1_iff_zle";
  1.1794 -val add1_zle_iff = thm "add1_zle_iff";
  1.1795 -val add1_left_zle_iff = thm "add1_left_zle_iff";
  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.1816 -val adjust_eq = thm "adjust_eq";
  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.1903 -val zdiv_zadd1_eq = thm "zdiv_zadd1_eq";
  1.1904 -val zmod_zadd1_eq = thm "zmod_zadd1_eq";
  1.1905 -val zmod_div_trivial = thm "zmod_div_trivial";
  1.1906 -val zmod_mod_trivial = thm "zmod_mod_trivial";
  1.1907 -val zmod_zadd_left_eq = thm "zmod_zadd_left_eq";
  1.1908 -val zmod_zadd_right_eq = thm "zmod_zadd_right_eq";
  1.1909 -val zdiv_zadd_self1 = thm "zdiv_zadd_self1";
  1.1910 -val zdiv_zadd_self2 = thm "zdiv_zadd_self2";
  1.1911 -val zmod_zadd_self1 = thm "zmod_zadd_self1";
  1.1912 -val zmod_zadd_self2 = thm "zmod_zadd_self2";
  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 -