src/HOL/Integ/IntDiv.ML
 author wenzelm Sun Jul 16 20:56:32 2000 +0200 (2000-07-16) changeset 9367 df7a4824111e parent 9108 9fff97d29837 child 9422 4b6bc2b347e5 permissions -rw-r--r--
tuned;
```     1 (*  Title:      HOL/IntDiv.ML
```
```     2     ID:         \$Id\$
```
```     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     4     Copyright   1999  University of Cambridge
```
```     5
```
```     6 The division operators div, mod and the divides relation "dvd"
```
```     7
```
```     8 Here is the division algorithm in ML:
```
```     9
```
```    10     fun posDivAlg (a,b) =
```
```    11       if a<b then (0,a)
```
```    12       else let val (q,r) = posDivAlg(a, 2*b)
```
```    13 	       in  if 0<=r-b then (2*q+1, r-b) else (2*q, r)
```
```    14 	   end;
```
```    15
```
```    16     fun negDivAlg (a,b) =
```
```    17       if 0<=a+b then (~1,a+b)
```
```    18       else let val (q,r) = negDivAlg(a, 2*b)
```
```    19 	       in  if 0<=r-b then (2*q+1, r-b) else (2*q, r)
```
```    20 	   end;
```
```    21
```
```    22     fun negateSnd (q,r:int) = (q,~r);
```
```    23
```
```    24     fun divAlg (a,b) = if 0<=a then
```
```    25 			  if b>0 then posDivAlg (a,b)
```
```    26 			   else if a=0 then (0,0)
```
```    27 				else negateSnd (negDivAlg (~a,~b))
```
```    28 		       else
```
```    29 			  if 0<b then negDivAlg (a,b)
```
```    30 			  else        negateSnd (posDivAlg (~a,~b));
```
```    31 *)
```
```    32
```
```    33 Addsimps [zless_nat_conj];
```
```    34
```
```    35 (*** Uniqueness and monotonicity of quotients and remainders ***)
```
```    36
```
```    37 Goal "[| b*q' + r'  <= b*q + r;  #0 <= r';  #0 < b;  r < b |] \
```
```    38 \     ==> q' <= (q::int)";
```
```    39 by (subgoal_tac "r' + b * (q'-q) <= r" 1);
```
```    40 by (simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 2);
```
```    41 by (subgoal_tac "#0 < b * (#1 + q - q')" 1);
```
```    42 by (etac order_le_less_trans 2);
```
```    43 by (full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2,
```
```    44 				       zadd_zmult_distrib2]) 2);
```
```    45 by (subgoal_tac "b * q' < b * (#1 + q)" 1);
```
```    46 by (full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2,
```
```    47 				       zadd_zmult_distrib2]) 2);
```
```    48 by (Asm_full_simp_tac 1);
```
```    49 qed "unique_quotient_lemma";
```
```    50
```
```    51 Goal "[| b*q' + r' <= b*q + r;  r <= #0;  b < #0;  b < r' |] \
```
```    52 \     ==> q <= (q'::int)";
```
```    53 by (res_inst_tac [("b", "-b"), ("r", "-r'"), ("r'", "-r")]
```
```    54     unique_quotient_lemma 1);
```
```    55 by (auto_tac (claset(),
```
```    56 	      simpset() addsimps [zmult_zminus, zmult_zminus_right]));
```
```    57 qed "unique_quotient_lemma_neg";
```
```    58
```
```    59
```
```    60 Goal "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  b ~= #0 |] \
```
```    61 \     ==> q = q'";
```
```    62 by (asm_full_simp_tac
```
```    63     (simpset() addsimps split_ifs@
```
```    64                         [quorem_def, linorder_neq_iff]) 1);
```
```    65 by Safe_tac;
```
```    66 by (ALLGOALS Asm_full_simp_tac);
```
```    67 by (REPEAT
```
```    68     (blast_tac (claset() addIs [order_antisym]
```
```    69 			 addDs [order_eq_refl RS unique_quotient_lemma,
```
```    70 				order_eq_refl RS unique_quotient_lemma_neg,
```
```    71 				sym]) 1));
```
```    72 qed "unique_quotient";
```
```    73
```
```    74
```
```    75 Goal "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  b ~= #0 |] \
```
```    76 \     ==> r = r'";
```
```    77 by (subgoal_tac "q = q'" 1);
```
```    78 by (blast_tac (claset() addIs [unique_quotient]) 2);
```
```    79 by (asm_full_simp_tac (simpset() addsimps [quorem_def]) 1);
```
```    80 qed "unique_remainder";
```
```    81
```
```    82
```
```    83 (*** Correctness of posDivAlg, the division algorithm for a>=0 and b>0 ***)
```
```    84
```
```    85
```
```    86 Goal "adjust a b (q,r) = (let diff = r-b in \
```
```    87 \                         if #0 <= diff then (#2*q + #1, diff)  \
```
```    88 \                                       else (#2*q, r))";
```
```    89 by (simp_tac (simpset() addsimps [Let_def,adjust_def]) 1);
```
```    90 qed "adjust_eq";
```
```    91 Addsimps [adjust_eq];
```
```    92
```
```    93 (*Proving posDivAlg's termination condition*)
```
```    94 val [tc] = posDivAlg.tcs;
```
```    95 goalw_cterm [] (cterm_of (sign_of (the_context ())) (HOLogic.mk_Trueprop tc));
```
```    96 by Auto_tac;
```
```    97 val lemma = result();
```
```    98
```
```    99 (* removing the termination condition from the generated theorems *)
```
```   100
```
```   101 bind_thm ("posDivAlg_raw_eqn", lemma RS hd posDivAlg.simps);
```
```   102
```
```   103 (**use with simproc to avoid re-proving the premise*)
```
```   104 Goal "#0 < b ==> \
```
```   105 \     posDivAlg (a,b) =      \
```
```   106 \      (if a<b then (#0,a) else adjust a b (posDivAlg(a, #2*b)))";
```
```   107 by (rtac (posDivAlg_raw_eqn RS trans) 1);
```
```   108 by (Asm_simp_tac 1);
```
```   109 qed "posDivAlg_eqn";
```
```   110
```
```   111 bind_thm ("posDivAlg_induct", lemma RS posDivAlg.induct);
```
```   112
```
```   113
```
```   114 (*Correctness of posDivAlg: it computes quotients correctly*)
```
```   115 Goal "#0 <= a --> #0 < b --> quorem ((a, b), posDivAlg (a, b))";
```
```   116 by (res_inst_tac [("u", "a"), ("v", "b")] posDivAlg_induct 1);
```
```   117 by Auto_tac;
```
```   118 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [quorem_def])));
```
```   119 (*base case: a<b*)
```
```   120 by (asm_full_simp_tac (simpset() addsimps [posDivAlg_eqn]) 1);
```
```   121 (*main argument*)
```
```   122 by (stac posDivAlg_eqn 1);
```
```   123 by (ALLGOALS Asm_simp_tac);
```
```   124 by (etac splitE 1);
```
```   125 by (auto_tac (claset(), simpset() addsimps [zadd_zmult_distrib2, Let_def]));
```
```   126 qed_spec_mp "posDivAlg_correct";
```
```   127
```
```   128
```
```   129 (*** Correctness of negDivAlg, the division algorithm for a<0 and b>0 ***)
```
```   130
```
```   131 (*Proving negDivAlg's termination condition*)
```
```   132 val [tc] = negDivAlg.tcs;
```
```   133 goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc));
```
```   134 by Auto_tac;
```
```   135 val lemma = result();
```
```   136
```
```   137 (* removing the termination condition from the generated theorems *)
```
```   138
```
```   139 bind_thm ("negDivAlg_raw_eqn", lemma RS hd negDivAlg.simps);
```
```   140
```
```   141 (**use with simproc to avoid re-proving the premise*)
```
```   142 Goal "#0 < b ==> \
```
```   143 \     negDivAlg (a,b) =      \
```
```   144 \      (if #0<=a+b then (#-1,a+b) else adjust a b (negDivAlg(a, #2*b)))";
```
```   145 by (rtac (negDivAlg_raw_eqn RS trans) 1);
```
```   146 by (Asm_simp_tac 1);
```
```   147 qed "negDivAlg_eqn";
```
```   148
```
```   149 bind_thm ("negDivAlg_induct", lemma RS negDivAlg.induct);
```
```   150
```
```   151
```
```   152 (*Correctness of negDivAlg: it computes quotients correctly
```
```   153   It doesn't work if a=0 because the 0/b=0 rather than -1*)
```
```   154 Goal "a < #0 --> #0 < b --> quorem ((a, b), negDivAlg (a, b))";
```
```   155 by (res_inst_tac [("u", "a"), ("v", "b")] negDivAlg_induct 1);
```
```   156 by Auto_tac;
```
```   157 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [quorem_def])));
```
```   158 (*base case: 0<=a+b*)
```
```   159 by (asm_full_simp_tac (simpset() addsimps [negDivAlg_eqn]) 1);
```
```   160 (*main argument*)
```
```   161 by (stac negDivAlg_eqn 1);
```
```   162 by (ALLGOALS Asm_simp_tac);
```
```   163 by (etac splitE 1);
```
```   164 by (auto_tac (claset(), simpset() addsimps [zadd_zmult_distrib2, Let_def]));
```
```   165 qed_spec_mp "negDivAlg_correct";
```
```   166
```
```   167
```
```   168 (*** Existence shown by proving the division algorithm to be correct ***)
```
```   169
```
```   170 (*the case a=0*)
```
```   171 Goal "b ~= #0 ==> quorem ((#0,b), (#0,#0))";
```
```   172 by (auto_tac (claset(),
```
```   173 	      simpset() addsimps [quorem_def, linorder_neq_iff]));
```
```   174 qed "quorem_0";
```
```   175
```
```   176 Goal "posDivAlg (#0, b) = (#0, #0)";
```
```   177 by (stac posDivAlg_raw_eqn 1);
```
```   178 by Auto_tac;
```
```   179 qed "posDivAlg_0";
```
```   180 Addsimps [posDivAlg_0];
```
```   181
```
```   182 Goal "negDivAlg (#-1, b) = (#-1, b-#1)";
```
```   183 by (stac negDivAlg_raw_eqn 1);
```
```   184 by Auto_tac;
```
```   185 qed "negDivAlg_minus1";
```
```   186 Addsimps [negDivAlg_minus1];
```
```   187
```
```   188 Goalw [negateSnd_def] "negateSnd(q,r) = (q,-r)";
```
```   189 by Auto_tac;
```
```   190 qed "negateSnd_eq";
```
```   191 Addsimps [negateSnd_eq];
```
```   192
```
```   193 Goal "quorem ((-a,-b), qr) ==> quorem ((a,b), negateSnd qr)";
```
```   194 by (auto_tac (claset(), simpset() addsimps split_ifs@[quorem_def]));
```
```   195 qed "quorem_neg";
```
```   196
```
```   197 Goal "b ~= #0 ==> quorem ((a,b), divAlg(a,b))";
```
```   198 by (auto_tac (claset(),
```
```   199 	      simpset() addsimps [quorem_0, divAlg_def]));
```
```   200 by (REPEAT_FIRST (resolve_tac [quorem_neg, posDivAlg_correct,
```
```   201 			       negDivAlg_correct]));
```
```   202 by (auto_tac (claset(),
```
```   203 	      simpset() addsimps [quorem_def, linorder_neq_iff]));
```
```   204 qed "divAlg_correct";
```
```   205
```
```   206 (** Aribtrary definitions for division by zero.  Useful to simplify
```
```   207     certain equations **)
```
```   208
```
```   209 Goal "a div (#0::int) = #0";
```
```   210 by (simp_tac (simpset() addsimps [div_def, divAlg_def, posDivAlg_raw_eqn]) 1);
```
```   211 qed "DIVISION_BY_ZERO_ZDIV";  (*NOT for adding to default simpset*)
```
```   212
```
```   213 Goal "a mod (#0::int) = a";
```
```   214 by (simp_tac (simpset() addsimps [mod_def, divAlg_def, posDivAlg_raw_eqn]) 1);
```
```   215 qed "DIVISION_BY_ZERO_ZMOD";  (*NOT for adding to default simpset*)
```
```   216
```
```   217 fun zdiv_undefined_case_tac s i =
```
```   218   case_tac s i THEN
```
```   219   asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO_ZDIV,
```
```   220 				    DIVISION_BY_ZERO_ZMOD]) i;
```
```   221
```
```   222 (** Basic laws about division and remainder **)
```
```   223
```
```   224 Goal "(a::int) = b * (a div b) + (a mod b)";
```
```   225 by (zdiv_undefined_case_tac "b = #0" 1);
```
```   226 by (cut_inst_tac [("a","a"),("b","b")] divAlg_correct 1);
```
```   227 by (auto_tac (claset(),
```
```   228 	      simpset() addsimps [quorem_def, div_def, mod_def]));
```
```   229 qed "zmod_zdiv_equality";
```
```   230
```
```   231 Goal "(#0::int) < b ==> #0 <= a mod b & a mod b < b";
```
```   232 by (cut_inst_tac [("a","a"),("b","b")] divAlg_correct 1);
```
```   233 by (auto_tac (claset(),
```
```   234 	      simpset() addsimps [quorem_def, mod_def]));
```
```   235 bind_thm ("pos_mod_sign", result() RS conjunct1);
```
```   236 bind_thm ("pos_mod_bound", result() RS conjunct2);
```
```   237
```
```   238 Goal "b < (#0::int) ==> a mod b <= #0 & b < a mod b";
```
```   239 by (cut_inst_tac [("a","a"),("b","b")] divAlg_correct 1);
```
```   240 by (auto_tac (claset(),
```
```   241 	      simpset() addsimps [quorem_def, div_def, mod_def]));
```
```   242 bind_thm ("neg_mod_sign", result() RS conjunct1);
```
```   243 bind_thm ("neg_mod_bound", result() RS conjunct2);
```
```   244
```
```   245
```
```   246 (** proving general properties of div and mod **)
```
```   247
```
```   248 Goal "b ~= #0 ==> quorem ((a, b), (a div b, a mod b))";
```
```   249 by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1);
```
```   250 by (auto_tac
```
```   251     (claset(),
```
```   252      simpset() addsimps [quorem_def, linorder_neq_iff,
```
```   253 			 pos_mod_sign,pos_mod_bound,
```
```   254 			 neg_mod_sign, neg_mod_bound]));
```
```   255 qed "quorem_div_mod";
```
```   256
```
```   257 Goal "[| quorem((a,b),(q,r));  b ~= #0 |] ==> a div b = q";
```
```   258 by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_quotient]) 1);
```
```   259 qed "quorem_div";
```
```   260
```
```   261 Goal "[| quorem((a,b),(q,r));  b ~= #0 |] ==> a mod b = r";
```
```   262 by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_remainder]) 1);
```
```   263 qed "quorem_mod";
```
```   264
```
```   265 Goal "[| (#0::int) <= a;  a < b |] ==> a div b = #0";
```
```   266 by (rtac quorem_div 1);
```
```   267 by (auto_tac (claset(), simpset() addsimps [quorem_def]));
```
```   268 qed "div_pos_pos_trivial";
```
```   269
```
```   270 Goal "[| a <= (#0::int);  b < a |] ==> a div b = #0";
```
```   271 by (rtac quorem_div 1);
```
```   272 by (auto_tac (claset(), simpset() addsimps [quorem_def]));
```
```   273 qed "div_neg_neg_trivial";
```
```   274
```
```   275 Goal "[| (#0::int) < a;  a+b <= #0 |] ==> a div b = #-1";
```
```   276 by (rtac quorem_div 1);
```
```   277 by (auto_tac (claset(), simpset() addsimps [quorem_def]));
```
```   278 qed "div_pos_neg_trivial";
```
```   279
```
```   280 (*There is no div_neg_pos_trivial because  #0 div b = #0 would supersede it*)
```
```   281
```
```   282 Goal "[| (#0::int) <= a;  a < b |] ==> a mod b = a";
```
```   283 by (res_inst_tac [("q","#0")] quorem_mod 1);
```
```   284 by (auto_tac (claset(), simpset() addsimps [quorem_def]));
```
```   285 qed "mod_pos_pos_trivial";
```
```   286
```
```   287 Goal "[| a <= (#0::int);  b < a |] ==> a mod b = a";
```
```   288 by (res_inst_tac [("q","#0")] quorem_mod 1);
```
```   289 by (auto_tac (claset(), simpset() addsimps [quorem_def]));
```
```   290 qed "mod_neg_neg_trivial";
```
```   291
```
```   292 Goal "[| (#0::int) < a;  a+b <= #0 |] ==> a mod b = a+b";
```
```   293 by (res_inst_tac [("q","#-1")] quorem_mod 1);
```
```   294 by (auto_tac (claset(), simpset() addsimps [quorem_def]));
```
```   295 qed "mod_pos_neg_trivial";
```
```   296
```
```   297 (*There is no mod_neg_pos_trivial...*)
```
```   298
```
```   299
```
```   300 (*Simpler laws such as -a div b = -(a div b) FAIL*)
```
```   301 Goal "(-a) div (-b) = a div (b::int)";
```
```   302 by (zdiv_undefined_case_tac "b = #0" 1);
```
```   303 by (stac ((simplify(simpset()) (quorem_div_mod RS quorem_neg))
```
```   304 	  RS quorem_div) 1);
```
```   305 by Auto_tac;
```
```   306 qed "zdiv_zminus_zminus";
```
```   307 Addsimps [zdiv_zminus_zminus];
```
```   308
```
```   309 (*Simpler laws such as -a mod b = -(a mod b) FAIL*)
```
```   310 Goal "(-a) mod (-b) = - (a mod (b::int))";
```
```   311 by (zdiv_undefined_case_tac "b = #0" 1);
```
```   312 by (stac ((simplify(simpset()) (quorem_div_mod RS quorem_neg))
```
```   313 	  RS quorem_mod) 1);
```
```   314 by Auto_tac;
```
```   315 qed "zmod_zminus_zminus";
```
```   316 Addsimps [zmod_zminus_zminus];
```
```   317
```
```   318
```
```   319 (*** division of a number by itself ***)
```
```   320
```
```   321 Goal "[| (#0::int) < a; a = r + a*q; r < a |] ==> #1 <= q";
```
```   322 by (subgoal_tac "#0 < a*q" 1);
```
```   323 by (arith_tac 2);
```
```   324 by (asm_full_simp_tac (simpset() addsimps [int_0_less_mult_iff]) 1);
```
```   325 val lemma1 = result();
```
```   326
```
```   327 Goal "[| (#0::int) < a; a = r + a*q; #0 <= r |] ==> q <= #1";
```
```   328 by (subgoal_tac "#0 <= a*(#1-q)" 1);
```
```   329 by (asm_simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 2);
```
```   330 by (asm_full_simp_tac (simpset() addsimps [int_0_le_mult_iff]) 1);
```
```   331 val lemma2 = result();
```
```   332
```
```   333 Goal "[| quorem((a,a),(q,r));  a ~= (#0::int) |] ==> q = #1";
```
```   334 by (asm_full_simp_tac
```
```   335     (simpset() addsimps split_ifs@[quorem_def, linorder_neq_iff]) 1);
```
```   336 by (rtac order_antisym 1);
```
```   337 by Safe_tac;
```
```   338 by Auto_tac;
```
```   339 by (res_inst_tac [("a", "-a"),("r", "-r")] lemma1 3);
```
```   340 by (res_inst_tac [("a", "-a"),("r", "-r")] lemma2 1);
```
```   341 by (REPEAT (force_tac  (claset() addIs [lemma1,lemma2],
```
```   342 	      simpset() addsimps [zadd_commute, zmult_zminus]) 1));
```
```   343 qed "self_quotient";
```
```   344
```
```   345 Goal "[| quorem((a,a),(q,r));  a ~= (#0::int) |] ==> r = #0";
```
```   346 by (ftac self_quotient 1);
```
```   347 by (assume_tac 1);
```
```   348 by (asm_full_simp_tac (simpset() addsimps [quorem_def]) 1);
```
```   349 qed "self_remainder";
```
```   350
```
```   351 Goal "a ~= #0 ==> a div a = (#1::int)";
```
```   352 by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS self_quotient]) 1);
```
```   353 qed "zdiv_self";
```
```   354 Addsimps [zdiv_self];
```
```   355
```
```   356 (*Here we have 0 mod 0 = 0, also assumed by Knuth (who puts m mod 0 = 0) *)
```
```   357 Goal "a mod a = (#0::int)";
```
```   358 by (zdiv_undefined_case_tac "a = #0" 1);
```
```   359 by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS self_remainder]) 1);
```
```   360 qed "zmod_self";
```
```   361 Addsimps [zmod_self];
```
```   362
```
```   363
```
```   364 (*** Computation of division and remainder ***)
```
```   365
```
```   366 Goal "(#0::int) div b = #0";
```
```   367 by (simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
```
```   368 qed "zdiv_zero";
```
```   369
```
```   370 Goal "(#0::int) < b ==> #-1 div b = #-1";
```
```   371 by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
```
```   372 qed "div_eq_minus1";
```
```   373
```
```   374 Goal "(#0::int) mod b = #0";
```
```   375 by (simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
```
```   376 qed "zmod_zero";
```
```   377
```
```   378 Addsimps [zdiv_zero, zmod_zero];
```
```   379
```
```   380 Goal "(#0::int) < b ==> #-1 div b = #-1";
```
```   381 by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
```
```   382 qed "zdiv_minus1";
```
```   383
```
```   384 Goal "(#0::int) < b ==> #-1 mod b = b-#1";
```
```   385 by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
```
```   386 qed "zmod_minus1";
```
```   387
```
```   388 (** a positive, b positive **)
```
```   389
```
```   390 Goal "[| #0 < a;  #0 <= b |] ==> a div b = fst (posDivAlg(a,b))";
```
```   391 by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
```
```   392 qed "div_pos_pos";
```
```   393
```
```   394 Goal "[| #0 < a;  #0 <= b |] ==> a mod b = snd (posDivAlg(a,b))";
```
```   395 by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
```
```   396 qed "mod_pos_pos";
```
```   397
```
```   398 (** a negative, b positive **)
```
```   399
```
```   400 Goal "[| a < #0;  #0 < b |] ==> a div b = fst (negDivAlg(a,b))";
```
```   401 by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
```
```   402 qed "div_neg_pos";
```
```   403
```
```   404 Goal "[| a < #0;  #0 < b |] ==> a mod b = snd (negDivAlg(a,b))";
```
```   405 by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
```
```   406 qed "mod_neg_pos";
```
```   407
```
```   408 (** a positive, b negative **)
```
```   409
```
```   410 Goal "[| #0 < a;  b < #0 |] ==> a div b = fst (negateSnd(negDivAlg(-a,-b)))";
```
```   411 by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
```
```   412 qed "div_pos_neg";
```
```   413
```
```   414 Goal "[| #0 < a;  b < #0 |] ==> a mod b = snd (negateSnd(negDivAlg(-a,-b)))";
```
```   415 by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
```
```   416 qed "mod_pos_neg";
```
```   417
```
```   418 (** a negative, b negative **)
```
```   419
```
```   420 Goal "[| a < #0;  b <= #0 |] ==> a div b = fst (negateSnd(posDivAlg(-a,-b)))";
```
```   421 by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
```
```   422 qed "div_neg_neg";
```
```   423
```
```   424 Goal "[| a < #0;  b <= #0 |] ==> a mod b = snd (negateSnd(posDivAlg(-a,-b)))";
```
```   425 by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
```
```   426 qed "mod_neg_neg";
```
```   427
```
```   428 Addsimps (map (read_instantiate_sg (sign_of IntDiv.thy)
```
```   429 	       [("a", "number_of ?v"), ("b", "number_of ?w")])
```
```   430 	  [div_pos_pos, div_neg_pos, div_pos_neg, div_neg_neg,
```
```   431 	   mod_pos_pos, mod_neg_pos, mod_pos_neg, mod_neg_neg,
```
```   432 	   posDivAlg_eqn, negDivAlg_eqn]);
```
```   433
```
```   434
```
```   435 (** Special-case simplification **)
```
```   436
```
```   437 Goal "a mod (#1::int) = #0";
```
```   438 by (cut_inst_tac [("a","a"),("b","#1")] pos_mod_sign 1);
```
```   439 by (cut_inst_tac [("a","a"),("b","#1")] pos_mod_bound 2);
```
```   440 by Auto_tac;
```
```   441 qed "zmod_1";
```
```   442 Addsimps [zmod_1];
```
```   443
```
```   444 Goal "a div (#1::int) = a";
```
```   445 by (cut_inst_tac [("a","a"),("b","#1")] zmod_zdiv_equality 1);
```
```   446 by Auto_tac;
```
```   447 qed "zdiv_1";
```
```   448 Addsimps [zdiv_1];
```
```   449
```
```   450 Goal "a mod (#-1::int) = #0";
```
```   451 by (cut_inst_tac [("a","a"),("b","#-1")] neg_mod_sign 1);
```
```   452 by (cut_inst_tac [("a","a"),("b","#-1")] neg_mod_bound 2);
```
```   453 by Auto_tac;
```
```   454 qed "zmod_minus1_right";
```
```   455 Addsimps [zmod_minus1_right];
```
```   456
```
```   457 Goal "a div (#-1::int) = -a";
```
```   458 by (cut_inst_tac [("a","a"),("b","#-1")] zmod_zdiv_equality 1);
```
```   459 by Auto_tac;
```
```   460 qed "zdiv_minus1_right";
```
```   461 Addsimps [zdiv_minus1_right];
```
```   462
```
```   463
```
```   464 (*** Monotonicity in the first argument (divisor) ***)
```
```   465
```
```   466 Goal "[| a <= a';  #0 < (b::int) |] ==> a div b <= a' div b";
```
```   467 by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1);
```
```   468 by (cut_inst_tac [("a","a'"),("b","b")] zmod_zdiv_equality 1);
```
```   469 by (rtac unique_quotient_lemma 1);
```
```   470 by (etac subst 1);
```
```   471 by (etac subst 1);
```
```   472 by (ALLGOALS (asm_simp_tac (simpset() addsimps [pos_mod_sign,pos_mod_bound])));
```
```   473 qed "zdiv_mono1";
```
```   474
```
```   475 Goal "[| a <= a';  (b::int) < #0 |] ==> a' div b <= a div b";
```
```   476 by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1);
```
```   477 by (cut_inst_tac [("a","a'"),("b","b")] zmod_zdiv_equality 1);
```
```   478 by (rtac unique_quotient_lemma_neg 1);
```
```   479 by (etac subst 1);
```
```   480 by (etac subst 1);
```
```   481 by (ALLGOALS (asm_simp_tac (simpset() addsimps [neg_mod_sign,neg_mod_bound])));
```
```   482 qed "zdiv_mono1_neg";
```
```   483
```
```   484
```
```   485 (*** Monotonicity in the second argument (dividend) ***)
```
```   486
```
```   487 Goal "[| b*q + r = b'*q' + r';  #0 <= b'*q' + r';  \
```
```   488 \        r' < b';  #0 <= r;  #0 < b';  b' <= b |]  \
```
```   489 \     ==> q <= (q'::int)";
```
```   490 by (subgoal_tac "#0 <= q'" 1);
```
```   491  by (subgoal_tac "#0 < b'*(q' + #1)" 2);
```
```   492   by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 3);
```
```   493  by (asm_full_simp_tac (simpset() addsimps [int_0_less_mult_iff]) 2);
```
```   494 by (subgoal_tac "b*q < b*(q' + #1)" 1);
```
```   495  by (Asm_full_simp_tac 1);
```
```   496 by (subgoal_tac "b*q = r' - r + b'*q'" 1);
```
```   497  by (Simp_tac 2);
```
```   498 by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1);
```
```   499 by (stac zadd_commute 1 THEN rtac zadd_zless_mono 1 THEN arith_tac 1);
```
```   500 by (rtac zmult_zle_mono1 1);
```
```   501 by Auto_tac;
```
```   502 qed "zdiv_mono2_lemma";
```
```   503
```
```   504 Goal "[| (#0::int) <= a;  #0 < b';  b' <= b |]  \
```
```   505 \     ==> a div b <= a div b'";
```
```   506 by (subgoal_tac "b ~= #0" 1);
```
```   507 by (arith_tac 2);
```
```   508 by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1);
```
```   509 by (cut_inst_tac [("a","a"),("b","b'")] zmod_zdiv_equality 1);
```
```   510 by (rtac zdiv_mono2_lemma 1);
```
```   511 by (etac subst 1);
```
```   512 by (etac subst 1);
```
```   513 by (ALLGOALS (asm_simp_tac (simpset() addsimps [pos_mod_sign,pos_mod_bound])));
```
```   514 qed "zdiv_mono2";
```
```   515
```
```   516 Goal "[| b*q + r = b'*q' + r';  b'*q' + r' < #0;  \
```
```   517 \        r < b;  #0 <= r';  #0 < b';  b' <= b |]  \
```
```   518 \     ==> q' <= (q::int)";
```
```   519 by (subgoal_tac "q' < #0" 1);
```
```   520  by (subgoal_tac "b'*q' < #0" 2);
```
```   521   by (arith_tac 3);
```
```   522  by (asm_full_simp_tac (simpset() addsimps [zmult_less_0_iff]) 2);
```
```   523 by (subgoal_tac "b*q' < b*(q + #1)" 1);
```
```   524  by (Asm_full_simp_tac 1);
```
```   525 by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1);
```
```   526 by (subgoal_tac "b*q' <= b'*q'" 1);
```
```   527  by (asm_simp_tac (simpset() addsimps [zmult_zle_mono1_neg]) 2);
```
```   528 by (subgoal_tac "b'*q' < b + b*q" 1);
```
```   529  by (Asm_simp_tac 2);
```
```   530 by (arith_tac 1);
```
```   531 qed "zdiv_mono2_neg_lemma";
```
```   532
```
```   533 Goal "[| a < (#0::int);  #0 < b';  b' <= b |]  \
```
```   534 \     ==> a div b' <= a div b";
```
```   535 by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1);
```
```   536 by (cut_inst_tac [("a","a"),("b","b'")] zmod_zdiv_equality 1);
```
```   537 by (rtac zdiv_mono2_neg_lemma 1);
```
```   538 by (etac subst 1);
```
```   539 by (etac subst 1);
```
```   540 by (ALLGOALS (asm_simp_tac (simpset() addsimps [pos_mod_sign,pos_mod_bound])));
```
```   541 qed "zdiv_mono2_neg";
```
```   542
```
```   543
```
```   544 (*** More algebraic laws for div and mod ***)
```
```   545
```
```   546 (** proving (a*b) div c = a * (b div c) + a * (b mod c) **)
```
```   547
```
```   548 Goal "[| quorem((b,c),(q,r));  c ~= #0 |] \
```
```   549 \     ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))";
```
```   550 by (auto_tac
```
```   551     (claset(),
```
```   552      simpset() addsimps split_ifs@
```
```   553                         [quorem_def, linorder_neq_iff,
```
```   554 			 zadd_zmult_distrib2,
```
```   555 			 pos_mod_sign,pos_mod_bound,
```
```   556 			 neg_mod_sign, neg_mod_bound]));
```
```   557 by (ALLGOALS(rtac zmod_zdiv_equality));
```
```   558 val lemma = result();
```
```   559
```
```   560 Goal "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)";
```
```   561 by (zdiv_undefined_case_tac "c = #0" 1);
```
```   562 by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_div]) 1);
```
```   563 qed "zdiv_zmult1_eq";
```
```   564
```
```   565 Goal "(a*b) mod c = a*(b mod c) mod (c::int)";
```
```   566 by (zdiv_undefined_case_tac "c = #0" 1);
```
```   567 by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_mod]) 1);
```
```   568 qed "zmod_zmult1_eq";
```
```   569
```
```   570 Goal "b ~= (#0::int) ==> (a*b) div b = a";
```
```   571 by (asm_simp_tac (simpset() addsimps [zdiv_zmult1_eq]) 1);
```
```   572 qed "zdiv_zmult_self1";
```
```   573
```
```   574 Goal "b ~= (#0::int) ==> (b*a) div b = a";
```
```   575 by (stac zmult_commute 1 THEN etac zdiv_zmult_self1 1);
```
```   576 qed "zdiv_zmult_self2";
```
```   577
```
```   578 Addsimps [zdiv_zmult_self1, zdiv_zmult_self2];
```
```   579
```
```   580 Goal "(a*b) mod b = (#0::int)";
```
```   581 by (simp_tac (simpset() addsimps [zmod_zmult1_eq]) 1);
```
```   582 qed "zmod_zmult_self1";
```
```   583
```
```   584 Goal "(b*a) mod b = (#0::int)";
```
```   585 by (simp_tac (simpset() addsimps [zmult_commute, zmod_zmult1_eq]) 1);
```
```   586 qed "zmod_zmult_self2";
```
```   587
```
```   588 Addsimps [zmod_zmult_self1, zmod_zmult_self2];
```
```   589
```
```   590
```
```   591 (** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **)
```
```   592
```
```   593 Goal "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  c ~= #0 |] \
```
```   594 \     ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))";
```
```   595 by (auto_tac
```
```   596     (claset(),
```
```   597      simpset() addsimps split_ifs@
```
```   598                         [quorem_def, linorder_neq_iff,
```
```   599 			 zadd_zmult_distrib2,
```
```   600 			 pos_mod_sign,pos_mod_bound,
```
```   601 			 neg_mod_sign, neg_mod_bound]));
```
```   602 by (ALLGOALS(rtac zmod_zdiv_equality));
```
```   603 val lemma = result();
```
```   604
```
```   605 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
```
```   606 Goal "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)";
```
```   607 by (zdiv_undefined_case_tac "c = #0" 1);
```
```   608 by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod]
```
```   609 			       MRS lemma RS quorem_div]) 1);
```
```   610 qed "zdiv_zadd1_eq";
```
```   611
```
```   612 Goal "(a+b) mod (c::int) = (a mod c + b mod c) mod c";
```
```   613 by (zdiv_undefined_case_tac "c = #0" 1);
```
```   614 by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod]
```
```   615 			       MRS lemma RS quorem_mod]) 1);
```
```   616 qed "zmod_zadd1_eq";
```
```   617
```
```   618
```
```   619 Goal "(a mod b) div b = (#0::int)";
```
```   620 by (zdiv_undefined_case_tac "b = #0" 1);
```
```   621 by (auto_tac (claset(),
```
```   622        simpset() addsimps [linorder_neq_iff,
```
```   623 			   pos_mod_sign, pos_mod_bound, div_pos_pos_trivial,
```
```   624 			   neg_mod_sign, neg_mod_bound, div_neg_neg_trivial]));
```
```   625 qed "mod_div_trivial";
```
```   626 Addsimps [mod_div_trivial];
```
```   627
```
```   628 Goal "(a mod b) mod b = a mod (b::int)";
```
```   629 by (zdiv_undefined_case_tac "b = #0" 1);
```
```   630 by (auto_tac (claset(),
```
```   631        simpset() addsimps [linorder_neq_iff,
```
```   632 			   pos_mod_sign, pos_mod_bound, mod_pos_pos_trivial,
```
```   633 			   neg_mod_sign, neg_mod_bound, mod_neg_neg_trivial]));
```
```   634 qed "mod_mod_trivial";
```
```   635 Addsimps [mod_mod_trivial];
```
```   636
```
```   637
```
```   638 Goal "a ~= (#0::int) ==> (a+b) div a = b div a + #1";
```
```   639 by (asm_simp_tac (simpset() addsimps [zdiv_zadd1_eq]) 1);
```
```   640 qed "zdiv_zadd_self1";
```
```   641
```
```   642 Goal "a ~= (#0::int) ==> (b+a) div a = b div a + #1";
```
```   643 by (asm_simp_tac (simpset() addsimps [zdiv_zadd1_eq]) 1);
```
```   644 qed "zdiv_zadd_self2";
```
```   645 Addsimps [zdiv_zadd_self1, zdiv_zadd_self2];
```
```   646
```
```   647 Goal "(a+b) mod a = b mod (a::int)";
```
```   648 by (zdiv_undefined_case_tac "a = #0" 1);
```
```   649 by (asm_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1);
```
```   650 qed "zmod_zadd_self1";
```
```   651
```
```   652 Goal "(b+a) mod a = b mod (a::int)";
```
```   653 by (zdiv_undefined_case_tac "a = #0" 1);
```
```   654 by (asm_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1);
```
```   655 qed "zmod_zadd_self2";
```
```   656 Addsimps [zmod_zadd_self1, zmod_zadd_self2];
```
```   657
```
```   658
```
```   659 (*** proving  a div (b*c) = (a div b) div c ***)
```
```   660
```
```   661 (*The condition c>0 seems necessary.  Consider that 7 div ~6 = ~2 but
```
```   662   7 div 2 div ~3 = 3 div ~3 = ~1.  The subcase (a div b) mod c = 0 seems
```
```   663   to cause particular problems.*)
```
```   664
```
```   665 (** first, four lemmas to bound the remainder for the cases b<0 and b>0 **)
```
```   666
```
```   667 Goal "[| (#0::int) < c;  b < r;  r <= #0 |] ==> b*c < b*(q mod c) + r";
```
```   668 by (subgoal_tac "b * (c - q mod c) < r * #1" 1);
```
```   669 by (asm_full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 1);
```
```   670 by (rtac order_le_less_trans 1);
```
```   671 by (etac zmult_zless_mono1 2);
```
```   672 by (rtac zmult_zle_mono2_neg 1);
```
```   673 by (auto_tac
```
```   674     (claset(),
```
```   675      simpset() addsimps zcompare_rls@
```
```   676                         [zadd_commute, add1_zle_eq, pos_mod_bound]));
```
```   677 val lemma1 = result();
```
```   678
```
```   679 Goal "[| (#0::int) < c;   b < r;  r <= #0 |] ==> b * (q mod c) + r <= #0";
```
```   680 by (subgoal_tac "b * (q mod c) <= #0" 1);
```
```   681 by (arith_tac 1);
```
```   682 by (asm_simp_tac (simpset() addsimps [zmult_le_0_iff, pos_mod_sign]) 1);
```
```   683 val lemma2 = result();
```
```   684
```
```   685 Goal "[| (#0::int) < c;  #0 <= r;  r < b |] ==> #0 <= b * (q mod c) + r";
```
```   686 by (subgoal_tac "#0 <= b * (q mod c)" 1);
```
```   687 by (arith_tac 1);
```
```   688 by (asm_simp_tac (simpset() addsimps [int_0_le_mult_iff, pos_mod_sign]) 1);
```
```   689 val lemma3 = result();
```
```   690
```
```   691 Goal "[| (#0::int) < c; #0 <= r; r < b |] ==> b * (q mod c) + r < b * c";
```
```   692 by (subgoal_tac "r * #1 < b * (c - q mod c)" 1);
```
```   693 by (asm_full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 1);
```
```   694 by (rtac order_less_le_trans 1);
```
```   695 by (etac zmult_zless_mono1 1);
```
```   696 by (rtac zmult_zle_mono2 2);
```
```   697 by (auto_tac
```
```   698     (claset(),
```
```   699      simpset() addsimps zcompare_rls@
```
```   700                         [zadd_commute, add1_zle_eq, pos_mod_bound]));
```
```   701 val lemma4 = result();
```
```   702
```
```   703 Goal "[| quorem ((a,b), (q,r));  b ~= #0;  #0 < c |] \
```
```   704 \     ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))";
```
```   705 by (auto_tac
```
```   706     (claset(),
```
```   707      simpset() addsimps zmult_ac@
```
```   708                         [zmod_zdiv_equality, quorem_def, linorder_neq_iff,
```
```   709 			 int_0_less_mult_iff,
```
```   710 			 zadd_zmult_distrib2 RS sym,
```
```   711 			 lemma1, lemma2, lemma3, lemma4]));
```
```   712 val lemma = result();
```
```   713
```
```   714 Goal "(#0::int) < c ==> a div (b*c) = (a div b) div c";
```
```   715 by (zdiv_undefined_case_tac "b = #0" 1);
```
```   716 by (force_tac (claset(),
```
```   717 	       simpset() addsimps [quorem_div_mod RS lemma RS quorem_div,
```
```   718 				   zmult_eq_0_iff]) 1);
```
```   719 qed "zdiv_zmult2_eq";
```
```   720
```
```   721 Goal "(#0::int) < c ==> a mod (b*c) = b*(a div b mod c) + a mod b";
```
```   722 by (zdiv_undefined_case_tac "b = #0" 1);
```
```   723 by (force_tac (claset(),
```
```   724 	       simpset() addsimps [quorem_div_mod RS lemma RS quorem_mod,
```
```   725 				   zmult_eq_0_iff]) 1);
```
```   726 qed "zmod_zmult2_eq";
```
```   727
```
```   728
```
```   729 (*** Cancellation of common factors in "div" ***)
```
```   730
```
```   731 Goal "[| (#0::int) < b;  c ~= #0 |] ==> (c*a) div (c*b) = a div b";
```
```   732 by (stac zdiv_zmult2_eq 1);
```
```   733 by Auto_tac;
```
```   734 val lemma1 = result();
```
```   735
```
```   736 Goal "[| b < (#0::int);  c ~= #0 |] ==> (c*a) div (c*b) = a div b";
```
```   737 by (subgoal_tac "(c * (-a)) div (c * (-b)) = (-a) div (-b)" 1);
```
```   738 by (rtac lemma1 2);
```
```   739 by Auto_tac;
```
```   740 val lemma2 = result();
```
```   741
```
```   742 Goal "c ~= (#0::int) ==> (c*a) div (c*b) = a div b";
```
```   743 by (zdiv_undefined_case_tac "b = #0" 1);
```
```   744 by (auto_tac
```
```   745     (claset(),
```
```   746      simpset() addsimps [read_instantiate [("x", "b")] linorder_neq_iff,
```
```   747 			 lemma1, lemma2]));
```
```   748 qed "zdiv_zmult_zmult1";
```
```   749
```
```   750 Goal "c ~= (#0::int) ==> (a*c) div (b*c) = a div b";
```
```   751 by (dtac zdiv_zmult_zmult1 1);
```
```   752 by (auto_tac (claset(), simpset() addsimps [zmult_commute]));
```
```   753 qed "zdiv_zmult_zmult2";
```
```   754
```
```   755
```
```   756
```
```   757 (*** Distribution of factors over "mod" ***)
```
```   758
```
```   759 Goal "[| (#0::int) < b;  c ~= #0 |] ==> (c*a) mod (c*b) = c * (a mod b)";
```
```   760 by (stac zmod_zmult2_eq 1);
```
```   761 by Auto_tac;
```
```   762 val lemma1 = result();
```
```   763
```
```   764 Goal "[| b < (#0::int);  c ~= #0 |] ==> (c*a) mod (c*b) = c * (a mod b)";
```
```   765 by (subgoal_tac "(c * (-a)) mod (c * (-b)) = c * ((-a) mod (-b))" 1);
```
```   766 by (rtac lemma1 2);
```
```   767 by Auto_tac;
```
```   768 val lemma2 = result();
```
```   769
```
```   770 Goal "(c*a) mod (c*b) = (c::int) * (a mod b)";
```
```   771 by (zdiv_undefined_case_tac "b = #0" 1);
```
```   772 by (zdiv_undefined_case_tac "c = #0" 1);
```
```   773 by (auto_tac
```
```   774     (claset(),
```
```   775      simpset() addsimps [read_instantiate [("x", "b")] linorder_neq_iff,
```
```   776 			 lemma1, lemma2]));
```
```   777 qed "zmod_zmult_zmult1";
```
```   778
```
```   779 Goal "(a*c) mod (b*c) = (a mod b) * (c::int)";
```
```   780 by (cut_inst_tac [("c","c")] zmod_zmult_zmult1 1);
```
```   781 by (auto_tac (claset(), simpset() addsimps [zmult_commute]));
```
```   782 qed "zmod_zmult_zmult2";
```
```   783
```
```   784
```
```   785 (*** Speeding up the division algorithm with shifting ***)
```
```   786
```
```   787 (** computing "div" by shifting **)
```
```   788
```
```   789 Goal "(#0::int) <= a ==> (#1 + #2*b) div (#2*a) = b div a";
```
```   790 by (zdiv_undefined_case_tac "a = #0" 1);
```
```   791 by (subgoal_tac "#1 <= a" 1);
```
```   792  by (arith_tac 2);
```
```   793 by (subgoal_tac "#1 < a * #2" 1);
```
```   794  by (arith_tac 2);
```
```   795 by (subgoal_tac "#2*(#1 + b mod a) <= #2*a" 1);
```
```   796  by (rtac zmult_zle_mono2 2);
```
```   797 by (auto_tac (claset(),
```
```   798 	      simpset() addsimps [zadd_commute, zmult_commute,
```
```   799 				  add1_zle_eq, pos_mod_bound]));
```
```   800 by (stac zdiv_zadd1_eq 1);
```
```   801 by (asm_simp_tac (simpset() addsimps [zdiv_zmult_zmult2, zmod_zmult_zmult2,
```
```   802 				      div_pos_pos_trivial]) 1);
```
```   803 by (stac div_pos_pos_trivial 1);
```
```   804 by (asm_simp_tac (simpset()
```
```   805            addsimps [mod_pos_pos_trivial,
```
```   806                     pos_mod_sign RS zadd_zle_mono1 RSN (2,order_trans)]) 1);
```
```   807 by (auto_tac (claset(),
```
```   808 	      simpset() addsimps [mod_pos_pos_trivial]));
```
```   809 by (subgoal_tac "#0 <= b mod a" 1);
```
```   810  by (asm_simp_tac (simpset() addsimps [pos_mod_sign]) 2);
```
```   811 by (arith_tac 1);
```
```   812 qed "pos_zdiv_mult_2";
```
```   813
```
```   814
```
```   815 Goal "a <= (#0::int) ==> (#1 + #2*b) div (#2*a) = (b+#1) div a";
```
```   816 by (subgoal_tac "(#1 + #2*(-b-#1)) div (#2 * (-a)) = (-b-#1) div (-a)" 1);
```
```   817 by (rtac pos_zdiv_mult_2 2);
```
```   818 by (auto_tac (claset(),
```
```   819 	      simpset() addsimps [zmult_zminus_right]));
```
```   820 by (subgoal_tac "(#-1 - (#2 * b)) = - (#1 + (#2 * b))" 1);
```
```   821 by (Simp_tac 2);
```
```   822 by (asm_full_simp_tac (HOL_ss
```
```   823 		       addsimps [zdiv_zminus_zminus, zdiff_def,
```
```   824 				 zminus_zadd_distrib RS sym]) 1);
```
```   825 qed "neg_zdiv_mult_2";
```
```   826
```
```   827
```
```   828 (*Not clear why this must be proved separately; probably number_of causes
```
```   829   simplification problems*)
```
```   830 Goal "~ #0 <= x ==> x <= (#0::int)";
```
```   831 by Auto_tac;
```
```   832 val lemma = result();
```
```   833
```
```   834 Goal "number_of (v BIT b) div number_of (w BIT False) = \
```
```   835 \         (if ~b | (#0::int) <= number_of w                   \
```
```   836 \          then number_of v div (number_of w)    \
```
```   837 \          else (number_of v + (#1::int)) div (number_of w))";
```
```   838 by (simp_tac (simpset_of Int.thy
```
```   839 			 addsimps [zadd_assoc, number_of_BIT]) 1);
```
```   840 by (asm_simp_tac (simpset()
```
```   841                   delsimps bin_arith_extra_simps@bin_rel_simps
```
```   842 		  addsimps [zdiv_zmult_zmult1,
```
```   843 			    pos_zdiv_mult_2, lemma, neg_zdiv_mult_2]) 1);
```
```   844 qed "zdiv_number_of_BIT";
```
```   845
```
```   846 Addsimps [zdiv_number_of_BIT];
```
```   847
```
```   848
```
```   849 (** computing "mod" by shifting (proofs resemble those for "div") **)
```
```   850
```
```   851 Goal "(#0::int) <= a ==> (#1 + #2*b) mod (#2*a) = #1 + #2 * (b mod a)";
```
```   852 by (zdiv_undefined_case_tac "a = #0" 1);
```
```   853 by (subgoal_tac "#1 <= a" 1);
```
```   854  by (arith_tac 2);
```
```   855 by (subgoal_tac "#1 < a * #2" 1);
```
```   856  by (arith_tac 2);
```
```   857 by (subgoal_tac "#2*(#1 + b mod a) <= #2*a" 1);
```
```   858  by (rtac zmult_zle_mono2 2);
```
```   859 by (auto_tac (claset(),
```
```   860 	      simpset() addsimps [zadd_commute, zmult_commute,
```
```   861 				  add1_zle_eq, pos_mod_bound]));
```
```   862 by (stac zmod_zadd1_eq 1);
```
```   863 by (asm_simp_tac (simpset() addsimps [zmod_zmult_zmult2,
```
```   864 				      mod_pos_pos_trivial]) 1);
```
```   865 by (rtac mod_pos_pos_trivial 1);
```
```   866 by (asm_simp_tac (simpset()
```
```   867                   addsimps [mod_pos_pos_trivial,
```
```   868                     pos_mod_sign RS zadd_zle_mono1 RSN (2,order_trans)]) 1);
```
```   869 by (auto_tac (claset(),
```
```   870 	      simpset() addsimps [mod_pos_pos_trivial]));
```
```   871 by (subgoal_tac "#0 <= b mod a" 1);
```
```   872  by (asm_simp_tac (simpset() addsimps [pos_mod_sign]) 2);
```
```   873 by (arith_tac 1);
```
```   874 qed "pos_zmod_mult_2";
```
```   875
```
```   876
```
```   877 Goal "a <= (#0::int) ==> (#1 + #2*b) mod (#2*a) = #2 * ((b+#1) mod a) - #1";
```
```   878 by (subgoal_tac
```
```   879     "(#1 + #2*(-b-#1)) mod (#2*(-a)) = #1 + #2*((-b-#1) mod (-a))" 1);
```
```   880 by (rtac pos_zmod_mult_2 2);
```
```   881 by (auto_tac (claset(),
```
```   882 	      simpset() addsimps [zmult_zminus_right]));
```
```   883 by (subgoal_tac "(#-1 - (#2 * b)) = - (#1 + (#2 * b))" 1);
```
```   884 by (Simp_tac 2);
```
```   885 by (asm_full_simp_tac (HOL_ss
```
```   886 		       addsimps [zmod_zminus_zminus, zdiff_def,
```
```   887 				 zminus_zadd_distrib RS sym]) 1);
```
```   888 by (dtac (zminus_equation RS iffD1 RS sym) 1);
```
```   889 by Auto_tac;
```
```   890 qed "neg_zmod_mult_2";
```
```   891
```
```   892 Goal "number_of (v BIT b) mod number_of (w BIT False) = \
```
```   893 \         (if b then \
```
```   894 \               if (#0::int) <= number_of w \
```
```   895 \               then #2 * (number_of v mod number_of w) + #1    \
```
```   896 \               else #2 * ((number_of v + (#1::int)) mod number_of w) - #1  \
```
```   897 \          else #2 * (number_of v mod number_of w))";
```
```   898 by (simp_tac (simpset_of Int.thy
```
```   899 			 addsimps [zadd_assoc, number_of_BIT]) 1);
```
```   900 by (asm_simp_tac (simpset()
```
```   901 		  delsimps bin_arith_extra_simps@bin_rel_simps
```
```   902 		  addsimps [zmod_zmult_zmult1,
```
```   903 			    pos_zmod_mult_2, lemma, neg_zmod_mult_2]) 1);
```
```   904 qed "zmod_number_of_BIT";
```
```   905
```
```   906 Addsimps [zmod_number_of_BIT];
```
```   907
```
```   908
```
```   909 (** Quotients of signs **)
```
```   910
```
```   911 Goal "[| a < (#0::int);  #0 < b |] ==> a div b < #0";
```
```   912 by (subgoal_tac "a div b <= #-1" 1);
```
```   913 by (Force_tac 1);
```
```   914 by (rtac order_trans 1);
```
```   915 by (res_inst_tac [("a'","#-1")]  zdiv_mono1 1);
```
```   916 by (auto_tac (claset(), simpset() addsimps [zdiv_minus1]));
```
```   917 qed "div_neg_pos_less0";
```
```   918
```
```   919 Goal "[| (#0::int) <= a;  b < #0 |] ==> a div b <= #0";
```
```   920 by (dtac zdiv_mono1_neg 1);
```
```   921 by Auto_tac;
```
```   922 qed "div_nonneg_neg_le0";
```
```   923
```
```   924 Goal "(#0::int) < b ==> (#0 <= a div b) = (#0 <= a)";
```
```   925 by Auto_tac;
```
```   926 by (dtac zdiv_mono1 2);
```
```   927 by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff]));
```
```   928 by (full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
```
```   929 by (blast_tac (claset() addIs [div_neg_pos_less0]) 1);
```
```   930 qed "pos_imp_zdiv_nonneg_iff";
```
```   931
```
```   932 Goal "b < (#0::int) ==> (#0 <= a div b) = (a <= (#0::int))";
```
```   933 by (stac (zdiv_zminus_zminus RS sym) 1);
```
```   934 by (stac pos_imp_zdiv_nonneg_iff 1);
```
```   935 by Auto_tac;
```
```   936 qed "neg_imp_zdiv_nonneg_iff";
```
```   937
```
```   938 (*But not (a div b <= 0 iff a<=0); consider a=1, b=2 when a div b = 0.*)
```
```   939 Goal "(#0::int) < b ==> (a div b < #0) = (a < #0)";
```
```   940 by (asm_simp_tac (simpset() addsimps [linorder_not_le RS sym,
```
```   941 				      pos_imp_zdiv_nonneg_iff]) 1);
```
```   942 qed "pos_imp_zdiv_neg_iff";
```
```   943
```
```   944 (*Again the law fails for <=: consider a = -1, b = -2 when a div b = 0*)
```
```   945 Goal "b < (#0::int) ==> (a div b < #0) = (#0 < a)";
```
```   946 by (asm_simp_tac (simpset() addsimps [linorder_not_le RS sym,
```
```   947 				      neg_imp_zdiv_nonneg_iff]) 1);
```
```   948 qed "neg_imp_zdiv_neg_iff";
```