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