src/ZF/IntDiv.thy
author wenzelm
Tue Jul 31 19:40:22 2007 +0200 (2007-07-31)
changeset 24091 109f19a13872
parent 23146 0bc590051d95
child 24893 b8ef7afe3a6b
permissions -rw-r--r--
added Tools/lin_arith.ML;
     1 (*  Title:      ZF/IntDiv.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1999  University of Cambridge
     5 
     6 Here is the division algorithm in ML:
     7 
     8     fun posDivAlg (a,b) =
     9       if a<b then (0,a)
    10       else let val (q,r) = posDivAlg(a, 2*b)
    11 	       in  if 0<=r-b then (2*q+1, r-b) else (2*q, r)
    12 	   end
    13 
    14     fun negDivAlg (a,b) =
    15       if 0<=a+b then (~1,a+b)
    16       else let val (q,r) = negDivAlg(a, 2*b)
    17 	       in  if 0<=r-b then (2*q+1, r-b) else (2*q, r)
    18 	   end;
    19 
    20     fun negateSnd (q,r:int) = (q,~r);
    21 
    22     fun divAlg (a,b) = if 0<=a then 
    23 			  if b>0 then posDivAlg (a,b) 
    24 			   else if a=0 then (0,0)
    25 				else negateSnd (negDivAlg (~a,~b))
    26 		       else 
    27 			  if 0<b then negDivAlg (a,b)
    28 			  else        negateSnd (posDivAlg (~a,~b));
    29 
    30 *)
    31 
    32 header{*The Division Operators Div and Mod*}
    33 
    34 theory IntDiv imports IntArith OrderArith begin
    35 
    36 constdefs
    37   quorem :: "[i,i] => o"
    38     "quorem == %<a,b> <q,r>.
    39                       a = b$*q $+ r &
    40                       (#0$<b & #0$<=r & r$<b | ~(#0$<b) & b$<r & r $<= #0)"
    41 
    42   adjust :: "[i,i] => i"
    43     "adjust(b) == %<q,r>. if #0 $<= r$-b then <#2$*q $+ #1,r$-b>
    44                           else <#2$*q,r>"
    45 
    46 
    47 (** the division algorithm **)
    48 
    49 constdefs posDivAlg :: "i => i"
    50 (*for the case a>=0, b>0*)
    51 (*recdef posDivAlg "inv_image less_than (%(a,b). nat_of(a $- b $+ #1))"*)
    52     "posDivAlg(ab) ==
    53        wfrec(measure(int*int, %<a,b>. nat_of (a $- b $+ #1)),
    54 	     ab,
    55 	     %<a,b> f. if (a$<b | b$<=#0) then <#0,a>
    56                        else adjust(b, f ` <a,#2$*b>))"
    57 
    58 
    59 (*for the case a<0, b>0*)
    60 constdefs negDivAlg :: "i => i"
    61 (*recdef negDivAlg "inv_image less_than (%(a,b). nat_of(- a $- b))"*)
    62     "negDivAlg(ab) ==
    63        wfrec(measure(int*int, %<a,b>. nat_of ($- a $- b)),
    64 	     ab,
    65 	     %<a,b> f. if (#0 $<= a$+b | b$<=#0) then <#-1,a$+b>
    66                        else adjust(b, f ` <a,#2$*b>))"
    67 
    68 (*for the general case b\<noteq>0*)
    69 
    70 constdefs
    71   negateSnd :: "i => i"
    72     "negateSnd == %<q,r>. <q, $-r>"
    73 
    74   (*The full division algorithm considers all possible signs for a, b
    75     including the special case a=0, b<0, because negDivAlg requires a<0*)
    76   divAlg :: "i => i"
    77     "divAlg ==
    78        %<a,b>. if #0 $<= a then
    79                   if #0 $<= b then posDivAlg (<a,b>)
    80                   else if a=#0 then <#0,#0>
    81                        else negateSnd (negDivAlg (<$-a,$-b>))
    82                else 
    83                   if #0$<b then negDivAlg (<a,b>)
    84                   else         negateSnd (posDivAlg (<$-a,$-b>))"
    85 
    86   zdiv  :: "[i,i]=>i"                    (infixl "zdiv" 70) 
    87     "a zdiv b == fst (divAlg (<intify(a), intify(b)>))"
    88 
    89   zmod  :: "[i,i]=>i"                    (infixl "zmod" 70)
    90     "a zmod b == snd (divAlg (<intify(a), intify(b)>))"
    91 
    92 
    93 (** Some basic laws by Sidi Ehmety (need linear arithmetic!) **)
    94 
    95 lemma zspos_add_zspos_imp_zspos: "[| #0 $< x;  #0 $< y |] ==> #0 $< x $+ y"
    96 apply (rule_tac y = "y" in zless_trans)
    97 apply (rule_tac [2] zdiff_zless_iff [THEN iffD1])
    98 apply auto
    99 done
   100 
   101 lemma zpos_add_zpos_imp_zpos: "[| #0 $<= x;  #0 $<= y |] ==> #0 $<= x $+ y"
   102 apply (rule_tac y = "y" in zle_trans)
   103 apply (rule_tac [2] zdiff_zle_iff [THEN iffD1])
   104 apply auto
   105 done
   106 
   107 lemma zneg_add_zneg_imp_zneg: "[| x $< #0;  y $< #0 |] ==> x $+ y $< #0"
   108 apply (rule_tac y = "y" in zless_trans)
   109 apply (rule zless_zdiff_iff [THEN iffD1])
   110 apply auto
   111 done
   112 
   113 (* this theorem is used below *)
   114 lemma zneg_or_0_add_zneg_or_0_imp_zneg_or_0:
   115      "[| x $<= #0;  y $<= #0 |] ==> x $+ y $<= #0"
   116 apply (rule_tac y = "y" in zle_trans)
   117 apply (rule zle_zdiff_iff [THEN iffD1])
   118 apply auto
   119 done
   120 
   121 lemma zero_lt_zmagnitude: "[| #0 $< k; k \<in> int |] ==> 0 < zmagnitude(k)"
   122 apply (drule zero_zless_imp_znegative_zminus)
   123 apply (drule_tac [2] zneg_int_of)
   124 apply (auto simp add: zminus_equation [of k])
   125 apply (subgoal_tac "0 < zmagnitude ($# succ (n))")
   126  apply simp
   127 apply (simp only: zmagnitude_int_of)
   128 apply simp
   129 done
   130 
   131 
   132 (*** Inequality lemmas involving $#succ(m) ***)
   133 
   134 lemma zless_add_succ_iff:
   135      "(w $< z $+ $# succ(m)) <-> (w $< z $+ $#m | intify(w) = z $+ $#m)"
   136 apply (auto simp add: zless_iff_succ_zadd zadd_assoc int_of_add [symmetric])
   137 apply (rule_tac [3] x = "0" in bexI)
   138 apply (cut_tac m = "m" in int_succ_int_1)
   139 apply (cut_tac m = "n" in int_succ_int_1)
   140 apply simp
   141 apply (erule natE)
   142 apply auto
   143 apply (rule_tac x = "succ (n) " in bexI)
   144 apply auto
   145 done
   146 
   147 lemma zadd_succ_lemma:
   148      "z \<in> int ==> (w $+ $# succ(m) $<= z) <-> (w $+ $#m $< z)"
   149 apply (simp only: not_zless_iff_zle [THEN iff_sym] zless_add_succ_iff)
   150 apply (auto intro: zle_anti_sym elim: zless_asym
   151             simp add: zless_imp_zle not_zless_iff_zle)
   152 done
   153 
   154 lemma zadd_succ_zle_iff: "(w $+ $# succ(m) $<= z) <-> (w $+ $#m $< z)"
   155 apply (cut_tac z = "intify (z)" in zadd_succ_lemma)
   156 apply auto
   157 done
   158 
   159 (** Inequality reasoning **)
   160 
   161 lemma zless_add1_iff_zle: "(w $< z $+ #1) <-> (w$<=z)"
   162 apply (subgoal_tac "#1 = $# 1")
   163 apply (simp only: zless_add_succ_iff zle_def)
   164 apply auto
   165 done
   166 
   167 lemma add1_zle_iff: "(w $+ #1 $<= z) <-> (w $< z)"
   168 apply (subgoal_tac "#1 = $# 1")
   169 apply (simp only: zadd_succ_zle_iff)
   170 apply auto
   171 done
   172 
   173 lemma add1_left_zle_iff: "(#1 $+ w $<= z) <-> (w $< z)"
   174 apply (subst zadd_commute)
   175 apply (rule add1_zle_iff)
   176 done
   177 
   178 
   179 (*** Monotonicity of Multiplication ***)
   180 
   181 lemma zmult_mono_lemma: "k \<in> nat ==> i $<= j ==> i $* $#k $<= j $* $#k"
   182 apply (induct_tac "k")
   183  prefer 2 apply (subst int_succ_int_1)
   184 apply (simp_all (no_asm_simp) add: zadd_zmult_distrib2 zadd_zle_mono)
   185 done
   186 
   187 lemma zmult_zle_mono1: "[| i $<= j;  #0 $<= k |] ==> i$*k $<= j$*k"
   188 apply (subgoal_tac "i $* intify (k) $<= j $* intify (k) ")
   189 apply (simp (no_asm_use))
   190 apply (rule_tac b = "intify (k)" in not_zneg_mag [THEN subst])
   191 apply (rule_tac [3] zmult_mono_lemma)
   192 apply auto
   193 apply (simp add: znegative_iff_zless_0 not_zless_iff_zle [THEN iff_sym])
   194 done
   195 
   196 lemma zmult_zle_mono1_neg: "[| i $<= j;  k $<= #0 |] ==> j$*k $<= i$*k"
   197 apply (rule zminus_zle_zminus [THEN iffD1])
   198 apply (simp del: zmult_zminus_right
   199             add: zmult_zminus_right [symmetric] zmult_zle_mono1 zle_zminus)
   200 done
   201 
   202 lemma zmult_zle_mono2: "[| i $<= j;  #0 $<= k |] ==> k$*i $<= k$*j"
   203 apply (drule zmult_zle_mono1)
   204 apply (simp_all add: zmult_commute)
   205 done
   206 
   207 lemma zmult_zle_mono2_neg: "[| i $<= j;  k $<= #0 |] ==> k$*j $<= k$*i"
   208 apply (drule zmult_zle_mono1_neg)
   209 apply (simp_all add: zmult_commute)
   210 done
   211 
   212 (* $<= monotonicity, BOTH arguments*)
   213 lemma zmult_zle_mono:
   214      "[| i $<= j;  k $<= l;  #0 $<= j;  #0 $<= k |] ==> i$*k $<= j$*l"
   215 apply (erule zmult_zle_mono1 [THEN zle_trans])
   216 apply assumption
   217 apply (erule zmult_zle_mono2)
   218 apply assumption
   219 done
   220 
   221 
   222 (** strict, in 1st argument; proof is by induction on k>0 **)
   223 
   224 lemma zmult_zless_mono2_lemma [rule_format]:
   225      "[| i$<j; k \<in> nat |] ==> 0<k --> $#k $* i $< $#k $* j"
   226 apply (induct_tac "k")
   227  prefer 2
   228  apply (subst int_succ_int_1)
   229  apply (erule natE)
   230 apply (simp_all add: zadd_zmult_distrib zadd_zless_mono zle_def)
   231 apply (frule nat_0_le)
   232 apply (subgoal_tac "i $+ (i $+ $# xa $* i) $< j $+ (j $+ $# xa $* j) ")
   233 apply (simp (no_asm_use))
   234 apply (rule zadd_zless_mono)
   235 apply (simp_all (no_asm_simp) add: zle_def)
   236 done
   237 
   238 lemma zmult_zless_mono2: "[| i$<j;  #0 $< k |] ==> k$*i $< k$*j"
   239 apply (subgoal_tac "intify (k) $* i $< intify (k) $* j")
   240 apply (simp (no_asm_use))
   241 apply (rule_tac b = "intify (k)" in not_zneg_mag [THEN subst])
   242 apply (rule_tac [3] zmult_zless_mono2_lemma)
   243 apply auto
   244 apply (simp add: znegative_iff_zless_0)
   245 apply (drule zless_trans, assumption)
   246 apply (auto simp add: zero_lt_zmagnitude)
   247 done
   248 
   249 lemma zmult_zless_mono1: "[| i$<j;  #0 $< k |] ==> i$*k $< j$*k"
   250 apply (drule zmult_zless_mono2)
   251 apply (simp_all add: zmult_commute)
   252 done
   253 
   254 (* < monotonicity, BOTH arguments*)
   255 lemma zmult_zless_mono:
   256      "[| i $< j;  k $< l;  #0 $< j;  #0 $< k |] ==> i$*k $< j$*l"
   257 apply (erule zmult_zless_mono1 [THEN zless_trans])
   258 apply assumption
   259 apply (erule zmult_zless_mono2)
   260 apply assumption
   261 done
   262 
   263 lemma zmult_zless_mono1_neg: "[| i $< j;  k $< #0 |] ==> j$*k $< i$*k"
   264 apply (rule zminus_zless_zminus [THEN iffD1])
   265 apply (simp del: zmult_zminus_right 
   266             add: zmult_zminus_right [symmetric] zmult_zless_mono1 zless_zminus)
   267 done
   268 
   269 lemma zmult_zless_mono2_neg: "[| i $< j;  k $< #0 |] ==> k$*j $< k$*i"
   270 apply (rule zminus_zless_zminus [THEN iffD1])
   271 apply (simp del: zmult_zminus 
   272             add: zmult_zminus [symmetric] zmult_zless_mono2 zless_zminus)
   273 done
   274 
   275 
   276 (** Products of zeroes **)
   277 
   278 lemma zmult_eq_lemma:
   279      "[| m \<in> int; n \<in> int |] ==> (m = #0 | n = #0) <-> (m$*n = #0)"
   280 apply (case_tac "m $< #0")
   281 apply (auto simp add: not_zless_iff_zle zle_def neq_iff_zless)
   282 apply (force dest: zmult_zless_mono1_neg zmult_zless_mono1)+
   283 done
   284 
   285 lemma zmult_eq_0_iff [iff]: "(m$*n = #0) <-> (intify(m) = #0 | intify(n) = #0)"
   286 apply (simp add: zmult_eq_lemma)
   287 done
   288 
   289 
   290 (** Cancellation laws for k*m < k*n and m*k < n*k, also for <= and =,
   291     but not (yet?) for k*m < n*k. **)
   292 
   293 lemma zmult_zless_lemma:
   294      "[| k \<in> int; m \<in> int; n \<in> int |]  
   295       ==> (m$*k $< n$*k) <-> ((#0 $< k & m$<n) | (k $< #0 & n$<m))"
   296 apply (case_tac "k = #0")
   297 apply (auto simp add: neq_iff_zless zmult_zless_mono1 zmult_zless_mono1_neg)
   298 apply (auto simp add: not_zless_iff_zle 
   299                       not_zle_iff_zless [THEN iff_sym, of "m$*k"] 
   300                       not_zle_iff_zless [THEN iff_sym, of m])
   301 apply (auto elim: notE
   302             simp add: zless_imp_zle zmult_zle_mono1 zmult_zle_mono1_neg)
   303 done
   304 
   305 lemma zmult_zless_cancel2:
   306      "(m$*k $< n$*k) <-> ((#0 $< k & m$<n) | (k $< #0 & n$<m))"
   307 apply (cut_tac k = "intify (k)" and m = "intify (m)" and n = "intify (n)" 
   308        in zmult_zless_lemma)
   309 apply auto
   310 done
   311 
   312 lemma zmult_zless_cancel1:
   313      "(k$*m $< k$*n) <-> ((#0 $< k & m$<n) | (k $< #0 & n$<m))"
   314 by (simp add: zmult_commute [of k] zmult_zless_cancel2)
   315 
   316 lemma zmult_zle_cancel2:
   317      "(m$*k $<= n$*k) <-> ((#0 $< k --> m$<=n) & (k $< #0 --> n$<=m))"
   318 by (auto simp add: not_zless_iff_zle [THEN iff_sym] zmult_zless_cancel2)
   319 
   320 lemma zmult_zle_cancel1:
   321      "(k$*m $<= k$*n) <-> ((#0 $< k --> m$<=n) & (k $< #0 --> n$<=m))"
   322 by (auto simp add: not_zless_iff_zle [THEN iff_sym] zmult_zless_cancel1)
   323 
   324 lemma int_eq_iff_zle: "[| m \<in> int; n \<in> int |] ==> m=n <-> (m $<= n & n $<= m)"
   325 apply (blast intro: zle_refl zle_anti_sym)
   326 done
   327 
   328 lemma zmult_cancel2_lemma:
   329      "[| k \<in> int; m \<in> int; n \<in> int |] ==> (m$*k = n$*k) <-> (k=#0 | m=n)"
   330 apply (simp add: int_eq_iff_zle [of "m$*k"] int_eq_iff_zle [of m])
   331 apply (auto simp add: zmult_zle_cancel2 neq_iff_zless)
   332 done
   333 
   334 lemma zmult_cancel2 [simp]:
   335      "(m$*k = n$*k) <-> (intify(k) = #0 | intify(m) = intify(n))"
   336 apply (rule iff_trans)
   337 apply (rule_tac [2] zmult_cancel2_lemma)
   338 apply auto
   339 done
   340 
   341 lemma zmult_cancel1 [simp]:
   342      "(k$*m = k$*n) <-> (intify(k) = #0 | intify(m) = intify(n))"
   343 by (simp add: zmult_commute [of k] zmult_cancel2)
   344 
   345 
   346 subsection{* Uniqueness and monotonicity of quotients and remainders *}
   347 
   348 lemma unique_quotient_lemma:
   349      "[| b$*q' $+ r' $<= b$*q $+ r;  #0 $<= r';  #0 $< b;  r $< b |]  
   350       ==> q' $<= q"
   351 apply (subgoal_tac "r' $+ b $* (q'$-q) $<= r")
   352  prefer 2 apply (simp add: zdiff_zmult_distrib2 zadd_ac zcompare_rls)
   353 apply (subgoal_tac "#0 $< b $* (#1 $+ q $- q') ")
   354  prefer 2
   355  apply (erule zle_zless_trans)
   356  apply (simp add: zdiff_zmult_distrib2 zadd_zmult_distrib2 zadd_ac zcompare_rls)
   357  apply (erule zle_zless_trans)
   358  apply (simp add: ); 
   359 apply (subgoal_tac "b $* q' $< b $* (#1 $+ q)")
   360  prefer 2 
   361  apply (simp add: zdiff_zmult_distrib2 zadd_zmult_distrib2 zadd_ac zcompare_rls)
   362 apply (auto elim: zless_asym
   363         simp add: zmult_zless_cancel1 zless_add1_iff_zle zadd_ac zcompare_rls)
   364 done
   365 
   366 lemma unique_quotient_lemma_neg:
   367      "[| b$*q' $+ r' $<= b$*q $+ r;  r $<= #0;  b $< #0;  b $< r' |]  
   368       ==> q $<= q'"
   369 apply (rule_tac b = "$-b" and r = "$-r'" and r' = "$-r" 
   370        in unique_quotient_lemma)
   371 apply (auto simp del: zminus_zadd_distrib
   372             simp add: zminus_zadd_distrib [symmetric] zle_zminus zless_zminus)
   373 done
   374 
   375 
   376 lemma unique_quotient:
   377      "[| quorem (<a,b>, <q,r>);  quorem (<a,b>, <q',r'>);  b \<in> int; b ~= #0;  
   378          q \<in> int; q' \<in> int |] ==> q = q'"
   379 apply (simp add: split_ifs quorem_def neq_iff_zless)
   380 apply safe
   381 apply simp_all
   382 apply (blast intro: zle_anti_sym
   383              dest: zle_eq_refl [THEN unique_quotient_lemma] 
   384                    zle_eq_refl [THEN unique_quotient_lemma_neg] sym)+
   385 done
   386 
   387 lemma unique_remainder:
   388      "[| quorem (<a,b>, <q,r>);  quorem (<a,b>, <q',r'>);  b \<in> int; b ~= #0;  
   389          q \<in> int; q' \<in> int;  
   390          r \<in> int; r' \<in> int |] ==> r = r'"
   391 apply (subgoal_tac "q = q'")
   392  prefer 2 apply (blast intro: unique_quotient)
   393 apply (simp add: quorem_def)
   394 done
   395 
   396 
   397 subsection{*Correctness of posDivAlg, 
   398            the Division Algorithm for @{text "a\<ge>0"} and @{text "b>0"} *}
   399 
   400 lemma adjust_eq [simp]:
   401      "adjust(b, <q,r>) = (let diff = r$-b in  
   402                           if #0 $<= diff then <#2$*q $+ #1,diff>   
   403                                          else <#2$*q,r>)"
   404 by (simp add: Let_def adjust_def)
   405 
   406 
   407 lemma posDivAlg_termination:
   408      "[| #0 $< b; ~ a $< b |]    
   409       ==> nat_of(a $- #2 $\<times> b $+ #1) < nat_of(a $- b $+ #1)"
   410 apply (simp (no_asm) add: zless_nat_conj)
   411 apply (simp add: not_zless_iff_zle zless_add1_iff_zle zcompare_rls)
   412 done
   413 
   414 lemmas posDivAlg_unfold = def_wfrec [OF posDivAlg_def wf_measure]
   415 
   416 lemma posDivAlg_eqn:
   417      "[| #0 $< b; a \<in> int; b \<in> int |] ==>  
   418       posDivAlg(<a,b>) =       
   419        (if a$<b then <#0,a> else adjust(b, posDivAlg (<a, #2$*b>)))"
   420 apply (rule posDivAlg_unfold [THEN trans])
   421 apply (simp add: vimage_iff not_zless_iff_zle [THEN iff_sym])
   422 apply (blast intro: posDivAlg_termination)
   423 done
   424 
   425 lemma posDivAlg_induct_lemma [rule_format]:
   426   assumes prem:
   427         "!!a b. [| a \<in> int; b \<in> int;  
   428                    ~ (a $< b | b $<= #0) --> P(<a, #2 $* b>) |] ==> P(<a,b>)"
   429   shows "<u,v> \<in> int*int --> P(<u,v>)"
   430 apply (rule_tac a = "<u,v>" in wf_induct)
   431 apply (rule_tac A = "int*int" and f = "%<a,b>.nat_of (a $- b $+ #1)" 
   432        in wf_measure)
   433 apply clarify
   434 apply (rule prem)
   435 apply (drule_tac [3] x = "<xa, #2 $\<times> y>" in spec)
   436 apply auto
   437 apply (simp add: not_zle_iff_zless posDivAlg_termination)
   438 done
   439 
   440 
   441 lemma posDivAlg_induct [consumes 2]:
   442   assumes u_int: "u \<in> int"
   443       and v_int: "v \<in> int"
   444       and ih: "!!a b. [| a \<in> int; b \<in> int;
   445                      ~ (a $< b | b $<= #0) --> P(a, #2 $* b) |] ==> P(a,b)"
   446   shows "P(u,v)"
   447 apply (subgoal_tac "(%<x,y>. P (x,y)) (<u,v>)")
   448 apply simp
   449 apply (rule posDivAlg_induct_lemma)
   450 apply (simp (no_asm_use))
   451 apply (rule ih)
   452 apply (auto simp add: u_int v_int)
   453 done
   454 
   455 (*FIXME: use intify in integ_of so that we always have integ_of w \<in> int.
   456     then this rewrite can work for ALL constants!!*)
   457 lemma intify_eq_0_iff_zle: "intify(m) = #0 <-> (m $<= #0 & #0 $<= m)"
   458 apply (simp (no_asm) add: int_eq_iff_zle)
   459 done
   460 
   461 
   462 subsection{* Some convenient biconditionals for products of signs *}
   463 
   464 lemma zmult_pos: "[| #0 $< i; #0 $< j |] ==> #0 $< i $* j"
   465 apply (drule zmult_zless_mono1)
   466 apply auto
   467 done
   468 
   469 lemma zmult_neg: "[| i $< #0; j $< #0 |] ==> #0 $< i $* j"
   470 apply (drule zmult_zless_mono1_neg)
   471 apply auto
   472 done
   473 
   474 lemma zmult_pos_neg: "[| #0 $< i; j $< #0 |] ==> i $* j $< #0"
   475 apply (drule zmult_zless_mono1_neg)
   476 apply auto
   477 done
   478 
   479 (** Inequality reasoning **)
   480 
   481 lemma int_0_less_lemma:
   482      "[| x \<in> int; y \<in> int |]  
   483       ==> (#0 $< x $* y) <-> (#0 $< x & #0 $< y | x $< #0 & y $< #0)"
   484 apply (auto simp add: zle_def not_zless_iff_zle zmult_pos zmult_neg)
   485 apply (rule ccontr) 
   486 apply (rule_tac [2] ccontr) 
   487 apply (auto simp add: zle_def not_zless_iff_zle)
   488 apply (erule_tac P = "#0$< x$* y" in rev_mp)
   489 apply (erule_tac [2] P = "#0$< x$* y" in rev_mp)
   490 apply (drule zmult_pos_neg, assumption) 
   491  prefer 2
   492  apply (drule zmult_pos_neg, assumption) 
   493 apply (auto dest: zless_not_sym simp add: zmult_commute)
   494 done
   495 
   496 lemma int_0_less_mult_iff:
   497      "(#0 $< x $* y) <-> (#0 $< x & #0 $< y | x $< #0 & y $< #0)"
   498 apply (cut_tac x = "intify (x)" and y = "intify (y)" in int_0_less_lemma)
   499 apply auto
   500 done
   501 
   502 lemma int_0_le_lemma:
   503      "[| x \<in> int; y \<in> int |]  
   504       ==> (#0 $<= x $* y) <-> (#0 $<= x & #0 $<= y | x $<= #0 & y $<= #0)"
   505 by (auto simp add: zle_def not_zless_iff_zle int_0_less_mult_iff)
   506 
   507 lemma int_0_le_mult_iff:
   508      "(#0 $<= x $* y) <-> ((#0 $<= x & #0 $<= y) | (x $<= #0 & y $<= #0))"
   509 apply (cut_tac x = "intify (x)" and y = "intify (y)" in int_0_le_lemma)
   510 apply auto
   511 done
   512 
   513 lemma zmult_less_0_iff:
   514      "(x $* y $< #0) <-> (#0 $< x & y $< #0 | x $< #0 & #0 $< y)"
   515 apply (auto simp add: int_0_le_mult_iff not_zle_iff_zless [THEN iff_sym])
   516 apply (auto dest: zless_not_sym simp add: not_zle_iff_zless)
   517 done
   518 
   519 lemma zmult_le_0_iff:
   520      "(x $* y $<= #0) <-> (#0 $<= x & y $<= #0 | x $<= #0 & #0 $<= y)"
   521 by (auto dest: zless_not_sym
   522          simp add: int_0_less_mult_iff not_zless_iff_zle [THEN iff_sym])
   523 
   524 
   525 (*Typechecking for posDivAlg*)
   526 lemma posDivAlg_type [rule_format]:
   527      "[| a \<in> int; b \<in> int |] ==> posDivAlg(<a,b>) \<in> int * int"
   528 apply (rule_tac u = "a" and v = "b" in posDivAlg_induct)
   529 apply assumption+
   530 apply (case_tac "#0 $< ba")
   531  apply (simp add: posDivAlg_eqn adjust_def integ_of_type 
   532              split add: split_if_asm)
   533  apply clarify
   534  apply (simp add: int_0_less_mult_iff not_zle_iff_zless)
   535 apply (simp add: not_zless_iff_zle)
   536 apply (subst posDivAlg_unfold)
   537 apply simp
   538 done
   539 
   540 (*Correctness of posDivAlg: it computes quotients correctly*)
   541 lemma posDivAlg_correct [rule_format]:
   542      "[| a \<in> int; b \<in> int |]  
   543       ==> #0 $<= a --> #0 $< b --> quorem (<a,b>, posDivAlg(<a,b>))"
   544 apply (rule_tac u = "a" and v = "b" in posDivAlg_induct)
   545 apply auto
   546    apply (simp_all add: quorem_def)
   547    txt{*base case: a<b*}
   548    apply (simp add: posDivAlg_eqn)
   549   apply (simp add: not_zless_iff_zle [THEN iff_sym])
   550  apply (simp add: int_0_less_mult_iff)
   551 txt{*main argument*}
   552 apply (subst posDivAlg_eqn)
   553 apply (simp_all (no_asm_simp))
   554 apply (erule splitE)
   555 apply (rule posDivAlg_type)
   556 apply (simp_all add: int_0_less_mult_iff)
   557 apply (auto simp add: zadd_zmult_distrib2 Let_def)
   558 txt{*now just linear arithmetic*}
   559 apply (simp add: not_zle_iff_zless zdiff_zless_iff)
   560 done
   561 
   562 
   563 subsection{*Correctness of negDivAlg, the division algorithm for a<0 and b>0*}
   564 
   565 lemma negDivAlg_termination:
   566      "[| #0 $< b; a $+ b $< #0 |] 
   567       ==> nat_of($- a $- #2 $* b) < nat_of($- a $- b)"
   568 apply (simp (no_asm) add: zless_nat_conj)
   569 apply (simp add: zcompare_rls not_zle_iff_zless zless_zdiff_iff [THEN iff_sym]
   570                  zless_zminus)
   571 done
   572 
   573 lemmas negDivAlg_unfold = def_wfrec [OF negDivAlg_def wf_measure]
   574 
   575 lemma negDivAlg_eqn:
   576      "[| #0 $< b; a : int; b : int |] ==>  
   577       negDivAlg(<a,b>) =       
   578        (if #0 $<= a$+b then <#-1,a$+b>  
   579                        else adjust(b, negDivAlg (<a, #2$*b>)))"
   580 apply (rule negDivAlg_unfold [THEN trans])
   581 apply (simp (no_asm_simp) add: vimage_iff not_zless_iff_zle [THEN iff_sym])
   582 apply (blast intro: negDivAlg_termination)
   583 done
   584 
   585 lemma negDivAlg_induct_lemma [rule_format]:
   586   assumes prem:
   587         "!!a b. [| a \<in> int; b \<in> int;  
   588                    ~ (#0 $<= a $+ b | b $<= #0) --> P(<a, #2 $* b>) |]  
   589                 ==> P(<a,b>)"
   590   shows "<u,v> \<in> int*int --> P(<u,v>)"
   591 apply (rule_tac a = "<u,v>" in wf_induct)
   592 apply (rule_tac A = "int*int" and f = "%<a,b>.nat_of ($- a $- b)" 
   593        in wf_measure)
   594 apply clarify
   595 apply (rule prem)
   596 apply (drule_tac [3] x = "<xa, #2 $\<times> y>" in spec)
   597 apply auto
   598 apply (simp add: not_zle_iff_zless negDivAlg_termination)
   599 done
   600 
   601 lemma negDivAlg_induct [consumes 2]:
   602   assumes u_int: "u \<in> int"
   603       and v_int: "v \<in> int"
   604       and ih: "!!a b. [| a \<in> int; b \<in> int;  
   605                          ~ (#0 $<= a $+ b | b $<= #0) --> P(a, #2 $* b) |]  
   606                       ==> P(a,b)"
   607   shows "P(u,v)"
   608 apply (subgoal_tac " (%<x,y>. P (x,y)) (<u,v>)")
   609 apply simp
   610 apply (rule negDivAlg_induct_lemma)
   611 apply (simp (no_asm_use))
   612 apply (rule ih)
   613 apply (auto simp add: u_int v_int)
   614 done
   615 
   616 
   617 (*Typechecking for negDivAlg*)
   618 lemma negDivAlg_type:
   619      "[| a \<in> int; b \<in> int |] ==> negDivAlg(<a,b>) \<in> int * int"
   620 apply (rule_tac u = "a" and v = "b" in negDivAlg_induct)
   621 apply assumption+
   622 apply (case_tac "#0 $< ba")
   623  apply (simp add: negDivAlg_eqn adjust_def integ_of_type 
   624              split add: split_if_asm)
   625  apply clarify
   626  apply (simp add: int_0_less_mult_iff not_zle_iff_zless)
   627 apply (simp add: not_zless_iff_zle)
   628 apply (subst negDivAlg_unfold)
   629 apply simp
   630 done
   631 
   632 
   633 (*Correctness of negDivAlg: it computes quotients correctly
   634   It doesn't work if a=0 because the 0/b=0 rather than -1*)
   635 lemma negDivAlg_correct [rule_format]:
   636      "[| a \<in> int; b \<in> int |]  
   637       ==> a $< #0 --> #0 $< b --> quorem (<a,b>, negDivAlg(<a,b>))"
   638 apply (rule_tac u = "a" and v = "b" in negDivAlg_induct)
   639   apply auto
   640    apply (simp_all add: quorem_def)
   641    txt{*base case: @{term "0$<=a$+b"}*}
   642    apply (simp add: negDivAlg_eqn)
   643   apply (simp add: not_zless_iff_zle [THEN iff_sym])
   644  apply (simp add: int_0_less_mult_iff)
   645 txt{*main argument*}
   646 apply (subst negDivAlg_eqn)
   647 apply (simp_all (no_asm_simp))
   648 apply (erule splitE)
   649 apply (rule negDivAlg_type)
   650 apply (simp_all add: int_0_less_mult_iff)
   651 apply (auto simp add: zadd_zmult_distrib2 Let_def)
   652 txt{*now just linear arithmetic*}
   653 apply (simp add: not_zle_iff_zless zdiff_zless_iff)
   654 done
   655 
   656 
   657 subsection{* Existence shown by proving the division algorithm to be correct *}
   658 
   659 (*the case a=0*)
   660 lemma quorem_0: "[|b \<noteq> #0;  b \<in> int|] ==> quorem (<#0,b>, <#0,#0>)"
   661 by (force simp add: quorem_def neq_iff_zless)
   662 
   663 lemma posDivAlg_zero_divisor: "posDivAlg(<a,#0>) = <#0,a>"
   664 apply (subst posDivAlg_unfold)
   665 apply simp
   666 done
   667 
   668 lemma posDivAlg_0 [simp]: "posDivAlg (<#0,b>) = <#0,#0>"
   669 apply (subst posDivAlg_unfold)
   670 apply (simp add: not_zle_iff_zless)
   671 done
   672 
   673 
   674 (*Needed below.  Actually it's an equivalence.*)
   675 lemma linear_arith_lemma: "~ (#0 $<= #-1 $+ b) ==> (b $<= #0)"
   676 apply (simp add: not_zle_iff_zless)
   677 apply (drule zminus_zless_zminus [THEN iffD2])
   678 apply (simp add: zadd_commute zless_add1_iff_zle zle_zminus)
   679 done
   680 
   681 lemma negDivAlg_minus1 [simp]: "negDivAlg (<#-1,b>) = <#-1, b$-#1>"
   682 apply (subst negDivAlg_unfold)
   683 apply (simp add: linear_arith_lemma integ_of_type vimage_iff)
   684 done
   685 
   686 lemma negateSnd_eq [simp]: "negateSnd (<q,r>) = <q, $-r>"
   687 apply (unfold negateSnd_def)
   688 apply auto
   689 done
   690 
   691 lemma negateSnd_type: "qr \<in> int * int ==> negateSnd (qr) \<in> int * int"
   692 apply (unfold negateSnd_def)
   693 apply auto
   694 done
   695 
   696 lemma quorem_neg:
   697      "[|quorem (<$-a,$-b>, qr);  a \<in> int;  b \<in> int;  qr \<in> int * int|]   
   698       ==> quorem (<a,b>, negateSnd(qr))"
   699 apply clarify
   700 apply (auto elim: zless_asym simp add: quorem_def zless_zminus)
   701 txt{*linear arithmetic from here on*}
   702 apply (simp_all add: zminus_equation [of a] zminus_zless)
   703 apply (cut_tac [2] z = "b" and w = "#0" in zless_linear)
   704 apply (cut_tac [1] z = "b" and w = "#0" in zless_linear)
   705 apply auto
   706 apply (blast dest: zle_zless_trans)+
   707 done
   708 
   709 lemma divAlg_correct:
   710      "[|b \<noteq> #0;  a \<in> int;  b \<in> int|] ==> quorem (<a,b>, divAlg(<a,b>))"
   711 apply (auto simp add: quorem_0 divAlg_def)
   712 apply (safe intro!: quorem_neg posDivAlg_correct negDivAlg_correct
   713                     posDivAlg_type negDivAlg_type) 
   714 apply (auto simp add: quorem_def neq_iff_zless)
   715 txt{*linear arithmetic from here on*}
   716 apply (auto simp add: zle_def)
   717 done
   718 
   719 lemma divAlg_type: "[|a \<in> int;  b \<in> int|] ==> divAlg(<a,b>) \<in> int * int"
   720 apply (auto simp add: divAlg_def)
   721 apply (auto simp add: posDivAlg_type negDivAlg_type negateSnd_type)
   722 done
   723 
   724 
   725 (** intify cancellation **)
   726 
   727 lemma zdiv_intify1 [simp]: "intify(x) zdiv y = x zdiv y"
   728 apply (simp (no_asm) add: zdiv_def)
   729 done
   730 
   731 lemma zdiv_intify2 [simp]: "x zdiv intify(y) = x zdiv y"
   732 apply (simp (no_asm) add: zdiv_def)
   733 done
   734 
   735 lemma zdiv_type [iff,TC]: "z zdiv w \<in> int"
   736 apply (unfold zdiv_def)
   737 apply (blast intro: fst_type divAlg_type)
   738 done
   739 
   740 lemma zmod_intify1 [simp]: "intify(x) zmod y = x zmod y"
   741 apply (simp (no_asm) add: zmod_def)
   742 done
   743 
   744 lemma zmod_intify2 [simp]: "x zmod intify(y) = x zmod y"
   745 apply (simp (no_asm) add: zmod_def)
   746 done
   747 
   748 lemma zmod_type [iff,TC]: "z zmod w \<in> int"
   749 apply (unfold zmod_def)
   750 apply (rule snd_type)
   751 apply (blast intro: divAlg_type)
   752 done
   753 
   754 
   755 (** Arbitrary definitions for division by zero.  Useful to simplify 
   756     certain equations **)
   757 
   758 lemma DIVISION_BY_ZERO_ZDIV: "a zdiv #0 = #0"
   759 apply (simp (no_asm) add: zdiv_def divAlg_def posDivAlg_zero_divisor)
   760 done  (*NOT for adding to default simpset*)
   761 
   762 lemma DIVISION_BY_ZERO_ZMOD: "a zmod #0 = intify(a)"
   763 apply (simp (no_asm) add: zmod_def divAlg_def posDivAlg_zero_divisor)
   764 done  (*NOT for adding to default simpset*)
   765 
   766 
   767 
   768 (** Basic laws about division and remainder **)
   769 
   770 lemma raw_zmod_zdiv_equality:
   771      "[| a \<in> int; b \<in> int |] ==> a = b $* (a zdiv b) $+ (a zmod b)"
   772 apply (case_tac "b = #0")
   773  apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) 
   774 apply (cut_tac a = "a" and b = "b" in divAlg_correct)
   775 apply (auto simp add: quorem_def zdiv_def zmod_def split_def)
   776 done
   777 
   778 lemma zmod_zdiv_equality: "intify(a) = b $* (a zdiv b) $+ (a zmod b)"
   779 apply (rule trans)
   780 apply (rule_tac b = "intify (b)" in raw_zmod_zdiv_equality)
   781 apply auto
   782 done
   783 
   784 lemma pos_mod: "#0 $< b ==> #0 $<= a zmod b & a zmod b $< b"
   785 apply (cut_tac a = "intify (a)" and b = "intify (b)" in divAlg_correct)
   786 apply (auto simp add: intify_eq_0_iff_zle quorem_def zmod_def split_def)
   787 apply (blast dest: zle_zless_trans)+
   788 done
   789 
   790 lemmas pos_mod_sign = pos_mod [THEN conjunct1, standard]
   791 and    pos_mod_bound = pos_mod [THEN conjunct2, standard]
   792 
   793 lemma neg_mod: "b $< #0 ==> a zmod b $<= #0 & b $< a zmod b"
   794 apply (cut_tac a = "intify (a)" and b = "intify (b)" in divAlg_correct)
   795 apply (auto simp add: intify_eq_0_iff_zle quorem_def zmod_def split_def)
   796 apply (blast dest: zle_zless_trans)
   797 apply (blast dest: zless_trans)+
   798 done
   799 
   800 lemmas neg_mod_sign = neg_mod [THEN conjunct1, standard]
   801 and    neg_mod_bound = neg_mod [THEN conjunct2, standard]
   802 
   803 
   804 (** proving general properties of zdiv and zmod **)
   805 
   806 lemma quorem_div_mod:
   807      "[|b \<noteq> #0;  a \<in> int;  b \<in> int |]  
   808       ==> quorem (<a,b>, <a zdiv b, a zmod b>)"
   809 apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality)
   810 apply (auto simp add: quorem_def neq_iff_zless pos_mod_sign pos_mod_bound 
   811                       neg_mod_sign neg_mod_bound)
   812 done
   813 
   814 (*Surely quorem(<a,b>,<q,r>) implies a \<in> int, but it doesn't matter*)
   815 lemma quorem_div:
   816      "[| quorem(<a,b>,<q,r>);  b \<noteq> #0;  a \<in> int;  b \<in> int;  q \<in> int |]  
   817       ==> a zdiv b = q"
   818 by (blast intro: quorem_div_mod [THEN unique_quotient])
   819 
   820 lemma quorem_mod:
   821      "[| quorem(<a,b>,<q,r>); b \<noteq> #0; a \<in> int; b \<in> int; q \<in> int; r \<in> int |] 
   822       ==> a zmod b = r"
   823 by (blast intro: quorem_div_mod [THEN unique_remainder])
   824 
   825 lemma zdiv_pos_pos_trivial_raw:
   826      "[| a \<in> int;  b \<in> int;  #0 $<= a;  a $< b |] ==> a zdiv b = #0"
   827 apply (rule quorem_div)
   828 apply (auto simp add: quorem_def)
   829 (*linear arithmetic*)
   830 apply (blast dest: zle_zless_trans)+
   831 done
   832 
   833 lemma zdiv_pos_pos_trivial: "[| #0 $<= a;  a $< b |] ==> a zdiv b = #0"
   834 apply (cut_tac a = "intify (a)" and b = "intify (b)" 
   835        in zdiv_pos_pos_trivial_raw)
   836 apply auto
   837 done
   838 
   839 lemma zdiv_neg_neg_trivial_raw:
   840      "[| a \<in> int;  b \<in> int;  a $<= #0;  b $< a |] ==> a zdiv b = #0"
   841 apply (rule_tac r = "a" in quorem_div)
   842 apply (auto simp add: quorem_def)
   843 (*linear arithmetic*)
   844 apply (blast dest: zle_zless_trans zless_trans)+
   845 done
   846 
   847 lemma zdiv_neg_neg_trivial: "[| a $<= #0;  b $< a |] ==> a zdiv b = #0"
   848 apply (cut_tac a = "intify (a)" and b = "intify (b)" 
   849        in zdiv_neg_neg_trivial_raw)
   850 apply auto
   851 done
   852 
   853 lemma zadd_le_0_lemma: "[| a$+b $<= #0;  #0 $< a;  #0 $< b |] ==> False"
   854 apply (drule_tac z' = "#0" and z = "b" in zadd_zless_mono)
   855 apply (auto simp add: zle_def)
   856 apply (blast dest: zless_trans)
   857 done
   858 
   859 lemma zdiv_pos_neg_trivial_raw:
   860      "[| a \<in> int;  b \<in> int;  #0 $< a;  a$+b $<= #0 |] ==> a zdiv b = #-1"
   861 apply (rule_tac r = "a $+ b" in quorem_div)
   862 apply (auto simp add: quorem_def)
   863 (*linear arithmetic*)
   864 apply (blast dest: zadd_le_0_lemma zle_zless_trans)+
   865 done
   866 
   867 lemma zdiv_pos_neg_trivial: "[| #0 $< a;  a$+b $<= #0 |] ==> a zdiv b = #-1"
   868 apply (cut_tac a = "intify (a)" and b = "intify (b)" 
   869        in zdiv_pos_neg_trivial_raw)
   870 apply auto
   871 done
   872 
   873 (*There is no zdiv_neg_pos_trivial because  #0 zdiv b = #0 would supersede it*)
   874 
   875 
   876 lemma zmod_pos_pos_trivial_raw:
   877      "[| a \<in> int;  b \<in> int;  #0 $<= a;  a $< b |] ==> a zmod b = a"
   878 apply (rule_tac q = "#0" in quorem_mod)
   879 apply (auto simp add: quorem_def)
   880 (*linear arithmetic*)
   881 apply (blast dest: zle_zless_trans)+
   882 done
   883 
   884 lemma zmod_pos_pos_trivial: "[| #0 $<= a;  a $< b |] ==> a zmod b = intify(a)"
   885 apply (cut_tac a = "intify (a)" and b = "intify (b)" 
   886        in zmod_pos_pos_trivial_raw)
   887 apply auto
   888 done
   889 
   890 lemma zmod_neg_neg_trivial_raw:
   891      "[| a \<in> int;  b \<in> int;  a $<= #0;  b $< a |] ==> a zmod b = a"
   892 apply (rule_tac q = "#0" in quorem_mod)
   893 apply (auto simp add: quorem_def)
   894 (*linear arithmetic*)
   895 apply (blast dest: zle_zless_trans zless_trans)+
   896 done
   897 
   898 lemma zmod_neg_neg_trivial: "[| a $<= #0;  b $< a |] ==> a zmod b = intify(a)"
   899 apply (cut_tac a = "intify (a)" and b = "intify (b)" 
   900        in zmod_neg_neg_trivial_raw)
   901 apply auto
   902 done
   903 
   904 lemma zmod_pos_neg_trivial_raw:
   905      "[| a \<in> int;  b \<in> int;  #0 $< a;  a$+b $<= #0 |] ==> a zmod b = a$+b"
   906 apply (rule_tac q = "#-1" in quorem_mod)
   907 apply (auto simp add: quorem_def)
   908 (*linear arithmetic*)
   909 apply (blast dest: zadd_le_0_lemma zle_zless_trans)+
   910 done
   911 
   912 lemma zmod_pos_neg_trivial: "[| #0 $< a;  a$+b $<= #0 |] ==> a zmod b = a$+b"
   913 apply (cut_tac a = "intify (a)" and b = "intify (b)" 
   914        in zmod_pos_neg_trivial_raw)
   915 apply auto
   916 done
   917 
   918 (*There is no zmod_neg_pos_trivial...*)
   919 
   920 
   921 (*Simpler laws such as -a zdiv b = -(a zdiv b) FAIL*)
   922 
   923 lemma zdiv_zminus_zminus_raw:
   924      "[|a \<in> int;  b \<in> int|] ==> ($-a) zdiv ($-b) = a zdiv b"
   925 apply (case_tac "b = #0")
   926  apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) 
   927 apply (subst quorem_div_mod [THEN quorem_neg, simplified, THEN quorem_div])
   928 apply auto
   929 done
   930 
   931 lemma zdiv_zminus_zminus [simp]: "($-a) zdiv ($-b) = a zdiv b"
   932 apply (cut_tac a = "intify (a)" and b = "intify (b)" in zdiv_zminus_zminus_raw)
   933 apply auto
   934 done
   935 
   936 (*Simpler laws such as -a zmod b = -(a zmod b) FAIL*)
   937 lemma zmod_zminus_zminus_raw:
   938      "[|a \<in> int;  b \<in> int|] ==> ($-a) zmod ($-b) = $- (a zmod b)"
   939 apply (case_tac "b = #0")
   940  apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) 
   941 apply (subst quorem_div_mod [THEN quorem_neg, simplified, THEN quorem_mod])
   942 apply auto
   943 done
   944 
   945 lemma zmod_zminus_zminus [simp]: "($-a) zmod ($-b) = $- (a zmod b)"
   946 apply (cut_tac a = "intify (a)" and b = "intify (b)" in zmod_zminus_zminus_raw)
   947 apply auto
   948 done
   949 
   950 
   951 subsection{* division of a number by itself *}
   952 
   953 lemma self_quotient_aux1: "[| #0 $< a; a = r $+ a$*q; r $< a |] ==> #1 $<= q"
   954 apply (subgoal_tac "#0 $< a$*q")
   955 apply (cut_tac w = "#0" and z = "q" in add1_zle_iff)
   956 apply (simp add: int_0_less_mult_iff)
   957 apply (blast dest: zless_trans)
   958 (*linear arithmetic...*)
   959 apply (drule_tac t = "%x. x $- r" in subst_context)
   960 apply (drule sym)
   961 apply (simp add: zcompare_rls)
   962 done
   963 
   964 lemma self_quotient_aux2: "[| #0 $< a; a = r $+ a$*q; #0 $<= r |] ==> q $<= #1"
   965 apply (subgoal_tac "#0 $<= a$* (#1$-q)")
   966  apply (simp add: int_0_le_mult_iff zcompare_rls)
   967  apply (blast dest: zle_zless_trans)
   968 apply (simp add: zdiff_zmult_distrib2)
   969 apply (drule_tac t = "%x. x $- a $* q" in subst_context)
   970 apply (simp add: zcompare_rls)
   971 done
   972 
   973 lemma self_quotient:
   974      "[| quorem(<a,a>,<q,r>);  a \<in> int;  q \<in> int;  a \<noteq> #0|] ==> q = #1"
   975 apply (simp add: split_ifs quorem_def neq_iff_zless)
   976 apply (rule zle_anti_sym)
   977 apply safe
   978 apply auto
   979 prefer 4 apply (blast dest: zless_trans)
   980 apply (blast dest: zless_trans)
   981 apply (rule_tac [3] a = "$-a" and r = "$-r" in self_quotient_aux1)
   982 apply (rule_tac a = "$-a" and r = "$-r" in self_quotient_aux2)
   983 apply (rule_tac [6] zminus_equation [THEN iffD1])
   984 apply (rule_tac [2] zminus_equation [THEN iffD1])
   985 apply (force intro: self_quotient_aux1 self_quotient_aux2
   986   simp add: zadd_commute zmult_zminus)+
   987 done
   988 
   989 lemma self_remainder:
   990      "[|quorem(<a,a>,<q,r>); a \<in> int; q \<in> int; r \<in> int; a \<noteq> #0|] ==> r = #0"
   991 apply (frule self_quotient)
   992 apply (auto simp add: quorem_def)
   993 done
   994 
   995 lemma zdiv_self_raw: "[|a \<noteq> #0; a \<in> int|] ==> a zdiv a = #1"
   996 apply (blast intro: quorem_div_mod [THEN self_quotient])
   997 done
   998 
   999 lemma zdiv_self [simp]: "intify(a) \<noteq> #0 ==> a zdiv a = #1"
  1000 apply (drule zdiv_self_raw)
  1001 apply auto
  1002 done
  1003 
  1004 (*Here we have 0 zmod 0 = 0, also assumed by Knuth (who puts m zmod 0 = 0) *)
  1005 lemma zmod_self_raw: "a \<in> int ==> a zmod a = #0"
  1006 apply (case_tac "a = #0")
  1007  apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) 
  1008 apply (blast intro: quorem_div_mod [THEN self_remainder])
  1009 done
  1010 
  1011 lemma zmod_self [simp]: "a zmod a = #0"
  1012 apply (cut_tac a = "intify (a)" in zmod_self_raw)
  1013 apply auto
  1014 done
  1015 
  1016 
  1017 subsection{* Computation of division and remainder *}
  1018 
  1019 lemma zdiv_zero [simp]: "#0 zdiv b = #0"
  1020 apply (simp (no_asm) add: zdiv_def divAlg_def)
  1021 done
  1022 
  1023 lemma zdiv_eq_minus1: "#0 $< b ==> #-1 zdiv b = #-1"
  1024 apply (simp (no_asm_simp) add: zdiv_def divAlg_def)
  1025 done
  1026 
  1027 lemma zmod_zero [simp]: "#0 zmod b = #0"
  1028 apply (simp (no_asm) add: zmod_def divAlg_def)
  1029 done
  1030 
  1031 lemma zdiv_minus1: "#0 $< b ==> #-1 zdiv b = #-1"
  1032 apply (simp (no_asm_simp) add: zdiv_def divAlg_def)
  1033 done
  1034 
  1035 lemma zmod_minus1: "#0 $< b ==> #-1 zmod b = b $- #1"
  1036 apply (simp (no_asm_simp) add: zmod_def divAlg_def)
  1037 done
  1038 
  1039 (** a positive, b positive **)
  1040 
  1041 lemma zdiv_pos_pos: "[| #0 $< a;  #0 $<= b |]  
  1042       ==> a zdiv b = fst (posDivAlg(<intify(a), intify(b)>))"
  1043 apply (simp (no_asm_simp) add: zdiv_def divAlg_def)
  1044 apply (auto simp add: zle_def)
  1045 done
  1046 
  1047 lemma zmod_pos_pos:
  1048      "[| #0 $< a;  #0 $<= b |]  
  1049       ==> a zmod b = snd (posDivAlg(<intify(a), intify(b)>))"
  1050 apply (simp (no_asm_simp) add: zmod_def divAlg_def)
  1051 apply (auto simp add: zle_def)
  1052 done
  1053 
  1054 (** a negative, b positive **)
  1055 
  1056 lemma zdiv_neg_pos:
  1057      "[| a $< #0;  #0 $< b |]  
  1058       ==> a zdiv b = fst (negDivAlg(<intify(a), intify(b)>))"
  1059 apply (simp (no_asm_simp) add: zdiv_def divAlg_def)
  1060 apply (blast dest: zle_zless_trans)
  1061 done
  1062 
  1063 lemma zmod_neg_pos:
  1064      "[| a $< #0;  #0 $< b |]  
  1065       ==> a zmod b = snd (negDivAlg(<intify(a), intify(b)>))"
  1066 apply (simp (no_asm_simp) add: zmod_def divAlg_def)
  1067 apply (blast dest: zle_zless_trans)
  1068 done
  1069 
  1070 (** a positive, b negative **)
  1071 
  1072 lemma zdiv_pos_neg:
  1073      "[| #0 $< a;  b $< #0 |]  
  1074       ==> a zdiv b = fst (negateSnd(negDivAlg (<$-a, $-b>)))"
  1075 apply (simp (no_asm_simp) add: zdiv_def divAlg_def intify_eq_0_iff_zle)
  1076 apply auto
  1077 apply (blast dest: zle_zless_trans)+
  1078 apply (blast dest: zless_trans)
  1079 apply (blast intro: zless_imp_zle)
  1080 done
  1081 
  1082 lemma zmod_pos_neg:
  1083      "[| #0 $< a;  b $< #0 |]  
  1084       ==> a zmod b = snd (negateSnd(negDivAlg (<$-a, $-b>)))"
  1085 apply (simp (no_asm_simp) add: zmod_def divAlg_def intify_eq_0_iff_zle)
  1086 apply auto
  1087 apply (blast dest: zle_zless_trans)+
  1088 apply (blast dest: zless_trans)
  1089 apply (blast intro: zless_imp_zle)
  1090 done
  1091 
  1092 (** a negative, b negative **)
  1093 
  1094 lemma zdiv_neg_neg:
  1095      "[| a $< #0;  b $<= #0 |]  
  1096       ==> a zdiv b = fst (negateSnd(posDivAlg(<$-a, $-b>)))"
  1097 apply (simp (no_asm_simp) add: zdiv_def divAlg_def)
  1098 apply auto
  1099 apply (blast dest!: zle_zless_trans)+
  1100 done
  1101 
  1102 lemma zmod_neg_neg:
  1103      "[| a $< #0;  b $<= #0 |]  
  1104       ==> a zmod b = snd (negateSnd(posDivAlg(<$-a, $-b>)))"
  1105 apply (simp (no_asm_simp) add: zmod_def divAlg_def)
  1106 apply auto
  1107 apply (blast dest!: zle_zless_trans)+
  1108 done
  1109 
  1110 declare zdiv_pos_pos [of "integ_of (v)" "integ_of (w)", standard, simp]
  1111 declare zdiv_neg_pos [of "integ_of (v)" "integ_of (w)", standard, simp]
  1112 declare zdiv_pos_neg [of "integ_of (v)" "integ_of (w)", standard, simp]
  1113 declare zdiv_neg_neg [of "integ_of (v)" "integ_of (w)", standard, simp]
  1114 declare zmod_pos_pos [of "integ_of (v)" "integ_of (w)", standard, simp]
  1115 declare zmod_neg_pos [of "integ_of (v)" "integ_of (w)", standard, simp]
  1116 declare zmod_pos_neg [of "integ_of (v)" "integ_of (w)", standard, simp]
  1117 declare zmod_neg_neg [of "integ_of (v)" "integ_of (w)", standard, simp]
  1118 declare posDivAlg_eqn [of concl: "integ_of (v)" "integ_of (w)", standard, simp]
  1119 declare negDivAlg_eqn [of concl: "integ_of (v)" "integ_of (w)", standard, simp]
  1120 
  1121 
  1122 (** Special-case simplification **)
  1123 
  1124 lemma zmod_1 [simp]: "a zmod #1 = #0"
  1125 apply (cut_tac a = "a" and b = "#1" in pos_mod_sign)
  1126 apply (cut_tac [2] a = "a" and b = "#1" in pos_mod_bound)
  1127 apply auto
  1128 (*arithmetic*)
  1129 apply (drule add1_zle_iff [THEN iffD2])
  1130 apply (rule zle_anti_sym)
  1131 apply auto
  1132 done
  1133 
  1134 lemma zdiv_1 [simp]: "a zdiv #1 = intify(a)"
  1135 apply (cut_tac a = "a" and b = "#1" in zmod_zdiv_equality)
  1136 apply auto
  1137 done
  1138 
  1139 lemma zmod_minus1_right [simp]: "a zmod #-1 = #0"
  1140 apply (cut_tac a = "a" and b = "#-1" in neg_mod_sign)
  1141 apply (cut_tac [2] a = "a" and b = "#-1" in neg_mod_bound)
  1142 apply auto
  1143 (*arithmetic*)
  1144 apply (drule add1_zle_iff [THEN iffD2])
  1145 apply (rule zle_anti_sym)
  1146 apply auto
  1147 done
  1148 
  1149 lemma zdiv_minus1_right_raw: "a \<in> int ==> a zdiv #-1 = $-a"
  1150 apply (cut_tac a = "a" and b = "#-1" in zmod_zdiv_equality)
  1151 apply auto
  1152 apply (rule equation_zminus [THEN iffD2])
  1153 apply auto
  1154 done
  1155 
  1156 lemma zdiv_minus1_right: "a zdiv #-1 = $-a"
  1157 apply (cut_tac a = "intify (a)" in zdiv_minus1_right_raw)
  1158 apply auto
  1159 done
  1160 declare zdiv_minus1_right [simp]
  1161 
  1162 
  1163 subsection{* Monotonicity in the first argument (divisor) *}
  1164 
  1165 lemma zdiv_mono1: "[| a $<= a';  #0 $< b |] ==> a zdiv b $<= a' zdiv b"
  1166 apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality)
  1167 apply (cut_tac a = "a'" and b = "b" in zmod_zdiv_equality)
  1168 apply (rule unique_quotient_lemma)
  1169 apply (erule subst)
  1170 apply (erule subst)
  1171 apply (simp_all (no_asm_simp) add: pos_mod_sign pos_mod_bound)
  1172 done
  1173 
  1174 lemma zdiv_mono1_neg: "[| a $<= a';  b $< #0 |] ==> a' zdiv b $<= a zdiv b"
  1175 apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality)
  1176 apply (cut_tac a = "a'" and b = "b" in zmod_zdiv_equality)
  1177 apply (rule unique_quotient_lemma_neg)
  1178 apply (erule subst)
  1179 apply (erule subst)
  1180 apply (simp_all (no_asm_simp) add: neg_mod_sign neg_mod_bound)
  1181 done
  1182 
  1183 
  1184 subsection{* Monotonicity in the second argument (dividend) *}
  1185 
  1186 lemma q_pos_lemma:
  1187      "[| #0 $<= b'$*q' $+ r'; r' $< b';  #0 $< b' |] ==> #0 $<= q'"
  1188 apply (subgoal_tac "#0 $< b'$* (q' $+ #1)")
  1189  apply (simp add: int_0_less_mult_iff)
  1190  apply (blast dest: zless_trans intro: zless_add1_iff_zle [THEN iffD1])
  1191 apply (simp add: zadd_zmult_distrib2)
  1192 apply (erule zle_zless_trans)
  1193 apply (erule zadd_zless_mono2)
  1194 done
  1195 
  1196 lemma zdiv_mono2_lemma:
  1197      "[| b$*q $+ r = b'$*q' $+ r';  #0 $<= b'$*q' $+ r';   
  1198          r' $< b';  #0 $<= r;  #0 $< b';  b' $<= b |]   
  1199       ==> q $<= q'"
  1200 apply (frule q_pos_lemma, assumption+) 
  1201 apply (subgoal_tac "b$*q $< b$* (q' $+ #1)")
  1202  apply (simp add: zmult_zless_cancel1)
  1203  apply (force dest: zless_add1_iff_zle [THEN iffD1] zless_trans zless_zle_trans)
  1204 apply (subgoal_tac "b$*q = r' $- r $+ b'$*q'")
  1205  prefer 2 apply (simp add: zcompare_rls)
  1206 apply (simp (no_asm_simp) add: zadd_zmult_distrib2)
  1207 apply (subst zadd_commute [of "b $\<times> q'"], rule zadd_zless_mono)
  1208  prefer 2 apply (blast intro: zmult_zle_mono1)
  1209 apply (subgoal_tac "r' $+ #0 $< b $+ r")
  1210  apply (simp add: zcompare_rls)
  1211 apply (rule zadd_zless_mono)
  1212  apply auto
  1213 apply (blast dest: zless_zle_trans)
  1214 done
  1215 
  1216 
  1217 lemma zdiv_mono2_raw:
  1218      "[| #0 $<= a;  #0 $< b';  b' $<= b;  a \<in> int |]   
  1219       ==> a zdiv b $<= a zdiv b'"
  1220 apply (subgoal_tac "#0 $< b")
  1221  prefer 2 apply (blast dest: zless_zle_trans)
  1222 apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality)
  1223 apply (cut_tac a = "a" and b = "b'" in zmod_zdiv_equality)
  1224 apply (rule zdiv_mono2_lemma)
  1225 apply (erule subst)
  1226 apply (erule subst)
  1227 apply (simp_all add: pos_mod_sign pos_mod_bound)
  1228 done
  1229 
  1230 lemma zdiv_mono2:
  1231      "[| #0 $<= a;  #0 $< b';  b' $<= b |]   
  1232       ==> a zdiv b $<= a zdiv b'"
  1233 apply (cut_tac a = "intify (a)" in zdiv_mono2_raw)
  1234 apply auto
  1235 done
  1236 
  1237 lemma q_neg_lemma:
  1238      "[| b'$*q' $+ r' $< #0;  #0 $<= r';  #0 $< b' |] ==> q' $< #0"
  1239 apply (subgoal_tac "b'$*q' $< #0")
  1240  prefer 2 apply (force intro: zle_zless_trans)
  1241 apply (simp add: zmult_less_0_iff)
  1242 apply (blast dest: zless_trans)
  1243 done
  1244 
  1245 
  1246 
  1247 lemma zdiv_mono2_neg_lemma:
  1248      "[| b$*q $+ r = b'$*q' $+ r';  b'$*q' $+ r' $< #0;   
  1249          r $< b;  #0 $<= r';  #0 $< b';  b' $<= b |]   
  1250       ==> q' $<= q"
  1251 apply (subgoal_tac "#0 $< b")
  1252  prefer 2 apply (blast dest: zless_zle_trans)
  1253 apply (frule q_neg_lemma, assumption+) 
  1254 apply (subgoal_tac "b$*q' $< b$* (q $+ #1)")
  1255  apply (simp add: zmult_zless_cancel1)
  1256  apply (blast dest: zless_trans zless_add1_iff_zle [THEN iffD1])
  1257 apply (simp (no_asm_simp) add: zadd_zmult_distrib2)
  1258 apply (subgoal_tac "b$*q' $<= b'$*q'")
  1259  prefer 2
  1260  apply (simp add: zmult_zle_cancel2)
  1261  apply (blast dest: zless_trans)
  1262 apply (subgoal_tac "b'$*q' $+ r $< b $+ (b$*q $+ r)")
  1263  prefer 2
  1264  apply (erule ssubst)
  1265  apply simp
  1266  apply (drule_tac w' = "r" and z' = "#0" in zadd_zless_mono)
  1267   apply (assumption)
  1268  apply simp
  1269 apply (simp (no_asm_use) add: zadd_commute)
  1270 apply (rule zle_zless_trans)
  1271  prefer 2 apply (assumption)
  1272 apply (simp (no_asm_simp) add: zmult_zle_cancel2)
  1273 apply (blast dest: zless_trans)
  1274 done
  1275 
  1276 lemma zdiv_mono2_neg_raw:
  1277      "[| a $< #0;  #0 $< b';  b' $<= b;  a \<in> int |]   
  1278       ==> a zdiv b' $<= a zdiv b"
  1279 apply (subgoal_tac "#0 $< b")
  1280  prefer 2 apply (blast dest: zless_zle_trans)
  1281 apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality)
  1282 apply (cut_tac a = "a" and b = "b'" in zmod_zdiv_equality)
  1283 apply (rule zdiv_mono2_neg_lemma)
  1284 apply (erule subst)
  1285 apply (erule subst)
  1286 apply (simp_all add: pos_mod_sign pos_mod_bound)
  1287 done
  1288 
  1289 lemma zdiv_mono2_neg: "[| a $< #0;  #0 $< b';  b' $<= b |]   
  1290       ==> a zdiv b' $<= a zdiv b"
  1291 apply (cut_tac a = "intify (a)" in zdiv_mono2_neg_raw)
  1292 apply auto
  1293 done
  1294 
  1295 
  1296 
  1297 subsection{* More algebraic laws for zdiv and zmod *}
  1298 
  1299 (** proving (a*b) zdiv c = a $* (b zdiv c) $+ a * (b zmod c) **)
  1300 
  1301 lemma zmult1_lemma:
  1302      "[| quorem(<b,c>, <q,r>);  c \<in> int;  c \<noteq> #0 |]  
  1303       ==> quorem (<a$*b, c>, <a$*q $+ (a$*r) zdiv c, (a$*r) zmod c>)"
  1304 apply (auto simp add: split_ifs quorem_def neq_iff_zless zadd_zmult_distrib2
  1305                       pos_mod_sign pos_mod_bound neg_mod_sign neg_mod_bound)
  1306 apply (auto intro: raw_zmod_zdiv_equality) 
  1307 done
  1308 
  1309 lemma zdiv_zmult1_eq_raw:
  1310      "[|b \<in> int;  c \<in> int|]  
  1311       ==> (a$*b) zdiv c = a$*(b zdiv c) $+ a$*(b zmod c) zdiv c"
  1312 apply (case_tac "c = #0")
  1313  apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) 
  1314 apply (rule quorem_div_mod [THEN zmult1_lemma, THEN quorem_div])
  1315 apply auto
  1316 done
  1317 
  1318 lemma zdiv_zmult1_eq: "(a$*b) zdiv c = a$*(b zdiv c) $+ a$*(b zmod c) zdiv c"
  1319 apply (cut_tac b = "intify (b)" and c = "intify (c)" in zdiv_zmult1_eq_raw)
  1320 apply auto
  1321 done
  1322 
  1323 lemma zmod_zmult1_eq_raw:
  1324      "[|b \<in> int;  c \<in> int|] ==> (a$*b) zmod c = a$*(b zmod c) zmod c"
  1325 apply (case_tac "c = #0")
  1326  apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) 
  1327 apply (rule quorem_div_mod [THEN zmult1_lemma, THEN quorem_mod])
  1328 apply auto
  1329 done
  1330 
  1331 lemma zmod_zmult1_eq: "(a$*b) zmod c = a$*(b zmod c) zmod c"
  1332 apply (cut_tac b = "intify (b)" and c = "intify (c)" in zmod_zmult1_eq_raw)
  1333 apply auto
  1334 done
  1335 
  1336 lemma zmod_zmult1_eq': "(a$*b) zmod c = ((a zmod c) $* b) zmod c"
  1337 apply (rule trans)
  1338 apply (rule_tac b = " (b $* a) zmod c" in trans)
  1339 apply (rule_tac [2] zmod_zmult1_eq)
  1340 apply (simp_all (no_asm) add: zmult_commute)
  1341 done
  1342 
  1343 lemma zmod_zmult_distrib: "(a$*b) zmod c = ((a zmod c) $* (b zmod c)) zmod c"
  1344 apply (rule zmod_zmult1_eq' [THEN trans])
  1345 apply (rule zmod_zmult1_eq)
  1346 done
  1347 
  1348 lemma zdiv_zmult_self1 [simp]: "intify(b) \<noteq> #0 ==> (a$*b) zdiv b = intify(a)"
  1349 apply (simp (no_asm_simp) add: zdiv_zmult1_eq)
  1350 done
  1351 
  1352 lemma zdiv_zmult_self2 [simp]: "intify(b) \<noteq> #0 ==> (b$*a) zdiv b = intify(a)"
  1353 apply (subst zmult_commute , erule zdiv_zmult_self1)
  1354 done
  1355 
  1356 lemma zmod_zmult_self1 [simp]: "(a$*b) zmod b = #0"
  1357 apply (simp (no_asm) add: zmod_zmult1_eq)
  1358 done
  1359 
  1360 lemma zmod_zmult_self2 [simp]: "(b$*a) zmod b = #0"
  1361 apply (simp (no_asm) add: zmult_commute zmod_zmult1_eq)
  1362 done
  1363 
  1364 
  1365 (** proving (a$+b) zdiv c = 
  1366             a zdiv c $+ b zdiv c $+ ((a zmod c $+ b zmod c) zdiv c) **)
  1367 
  1368 lemma zadd1_lemma:
  1369      "[| quorem(<a,c>, <aq,ar>);  quorem(<b,c>, <bq,br>);   
  1370          c \<in> int;  c \<noteq> #0 |]  
  1371       ==> quorem (<a$+b, c>, <aq $+ bq $+ (ar$+br) zdiv c, (ar$+br) zmod c>)"
  1372 apply (auto simp add: split_ifs quorem_def neq_iff_zless zadd_zmult_distrib2
  1373                       pos_mod_sign pos_mod_bound neg_mod_sign neg_mod_bound)
  1374 apply (auto intro: raw_zmod_zdiv_equality)
  1375 done
  1376 
  1377 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
  1378 lemma zdiv_zadd1_eq_raw:
  1379      "[|a \<in> int; b \<in> int; c \<in> int|] ==>  
  1380       (a$+b) zdiv c = a zdiv c $+ b zdiv c $+ ((a zmod c $+ b zmod c) zdiv c)"
  1381 apply (case_tac "c = #0")
  1382  apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) 
  1383 apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod,
  1384                                  THEN quorem_div])
  1385 done
  1386 
  1387 lemma zdiv_zadd1_eq:
  1388      "(a$+b) zdiv c = a zdiv c $+ b zdiv c $+ ((a zmod c $+ b zmod c) zdiv c)"
  1389 apply (cut_tac a = "intify (a)" and b = "intify (b)" and c = "intify (c)" 
  1390        in zdiv_zadd1_eq_raw)
  1391 apply auto
  1392 done
  1393 
  1394 lemma zmod_zadd1_eq_raw:
  1395      "[|a \<in> int; b \<in> int; c \<in> int|]   
  1396       ==> (a$+b) zmod c = (a zmod c $+ b zmod c) zmod c"
  1397 apply (case_tac "c = #0")
  1398  apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) 
  1399 apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod, 
  1400                                  THEN quorem_mod])
  1401 done
  1402 
  1403 lemma zmod_zadd1_eq: "(a$+b) zmod c = (a zmod c $+ b zmod c) zmod c"
  1404 apply (cut_tac a = "intify (a)" and b = "intify (b)" and c = "intify (c)" 
  1405        in zmod_zadd1_eq_raw)
  1406 apply auto
  1407 done
  1408 
  1409 lemma zmod_div_trivial_raw:
  1410      "[|a \<in> int; b \<in> int|] ==> (a zmod b) zdiv b = #0"
  1411 apply (case_tac "b = #0")
  1412  apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) 
  1413 apply (auto simp add: neq_iff_zless pos_mod_sign pos_mod_bound
  1414          zdiv_pos_pos_trivial neg_mod_sign neg_mod_bound zdiv_neg_neg_trivial)
  1415 done
  1416 
  1417 lemma zmod_div_trivial [simp]: "(a zmod b) zdiv b = #0"
  1418 apply (cut_tac a = "intify (a)" and b = "intify (b)" in zmod_div_trivial_raw)
  1419 apply auto
  1420 done
  1421 
  1422 lemma zmod_mod_trivial_raw:
  1423      "[|a \<in> int; b \<in> int|] ==> (a zmod b) zmod b = a zmod b"
  1424 apply (case_tac "b = #0")
  1425  apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) 
  1426 apply (auto simp add: neq_iff_zless pos_mod_sign pos_mod_bound 
  1427        zmod_pos_pos_trivial neg_mod_sign neg_mod_bound zmod_neg_neg_trivial)
  1428 done
  1429 
  1430 lemma zmod_mod_trivial [simp]: "(a zmod b) zmod b = a zmod b"
  1431 apply (cut_tac a = "intify (a)" and b = "intify (b)" in zmod_mod_trivial_raw)
  1432 apply auto
  1433 done
  1434 
  1435 lemma zmod_zadd_left_eq: "(a$+b) zmod c = ((a zmod c) $+ b) zmod c"
  1436 apply (rule trans [symmetric])
  1437 apply (rule zmod_zadd1_eq)
  1438 apply (simp (no_asm))
  1439 apply (rule zmod_zadd1_eq [symmetric])
  1440 done
  1441 
  1442 lemma zmod_zadd_right_eq: "(a$+b) zmod c = (a $+ (b zmod c)) zmod c"
  1443 apply (rule trans [symmetric])
  1444 apply (rule zmod_zadd1_eq)
  1445 apply (simp (no_asm))
  1446 apply (rule zmod_zadd1_eq [symmetric])
  1447 done
  1448 
  1449 
  1450 lemma zdiv_zadd_self1 [simp]:
  1451      "intify(a) \<noteq> #0 ==> (a$+b) zdiv a = b zdiv a $+ #1"
  1452 by (simp (no_asm_simp) add: zdiv_zadd1_eq)
  1453 
  1454 lemma zdiv_zadd_self2 [simp]:
  1455      "intify(a) \<noteq> #0 ==> (b$+a) zdiv a = b zdiv a $+ #1"
  1456 by (simp (no_asm_simp) add: zdiv_zadd1_eq)
  1457 
  1458 lemma zmod_zadd_self1 [simp]: "(a$+b) zmod a = b zmod a"
  1459 apply (case_tac "a = #0")
  1460  apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) 
  1461 apply (simp (no_asm_simp) add: zmod_zadd1_eq)
  1462 done
  1463 
  1464 lemma zmod_zadd_self2 [simp]: "(b$+a) zmod a = b zmod a"
  1465 apply (case_tac "a = #0")
  1466  apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) 
  1467 apply (simp (no_asm_simp) add: zmod_zadd1_eq)
  1468 done
  1469 
  1470 
  1471 subsection{* proving  a zdiv (b*c) = (a zdiv b) zdiv c *}
  1472 
  1473 (*The condition c>0 seems necessary.  Consider that 7 zdiv ~6 = ~2 but
  1474   7 zdiv 2 zdiv ~3 = 3 zdiv ~3 = ~1.  The subcase (a zdiv b) zmod c = 0 seems
  1475   to cause particular problems.*)
  1476 
  1477 (** first, four lemmas to bound the remainder for the cases b<0 and b>0 **)
  1478 
  1479 lemma zdiv_zmult2_aux1:
  1480      "[| #0 $< c;  b $< r;  r $<= #0 |] ==> b$*c $< b$*(q zmod c) $+ r"
  1481 apply (subgoal_tac "b $* (c $- q zmod c) $< r $* #1")
  1482 apply (simp add: zdiff_zmult_distrib2 zadd_commute zcompare_rls)
  1483 apply (rule zle_zless_trans)
  1484 apply (erule_tac [2] zmult_zless_mono1)
  1485 apply (rule zmult_zle_mono2_neg)
  1486 apply (auto simp add: zcompare_rls zadd_commute add1_zle_iff pos_mod_bound)
  1487 apply (blast intro: zless_imp_zle dest: zless_zle_trans)
  1488 done
  1489 
  1490 lemma zdiv_zmult2_aux2:
  1491      "[| #0 $< c;   b $< r;  r $<= #0 |] ==> b $* (q zmod c) $+ r $<= #0"
  1492 apply (subgoal_tac "b $* (q zmod c) $<= #0")
  1493  prefer 2
  1494  apply (simp add: zmult_le_0_iff pos_mod_sign) 
  1495  apply (blast intro: zless_imp_zle dest: zless_zle_trans)
  1496 (*arithmetic*)
  1497 apply (drule zadd_zle_mono)
  1498 apply assumption
  1499 apply (simp add: zadd_commute)
  1500 done
  1501 
  1502 lemma zdiv_zmult2_aux3:
  1503      "[| #0 $< c;  #0 $<= r;  r $< b |] ==> #0 $<= b $* (q zmod c) $+ r"
  1504 apply (subgoal_tac "#0 $<= b $* (q zmod c)")
  1505  prefer 2
  1506  apply (simp add: int_0_le_mult_iff pos_mod_sign) 
  1507  apply (blast intro: zless_imp_zle dest: zle_zless_trans)
  1508 (*arithmetic*)
  1509 apply (drule zadd_zle_mono)
  1510 apply assumption
  1511 apply (simp add: zadd_commute)
  1512 done
  1513 
  1514 lemma zdiv_zmult2_aux4:
  1515      "[| #0 $< c; #0 $<= r; r $< b |] ==> b $* (q zmod c) $+ r $< b $* c"
  1516 apply (subgoal_tac "r $* #1 $< b $* (c $- q zmod c)")
  1517 apply (simp add: zdiff_zmult_distrib2 zadd_commute zcompare_rls)
  1518 apply (rule zless_zle_trans)
  1519 apply (erule zmult_zless_mono1)
  1520 apply (rule_tac [2] zmult_zle_mono2)
  1521 apply (auto simp add: zcompare_rls zadd_commute add1_zle_iff pos_mod_bound)
  1522 apply (blast intro: zless_imp_zle dest: zle_zless_trans)
  1523 done
  1524 
  1525 lemma zdiv_zmult2_lemma:
  1526      "[| quorem (<a,b>, <q,r>);  a \<in> int;  b \<in> int;  b \<noteq> #0;  #0 $< c |]  
  1527       ==> quorem (<a,b$*c>, <q zdiv c, b$*(q zmod c) $+ r>)"
  1528 apply (auto simp add: zmult_ac zmod_zdiv_equality [symmetric] quorem_def
  1529                neq_iff_zless int_0_less_mult_iff 
  1530                zadd_zmult_distrib2 [symmetric] zdiv_zmult2_aux1 zdiv_zmult2_aux2
  1531                zdiv_zmult2_aux3 zdiv_zmult2_aux4)
  1532 apply (blast dest: zless_trans)+
  1533 done
  1534 
  1535 lemma zdiv_zmult2_eq_raw:
  1536      "[|#0 $< c;  a \<in> int;  b \<in> int|] ==> a zdiv (b$*c) = (a zdiv b) zdiv c"
  1537 apply (case_tac "b = #0")
  1538  apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) 
  1539 apply (rule quorem_div_mod [THEN zdiv_zmult2_lemma, THEN quorem_div])
  1540 apply (auto simp add: intify_eq_0_iff_zle)
  1541 apply (blast dest: zle_zless_trans)
  1542 done
  1543 
  1544 lemma zdiv_zmult2_eq: "#0 $< c ==> a zdiv (b$*c) = (a zdiv b) zdiv c"
  1545 apply (cut_tac a = "intify (a)" and b = "intify (b)" in zdiv_zmult2_eq_raw)
  1546 apply auto
  1547 done
  1548 
  1549 lemma zmod_zmult2_eq_raw:
  1550      "[|#0 $< c;  a \<in> int;  b \<in> int|]  
  1551       ==> a zmod (b$*c) = b$*(a zdiv b zmod c) $+ a zmod b"
  1552 apply (case_tac "b = #0")
  1553  apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) 
  1554 apply (rule quorem_div_mod [THEN zdiv_zmult2_lemma, THEN quorem_mod])
  1555 apply (auto simp add: intify_eq_0_iff_zle)
  1556 apply (blast dest: zle_zless_trans)
  1557 done
  1558 
  1559 lemma zmod_zmult2_eq:
  1560      "#0 $< c ==> a zmod (b$*c) = b$*(a zdiv b zmod c) $+ a zmod b"
  1561 apply (cut_tac a = "intify (a)" and b = "intify (b)" in zmod_zmult2_eq_raw)
  1562 apply auto
  1563 done
  1564 
  1565 subsection{* Cancellation of common factors in "zdiv" *}
  1566 
  1567 lemma zdiv_zmult_zmult1_aux1:
  1568      "[| #0 $< b;  intify(c) \<noteq> #0 |] ==> (c$*a) zdiv (c$*b) = a zdiv b"
  1569 apply (subst zdiv_zmult2_eq)
  1570 apply auto
  1571 done
  1572 
  1573 lemma zdiv_zmult_zmult1_aux2:
  1574      "[| b $< #0;  intify(c) \<noteq> #0 |] ==> (c$*a) zdiv (c$*b) = a zdiv b"
  1575 apply (subgoal_tac " (c $* ($-a)) zdiv (c $* ($-b)) = ($-a) zdiv ($-b)")
  1576 apply (rule_tac [2] zdiv_zmult_zmult1_aux1)
  1577 apply auto
  1578 done
  1579 
  1580 lemma zdiv_zmult_zmult1_raw:
  1581      "[|intify(c) \<noteq> #0; b \<in> int|] ==> (c$*a) zdiv (c$*b) = a zdiv b"
  1582 apply (case_tac "b = #0")
  1583  apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) 
  1584 apply (auto simp add: neq_iff_zless [of b]
  1585   zdiv_zmult_zmult1_aux1 zdiv_zmult_zmult1_aux2)
  1586 done
  1587 
  1588 lemma zdiv_zmult_zmult1: "intify(c) \<noteq> #0 ==> (c$*a) zdiv (c$*b) = a zdiv b"
  1589 apply (cut_tac b = "intify (b)" in zdiv_zmult_zmult1_raw)
  1590 apply auto
  1591 done
  1592 
  1593 lemma zdiv_zmult_zmult2: "intify(c) \<noteq> #0 ==> (a$*c) zdiv (b$*c) = a zdiv b"
  1594 apply (drule zdiv_zmult_zmult1)
  1595 apply (auto simp add: zmult_commute)
  1596 done
  1597 
  1598 
  1599 subsection{* Distribution of factors over "zmod" *}
  1600 
  1601 lemma zmod_zmult_zmult1_aux1:
  1602      "[| #0 $< b;  intify(c) \<noteq> #0 |]  
  1603       ==> (c$*a) zmod (c$*b) = c $* (a zmod b)"
  1604 apply (subst zmod_zmult2_eq)
  1605 apply auto
  1606 done
  1607 
  1608 lemma zmod_zmult_zmult1_aux2:
  1609      "[| b $< #0;  intify(c) \<noteq> #0 |]  
  1610       ==> (c$*a) zmod (c$*b) = c $* (a zmod b)"
  1611 apply (subgoal_tac " (c $* ($-a)) zmod (c $* ($-b)) = c $* (($-a) zmod ($-b))")
  1612 apply (rule_tac [2] zmod_zmult_zmult1_aux1)
  1613 apply auto
  1614 done
  1615 
  1616 lemma zmod_zmult_zmult1_raw:
  1617      "[|b \<in> int; c \<in> int|] ==> (c$*a) zmod (c$*b) = c $* (a zmod b)"
  1618 apply (case_tac "b = #0")
  1619  apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) 
  1620 apply (case_tac "c = #0")
  1621  apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) 
  1622 apply (auto simp add: neq_iff_zless [of b]
  1623   zmod_zmult_zmult1_aux1 zmod_zmult_zmult1_aux2)
  1624 done
  1625 
  1626 lemma zmod_zmult_zmult1: "(c$*a) zmod (c$*b) = c $* (a zmod b)"
  1627 apply (cut_tac b = "intify (b)" and c = "intify (c)" in zmod_zmult_zmult1_raw)
  1628 apply auto
  1629 done
  1630 
  1631 lemma zmod_zmult_zmult2: "(a$*c) zmod (b$*c) = (a zmod b) $* c"
  1632 apply (cut_tac c = "c" in zmod_zmult_zmult1)
  1633 apply (auto simp add: zmult_commute)
  1634 done
  1635 
  1636 
  1637 (** Quotients of signs **)
  1638 
  1639 lemma zdiv_neg_pos_less0: "[| a $< #0;  #0 $< b |] ==> a zdiv b $< #0"
  1640 apply (subgoal_tac "a zdiv b $<= #-1")
  1641 apply (erule zle_zless_trans)
  1642 apply (simp (no_asm))
  1643 apply (rule zle_trans)
  1644 apply (rule_tac a' = "#-1" in zdiv_mono1)
  1645 apply (rule zless_add1_iff_zle [THEN iffD1])
  1646 apply (simp (no_asm))
  1647 apply (auto simp add: zdiv_minus1)
  1648 done
  1649 
  1650 lemma zdiv_nonneg_neg_le0: "[| #0 $<= a;  b $< #0 |] ==> a zdiv b $<= #0"
  1651 apply (drule zdiv_mono1_neg)
  1652 apply auto
  1653 done
  1654 
  1655 lemma pos_imp_zdiv_nonneg_iff: "#0 $< b ==> (#0 $<= a zdiv b) <-> (#0 $<= a)"
  1656 apply auto
  1657 apply (drule_tac [2] zdiv_mono1)
  1658 apply (auto simp add: neq_iff_zless)
  1659 apply (simp (no_asm_use) add: not_zless_iff_zle [THEN iff_sym])
  1660 apply (blast intro: zdiv_neg_pos_less0)
  1661 done
  1662 
  1663 lemma neg_imp_zdiv_nonneg_iff: "b $< #0 ==> (#0 $<= a zdiv b) <-> (a $<= #0)"
  1664 apply (subst zdiv_zminus_zminus [symmetric])
  1665 apply (rule iff_trans)
  1666 apply (rule pos_imp_zdiv_nonneg_iff)
  1667 apply auto
  1668 done
  1669 
  1670 (*But not (a zdiv b $<= 0 iff a$<=0); consider a=1, b=2 when a zdiv b = 0.*)
  1671 lemma pos_imp_zdiv_neg_iff: "#0 $< b ==> (a zdiv b $< #0) <-> (a $< #0)"
  1672 apply (simp (no_asm_simp) add: not_zle_iff_zless [THEN iff_sym])
  1673 apply (erule pos_imp_zdiv_nonneg_iff)
  1674 done
  1675 
  1676 (*Again the law fails for $<=: consider a = -1, b = -2 when a zdiv b = 0*)
  1677 lemma neg_imp_zdiv_neg_iff: "b $< #0 ==> (a zdiv b $< #0) <-> (#0 $< a)"
  1678 apply (simp (no_asm_simp) add: not_zle_iff_zless [THEN iff_sym])
  1679 apply (erule neg_imp_zdiv_nonneg_iff)
  1680 done
  1681 
  1682 (*
  1683  THESE REMAIN TO BE CONVERTED -- but aren't that useful!
  1684 
  1685  subsection{* Speeding up the division algorithm with shifting *}
  1686 
  1687  (** computing "zdiv" by shifting **)
  1688 
  1689  lemma pos_zdiv_mult_2: "#0 $<= a ==> (#1 $+ #2$*b) zdiv (#2$*a) = b zdiv a"
  1690  apply (case_tac "a = #0")
  1691  apply (subgoal_tac "#1 $<= a")
  1692   apply (arith_tac 2)
  1693  apply (subgoal_tac "#1 $< a $* #2")
  1694   apply (arith_tac 2)
  1695  apply (subgoal_tac "#2$* (#1 $+ b zmod a) $<= #2$*a")
  1696   apply (rule_tac [2] zmult_zle_mono2)
  1697  apply (auto simp add: zadd_commute zmult_commute add1_zle_iff pos_mod_bound)
  1698  apply (subst zdiv_zadd1_eq)
  1699  apply (simp (no_asm_simp) add: zdiv_zmult_zmult2 zmod_zmult_zmult2 zdiv_pos_pos_trivial)
  1700  apply (subst zdiv_pos_pos_trivial)
  1701  apply (simp (no_asm_simp) add: [zmod_pos_pos_trivial pos_mod_sign [THEN zadd_zle_mono1] RSN (2,zle_trans) ])
  1702  apply (auto simp add: zmod_pos_pos_trivial)
  1703  apply (subgoal_tac "#0 $<= b zmod a")
  1704   apply (asm_simp_tac (simpset () add: pos_mod_sign) 2)
  1705  apply arith
  1706  done
  1707 
  1708 
  1709  lemma neg_zdiv_mult_2: "a $<= #0 ==> (#1 $+ #2$*b) zdiv (#2$*a) <-> (b$+#1) zdiv a"
  1710  apply (subgoal_tac " (#1 $+ #2$* ($-b-#1)) zdiv (#2 $* ($-a)) <-> ($-b-#1) zdiv ($-a)")
  1711  apply (rule_tac [2] pos_zdiv_mult_2)
  1712  apply (auto simp add: zmult_zminus_right)
  1713  apply (subgoal_tac " (#-1 - (#2 $* b)) = - (#1 $+ (#2 $* b))")
  1714  apply (Simp_tac 2)
  1715  apply (asm_full_simp_tac (HOL_ss add: zdiv_zminus_zminus zdiff_def zminus_zadd_distrib [symmetric])
  1716  done
  1717 
  1718 
  1719  (*Not clear why this must be proved separately; probably integ_of causes
  1720    simplification problems*)
  1721  lemma lemma: "~ #0 $<= x ==> x $<= #0"
  1722  apply auto
  1723  done
  1724 
  1725  lemma zdiv_integ_of_BIT: "integ_of (v BIT b) zdiv integ_of (w BIT False) =  
  1726            (if ~b | #0 $<= integ_of w                    
  1727             then integ_of v zdiv (integ_of w)     
  1728             else (integ_of v $+ #1) zdiv (integ_of w))"
  1729  apply (simp_tac (simpset_of Int.thy add: zadd_assoc integ_of_BIT)
  1730  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)
  1731  done
  1732 
  1733  declare zdiv_integ_of_BIT [simp]
  1734 
  1735 
  1736  (** computing "zmod" by shifting (proofs resemble those for "zdiv") **)
  1737 
  1738  lemma pos_zmod_mult_2: "#0 $<= a ==> (#1 $+ #2$*b) zmod (#2$*a) = #1 $+ #2 $* (b zmod a)"
  1739  apply (case_tac "a = #0")
  1740  apply (subgoal_tac "#1 $<= a")
  1741   apply (arith_tac 2)
  1742  apply (subgoal_tac "#1 $< a $* #2")
  1743   apply (arith_tac 2)
  1744  apply (subgoal_tac "#2$* (#1 $+ b zmod a) $<= #2$*a")
  1745   apply (rule_tac [2] zmult_zle_mono2)
  1746  apply (auto simp add: zadd_commute zmult_commute add1_zle_iff pos_mod_bound)
  1747  apply (subst zmod_zadd1_eq)
  1748  apply (simp (no_asm_simp) add: zmod_zmult_zmult2 zmod_pos_pos_trivial)
  1749  apply (rule zmod_pos_pos_trivial)
  1750  apply (simp (no_asm_simp) # add: [zmod_pos_pos_trivial pos_mod_sign [THEN zadd_zle_mono1] RSN (2,zle_trans) ])
  1751  apply (auto simp add: zmod_pos_pos_trivial)
  1752  apply (subgoal_tac "#0 $<= b zmod a")
  1753   apply (asm_simp_tac (simpset () add: pos_mod_sign) 2)
  1754  apply arith
  1755  done
  1756 
  1757 
  1758  lemma neg_zmod_mult_2: "a $<= #0 ==> (#1 $+ #2$*b) zmod (#2$*a) = #2 $* ((b$+#1) zmod a) - #1"
  1759  apply (subgoal_tac " (#1 $+ #2$* ($-b-#1)) zmod (#2$* ($-a)) = #1 $+ #2$* (($-b-#1) zmod ($-a))")
  1760  apply (rule_tac [2] pos_zmod_mult_2)
  1761  apply (auto simp add: zmult_zminus_right)
  1762  apply (subgoal_tac " (#-1 - (#2 $* b)) = - (#1 $+ (#2 $* b))")
  1763  apply (Simp_tac 2)
  1764  apply (asm_full_simp_tac (HOL_ss add: zmod_zminus_zminus zdiff_def zminus_zadd_distrib [symmetric])
  1765  apply (dtac (zminus_equation [THEN iffD1, symmetric])
  1766  apply auto
  1767  done
  1768 
  1769  lemma zmod_integ_of_BIT: "integ_of (v BIT b) zmod integ_of (w BIT False) =  
  1770            (if b then  
  1771                  if #0 $<= integ_of w  
  1772                  then #2 $* (integ_of v zmod integ_of w) $+ #1     
  1773                  else #2 $* ((integ_of v $+ #1) zmod integ_of w) - #1   
  1774             else #2 $* (integ_of v zmod integ_of w))"
  1775  apply (simp_tac (simpset_of Int.thy add: zadd_assoc integ_of_BIT)
  1776  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)
  1777  done
  1778 
  1779  declare zmod_integ_of_BIT [simp]
  1780 *)
  1781 
  1782 ML{*
  1783 val zspos_add_zspos_imp_zspos = thm "zspos_add_zspos_imp_zspos";
  1784 val zpos_add_zpos_imp_zpos = thm "zpos_add_zpos_imp_zpos";
  1785 val zneg_add_zneg_imp_zneg = thm "zneg_add_zneg_imp_zneg";
  1786 val zneg_or_0_add_zneg_or_0_imp_zneg_or_0 = thm "zneg_or_0_add_zneg_or_0_imp_zneg_or_0";
  1787 val zero_lt_zmagnitude = thm "zero_lt_zmagnitude";
  1788 val zless_add_succ_iff = thm "zless_add_succ_iff";
  1789 val zadd_succ_zle_iff = thm "zadd_succ_zle_iff";
  1790 val zless_add1_iff_zle = thm "zless_add1_iff_zle";
  1791 val add1_zle_iff = thm "add1_zle_iff";
  1792 val add1_left_zle_iff = thm "add1_left_zle_iff";
  1793 val zmult_zle_mono1 = thm "zmult_zle_mono1";
  1794 val zmult_zle_mono1_neg = thm "zmult_zle_mono1_neg";
  1795 val zmult_zle_mono2 = thm "zmult_zle_mono2";
  1796 val zmult_zle_mono2_neg = thm "zmult_zle_mono2_neg";
  1797 val zmult_zle_mono = thm "zmult_zle_mono";
  1798 val zmult_zless_mono2 = thm "zmult_zless_mono2";
  1799 val zmult_zless_mono1 = thm "zmult_zless_mono1";
  1800 val zmult_zless_mono = thm "zmult_zless_mono";
  1801 val zmult_zless_mono1_neg = thm "zmult_zless_mono1_neg";
  1802 val zmult_zless_mono2_neg = thm "zmult_zless_mono2_neg";
  1803 val zmult_eq_0_iff = thm "zmult_eq_0_iff";
  1804 val zmult_zless_cancel2 = thm "zmult_zless_cancel2";
  1805 val zmult_zless_cancel1 = thm "zmult_zless_cancel1";
  1806 val zmult_zle_cancel2 = thm "zmult_zle_cancel2";
  1807 val zmult_zle_cancel1 = thm "zmult_zle_cancel1";
  1808 val int_eq_iff_zle = thm "int_eq_iff_zle";
  1809 val zmult_cancel2 = thm "zmult_cancel2";
  1810 val zmult_cancel1 = thm "zmult_cancel1";
  1811 val unique_quotient = thm "unique_quotient";
  1812 val unique_remainder = thm "unique_remainder";
  1813 val adjust_eq = thm "adjust_eq";
  1814 val posDivAlg_termination = thm "posDivAlg_termination";
  1815 val posDivAlg_unfold = thm "posDivAlg_unfold";
  1816 val posDivAlg_eqn = thm "posDivAlg_eqn";
  1817 val posDivAlg_induct = thm "posDivAlg_induct";
  1818 val intify_eq_0_iff_zle = thm "intify_eq_0_iff_zle";
  1819 val zmult_pos = thm "zmult_pos";
  1820 val zmult_neg = thm "zmult_neg";
  1821 val zmult_pos_neg = thm "zmult_pos_neg";
  1822 val int_0_less_mult_iff = thm "int_0_less_mult_iff";
  1823 val int_0_le_mult_iff = thm "int_0_le_mult_iff";
  1824 val zmult_less_0_iff = thm "zmult_less_0_iff";
  1825 val zmult_le_0_iff = thm "zmult_le_0_iff";
  1826 val posDivAlg_type = thm "posDivAlg_type";
  1827 val posDivAlg_correct = thm "posDivAlg_correct";
  1828 val negDivAlg_termination = thm "negDivAlg_termination";
  1829 val negDivAlg_unfold = thm "negDivAlg_unfold";
  1830 val negDivAlg_eqn = thm "negDivAlg_eqn";
  1831 val negDivAlg_induct = thm "negDivAlg_induct";
  1832 val negDivAlg_type = thm "negDivAlg_type";
  1833 val negDivAlg_correct = thm "negDivAlg_correct";
  1834 val quorem_0 = thm "quorem_0";
  1835 val posDivAlg_zero_divisor = thm "posDivAlg_zero_divisor";
  1836 val posDivAlg_0 = thm "posDivAlg_0";
  1837 val negDivAlg_minus1 = thm "negDivAlg_minus1";
  1838 val negateSnd_eq = thm "negateSnd_eq";
  1839 val negateSnd_type = thm "negateSnd_type";
  1840 val quorem_neg = thm "quorem_neg";
  1841 val divAlg_correct = thm "divAlg_correct";
  1842 val divAlg_type = thm "divAlg_type";
  1843 val zdiv_intify1 = thm "zdiv_intify1";
  1844 val zdiv_intify2 = thm "zdiv_intify2";
  1845 val zdiv_type = thm "zdiv_type";
  1846 val zmod_intify1 = thm "zmod_intify1";
  1847 val zmod_intify2 = thm "zmod_intify2";
  1848 val zmod_type = thm "zmod_type";
  1849 val DIVISION_BY_ZERO_ZDIV = thm "DIVISION_BY_ZERO_ZDIV";
  1850 val DIVISION_BY_ZERO_ZMOD = thm "DIVISION_BY_ZERO_ZMOD";
  1851 val zmod_zdiv_equality = thm "zmod_zdiv_equality";
  1852 val pos_mod = thm "pos_mod";
  1853 val pos_mod_sign = thm "pos_mod_sign";
  1854 val neg_mod = thm "neg_mod";
  1855 val neg_mod_sign = thm "neg_mod_sign";
  1856 val quorem_div_mod = thm "quorem_div_mod";
  1857 val quorem_div = thm "quorem_div";
  1858 val quorem_mod = thm "quorem_mod";
  1859 val zdiv_pos_pos_trivial = thm "zdiv_pos_pos_trivial";
  1860 val zdiv_neg_neg_trivial = thm "zdiv_neg_neg_trivial";
  1861 val zdiv_pos_neg_trivial = thm "zdiv_pos_neg_trivial";
  1862 val zmod_pos_pos_trivial = thm "zmod_pos_pos_trivial";
  1863 val zmod_neg_neg_trivial = thm "zmod_neg_neg_trivial";
  1864 val zmod_pos_neg_trivial = thm "zmod_pos_neg_trivial";
  1865 val zdiv_zminus_zminus = thm "zdiv_zminus_zminus";
  1866 val zmod_zminus_zminus = thm "zmod_zminus_zminus";
  1867 val self_quotient = thm "self_quotient";
  1868 val self_remainder = thm "self_remainder";
  1869 val zdiv_self = thm "zdiv_self";
  1870 val zmod_self = thm "zmod_self";
  1871 val zdiv_zero = thm "zdiv_zero";
  1872 val zdiv_eq_minus1 = thm "zdiv_eq_minus1";
  1873 val zmod_zero = thm "zmod_zero";
  1874 val zdiv_minus1 = thm "zdiv_minus1";
  1875 val zmod_minus1 = thm "zmod_minus1";
  1876 val zdiv_pos_pos = thm "zdiv_pos_pos";
  1877 val zmod_pos_pos = thm "zmod_pos_pos";
  1878 val zdiv_neg_pos = thm "zdiv_neg_pos";
  1879 val zmod_neg_pos = thm "zmod_neg_pos";
  1880 val zdiv_pos_neg = thm "zdiv_pos_neg";
  1881 val zmod_pos_neg = thm "zmod_pos_neg";
  1882 val zdiv_neg_neg = thm "zdiv_neg_neg";
  1883 val zmod_neg_neg = thm "zmod_neg_neg";
  1884 val zmod_1 = thm "zmod_1";
  1885 val zdiv_1 = thm "zdiv_1";
  1886 val zmod_minus1_right = thm "zmod_minus1_right";
  1887 val zdiv_minus1_right = thm "zdiv_minus1_right";
  1888 val zdiv_mono1 = thm "zdiv_mono1";
  1889 val zdiv_mono1_neg = thm "zdiv_mono1_neg";
  1890 val zdiv_mono2 = thm "zdiv_mono2";
  1891 val zdiv_mono2_neg = thm "zdiv_mono2_neg";
  1892 val zdiv_zmult1_eq = thm "zdiv_zmult1_eq";
  1893 val zmod_zmult1_eq = thm "zmod_zmult1_eq";
  1894 val zmod_zmult1_eq' = thm "zmod_zmult1_eq'";
  1895 val zmod_zmult_distrib = thm "zmod_zmult_distrib";
  1896 val zdiv_zmult_self1 = thm "zdiv_zmult_self1";
  1897 val zdiv_zmult_self2 = thm "zdiv_zmult_self2";
  1898 val zmod_zmult_self1 = thm "zmod_zmult_self1";
  1899 val zmod_zmult_self2 = thm "zmod_zmult_self2";
  1900 val zdiv_zadd1_eq = thm "zdiv_zadd1_eq";
  1901 val zmod_zadd1_eq = thm "zmod_zadd1_eq";
  1902 val zmod_div_trivial = thm "zmod_div_trivial";
  1903 val zmod_mod_trivial = thm "zmod_mod_trivial";
  1904 val zmod_zadd_left_eq = thm "zmod_zadd_left_eq";
  1905 val zmod_zadd_right_eq = thm "zmod_zadd_right_eq";
  1906 val zdiv_zadd_self1 = thm "zdiv_zadd_self1";
  1907 val zdiv_zadd_self2 = thm "zdiv_zadd_self2";
  1908 val zmod_zadd_self1 = thm "zmod_zadd_self1";
  1909 val zmod_zadd_self2 = thm "zmod_zadd_self2";
  1910 val zdiv_zmult2_eq = thm "zdiv_zmult2_eq";
  1911 val zmod_zmult2_eq = thm "zmod_zmult2_eq";
  1912 val zdiv_zmult_zmult1 = thm "zdiv_zmult_zmult1";
  1913 val zdiv_zmult_zmult2 = thm "zdiv_zmult_zmult2";
  1914 val zmod_zmult_zmult1 = thm "zmod_zmult_zmult1";
  1915 val zmod_zmult_zmult2 = thm "zmod_zmult_zmult2";
  1916 val zdiv_neg_pos_less0 = thm "zdiv_neg_pos_less0";
  1917 val zdiv_nonneg_neg_le0 = thm "zdiv_nonneg_neg_le0";
  1918 val pos_imp_zdiv_nonneg_iff = thm "pos_imp_zdiv_nonneg_iff";
  1919 val neg_imp_zdiv_nonneg_iff = thm "neg_imp_zdiv_nonneg_iff";
  1920 val pos_imp_zdiv_neg_iff = thm "pos_imp_zdiv_neg_iff";
  1921 val neg_imp_zdiv_neg_iff = thm "neg_imp_zdiv_neg_iff";
  1922 *}
  1923 
  1924 end
  1925