src/HOL/Divides.ML
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 6073 fba734ba6894
child 6865 5577ffe4c2f1
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
paulson@3366
     1
(*  Title:      HOL/Divides.ML
paulson@3366
     2
    ID:         $Id$
paulson@3366
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@3366
     4
    Copyright   1993  University of Cambridge
paulson@3366
     5
paulson@3366
     6
The division operators div, mod and the divides relation "dvd"
paulson@3366
     7
*)
paulson@3366
     8
paulson@3366
     9
paulson@3366
    10
(** Less-then properties **)
paulson@3366
    11
paulson@3366
    12
val wf_less_trans = [eq_reflection, wf_pred_nat RS wf_trancl] MRS 
paulson@3366
    13
                    def_wfrec RS trans;
paulson@3366
    14
paulson@3366
    15
(*** Remainder ***)
paulson@3366
    16
wenzelm@5069
    17
Goal "(%m. m mod n) = wfrec (trancl pred_nat) \
paulson@5415
    18
\                           (%f j. if j<n then j else f (j-n))";
wenzelm@4089
    19
by (simp_tac (simpset() addsimps [mod_def]) 1);
paulson@3366
    20
qed "mod_eq";
paulson@3366
    21
paulson@5143
    22
Goal "m<n ==> m mod n = m";
paulson@3366
    23
by (rtac (mod_eq RS wf_less_trans) 1);
paulson@3366
    24
by (Asm_simp_tac 1);
paulson@3366
    25
qed "mod_less";
paulson@3366
    26
paulson@5143
    27
Goal "[| 0<n;  ~m<n |] ==> m mod n = (m-n) mod n";
paulson@3366
    28
by (rtac (mod_eq RS wf_less_trans) 1);
wenzelm@4089
    29
by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1);
paulson@3366
    30
qed "mod_geq";
paulson@3366
    31
paulson@5415
    32
(*Avoids the ugly ~m<n above*)
paulson@5415
    33
Goal "[| 0<n;  n<=m |] ==> m mod n = (m-n) mod n";
paulson@5415
    34
by (asm_simp_tac (simpset() addsimps [mod_geq, not_less_iff_le]) 1);
paulson@5415
    35
qed "le_mod_geq";
paulson@5415
    36
paulson@4774
    37
(*NOT suitable for rewriting: loops*)
paulson@5143
    38
Goal "0<n ==> m mod n = (if m<n then m else (m-n) mod n)";
paulson@4774
    39
by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq]) 1);
paulson@4774
    40
qed "mod_if";
paulson@4774
    41
wenzelm@5069
    42
Goal "m mod 1 = 0";
paulson@3366
    43
by (induct_tac "m" 1);
wenzelm@4089
    44
by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_less, mod_geq])));
paulson@3366
    45
qed "mod_1";
paulson@3366
    46
Addsimps [mod_1];
paulson@3366
    47
paulson@5143
    48
Goal "0<n ==> n mod n = 0";
wenzelm@4089
    49
by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq]) 1);
paulson@3366
    50
qed "mod_self";
paulson@3366
    51
paulson@5143
    52
Goal "0<n ==> (m+n) mod n = m mod n";
paulson@3366
    53
by (subgoal_tac "(n + m) mod n = (n+m-n) mod n" 1);
paulson@3366
    54
by (stac (mod_geq RS sym) 2);
wenzelm@4089
    55
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute])));
paulson@4811
    56
qed "mod_add_self2";
paulson@4810
    57
paulson@5143
    58
Goal "0<n ==> (n+m) mod n = m mod n";
paulson@4811
    59
by (asm_simp_tac (simpset() addsimps [add_commute, mod_add_self2]) 1);
paulson@4811
    60
qed "mod_add_self1";
paulson@4810
    61
wenzelm@5069
    62
Goal "!!n. 0<n ==> (m + k*n) mod n = m mod n";
paulson@4810
    63
by (induct_tac "k" 1);
paulson@5537
    64
by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac @ [mod_add_self1])));
paulson@4811
    65
qed "mod_mult_self1";
paulson@4810
    66
paulson@5143
    67
Goal "0<n ==> (m + n*k) mod n = m mod n";
paulson@4811
    68
by (asm_simp_tac (simpset() addsimps [mult_commute, mod_mult_self1]) 1);
paulson@4811
    69
qed "mod_mult_self2";
paulson@4810
    70
paulson@4811
    71
Addsimps [mod_mult_self1, mod_mult_self2];
paulson@3366
    72
paulson@5143
    73
Goal "[| 0<k; 0<n |] ==> (m mod n)*k = (m*k) mod (n*k)";
paulson@3366
    74
by (res_inst_tac [("n","m")] less_induct 1);
paulson@4774
    75
by (stac mod_if 1);
paulson@4774
    76
by (Asm_simp_tac 1);
paulson@4774
    77
by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq, 
paulson@4774
    78
				      diff_less, diff_mult_distrib]) 1);
paulson@3366
    79
qed "mod_mult_distrib";
paulson@3366
    80
paulson@5143
    81
Goal "[| 0<k; 0<n |] ==> k*(m mod n) = (k*m) mod (k*n)";
paulson@3366
    82
by (res_inst_tac [("n","m")] less_induct 1);
paulson@4774
    83
by (stac mod_if 1);
paulson@4774
    84
by (Asm_simp_tac 1);
paulson@4774
    85
by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq, 
paulson@4774
    86
				      diff_less, diff_mult_distrib2]) 1);
paulson@3366
    87
qed "mod_mult_distrib2";
paulson@3366
    88
paulson@5143
    89
Goal "0<n ==> m*n mod n = 0";
paulson@3366
    90
by (induct_tac "m" 1);
wenzelm@4089
    91
by (asm_simp_tac (simpset() addsimps [mod_less]) 1);
berghofe@5183
    92
by (dres_inst_tac [("m","na*n")] mod_add_self2 1);
wenzelm@4089
    93
by (asm_full_simp_tac (simpset() addsimps [add_commute]) 1);
paulson@3366
    94
qed "mod_mult_self_is_0";
paulson@3366
    95
Addsimps [mod_mult_self_is_0];
paulson@3366
    96
paulson@3366
    97
(*** Quotient ***)
paulson@3366
    98
wenzelm@5069
    99
Goal "(%m. m div n) = wfrec (trancl pred_nat) \
paulson@3366
   100
                        \            (%f j. if j<n then 0 else Suc (f (j-n)))";
wenzelm@4089
   101
by (simp_tac (simpset() addsimps [div_def]) 1);
paulson@3366
   102
qed "div_eq";
paulson@3366
   103
paulson@5143
   104
Goal "m<n ==> m div n = 0";
paulson@3366
   105
by (rtac (div_eq RS wf_less_trans) 1);
paulson@3366
   106
by (Asm_simp_tac 1);
paulson@3366
   107
qed "div_less";
paulson@3366
   108
paulson@5143
   109
Goal "[| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)";
paulson@3366
   110
by (rtac (div_eq RS wf_less_trans) 1);
wenzelm@4089
   111
by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1);
paulson@3366
   112
qed "div_geq";
paulson@3366
   113
paulson@5415
   114
(*Avoids the ugly ~m<n above*)
paulson@5415
   115
Goal "[| 0<n;  n<=m |] ==> m div n = Suc((m-n) div n)";
paulson@5415
   116
by (asm_simp_tac (simpset() addsimps [div_geq, not_less_iff_le]) 1);
paulson@5415
   117
qed "le_div_geq";
paulson@5415
   118
paulson@4774
   119
(*NOT suitable for rewriting: loops*)
paulson@5143
   120
Goal "0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))";
paulson@4774
   121
by (asm_simp_tac (simpset() addsimps [div_less, div_geq]) 1);
paulson@4774
   122
qed "div_if";
paulson@4774
   123
paulson@3366
   124
(*Main Result about quotient and remainder.*)
paulson@5143
   125
Goal "0<n ==> (m div n)*n + m mod n = m";
paulson@3366
   126
by (res_inst_tac [("n","m")] less_induct 1);
paulson@4774
   127
by (stac mod_if 1);
paulson@4774
   128
by (ALLGOALS (asm_simp_tac 
paulson@5537
   129
	      (simpset() addsimps [add_assoc, div_less, div_geq,
paulson@5537
   130
				   add_diff_inverse, diff_less])));
paulson@3366
   131
qed "mod_div_equality";
paulson@3366
   132
nipkow@4358
   133
(* a simple rearrangement of mod_div_equality: *)
paulson@5143
   134
Goal "0<k ==> k*(m div k) = m - (m mod k)";
wenzelm@4423
   135
by (dres_inst_tac [("m","m")] mod_div_equality 1);
nipkow@4358
   136
by (EVERY1[etac subst, simp_tac (simpset() addsimps mult_ac),
nipkow@4358
   137
           K(IF_UNSOLVED no_tac)]);
nipkow@4358
   138
qed "mult_div_cancel";
nipkow@4358
   139
wenzelm@5069
   140
Goal "m div 1 = m";
paulson@3366
   141
by (induct_tac "m" 1);
wenzelm@4089
   142
by (ALLGOALS (asm_simp_tac (simpset() addsimps [div_less, div_geq])));
paulson@3366
   143
qed "div_1";
paulson@3366
   144
Addsimps [div_1];
paulson@3366
   145
paulson@5143
   146
Goal "0<n ==> n div n = 1";
wenzelm@4089
   147
by (asm_simp_tac (simpset() addsimps [div_less, div_geq]) 1);
paulson@3366
   148
qed "div_self";
paulson@3366
   149
paulson@4811
   150
paulson@5143
   151
Goal "0<n ==> (m+n) div n = Suc (m div n)";
paulson@4811
   152
by (subgoal_tac "(n + m) div n = Suc ((n+m-n) div n)" 1);
paulson@4811
   153
by (stac (div_geq RS sym) 2);
paulson@4811
   154
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute])));
paulson@4811
   155
qed "div_add_self2";
paulson@4811
   156
paulson@5143
   157
Goal "0<n ==> (n+m) div n = Suc (m div n)";
paulson@4811
   158
by (asm_simp_tac (simpset() addsimps [add_commute, div_add_self2]) 1);
paulson@4811
   159
qed "div_add_self1";
paulson@4811
   160
wenzelm@5069
   161
Goal "!!n. 0<n ==> (m + k*n) div n = k + m div n";
paulson@4811
   162
by (induct_tac "k" 1);
paulson@5537
   163
by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac @ [div_add_self1])));
paulson@4811
   164
qed "div_mult_self1";
paulson@4811
   165
paulson@5143
   166
Goal "0<n ==> (m + n*k) div n = k + m div n";
paulson@4811
   167
by (asm_simp_tac (simpset() addsimps [mult_commute, div_mult_self1]) 1);
paulson@4811
   168
qed "div_mult_self2";
paulson@4811
   169
paulson@4811
   170
Addsimps [div_mult_self1, div_mult_self2];
paulson@4811
   171
paulson@4811
   172
nipkow@3484
   173
(* Monotonicity of div in first argument *)
paulson@5143
   174
Goal "0<k ==> ALL m. m <= n --> (m div k) <= (n div k)";
nipkow@3484
   175
by (res_inst_tac [("n","n")] less_induct 1);
paulson@3718
   176
by (Clarify_tac 1);
paulson@5143
   177
by (case_tac "n<k" 1);
nipkow@3484
   178
(* 1  case n<k *)
wenzelm@4089
   179
by (asm_simp_tac (simpset() addsimps [div_less]) 1);
nipkow@3484
   180
(* 2  case n >= k *)
nipkow@3484
   181
by (case_tac "m<k" 1);
nipkow@3484
   182
(* 2.1  case m<k *)
wenzelm@4089
   183
by (asm_simp_tac (simpset() addsimps [div_less]) 1);
nipkow@3484
   184
(* 2.2  case m>=k *)
wenzelm@4089
   185
by (asm_simp_tac (simpset() addsimps [div_geq, diff_less, diff_le_mono]) 1);
nipkow@3484
   186
qed_spec_mp "div_le_mono";
nipkow@3484
   187
nipkow@3484
   188
nipkow@3484
   189
(* Antimonotonicity of div in second argument *)
paulson@5143
   190
Goal "[| 0<m; m<=n |] ==> (k div n) <= (k div m)";
nipkow@3484
   191
by (subgoal_tac "0<n" 1);
nipkow@6073
   192
 by (Asm_simp_tac 2);
nipkow@3484
   193
by (res_inst_tac [("n","k")] less_induct 1);
paulson@3496
   194
by (rename_tac "k" 1);
nipkow@3484
   195
by (case_tac "k<n" 1);
wenzelm@4089
   196
 by (asm_simp_tac (simpset() addsimps [div_less]) 1);
nipkow@3484
   197
by (subgoal_tac "~(k<m)" 1);
nipkow@6073
   198
 by (Asm_simp_tac 2);
wenzelm@4089
   199
by (asm_simp_tac (simpset() addsimps [div_geq]) 1);
nipkow@3484
   200
by (subgoal_tac "(k-n) div n <= (k-m) div n" 1);
paulson@5316
   201
by (REPEAT (eresolve_tac [div_le_mono,diff_le_mono2] 2));
paulson@5318
   202
by (rtac le_trans 1);
paulson@5316
   203
by (Asm_simp_tac 1);
paulson@5316
   204
by (asm_simp_tac (simpset() addsimps [diff_less]) 1);
nipkow@3484
   205
qed "div_le_mono2";
nipkow@3484
   206
paulson@5143
   207
Goal "0<n ==> m div n <= m";
nipkow@3484
   208
by (subgoal_tac "m div n <= m div 1" 1);
nipkow@3484
   209
by (Asm_full_simp_tac 1);
nipkow@3484
   210
by (rtac div_le_mono2 1);
nipkow@6073
   211
by (ALLGOALS Asm_simp_tac);
nipkow@3484
   212
qed "div_le_dividend";
nipkow@3484
   213
Addsimps [div_le_dividend];
nipkow@3484
   214
nipkow@3484
   215
(* Similar for "less than" *)
paulson@5143
   216
Goal "1<n ==> (0 < m) --> (m div n < m)";
nipkow@3484
   217
by (res_inst_tac [("n","m")] less_induct 1);
paulson@3496
   218
by (rename_tac "m" 1);
nipkow@3484
   219
by (case_tac "m<n" 1);
wenzelm@4089
   220
 by (asm_full_simp_tac (simpset() addsimps [div_less]) 1);
nipkow@3484
   221
by (subgoal_tac "0<n" 1);
nipkow@6073
   222
 by (Asm_simp_tac 2);
wenzelm@4089
   223
by (asm_full_simp_tac (simpset() addsimps [div_geq]) 1);
nipkow@3484
   224
by (case_tac "n<m" 1);
nipkow@3484
   225
 by (subgoal_tac "(m-n) div n < (m-n)" 1);
nipkow@3484
   226
  by (REPEAT (ares_tac [impI,less_trans_Suc] 1));
wenzelm@4089
   227
  by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1);
wenzelm@4089
   228
 by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1);
nipkow@3484
   229
(* case n=m *)
nipkow@3484
   230
by (subgoal_tac "m=n" 1);
nipkow@6073
   231
 by (Asm_simp_tac 2);
wenzelm@4089
   232
by (asm_simp_tac (simpset() addsimps [div_less]) 1);
nipkow@3484
   233
qed_spec_mp "div_less_dividend";
nipkow@3484
   234
Addsimps [div_less_dividend];
paulson@3366
   235
paulson@3366
   236
(*** Further facts about mod (mainly for the mutilated chess board ***)
paulson@3366
   237
paulson@5278
   238
Goal "0<n ==> Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))";
paulson@3366
   239
by (res_inst_tac [("n","m")] less_induct 1);
paulson@3366
   240
by (excluded_middle_tac "Suc(na)<n" 1);
paulson@3366
   241
(* case Suc(na) < n *)
paulson@3366
   242
by (forward_tac [lessI RS less_trans] 2);
paulson@5355
   243
by (asm_simp_tac (simpset() addsimps [mod_less, less_not_refl3]) 2);
paulson@3366
   244
(* case n <= Suc(na) *)
paulson@5415
   245
by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, le_Suc_eq, 
paulson@5415
   246
					   mod_geq]) 1);
paulson@5415
   247
by (etac disjE 1);
paulson@5415
   248
 by (asm_simp_tac (simpset() addsimps [mod_less]) 2);
paulson@5415
   249
by (asm_simp_tac (simpset() addsimps [Suc_diff_le, le_diff_less, 
paulson@5415
   250
				      le_mod_geq]) 1);
paulson@3366
   251
qed "mod_Suc";
paulson@3366
   252
paulson@5143
   253
Goal "0<n ==> m mod n < n";
paulson@3366
   254
by (res_inst_tac [("n","m")] less_induct 1);
paulson@5498
   255
by (case_tac "na<n" 1);
paulson@5498
   256
(*case n le na*)
paulson@5498
   257
by (asm_full_simp_tac (simpset() addsimps [mod_geq, diff_less]) 2);
paulson@3366
   258
(*case na<n*)
paulson@5498
   259
by (asm_simp_tac (simpset() addsimps [mod_less]) 1);
paulson@3366
   260
qed "mod_less_divisor";
paulson@3366
   261
paulson@3366
   262
paulson@3366
   263
(** Evens and Odds **)
paulson@3366
   264
paulson@3366
   265
(*With less_zeroE, causes case analysis on b<2*)
paulson@3366
   266
AddSEs [less_SucE];
paulson@3366
   267
paulson@5143
   268
Goal "b<2 ==> k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)";
paulson@3366
   269
by (subgoal_tac "k mod 2 < 2" 1);
wenzelm@4089
   270
by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2);
nipkow@4686
   271
by (Asm_simp_tac 1);
nipkow@4356
   272
by Safe_tac;
paulson@3366
   273
qed "mod2_cases";
paulson@3366
   274
wenzelm@5069
   275
Goal "Suc(Suc(m)) mod 2 = m mod 2";
paulson@3366
   276
by (subgoal_tac "m mod 2 < 2" 1);
wenzelm@4089
   277
by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2);
paulson@3724
   278
by Safe_tac;
wenzelm@4089
   279
by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_Suc])));
paulson@3366
   280
qed "mod2_Suc_Suc";
paulson@3366
   281
Addsimps [mod2_Suc_Suc];
paulson@3366
   282
wenzelm@5069
   283
Goal "(0 < m mod 2) = (m mod 2 = 1)";
paulson@3366
   284
by (subgoal_tac "m mod 2 < 2" 1);
wenzelm@4089
   285
by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2);
paulson@4477
   286
by Auto_tac;
nipkow@4356
   287
qed "mod2_gr_0";
nipkow@4356
   288
Addsimps [mod2_gr_0];
nipkow@4356
   289
wenzelm@5069
   290
Goal "(m+m) mod 2 = 0";
paulson@3366
   291
by (induct_tac "m" 1);
wenzelm@4089
   292
by (simp_tac (simpset() addsimps [mod_less]) 1);
paulson@3427
   293
by (Asm_simp_tac 1);
paulson@4385
   294
qed "mod2_add_self_eq_0";
paulson@4385
   295
Addsimps [mod2_add_self_eq_0];
paulson@4385
   296
wenzelm@5069
   297
Goal "((m+m)+n) mod 2 = n mod 2";
paulson@4385
   298
by (induct_tac "m" 1);
paulson@4385
   299
by (simp_tac (simpset() addsimps [mod_less]) 1);
paulson@4385
   300
by (Asm_simp_tac 1);
paulson@3366
   301
qed "mod2_add_self";
paulson@3366
   302
Addsimps [mod2_add_self];
paulson@3366
   303
paulson@5498
   304
(*Restore the default*)
paulson@3366
   305
Delrules [less_SucE];
paulson@3366
   306
paulson@3366
   307
(*** More division laws ***)
paulson@3366
   308
paulson@5143
   309
Goal "0<n ==> m*n div n = m";
paulson@3366
   310
by (cut_inst_tac [("m", "m*n")] mod_div_equality 1);
paulson@3457
   311
by (assume_tac 1);
wenzelm@4089
   312
by (asm_full_simp_tac (simpset() addsimps [mod_mult_self_is_0]) 1);
paulson@3366
   313
qed "div_mult_self_is_m";
paulson@3366
   314
Addsimps [div_mult_self_is_m];
paulson@3366
   315
paulson@3366
   316
(*Cancellation law for division*)
paulson@5143
   317
Goal "[| 0<n; 0<k |] ==> (k*m) div (k*n) = m div n";
paulson@3366
   318
by (res_inst_tac [("n","m")] less_induct 1);
paulson@3366
   319
by (case_tac "na<n" 1);
wenzelm@4089
   320
by (asm_simp_tac (simpset() addsimps [div_less, zero_less_mult_iff, 
paulson@3366
   321
                                     mult_less_mono2]) 1);
paulson@3366
   322
by (subgoal_tac "~ k*na < k*n" 1);
paulson@3366
   323
by (asm_simp_tac
wenzelm@4089
   324
     (simpset() addsimps [zero_less_mult_iff, div_geq,
paulson@5415
   325
			  diff_mult_distrib2 RS sym, diff_less]) 1);
wenzelm@4089
   326
by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, 
paulson@3366
   327
                                          le_refl RS mult_le_mono]) 1);
paulson@3366
   328
qed "div_cancel";
paulson@3366
   329
Addsimps [div_cancel];
paulson@3366
   330
paulson@5143
   331
Goal "[| 0<n; 0<k |] ==> (k*m) mod (k*n) = k * (m mod n)";
paulson@3366
   332
by (res_inst_tac [("n","m")] less_induct 1);
paulson@3366
   333
by (case_tac "na<n" 1);
wenzelm@4089
   334
by (asm_simp_tac (simpset() addsimps [mod_less, zero_less_mult_iff, 
paulson@3366
   335
                                     mult_less_mono2]) 1);
paulson@3366
   336
by (subgoal_tac "~ k*na < k*n" 1);
paulson@3366
   337
by (asm_simp_tac
wenzelm@4089
   338
     (simpset() addsimps [zero_less_mult_iff, mod_geq,
paulson@3366
   339
                         diff_mult_distrib2 RS sym, diff_less]) 1);
wenzelm@4089
   340
by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, 
paulson@3366
   341
                                          le_refl RS mult_le_mono]) 1);
paulson@3366
   342
qed "mult_mod_distrib";
paulson@3366
   343
paulson@3366
   344
paulson@3366
   345
(************************************************)
paulson@3366
   346
(** Divides Relation                           **)
paulson@3366
   347
(************************************************)
paulson@3366
   348
wenzelm@5069
   349
Goalw [dvd_def] "m dvd 0";
wenzelm@4089
   350
by (blast_tac (claset() addIs [mult_0_right RS sym]) 1);
paulson@3366
   351
qed "dvd_0_right";
paulson@3366
   352
Addsimps [dvd_0_right];
paulson@3366
   353
paulson@5143
   354
Goalw [dvd_def] "0 dvd m ==> m = 0";
wenzelm@4089
   355
by (fast_tac (claset() addss simpset()) 1);
paulson@3366
   356
qed "dvd_0_left";
paulson@3366
   357
wenzelm@5069
   358
Goalw [dvd_def] "1 dvd k";
paulson@3366
   359
by (Simp_tac 1);
paulson@3366
   360
qed "dvd_1_left";
paulson@3366
   361
AddIffs [dvd_1_left];
paulson@3366
   362
wenzelm@5069
   363
Goalw [dvd_def] "m dvd m";
wenzelm@4089
   364
by (blast_tac (claset() addIs [mult_1_right RS sym]) 1);
paulson@3366
   365
qed "dvd_refl";
paulson@3366
   366
Addsimps [dvd_refl];
paulson@3366
   367
paulson@5143
   368
Goalw [dvd_def] "[| m dvd n; n dvd p |] ==> m dvd p";
wenzelm@4089
   369
by (blast_tac (claset() addIs [mult_assoc] ) 1);
paulson@3366
   370
qed "dvd_trans";
paulson@3366
   371
paulson@5143
   372
Goalw [dvd_def] "[| m dvd n; n dvd m |] ==> m=n";
wenzelm@4089
   373
by (fast_tac (claset() addDs [mult_eq_self_implies_10]
wenzelm@4089
   374
                     addss (simpset() addsimps [mult_assoc, mult_eq_1_iff])) 1);
paulson@3366
   375
qed "dvd_anti_sym";
paulson@3366
   376
paulson@5143
   377
Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m + n)";
wenzelm@4089
   378
by (blast_tac (claset() addIs [add_mult_distrib2 RS sym]) 1);
paulson@3366
   379
qed "dvd_add";
paulson@3366
   380
paulson@5143
   381
Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m-n)";
wenzelm@4089
   382
by (blast_tac (claset() addIs [diff_mult_distrib2 RS sym]) 1);
paulson@3366
   383
qed "dvd_diff";
paulson@3366
   384
paulson@5143
   385
Goal "[| k dvd (m-n); k dvd n; n<=m |] ==> k dvd m";
paulson@3457
   386
by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1);
wenzelm@4089
   387
by (blast_tac (claset() addIs [dvd_add]) 1);
paulson@3366
   388
qed "dvd_diffD";
paulson@3366
   389
paulson@5143
   390
Goalw [dvd_def] "k dvd n ==> k dvd (m*n)";
wenzelm@4089
   391
by (blast_tac (claset() addIs [mult_left_commute]) 1);
paulson@3366
   392
qed "dvd_mult";
paulson@3366
   393
paulson@5143
   394
Goal "k dvd m ==> k dvd (m*n)";
paulson@3366
   395
by (stac mult_commute 1);
paulson@3366
   396
by (etac dvd_mult 1);
paulson@3366
   397
qed "dvd_mult2";
paulson@3366
   398
paulson@3366
   399
(* k dvd (m*k) *)
paulson@3366
   400
AddIffs [dvd_refl RS dvd_mult, dvd_refl RS dvd_mult2];
paulson@3366
   401
paulson@5143
   402
Goalw [dvd_def] "[| f dvd m; f dvd n; 0<n |] ==> f dvd (m mod n)";
paulson@3718
   403
by (Clarify_tac 1);
wenzelm@4089
   404
by (full_simp_tac (simpset() addsimps [zero_less_mult_iff]) 1);
paulson@3366
   405
by (res_inst_tac 
paulson@3366
   406
    [("x", "(((k div ka)*ka + k mod ka) - ((f*k) div (f*ka)) * ka)")] 
paulson@3366
   407
    exI 1);
wenzelm@4089
   408
by (asm_simp_tac (simpset() addsimps [diff_mult_distrib2, 
paulson@3366
   409
                                     mult_mod_distrib, add_mult_distrib2]) 1);
paulson@3366
   410
qed "dvd_mod";
paulson@3366
   411
paulson@5143
   412
Goal "[| k dvd (m mod n); k dvd n; 0<n |] ==> k dvd m";
paulson@3366
   413
by (subgoal_tac "k dvd ((m div n)*n + m mod n)" 1);
wenzelm@4089
   414
by (asm_simp_tac (simpset() addsimps [dvd_add, dvd_mult]) 2);
nipkow@4356
   415
by (asm_full_simp_tac (simpset() addsimps [mod_div_equality]) 1);
paulson@3366
   416
qed "dvd_mod_imp_dvd";
paulson@3366
   417
paulson@5143
   418
Goalw [dvd_def]  "!!k. [| (k*m) dvd (k*n); 0<k |] ==> m dvd n";
paulson@3366
   419
by (etac exE 1);
wenzelm@4089
   420
by (asm_full_simp_tac (simpset() addsimps mult_ac) 1);
paulson@3366
   421
by (Blast_tac 1);
paulson@3366
   422
qed "dvd_mult_cancel";
paulson@3366
   423
paulson@5143
   424
Goalw [dvd_def] "[| i dvd m; j dvd n|] ==> (i*j) dvd (m*n)";
paulson@3718
   425
by (Clarify_tac 1);
paulson@3366
   426
by (res_inst_tac [("x","k*ka")] exI 1);
wenzelm@4089
   427
by (asm_simp_tac (simpset() addsimps mult_ac) 1);
paulson@3366
   428
qed "mult_dvd_mono";
paulson@3366
   429
paulson@5143
   430
Goalw [dvd_def] "(i*j) dvd k ==> i dvd k";
wenzelm@4089
   431
by (full_simp_tac (simpset() addsimps [mult_assoc]) 1);
paulson@3366
   432
by (Blast_tac 1);
paulson@3366
   433
qed "dvd_mult_left";
paulson@3366
   434
paulson@5143
   435
Goalw [dvd_def] "[| k dvd n; 0 < n |] ==> k <= n";
paulson@3718
   436
by (Clarify_tac 1);
wenzelm@4089
   437
by (ALLGOALS (full_simp_tac (simpset() addsimps [zero_less_mult_iff])));
paulson@3457
   438
by (etac conjE 1);
paulson@3457
   439
by (rtac le_trans 1);
paulson@3457
   440
by (rtac (le_refl RS mult_le_mono) 2);
paulson@3366
   441
by (etac Suc_leI 2);
paulson@3366
   442
by (Simp_tac 1);
paulson@3366
   443
qed "dvd_imp_le";
paulson@3366
   444
paulson@5143
   445
Goalw [dvd_def] "0<k ==> (k dvd n) = (n mod k = 0)";
paulson@3724
   446
by Safe_tac;
paulson@5143
   447
by (asm_simp_tac (simpset() addsimps [mult_commute]) 1);
paulson@5143
   448
by (eres_inst_tac [("t","n")] (mod_div_equality RS subst) 1);
paulson@3366
   449
by (stac mult_commute 1);
paulson@3366
   450
by (Asm_simp_tac 1);
paulson@3366
   451
by (Blast_tac 1);
paulson@3366
   452
qed "dvd_eq_mod_eq_0";