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