src/HOL/Nat.ML
author wenzelm
Tue Jul 25 00:06:46 2000 +0200 (2000-07-25)
changeset 9436 62bb04ab4b01
parent 9108 9fff97d29837
child 9637 47d39a31eb2f
permissions -rw-r--r--
rearranged setup of arithmetic procedures, avoiding global reference values;
oheimb@2441
     1
(*  Title:      HOL/Nat.ML
clasohm@923
     2
    ID:         $Id$
wenzelm@9436
     3
    Author:     Lawrence C Paulson and Tobias Nipkow
wenzelm@9436
     4
wenzelm@9436
     5
Proofs about natural numbers and elementary arithmetic: addition,
wenzelm@9436
     6
multiplication, etc.  Some from the Hoare example from Norbert Galm.
clasohm@923
     7
*)
clasohm@923
     8
berghofe@5188
     9
(** conversion rules for nat_rec **)
berghofe@5188
    10
berghofe@5188
    11
val [nat_rec_0, nat_rec_Suc] = nat.recs;
wenzelm@9108
    12
bind_thm ("nat_rec_0", nat_rec_0);
wenzelm@9108
    13
bind_thm ("nat_rec_Suc", nat_rec_Suc);
berghofe@5188
    14
berghofe@5188
    15
(*These 2 rules ease the use of primitive recursion.  NOTE USE OF == *)
paulson@5316
    16
val prems = Goal
berghofe@5188
    17
    "[| !!n. f(n) == nat_rec c h n |] ==> f(0) = c";
berghofe@5188
    18
by (simp_tac (simpset() addsimps prems) 1);
berghofe@5188
    19
qed "def_nat_rec_0";
berghofe@5188
    20
paulson@5316
    21
val prems = Goal
berghofe@5188
    22
    "[| !!n. f(n) == nat_rec c h n |] ==> f(Suc(n)) = h n (f n)";
berghofe@5188
    23
by (simp_tac (simpset() addsimps prems) 1);
berghofe@5188
    24
qed "def_nat_rec_Suc";
berghofe@5188
    25
berghofe@5188
    26
val [nat_case_0, nat_case_Suc] = nat.cases;
wenzelm@9108
    27
bind_thm ("nat_case_0", nat_case_0);
wenzelm@9108
    28
bind_thm ("nat_case_Suc", nat_case_Suc);
berghofe@5188
    29
berghofe@5188
    30
Goal "n ~= 0 ==> EX m. n = Suc m";
wenzelm@8442
    31
by (case_tac "n" 1);
berghofe@5188
    32
by (REPEAT (Blast_tac 1));
berghofe@5188
    33
qed "not0_implies_Suc";
berghofe@5188
    34
paulson@8942
    35
Goal "!!n::nat. m<n ==> n ~= 0";
wenzelm@8442
    36
by (case_tac "n" 1);
berghofe@5188
    37
by (ALLGOALS Asm_full_simp_tac);
berghofe@5188
    38
qed "gr_implies_not0";
berghofe@5188
    39
paulson@8942
    40
Goal "!!n::nat. (n ~= 0) = (0 < n)";
wenzelm@8442
    41
by (case_tac "n" 1);
paulson@7089
    42
by Auto_tac;
berghofe@5188
    43
qed "neq0_conv";
berghofe@5188
    44
AddIffs [neq0_conv];
berghofe@5188
    45
paulson@8942
    46
Goal "!!n::nat. (0 ~= n) = (0 < n)";
wenzelm@8442
    47
by (case_tac "n" 1);
paulson@7089
    48
by Auto_tac;
nipkow@5644
    49
qed "zero_neq_conv";
nipkow@5644
    50
AddIffs [zero_neq_conv];
nipkow@5644
    51
berghofe@5188
    52
(*This theorem is useful with blast_tac: (n=0 ==> False) ==> 0<n *)
berghofe@5188
    53
bind_thm ("gr0I", [neq0_conv, notI] MRS iffD1);
berghofe@5188
    54
nipkow@8115
    55
Goal "(0<n) = (EX m. n = Suc m)";
nipkow@8115
    56
by(fast_tac (claset() addIs [not0_implies_Suc]) 1);
nipkow@8115
    57
qed "gr0_conv_Suc";
nipkow@8115
    58
paulson@8942
    59
Goal "!!n::nat. (~(0 < n)) = (n=0)";
berghofe@5188
    60
by (rtac iffI 1);
berghofe@5188
    61
 by (etac swap 1);
berghofe@5188
    62
 by (ALLGOALS Asm_full_simp_tac);
berghofe@5188
    63
qed "not_gr0";
nipkow@6109
    64
AddIffs [not_gr0];
berghofe@5188
    65
oheimb@8260
    66
Goal "(Suc n <= m') --> (? m. m' = Suc m)";
oheimb@8260
    67
by (induct_tac "m'" 1);
oheimb@8260
    68
by  Auto_tac;
oheimb@8260
    69
qed_spec_mp "Suc_le_D";
oheimb@8260
    70
paulson@6805
    71
(*Useful in certain inductive arguments*)
paulson@6805
    72
Goal "(m < Suc n) = (m=0 | (EX j. m = Suc j & j < n))";
wenzelm@8442
    73
by (case_tac "m" 1);
paulson@6805
    74
by Auto_tac;
paulson@6805
    75
qed "less_Suc_eq_0_disj";
paulson@6805
    76
paulson@7058
    77
Goalw [Least_nat_def]
paulson@7058
    78
 "[| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))";
paulson@7058
    79
by (rtac select_equality 1);
paulson@7058
    80
by (fold_goals_tac [Least_nat_def]);
paulson@7058
    81
by (safe_tac (claset() addSEs [LeastI]));
paulson@7058
    82
by (rename_tac "j" 1);
wenzelm@8442
    83
by (case_tac "j" 1);
paulson@7058
    84
by (Blast_tac 1);
paulson@7058
    85
by (blast_tac (claset() addDs [Suc_less_SucD, not_less_Least]) 1);
paulson@7058
    86
by (rename_tac "k n" 1);
wenzelm@8442
    87
by (case_tac "k" 1);
paulson@7058
    88
by (Blast_tac 1);
paulson@7058
    89
by (hyp_subst_tac 1);
paulson@7058
    90
by (rewtac Least_nat_def);
paulson@7058
    91
by (rtac (select_equality RS arg_cong RS sym) 1);
paulson@7089
    92
by (blast_tac (claset() addDs [Suc_mono]) 1);
paulson@7089
    93
by (cut_inst_tac [("m","m")] less_linear 1);
paulson@7089
    94
by (blast_tac (claset() addIs [Suc_mono]) 1);
paulson@7058
    95
qed "Least_Suc";
berghofe@5188
    96
paulson@7058
    97
val prems = Goal "[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n";
paulson@7058
    98
by (rtac less_induct 1);
wenzelm@8442
    99
by (case_tac "n" 1);
wenzelm@8442
   100
by (case_tac "nat" 2);
paulson@7089
   101
by (ALLGOALS (blast_tac (claset() addIs prems@[less_trans])));
paulson@7058
   102
qed "nat_induct2";
berghofe@5188
   103
paulson@8942
   104
Goal "min 0 n = (0::nat)";
paulson@3023
   105
by (rtac min_leastL 1);
nipkow@5983
   106
by (Simp_tac 1);
nipkow@2608
   107
qed "min_0L";
nipkow@1301
   108
paulson@8942
   109
Goal "min n 0 = (0::nat)";
paulson@3023
   110
by (rtac min_leastR 1);
nipkow@5983
   111
by (Simp_tac 1);
nipkow@2608
   112
qed "min_0R";
clasohm@923
   113
wenzelm@5069
   114
Goalw [min_def] "min (Suc m) (Suc n) = Suc(min m n)";
paulson@3023
   115
by (Simp_tac 1);
nipkow@2608
   116
qed "min_Suc_Suc";
oheimb@1660
   117
nipkow@2608
   118
Addsimps [min_0L,min_0R,min_Suc_Suc];
nipkow@6433
   119
paulson@8942
   120
Goalw [max_def] "max 0 n = (n::nat)";
nipkow@6433
   121
by (Simp_tac 1);
nipkow@6433
   122
qed "max_0L";
nipkow@6433
   123
paulson@8942
   124
Goalw [max_def] "max n 0 = (n::nat)";
nipkow@6433
   125
by (Simp_tac 1);
nipkow@6433
   126
qed "max_0R";
nipkow@6433
   127
nipkow@6433
   128
Goalw [max_def] "max (Suc m) (Suc n) = Suc(max m n)";
nipkow@6433
   129
by (Simp_tac 1);
nipkow@6433
   130
qed "max_Suc_Suc";
nipkow@6433
   131
nipkow@6433
   132
Addsimps [max_0L,max_0R,max_Suc_Suc];
wenzelm@9436
   133
wenzelm@9436
   134
wenzelm@9436
   135
(*** Basic rewrite rules for the arithmetic operators ***)
wenzelm@9436
   136
wenzelm@9436
   137
(** Difference **)
wenzelm@9436
   138
wenzelm@9436
   139
Goal "0 - n = (0::nat)";
wenzelm@9436
   140
by (induct_tac "n" 1);
wenzelm@9436
   141
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   142
qed "diff_0_eq_0";
wenzelm@9436
   143
wenzelm@9436
   144
(*Must simplify BEFORE the induction!  (Else we get a critical pair)
wenzelm@9436
   145
  Suc(m) - Suc(n)   rewrites to   pred(Suc(m) - n)  *)
wenzelm@9436
   146
Goal "Suc(m) - Suc(n) = m - n";
wenzelm@9436
   147
by (Simp_tac 1);
wenzelm@9436
   148
by (induct_tac "n" 1);
wenzelm@9436
   149
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   150
qed "diff_Suc_Suc";
wenzelm@9436
   151
wenzelm@9436
   152
Addsimps [diff_0_eq_0, diff_Suc_Suc];
wenzelm@9436
   153
wenzelm@9436
   154
(* Could be (and is, below) generalized in various ways;
wenzelm@9436
   155
   However, none of the generalizations are currently in the simpset,
wenzelm@9436
   156
   and I dread to think what happens if I put them in *)
wenzelm@9436
   157
Goal "0 < n ==> Suc(n-1) = n";
wenzelm@9436
   158
by (asm_simp_tac (simpset() addsplits [nat.split]) 1);
wenzelm@9436
   159
qed "Suc_pred";
wenzelm@9436
   160
Addsimps [Suc_pred];
wenzelm@9436
   161
wenzelm@9436
   162
Delsimps [diff_Suc];
wenzelm@9436
   163
wenzelm@9436
   164
wenzelm@9436
   165
(**** Inductive properties of the operators ****)
wenzelm@9436
   166
wenzelm@9436
   167
(*** Addition ***)
wenzelm@9436
   168
wenzelm@9436
   169
Goal "m + 0 = (m::nat)";
wenzelm@9436
   170
by (induct_tac "m" 1);
wenzelm@9436
   171
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   172
qed "add_0_right";
wenzelm@9436
   173
wenzelm@9436
   174
Goal "m + Suc(n) = Suc(m+n)";
wenzelm@9436
   175
by (induct_tac "m" 1);
wenzelm@9436
   176
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   177
qed "add_Suc_right";
wenzelm@9436
   178
wenzelm@9436
   179
Addsimps [add_0_right,add_Suc_right];
wenzelm@9436
   180
wenzelm@9436
   181
wenzelm@9436
   182
(*Associative law for addition*)
wenzelm@9436
   183
Goal "(m + n) + k = m + ((n + k)::nat)";
wenzelm@9436
   184
by (induct_tac "m" 1);
wenzelm@9436
   185
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   186
qed "add_assoc";
wenzelm@9436
   187
wenzelm@9436
   188
(*Commutative law for addition*)
wenzelm@9436
   189
Goal "m + n = n + (m::nat)";
wenzelm@9436
   190
by (induct_tac "m" 1);
wenzelm@9436
   191
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   192
qed "add_commute";
wenzelm@9436
   193
wenzelm@9436
   194
Goal "x+(y+z)=y+((x+z)::nat)";
wenzelm@9436
   195
by (rtac (add_commute RS trans) 1);
wenzelm@9436
   196
by (rtac (add_assoc RS trans) 1);
wenzelm@9436
   197
by (rtac (add_commute RS arg_cong) 1);
wenzelm@9436
   198
qed "add_left_commute";
wenzelm@9436
   199
wenzelm@9436
   200
(*Addition is an AC-operator*)
wenzelm@9436
   201
bind_thms ("add_ac", [add_assoc, add_commute, add_left_commute]);
wenzelm@9436
   202
wenzelm@9436
   203
Goal "(k + m = k + n) = (m=(n::nat))";
wenzelm@9436
   204
by (induct_tac "k" 1);
wenzelm@9436
   205
by (Simp_tac 1);
wenzelm@9436
   206
by (Asm_simp_tac 1);
wenzelm@9436
   207
qed "add_left_cancel";
wenzelm@9436
   208
wenzelm@9436
   209
Goal "(m + k = n + k) = (m=(n::nat))";
wenzelm@9436
   210
by (induct_tac "k" 1);
wenzelm@9436
   211
by (Simp_tac 1);
wenzelm@9436
   212
by (Asm_simp_tac 1);
wenzelm@9436
   213
qed "add_right_cancel";
wenzelm@9436
   214
wenzelm@9436
   215
Goal "(k + m <= k + n) = (m<=(n::nat))";
wenzelm@9436
   216
by (induct_tac "k" 1);
wenzelm@9436
   217
by (Simp_tac 1);
wenzelm@9436
   218
by (Asm_simp_tac 1);
wenzelm@9436
   219
qed "add_left_cancel_le";
wenzelm@9436
   220
wenzelm@9436
   221
Goal "(k + m < k + n) = (m<(n::nat))";
wenzelm@9436
   222
by (induct_tac "k" 1);
wenzelm@9436
   223
by (Simp_tac 1);
wenzelm@9436
   224
by (Asm_simp_tac 1);
wenzelm@9436
   225
qed "add_left_cancel_less";
wenzelm@9436
   226
wenzelm@9436
   227
Addsimps [add_left_cancel, add_right_cancel,
wenzelm@9436
   228
          add_left_cancel_le, add_left_cancel_less];
wenzelm@9436
   229
wenzelm@9436
   230
(** Reasoning about m+0=0, etc. **)
wenzelm@9436
   231
wenzelm@9436
   232
Goal "!!m::nat. (m+n = 0) = (m=0 & n=0)";
wenzelm@9436
   233
by (case_tac "m" 1);
wenzelm@9436
   234
by (Auto_tac);
wenzelm@9436
   235
qed "add_is_0";
wenzelm@9436
   236
AddIffs [add_is_0];
wenzelm@9436
   237
wenzelm@9436
   238
Goal "!!m::nat. (0 = m+n) = (m=0 & n=0)";
wenzelm@9436
   239
by (case_tac "m" 1);
wenzelm@9436
   240
by (Auto_tac);
wenzelm@9436
   241
qed "zero_is_add";
wenzelm@9436
   242
AddIffs [zero_is_add];
wenzelm@9436
   243
wenzelm@9436
   244
Goal "!!m::nat. (m+n=1) = (m=1 & n=0 | m=0 & n=1)";
wenzelm@9436
   245
by (case_tac "m" 1);
wenzelm@9436
   246
by (Auto_tac);
wenzelm@9436
   247
qed "add_is_1";
wenzelm@9436
   248
wenzelm@9436
   249
Goal "!!m::nat. (1=m+n) = (m=1 & n=0 | m=0 & n=1)";
wenzelm@9436
   250
by (case_tac "m" 1);
wenzelm@9436
   251
by (Auto_tac);
wenzelm@9436
   252
qed "one_is_add";
wenzelm@9436
   253
wenzelm@9436
   254
Goal "!!m::nat. (0<m+n) = (0<m | 0<n)";
wenzelm@9436
   255
by (simp_tac (simpset() delsimps [neq0_conv] addsimps [neq0_conv RS sym]) 1);
wenzelm@9436
   256
qed "add_gr_0";
wenzelm@9436
   257
AddIffs [add_gr_0];
wenzelm@9436
   258
wenzelm@9436
   259
(* Could be generalized, eg to "k<n ==> m+(n-(Suc k)) = (m+n)-(Suc k)" *)
wenzelm@9436
   260
Goal "!!m::nat. 0<n ==> m + (n-1) = (m+n)-1";
wenzelm@9436
   261
by (case_tac "m" 1);
wenzelm@9436
   262
by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc, Suc_n_not_n]
wenzelm@9436
   263
                                      addsplits [nat.split])));
wenzelm@9436
   264
qed "add_pred";
wenzelm@9436
   265
Addsimps [add_pred];
wenzelm@9436
   266
wenzelm@9436
   267
Goal "!!m::nat. m + n = m ==> n = 0";
wenzelm@9436
   268
by (dtac (add_0_right RS ssubst) 1);
wenzelm@9436
   269
by (asm_full_simp_tac (simpset() addsimps [add_assoc]
wenzelm@9436
   270
                                 delsimps [add_0_right]) 1);
wenzelm@9436
   271
qed "add_eq_self_zero";
wenzelm@9436
   272
wenzelm@9436
   273
wenzelm@9436
   274
(**** Additional theorems about "less than" ****)
wenzelm@9436
   275
wenzelm@9436
   276
(*Deleted less_natE; instead use less_eq_Suc_add RS exE*)
wenzelm@9436
   277
Goal "m<n --> (EX k. n=Suc(m+k))";
wenzelm@9436
   278
by (induct_tac "n" 1);
wenzelm@9436
   279
by (ALLGOALS (simp_tac (simpset() addsimps [order_le_less])));
wenzelm@9436
   280
by (blast_tac (claset() addSEs [less_SucE]
wenzelm@9436
   281
                        addSIs [add_0_right RS sym, add_Suc_right RS sym]) 1);
wenzelm@9436
   282
qed_spec_mp "less_eq_Suc_add";
wenzelm@9436
   283
wenzelm@9436
   284
Goal "n <= ((m + n)::nat)";
wenzelm@9436
   285
by (induct_tac "m" 1);
wenzelm@9436
   286
by (ALLGOALS Simp_tac);
wenzelm@9436
   287
by (etac le_SucI 1);
wenzelm@9436
   288
qed "le_add2";
wenzelm@9436
   289
wenzelm@9436
   290
Goal "n <= ((n + m)::nat)";
wenzelm@9436
   291
by (simp_tac (simpset() addsimps add_ac) 1);
wenzelm@9436
   292
by (rtac le_add2 1);
wenzelm@9436
   293
qed "le_add1";
wenzelm@9436
   294
wenzelm@9436
   295
bind_thm ("less_add_Suc1", (lessI RS (le_add1 RS le_less_trans)));
wenzelm@9436
   296
bind_thm ("less_add_Suc2", (lessI RS (le_add2 RS le_less_trans)));
wenzelm@9436
   297
wenzelm@9436
   298
Goal "(m<n) = (EX k. n=Suc(m+k))";
wenzelm@9436
   299
by (blast_tac (claset() addSIs [less_add_Suc1, less_eq_Suc_add]) 1);
wenzelm@9436
   300
qed "less_iff_Suc_add";
wenzelm@9436
   301
wenzelm@9436
   302
wenzelm@9436
   303
(*"i <= j ==> i <= j+m"*)
wenzelm@9436
   304
bind_thm ("trans_le_add1", le_add1 RSN (2,le_trans));
wenzelm@9436
   305
wenzelm@9436
   306
(*"i <= j ==> i <= m+j"*)
wenzelm@9436
   307
bind_thm ("trans_le_add2", le_add2 RSN (2,le_trans));
wenzelm@9436
   308
wenzelm@9436
   309
(*"i < j ==> i < j+m"*)
wenzelm@9436
   310
bind_thm ("trans_less_add1", le_add1 RSN (2,less_le_trans));
wenzelm@9436
   311
wenzelm@9436
   312
(*"i < j ==> i < m+j"*)
wenzelm@9436
   313
bind_thm ("trans_less_add2", le_add2 RSN (2,less_le_trans));
wenzelm@9436
   314
wenzelm@9436
   315
Goal "i+j < (k::nat) --> i<k";
wenzelm@9436
   316
by (induct_tac "j" 1);
wenzelm@9436
   317
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   318
by (blast_tac (claset() addDs [Suc_lessD]) 1);
wenzelm@9436
   319
qed_spec_mp "add_lessD1";
wenzelm@9436
   320
wenzelm@9436
   321
Goal "~ (i+j < (i::nat))";
wenzelm@9436
   322
by (rtac notI 1);
wenzelm@9436
   323
by (etac (add_lessD1 RS less_irrefl) 1);
wenzelm@9436
   324
qed "not_add_less1";
wenzelm@9436
   325
wenzelm@9436
   326
Goal "~ (j+i < (i::nat))";
wenzelm@9436
   327
by (simp_tac (simpset() addsimps [add_commute, not_add_less1]) 1);
wenzelm@9436
   328
qed "not_add_less2";
wenzelm@9436
   329
AddIffs [not_add_less1, not_add_less2];
wenzelm@9436
   330
wenzelm@9436
   331
Goal "m+k<=n --> m<=(n::nat)";
wenzelm@9436
   332
by (induct_tac "k" 1);
wenzelm@9436
   333
by (ALLGOALS (asm_simp_tac (simpset() addsimps le_simps)));
wenzelm@9436
   334
qed_spec_mp "add_leD1";
wenzelm@9436
   335
wenzelm@9436
   336
Goal "m+k<=n ==> k<=(n::nat)";
wenzelm@9436
   337
by (full_simp_tac (simpset() addsimps [add_commute]) 1);
wenzelm@9436
   338
by (etac add_leD1 1);
wenzelm@9436
   339
qed_spec_mp "add_leD2";
wenzelm@9436
   340
wenzelm@9436
   341
Goal "m+k<=n ==> m<=n & k<=(n::nat)";
wenzelm@9436
   342
by (blast_tac (claset() addDs [add_leD1, add_leD2]) 1);
wenzelm@9436
   343
bind_thm ("add_leE", result() RS conjE);
wenzelm@9436
   344
wenzelm@9436
   345
(*needs !!k for add_ac to work*)
wenzelm@9436
   346
Goal "!!k:: nat. [| k<l;  m+l = k+n |] ==> m<n";
wenzelm@9436
   347
by (force_tac (claset(),
wenzelm@9436
   348
              simpset() delsimps [add_Suc_right]
wenzelm@9436
   349
                        addsimps [less_iff_Suc_add,
wenzelm@9436
   350
                                  add_Suc_right RS sym] @ add_ac) 1);
wenzelm@9436
   351
qed "less_add_eq_less";
wenzelm@9436
   352
wenzelm@9436
   353
wenzelm@9436
   354
(*** Monotonicity of Addition ***)
wenzelm@9436
   355
wenzelm@9436
   356
(*strict, in 1st argument*)
wenzelm@9436
   357
Goal "i < j ==> i + k < j + (k::nat)";
wenzelm@9436
   358
by (induct_tac "k" 1);
wenzelm@9436
   359
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   360
qed "add_less_mono1";
wenzelm@9436
   361
wenzelm@9436
   362
(*strict, in both arguments*)
wenzelm@9436
   363
Goal "[|i < j; k < l|] ==> i + k < j + (l::nat)";
wenzelm@9436
   364
by (rtac (add_less_mono1 RS less_trans) 1);
wenzelm@9436
   365
by (REPEAT (assume_tac 1));
wenzelm@9436
   366
by (induct_tac "j" 1);
wenzelm@9436
   367
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   368
qed "add_less_mono";
wenzelm@9436
   369
wenzelm@9436
   370
(*A [clumsy] way of lifting < monotonicity to <= monotonicity *)
wenzelm@9436
   371
val [lt_mono,le] = Goal
wenzelm@9436
   372
     "[| !!i j::nat. i<j ==> f(i) < f(j);       \
wenzelm@9436
   373
\        i <= j                                 \
wenzelm@9436
   374
\     |] ==> f(i) <= (f(j)::nat)";
wenzelm@9436
   375
by (cut_facts_tac [le] 1);
wenzelm@9436
   376
by (asm_full_simp_tac (simpset() addsimps [order_le_less]) 1);
wenzelm@9436
   377
by (blast_tac (claset() addSIs [lt_mono]) 1);
wenzelm@9436
   378
qed "less_mono_imp_le_mono";
wenzelm@9436
   379
wenzelm@9436
   380
(*non-strict, in 1st argument*)
wenzelm@9436
   381
Goal "i<=j ==> i + k <= j + (k::nat)";
wenzelm@9436
   382
by (res_inst_tac [("f", "%j. j+k")] less_mono_imp_le_mono 1);
wenzelm@9436
   383
by (etac add_less_mono1 1);
wenzelm@9436
   384
by (assume_tac 1);
wenzelm@9436
   385
qed "add_le_mono1";
wenzelm@9436
   386
wenzelm@9436
   387
(*non-strict, in both arguments*)
wenzelm@9436
   388
Goal "[|i<=j;  k<=l |] ==> i + k <= j + (l::nat)";
wenzelm@9436
   389
by (etac (add_le_mono1 RS le_trans) 1);
wenzelm@9436
   390
by (simp_tac (simpset() addsimps [add_commute]) 1);
wenzelm@9436
   391
qed "add_le_mono";
wenzelm@9436
   392
wenzelm@9436
   393
wenzelm@9436
   394
(*** Multiplication ***)
wenzelm@9436
   395
wenzelm@9436
   396
(*right annihilation in product*)
wenzelm@9436
   397
Goal "!!m::nat. m * 0 = 0";
wenzelm@9436
   398
by (induct_tac "m" 1);
wenzelm@9436
   399
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   400
qed "mult_0_right";
wenzelm@9436
   401
wenzelm@9436
   402
(*right successor law for multiplication*)
wenzelm@9436
   403
Goal  "m * Suc(n) = m + (m * n)";
wenzelm@9436
   404
by (induct_tac "m" 1);
wenzelm@9436
   405
by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac)));
wenzelm@9436
   406
qed "mult_Suc_right";
wenzelm@9436
   407
wenzelm@9436
   408
Addsimps [mult_0_right, mult_Suc_right];
wenzelm@9436
   409
wenzelm@9436
   410
Goal "1 * n = n";
wenzelm@9436
   411
by (Asm_simp_tac 1);
wenzelm@9436
   412
qed "mult_1";
wenzelm@9436
   413
wenzelm@9436
   414
Goal "n * 1 = n";
wenzelm@9436
   415
by (Asm_simp_tac 1);
wenzelm@9436
   416
qed "mult_1_right";
wenzelm@9436
   417
wenzelm@9436
   418
(*Commutative law for multiplication*)
wenzelm@9436
   419
Goal "m * n = n * (m::nat)";
wenzelm@9436
   420
by (induct_tac "m" 1);
wenzelm@9436
   421
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   422
qed "mult_commute";
wenzelm@9436
   423
wenzelm@9436
   424
(*addition distributes over multiplication*)
wenzelm@9436
   425
Goal "(m + n)*k = (m*k) + ((n*k)::nat)";
wenzelm@9436
   426
by (induct_tac "m" 1);
wenzelm@9436
   427
by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac)));
wenzelm@9436
   428
qed "add_mult_distrib";
wenzelm@9436
   429
wenzelm@9436
   430
Goal "k*(m + n) = (k*m) + ((k*n)::nat)";
wenzelm@9436
   431
by (induct_tac "m" 1);
wenzelm@9436
   432
by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac)));
wenzelm@9436
   433
qed "add_mult_distrib2";
wenzelm@9436
   434
wenzelm@9436
   435
(*Associative law for multiplication*)
wenzelm@9436
   436
Goal "(m * n) * k = m * ((n * k)::nat)";
wenzelm@9436
   437
by (induct_tac "m" 1);
wenzelm@9436
   438
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_mult_distrib])));
wenzelm@9436
   439
qed "mult_assoc";
wenzelm@9436
   440
wenzelm@9436
   441
Goal "x*(y*z) = y*((x*z)::nat)";
wenzelm@9436
   442
by (rtac trans 1);
wenzelm@9436
   443
by (rtac mult_commute 1);
wenzelm@9436
   444
by (rtac trans 1);
wenzelm@9436
   445
by (rtac mult_assoc 1);
wenzelm@9436
   446
by (rtac (mult_commute RS arg_cong) 1);
wenzelm@9436
   447
qed "mult_left_commute";
wenzelm@9436
   448
wenzelm@9436
   449
bind_thms ("mult_ac", [mult_assoc,mult_commute,mult_left_commute]);
wenzelm@9436
   450
wenzelm@9436
   451
Goal "!!m::nat. (m*n = 0) = (m=0 | n=0)";
wenzelm@9436
   452
by (induct_tac "m" 1);
wenzelm@9436
   453
by (induct_tac "n" 2);
wenzelm@9436
   454
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   455
qed "mult_is_0";
wenzelm@9436
   456
wenzelm@9436
   457
Goal "!!m::nat. (0 = m*n) = (0=m | 0=n)";
wenzelm@9436
   458
by (stac eq_commute 1 THEN stac mult_is_0 1);
wenzelm@9436
   459
by Auto_tac;
wenzelm@9436
   460
qed "zero_is_mult";
wenzelm@9436
   461
wenzelm@9436
   462
Addsimps [mult_is_0, zero_is_mult];
wenzelm@9436
   463
wenzelm@9436
   464
wenzelm@9436
   465
(*** Difference ***)
wenzelm@9436
   466
wenzelm@9436
   467
Goal "!!m::nat. m - m = 0";
wenzelm@9436
   468
by (induct_tac "m" 1);
wenzelm@9436
   469
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   470
qed "diff_self_eq_0";
wenzelm@9436
   471
wenzelm@9436
   472
Addsimps [diff_self_eq_0];
wenzelm@9436
   473
wenzelm@9436
   474
(*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
wenzelm@9436
   475
Goal "~ m<n --> n+(m-n) = (m::nat)";
wenzelm@9436
   476
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
wenzelm@9436
   477
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   478
qed_spec_mp "add_diff_inverse";
wenzelm@9436
   479
wenzelm@9436
   480
Goal "n<=m ==> n+(m-n) = (m::nat)";
wenzelm@9436
   481
by (asm_simp_tac (simpset() addsimps [add_diff_inverse, not_less_iff_le]) 1);
wenzelm@9436
   482
qed "le_add_diff_inverse";
wenzelm@9436
   483
wenzelm@9436
   484
Goal "n<=m ==> (m-n)+n = (m::nat)";
wenzelm@9436
   485
by (asm_simp_tac (simpset() addsimps [le_add_diff_inverse, add_commute]) 1);
wenzelm@9436
   486
qed "le_add_diff_inverse2";
wenzelm@9436
   487
wenzelm@9436
   488
Addsimps  [le_add_diff_inverse, le_add_diff_inverse2];
wenzelm@9436
   489
wenzelm@9436
   490
wenzelm@9436
   491
(*** More results about difference ***)
wenzelm@9436
   492
wenzelm@9436
   493
Goal "n <= m ==> Suc(m)-n = Suc(m-n)";
wenzelm@9436
   494
by (etac rev_mp 1);
wenzelm@9436
   495
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
wenzelm@9436
   496
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   497
qed "Suc_diff_le";
wenzelm@9436
   498
wenzelm@9436
   499
Goal "m - n < Suc(m)";
wenzelm@9436
   500
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
wenzelm@9436
   501
by (etac less_SucE 3);
wenzelm@9436
   502
by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq])));
wenzelm@9436
   503
qed "diff_less_Suc";
wenzelm@9436
   504
wenzelm@9436
   505
Goal "m - n <= (m::nat)";
wenzelm@9436
   506
by (res_inst_tac [("m","m"), ("n","n")] diff_induct 1);
wenzelm@9436
   507
by (ALLGOALS (asm_simp_tac (simpset() addsimps [le_SucI])));
wenzelm@9436
   508
qed "diff_le_self";
wenzelm@9436
   509
Addsimps [diff_le_self];
wenzelm@9436
   510
wenzelm@9436
   511
(* j<k ==> j-n < k *)
wenzelm@9436
   512
bind_thm ("less_imp_diff_less", diff_le_self RS le_less_trans);
wenzelm@9436
   513
wenzelm@9436
   514
Goal "!!i::nat. i-j-k = i - (j+k)";
wenzelm@9436
   515
by (res_inst_tac [("m","i"),("n","j")] diff_induct 1);
wenzelm@9436
   516
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   517
qed "diff_diff_left";
wenzelm@9436
   518
wenzelm@9436
   519
Goal "(Suc m - n) - Suc k = m - n - k";
wenzelm@9436
   520
by (simp_tac (simpset() addsimps [diff_diff_left]) 1);
wenzelm@9436
   521
qed "Suc_diff_diff";
wenzelm@9436
   522
Addsimps [Suc_diff_diff];
wenzelm@9436
   523
wenzelm@9436
   524
Goal "0<n ==> n - Suc i < n";
wenzelm@9436
   525
by (case_tac "n" 1);
wenzelm@9436
   526
by Safe_tac;
wenzelm@9436
   527
by (asm_simp_tac (simpset() addsimps le_simps) 1);
wenzelm@9436
   528
qed "diff_Suc_less";
wenzelm@9436
   529
Addsimps [diff_Suc_less];
wenzelm@9436
   530
wenzelm@9436
   531
(*This and the next few suggested by Florian Kammueller*)
wenzelm@9436
   532
Goal "!!i::nat. i-j-k = i-k-j";
wenzelm@9436
   533
by (simp_tac (simpset() addsimps [diff_diff_left, add_commute]) 1);
wenzelm@9436
   534
qed "diff_commute";
wenzelm@9436
   535
wenzelm@9436
   536
Goal "k <= (j::nat) --> (i + j) - k = i + (j - k)";
wenzelm@9436
   537
by (res_inst_tac [("m","j"),("n","k")] diff_induct 1);
wenzelm@9436
   538
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   539
qed_spec_mp "diff_add_assoc";
wenzelm@9436
   540
wenzelm@9436
   541
Goal "k <= (j::nat) --> (j + i) - k = (j - k) + i";
wenzelm@9436
   542
by (asm_simp_tac (simpset() addsimps [add_commute, diff_add_assoc]) 1);
wenzelm@9436
   543
qed_spec_mp "diff_add_assoc2";
wenzelm@9436
   544
wenzelm@9436
   545
Goal "(n+m) - n = (m::nat)";
wenzelm@9436
   546
by (induct_tac "n" 1);
wenzelm@9436
   547
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   548
qed "diff_add_inverse";
wenzelm@9436
   549
wenzelm@9436
   550
Goal "(m+n) - n = (m::nat)";
wenzelm@9436
   551
by (simp_tac (simpset() addsimps [diff_add_assoc]) 1);
wenzelm@9436
   552
qed "diff_add_inverse2";
wenzelm@9436
   553
wenzelm@9436
   554
Goal "i <= (j::nat) ==> (j-i=k) = (j=k+i)";
wenzelm@9436
   555
by Safe_tac;
wenzelm@9436
   556
by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_add_inverse2])));
wenzelm@9436
   557
qed "le_imp_diff_is_add";
wenzelm@9436
   558
wenzelm@9436
   559
Goal "!!m::nat. (m-n = 0) = (m <= n)";
wenzelm@9436
   560
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
wenzelm@9436
   561
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   562
qed "diff_is_0_eq";
wenzelm@9436
   563
wenzelm@9436
   564
Goal "!!m::nat. (0 = m-n) = (m <= n)";
wenzelm@9436
   565
by (stac (diff_is_0_eq RS sym) 1);
wenzelm@9436
   566
by (rtac eq_sym_conv 1);
wenzelm@9436
   567
qed "zero_is_diff_eq";
wenzelm@9436
   568
Addsimps [diff_is_0_eq, zero_is_diff_eq];
wenzelm@9436
   569
wenzelm@9436
   570
Goal "!!m::nat. (0<n-m) = (m<n)";
wenzelm@9436
   571
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
wenzelm@9436
   572
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   573
qed "zero_less_diff";
wenzelm@9436
   574
Addsimps [zero_less_diff];
wenzelm@9436
   575
wenzelm@9436
   576
Goal "i < j  ==> EX k::nat. 0<k & i+k = j";
wenzelm@9436
   577
by (res_inst_tac [("x","j - i")] exI 1);
wenzelm@9436
   578
by (asm_simp_tac (simpset() addsimps [add_diff_inverse, less_not_sym]) 1);
wenzelm@9436
   579
qed "less_imp_add_positive";
wenzelm@9436
   580
wenzelm@9436
   581
Goal "P(k) --> (ALL n. P(Suc(n))--> P(n)) --> P(k-i)";
wenzelm@9436
   582
by (res_inst_tac [("m","k"),("n","i")] diff_induct 1);
wenzelm@9436
   583
by (ALLGOALS (Clarify_tac THEN' Simp_tac THEN' TRY o Blast_tac));
wenzelm@9436
   584
qed "zero_induct_lemma";
wenzelm@9436
   585
wenzelm@9436
   586
val prems = Goal "[| P(k);  !!n. P(Suc(n)) ==> P(n) |] ==> P(0)";
wenzelm@9436
   587
by (rtac (diff_self_eq_0 RS subst) 1);
wenzelm@9436
   588
by (rtac (zero_induct_lemma RS mp RS mp) 1);
wenzelm@9436
   589
by (REPEAT (ares_tac ([impI,allI]@prems) 1));
wenzelm@9436
   590
qed "zero_induct";
wenzelm@9436
   591
wenzelm@9436
   592
Goal "(k+m) - (k+n) = m - (n::nat)";
wenzelm@9436
   593
by (induct_tac "k" 1);
wenzelm@9436
   594
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   595
qed "diff_cancel";
wenzelm@9436
   596
wenzelm@9436
   597
Goal "(m+k) - (n+k) = m - (n::nat)";
wenzelm@9436
   598
by (asm_simp_tac
wenzelm@9436
   599
    (simpset() addsimps [diff_cancel, inst "n" "k" add_commute]) 1);
wenzelm@9436
   600
qed "diff_cancel2";
wenzelm@9436
   601
wenzelm@9436
   602
Goal "n - (n+m) = (0::nat)";
wenzelm@9436
   603
by (induct_tac "n" 1);
wenzelm@9436
   604
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   605
qed "diff_add_0";
wenzelm@9436
   606
wenzelm@9436
   607
wenzelm@9436
   608
(** Difference distributes over multiplication **)
wenzelm@9436
   609
wenzelm@9436
   610
Goal "!!m::nat. (m - n) * k = (m * k) - (n * k)";
wenzelm@9436
   611
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
wenzelm@9436
   612
by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_cancel])));
wenzelm@9436
   613
qed "diff_mult_distrib" ;
wenzelm@9436
   614
wenzelm@9436
   615
Goal "!!m::nat. k * (m - n) = (k * m) - (k * n)";
wenzelm@9436
   616
val mult_commute_k = read_instantiate [("m","k")] mult_commute;
wenzelm@9436
   617
by (simp_tac (simpset() addsimps [diff_mult_distrib, mult_commute_k]) 1);
wenzelm@9436
   618
qed "diff_mult_distrib2" ;
wenzelm@9436
   619
(*NOT added as rewrites, since sometimes they are used from right-to-left*)
wenzelm@9436
   620
wenzelm@9436
   621
wenzelm@9436
   622
(*** Monotonicity of Multiplication ***)
wenzelm@9436
   623
wenzelm@9436
   624
Goal "i <= (j::nat) ==> i*k<=j*k";
wenzelm@9436
   625
by (induct_tac "k" 1);
wenzelm@9436
   626
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_le_mono])));
wenzelm@9436
   627
qed "mult_le_mono1";
wenzelm@9436
   628
wenzelm@9436
   629
Goal "i <= (j::nat) ==> k*i <= k*j";
wenzelm@9436
   630
by (dtac mult_le_mono1 1);
wenzelm@9436
   631
by (asm_simp_tac (simpset() addsimps [mult_commute]) 1);
wenzelm@9436
   632
qed "mult_le_mono2";
wenzelm@9436
   633
wenzelm@9436
   634
(* <= monotonicity, BOTH arguments*)
wenzelm@9436
   635
Goal "[| i <= (j::nat); k <= l |] ==> i*k <= j*l";
wenzelm@9436
   636
by (etac (mult_le_mono1 RS le_trans) 1);
wenzelm@9436
   637
by (etac mult_le_mono2 1);
wenzelm@9436
   638
qed "mult_le_mono";
wenzelm@9436
   639
wenzelm@9436
   640
(*strict, in 1st argument; proof is by induction on k>0*)
wenzelm@9436
   641
Goal "!!i::nat. [| i<j; 0<k |] ==> k*i < k*j";
wenzelm@9436
   642
by (eres_inst_tac [("m1","0")] (less_eq_Suc_add RS exE) 1);
wenzelm@9436
   643
by (Asm_simp_tac 1);
wenzelm@9436
   644
by (induct_tac "x" 1);
wenzelm@9436
   645
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_less_mono])));
wenzelm@9436
   646
qed "mult_less_mono2";
wenzelm@9436
   647
wenzelm@9436
   648
Goal "!!i::nat. [| i<j; 0<k |] ==> i*k < j*k";
wenzelm@9436
   649
by (dtac mult_less_mono2 1);
wenzelm@9436
   650
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [mult_commute])));
wenzelm@9436
   651
qed "mult_less_mono1";
wenzelm@9436
   652
wenzelm@9436
   653
Goal "!!m::nat. (0 < m*n) = (0<m & 0<n)";
wenzelm@9436
   654
by (induct_tac "m" 1);
wenzelm@9436
   655
by (case_tac "n" 2);
wenzelm@9436
   656
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   657
qed "zero_less_mult_iff";
wenzelm@9436
   658
Addsimps [zero_less_mult_iff];
wenzelm@9436
   659
wenzelm@9436
   660
Goal "(1 <= m*n) = (1<=m & 1<=n)";
wenzelm@9436
   661
by (induct_tac "m" 1);
wenzelm@9436
   662
by (case_tac "n" 2);
wenzelm@9436
   663
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   664
qed "one_le_mult_iff";
wenzelm@9436
   665
Addsimps [one_le_mult_iff];
wenzelm@9436
   666
wenzelm@9436
   667
Goal "(m*n = 1) = (m=1 & n=1)";
wenzelm@9436
   668
by (induct_tac "m" 1);
wenzelm@9436
   669
by (Simp_tac 1);
wenzelm@9436
   670
by (induct_tac "n" 1);
wenzelm@9436
   671
by (Simp_tac 1);
wenzelm@9436
   672
by (fast_tac (claset() addss simpset()) 1);
wenzelm@9436
   673
qed "mult_eq_1_iff";
wenzelm@9436
   674
Addsimps [mult_eq_1_iff];
wenzelm@9436
   675
wenzelm@9436
   676
Goal "!!m::nat. 0<k ==> (m*k < n*k) = (m<n)";
wenzelm@9436
   677
by (safe_tac (claset() addSIs [mult_less_mono1]));
wenzelm@9436
   678
by (cut_facts_tac [less_linear] 1);
wenzelm@9436
   679
by (blast_tac (claset() addIs [mult_less_mono1] addEs [less_asym]) 1);
wenzelm@9436
   680
qed "mult_less_cancel2";
wenzelm@9436
   681
wenzelm@9436
   682
Goal "!!m::nat. 0<k ==> (k*m < k*n) = (m<n)";
wenzelm@9436
   683
by (dtac mult_less_cancel2 1);
wenzelm@9436
   684
by (etac subst 1);
wenzelm@9436
   685
by (simp_tac (simpset() addsimps [mult_commute]) 1);
wenzelm@9436
   686
qed "mult_less_cancel1";
wenzelm@9436
   687
Addsimps [mult_less_cancel1, mult_less_cancel2];
wenzelm@9436
   688
wenzelm@9436
   689
Goal "!!m::nat. 0<k ==> (m*k <= n*k) = (m<=n)";
wenzelm@9436
   690
by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
wenzelm@9436
   691
qed "mult_le_cancel2";
wenzelm@9436
   692
wenzelm@9436
   693
Goal "!!m::nat. 0<k ==> (k*m <= k*n) = (m<=n)";
wenzelm@9436
   694
by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
wenzelm@9436
   695
qed "mult_le_cancel1";
wenzelm@9436
   696
Addsimps [mult_le_cancel1, mult_le_cancel2];
wenzelm@9436
   697
wenzelm@9436
   698
Goal "(Suc k * m < Suc k * n) = (m < n)";
wenzelm@9436
   699
by (rtac mult_less_cancel1 1);
wenzelm@9436
   700
by (Simp_tac 1);
wenzelm@9436
   701
qed "Suc_mult_less_cancel1";
wenzelm@9436
   702
wenzelm@9436
   703
Goalw [le_def] "(Suc k * m <= Suc k * n) = (m <= n)";
wenzelm@9436
   704
by (simp_tac (simpset_of HOL.thy) 1);
wenzelm@9436
   705
by (rtac Suc_mult_less_cancel1 1);
wenzelm@9436
   706
qed "Suc_mult_le_cancel1";
wenzelm@9436
   707
wenzelm@9436
   708
Goal "0 < (k::nat) ==> (m*k = n*k) = (m=n)";
wenzelm@9436
   709
by (cut_facts_tac [less_linear] 1);
wenzelm@9436
   710
by Safe_tac;
wenzelm@9436
   711
by (assume_tac 2);
wenzelm@9436
   712
by (ALLGOALS (dtac mult_less_mono1 THEN' assume_tac));
wenzelm@9436
   713
by (ALLGOALS Asm_full_simp_tac);
wenzelm@9436
   714
qed "mult_cancel2";
wenzelm@9436
   715
wenzelm@9436
   716
Goal "0 < (k::nat) ==> (k*m = k*n) = (m=n)";
wenzelm@9436
   717
by (dtac mult_cancel2 1);
wenzelm@9436
   718
by (asm_full_simp_tac (simpset() addsimps [mult_commute]) 1);
wenzelm@9436
   719
qed "mult_cancel1";
wenzelm@9436
   720
Addsimps [mult_cancel1, mult_cancel2];
wenzelm@9436
   721
wenzelm@9436
   722
Goal "(Suc k * m = Suc k * n) = (m = n)";
wenzelm@9436
   723
by (rtac mult_cancel1 1);
wenzelm@9436
   724
by (Simp_tac 1);
wenzelm@9436
   725
qed "Suc_mult_cancel1";
wenzelm@9436
   726
wenzelm@9436
   727
wenzelm@9436
   728
(*Lemma for gcd*)
wenzelm@9436
   729
Goal "!!m::nat. m = m*n ==> n=1 | m=0";
wenzelm@9436
   730
by (dtac sym 1);
wenzelm@9436
   731
by (rtac disjCI 1);
wenzelm@9436
   732
by (rtac nat_less_cases 1 THEN assume_tac 2);
wenzelm@9436
   733
by (fast_tac (claset() addSEs [less_SucE] addss simpset()) 1);
wenzelm@9436
   734
by (best_tac (claset() addDs [mult_less_mono2] addss simpset()) 1);
wenzelm@9436
   735
qed "mult_eq_self_implies_10";