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