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