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