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