src/HOL/Nat.ML
author paulson
Thu Aug 17 12:02:01 2000 +0200 (2000-08-17)
changeset 9637 47d39a31eb2f
parent 9436 62bb04ab4b01
child 9870 2374ba026fc6
permissions -rw-r--r--
better rules for cancellation of common factors across comparisons
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
Goal "!!m::nat. m + n = m ==> n = 0";
wenzelm@9436
   260
by (dtac (add_0_right RS ssubst) 1);
wenzelm@9436
   261
by (asm_full_simp_tac (simpset() addsimps [add_assoc]
wenzelm@9436
   262
                                 delsimps [add_0_right]) 1);
wenzelm@9436
   263
qed "add_eq_self_zero";
wenzelm@9436
   264
wenzelm@9436
   265
wenzelm@9436
   266
(**** Additional theorems about "less than" ****)
wenzelm@9436
   267
wenzelm@9436
   268
(*Deleted less_natE; instead use less_eq_Suc_add RS exE*)
wenzelm@9436
   269
Goal "m<n --> (EX k. n=Suc(m+k))";
wenzelm@9436
   270
by (induct_tac "n" 1);
wenzelm@9436
   271
by (ALLGOALS (simp_tac (simpset() addsimps [order_le_less])));
wenzelm@9436
   272
by (blast_tac (claset() addSEs [less_SucE]
wenzelm@9436
   273
                        addSIs [add_0_right RS sym, add_Suc_right RS sym]) 1);
wenzelm@9436
   274
qed_spec_mp "less_eq_Suc_add";
wenzelm@9436
   275
wenzelm@9436
   276
Goal "n <= ((m + n)::nat)";
wenzelm@9436
   277
by (induct_tac "m" 1);
wenzelm@9436
   278
by (ALLGOALS Simp_tac);
wenzelm@9436
   279
by (etac le_SucI 1);
wenzelm@9436
   280
qed "le_add2";
wenzelm@9436
   281
wenzelm@9436
   282
Goal "n <= ((n + m)::nat)";
wenzelm@9436
   283
by (simp_tac (simpset() addsimps add_ac) 1);
wenzelm@9436
   284
by (rtac le_add2 1);
wenzelm@9436
   285
qed "le_add1";
wenzelm@9436
   286
wenzelm@9436
   287
bind_thm ("less_add_Suc1", (lessI RS (le_add1 RS le_less_trans)));
wenzelm@9436
   288
bind_thm ("less_add_Suc2", (lessI RS (le_add2 RS le_less_trans)));
wenzelm@9436
   289
wenzelm@9436
   290
Goal "(m<n) = (EX k. n=Suc(m+k))";
wenzelm@9436
   291
by (blast_tac (claset() addSIs [less_add_Suc1, less_eq_Suc_add]) 1);
wenzelm@9436
   292
qed "less_iff_Suc_add";
wenzelm@9436
   293
wenzelm@9436
   294
wenzelm@9436
   295
(*"i <= j ==> i <= j+m"*)
wenzelm@9436
   296
bind_thm ("trans_le_add1", le_add1 RSN (2,le_trans));
wenzelm@9436
   297
wenzelm@9436
   298
(*"i <= j ==> i <= m+j"*)
wenzelm@9436
   299
bind_thm ("trans_le_add2", le_add2 RSN (2,le_trans));
wenzelm@9436
   300
wenzelm@9436
   301
(*"i < j ==> i < j+m"*)
wenzelm@9436
   302
bind_thm ("trans_less_add1", le_add1 RSN (2,less_le_trans));
wenzelm@9436
   303
wenzelm@9436
   304
(*"i < j ==> i < m+j"*)
wenzelm@9436
   305
bind_thm ("trans_less_add2", le_add2 RSN (2,less_le_trans));
wenzelm@9436
   306
wenzelm@9436
   307
Goal "i+j < (k::nat) --> i<k";
wenzelm@9436
   308
by (induct_tac "j" 1);
wenzelm@9436
   309
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   310
by (blast_tac (claset() addDs [Suc_lessD]) 1);
wenzelm@9436
   311
qed_spec_mp "add_lessD1";
wenzelm@9436
   312
wenzelm@9436
   313
Goal "~ (i+j < (i::nat))";
wenzelm@9436
   314
by (rtac notI 1);
wenzelm@9436
   315
by (etac (add_lessD1 RS less_irrefl) 1);
wenzelm@9436
   316
qed "not_add_less1";
wenzelm@9436
   317
wenzelm@9436
   318
Goal "~ (j+i < (i::nat))";
wenzelm@9436
   319
by (simp_tac (simpset() addsimps [add_commute, not_add_less1]) 1);
wenzelm@9436
   320
qed "not_add_less2";
wenzelm@9436
   321
AddIffs [not_add_less1, not_add_less2];
wenzelm@9436
   322
wenzelm@9436
   323
Goal "m+k<=n --> m<=(n::nat)";
wenzelm@9436
   324
by (induct_tac "k" 1);
wenzelm@9436
   325
by (ALLGOALS (asm_simp_tac (simpset() addsimps le_simps)));
wenzelm@9436
   326
qed_spec_mp "add_leD1";
wenzelm@9436
   327
wenzelm@9436
   328
Goal "m+k<=n ==> k<=(n::nat)";
wenzelm@9436
   329
by (full_simp_tac (simpset() addsimps [add_commute]) 1);
wenzelm@9436
   330
by (etac add_leD1 1);
wenzelm@9436
   331
qed_spec_mp "add_leD2";
wenzelm@9436
   332
wenzelm@9436
   333
Goal "m+k<=n ==> m<=n & k<=(n::nat)";
wenzelm@9436
   334
by (blast_tac (claset() addDs [add_leD1, add_leD2]) 1);
wenzelm@9436
   335
bind_thm ("add_leE", result() RS conjE);
wenzelm@9436
   336
wenzelm@9436
   337
(*needs !!k for add_ac to work*)
wenzelm@9436
   338
Goal "!!k:: nat. [| k<l;  m+l = k+n |] ==> m<n";
wenzelm@9436
   339
by (force_tac (claset(),
wenzelm@9436
   340
              simpset() delsimps [add_Suc_right]
wenzelm@9436
   341
                        addsimps [less_iff_Suc_add,
wenzelm@9436
   342
                                  add_Suc_right RS sym] @ add_ac) 1);
wenzelm@9436
   343
qed "less_add_eq_less";
wenzelm@9436
   344
wenzelm@9436
   345
wenzelm@9436
   346
(*** Monotonicity of Addition ***)
wenzelm@9436
   347
wenzelm@9436
   348
(*strict, in 1st argument*)
wenzelm@9436
   349
Goal "i < j ==> i + k < j + (k::nat)";
wenzelm@9436
   350
by (induct_tac "k" 1);
wenzelm@9436
   351
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   352
qed "add_less_mono1";
wenzelm@9436
   353
wenzelm@9436
   354
(*strict, in both arguments*)
wenzelm@9436
   355
Goal "[|i < j; k < l|] ==> i + k < j + (l::nat)";
wenzelm@9436
   356
by (rtac (add_less_mono1 RS less_trans) 1);
wenzelm@9436
   357
by (REPEAT (assume_tac 1));
wenzelm@9436
   358
by (induct_tac "j" 1);
wenzelm@9436
   359
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   360
qed "add_less_mono";
wenzelm@9436
   361
wenzelm@9436
   362
(*A [clumsy] way of lifting < monotonicity to <= monotonicity *)
wenzelm@9436
   363
val [lt_mono,le] = Goal
wenzelm@9436
   364
     "[| !!i j::nat. i<j ==> f(i) < f(j);       \
wenzelm@9436
   365
\        i <= j                                 \
wenzelm@9436
   366
\     |] ==> f(i) <= (f(j)::nat)";
wenzelm@9436
   367
by (cut_facts_tac [le] 1);
wenzelm@9436
   368
by (asm_full_simp_tac (simpset() addsimps [order_le_less]) 1);
wenzelm@9436
   369
by (blast_tac (claset() addSIs [lt_mono]) 1);
wenzelm@9436
   370
qed "less_mono_imp_le_mono";
wenzelm@9436
   371
wenzelm@9436
   372
(*non-strict, in 1st argument*)
wenzelm@9436
   373
Goal "i<=j ==> i + k <= j + (k::nat)";
wenzelm@9436
   374
by (res_inst_tac [("f", "%j. j+k")] less_mono_imp_le_mono 1);
wenzelm@9436
   375
by (etac add_less_mono1 1);
wenzelm@9436
   376
by (assume_tac 1);
wenzelm@9436
   377
qed "add_le_mono1";
wenzelm@9436
   378
wenzelm@9436
   379
(*non-strict, in both arguments*)
wenzelm@9436
   380
Goal "[|i<=j;  k<=l |] ==> i + k <= j + (l::nat)";
wenzelm@9436
   381
by (etac (add_le_mono1 RS le_trans) 1);
wenzelm@9436
   382
by (simp_tac (simpset() addsimps [add_commute]) 1);
wenzelm@9436
   383
qed "add_le_mono";
wenzelm@9436
   384
wenzelm@9436
   385
wenzelm@9436
   386
(*** Multiplication ***)
wenzelm@9436
   387
wenzelm@9436
   388
(*right annihilation in product*)
wenzelm@9436
   389
Goal "!!m::nat. m * 0 = 0";
wenzelm@9436
   390
by (induct_tac "m" 1);
wenzelm@9436
   391
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   392
qed "mult_0_right";
wenzelm@9436
   393
wenzelm@9436
   394
(*right successor law for multiplication*)
wenzelm@9436
   395
Goal  "m * Suc(n) = m + (m * n)";
wenzelm@9436
   396
by (induct_tac "m" 1);
wenzelm@9436
   397
by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac)));
wenzelm@9436
   398
qed "mult_Suc_right";
wenzelm@9436
   399
wenzelm@9436
   400
Addsimps [mult_0_right, mult_Suc_right];
wenzelm@9436
   401
wenzelm@9436
   402
Goal "1 * n = n";
wenzelm@9436
   403
by (Asm_simp_tac 1);
wenzelm@9436
   404
qed "mult_1";
wenzelm@9436
   405
wenzelm@9436
   406
Goal "n * 1 = n";
wenzelm@9436
   407
by (Asm_simp_tac 1);
wenzelm@9436
   408
qed "mult_1_right";
wenzelm@9436
   409
wenzelm@9436
   410
(*Commutative law for multiplication*)
wenzelm@9436
   411
Goal "m * n = n * (m::nat)";
wenzelm@9436
   412
by (induct_tac "m" 1);
wenzelm@9436
   413
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   414
qed "mult_commute";
wenzelm@9436
   415
wenzelm@9436
   416
(*addition distributes over multiplication*)
wenzelm@9436
   417
Goal "(m + n)*k = (m*k) + ((n*k)::nat)";
wenzelm@9436
   418
by (induct_tac "m" 1);
wenzelm@9436
   419
by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac)));
wenzelm@9436
   420
qed "add_mult_distrib";
wenzelm@9436
   421
wenzelm@9436
   422
Goal "k*(m + n) = (k*m) + ((k*n)::nat)";
wenzelm@9436
   423
by (induct_tac "m" 1);
wenzelm@9436
   424
by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac)));
wenzelm@9436
   425
qed "add_mult_distrib2";
wenzelm@9436
   426
wenzelm@9436
   427
(*Associative law for multiplication*)
wenzelm@9436
   428
Goal "(m * n) * k = m * ((n * k)::nat)";
wenzelm@9436
   429
by (induct_tac "m" 1);
wenzelm@9436
   430
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_mult_distrib])));
wenzelm@9436
   431
qed "mult_assoc";
wenzelm@9436
   432
wenzelm@9436
   433
Goal "x*(y*z) = y*((x*z)::nat)";
wenzelm@9436
   434
by (rtac trans 1);
wenzelm@9436
   435
by (rtac mult_commute 1);
wenzelm@9436
   436
by (rtac trans 1);
wenzelm@9436
   437
by (rtac mult_assoc 1);
wenzelm@9436
   438
by (rtac (mult_commute RS arg_cong) 1);
wenzelm@9436
   439
qed "mult_left_commute";
wenzelm@9436
   440
wenzelm@9436
   441
bind_thms ("mult_ac", [mult_assoc,mult_commute,mult_left_commute]);
wenzelm@9436
   442
wenzelm@9436
   443
Goal "!!m::nat. (m*n = 0) = (m=0 | n=0)";
wenzelm@9436
   444
by (induct_tac "m" 1);
wenzelm@9436
   445
by (induct_tac "n" 2);
wenzelm@9436
   446
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   447
qed "mult_is_0";
wenzelm@9436
   448
wenzelm@9436
   449
Goal "!!m::nat. (0 = m*n) = (0=m | 0=n)";
wenzelm@9436
   450
by (stac eq_commute 1 THEN stac mult_is_0 1);
wenzelm@9436
   451
by Auto_tac;
wenzelm@9436
   452
qed "zero_is_mult";
wenzelm@9436
   453
wenzelm@9436
   454
Addsimps [mult_is_0, zero_is_mult];
wenzelm@9436
   455
wenzelm@9436
   456
wenzelm@9436
   457
(*** Difference ***)
wenzelm@9436
   458
wenzelm@9436
   459
Goal "!!m::nat. m - m = 0";
wenzelm@9436
   460
by (induct_tac "m" 1);
wenzelm@9436
   461
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   462
qed "diff_self_eq_0";
wenzelm@9436
   463
wenzelm@9436
   464
Addsimps [diff_self_eq_0];
wenzelm@9436
   465
wenzelm@9436
   466
(*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
wenzelm@9436
   467
Goal "~ m<n --> n+(m-n) = (m::nat)";
wenzelm@9436
   468
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
wenzelm@9436
   469
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   470
qed_spec_mp "add_diff_inverse";
wenzelm@9436
   471
wenzelm@9436
   472
Goal "n<=m ==> n+(m-n) = (m::nat)";
wenzelm@9436
   473
by (asm_simp_tac (simpset() addsimps [add_diff_inverse, not_less_iff_le]) 1);
wenzelm@9436
   474
qed "le_add_diff_inverse";
wenzelm@9436
   475
wenzelm@9436
   476
Goal "n<=m ==> (m-n)+n = (m::nat)";
wenzelm@9436
   477
by (asm_simp_tac (simpset() addsimps [le_add_diff_inverse, add_commute]) 1);
wenzelm@9436
   478
qed "le_add_diff_inverse2";
wenzelm@9436
   479
wenzelm@9436
   480
Addsimps  [le_add_diff_inverse, le_add_diff_inverse2];
wenzelm@9436
   481
wenzelm@9436
   482
wenzelm@9436
   483
(*** More results about difference ***)
wenzelm@9436
   484
wenzelm@9436
   485
Goal "n <= m ==> Suc(m)-n = Suc(m-n)";
wenzelm@9436
   486
by (etac rev_mp 1);
wenzelm@9436
   487
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
wenzelm@9436
   488
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   489
qed "Suc_diff_le";
wenzelm@9436
   490
wenzelm@9436
   491
Goal "m - n < Suc(m)";
wenzelm@9436
   492
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
wenzelm@9436
   493
by (etac less_SucE 3);
wenzelm@9436
   494
by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq])));
wenzelm@9436
   495
qed "diff_less_Suc";
wenzelm@9436
   496
wenzelm@9436
   497
Goal "m - n <= (m::nat)";
wenzelm@9436
   498
by (res_inst_tac [("m","m"), ("n","n")] diff_induct 1);
wenzelm@9436
   499
by (ALLGOALS (asm_simp_tac (simpset() addsimps [le_SucI])));
wenzelm@9436
   500
qed "diff_le_self";
wenzelm@9436
   501
Addsimps [diff_le_self];
wenzelm@9436
   502
wenzelm@9436
   503
(* j<k ==> j-n < k *)
wenzelm@9436
   504
bind_thm ("less_imp_diff_less", diff_le_self RS le_less_trans);
wenzelm@9436
   505
wenzelm@9436
   506
Goal "!!i::nat. i-j-k = i - (j+k)";
wenzelm@9436
   507
by (res_inst_tac [("m","i"),("n","j")] diff_induct 1);
wenzelm@9436
   508
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   509
qed "diff_diff_left";
wenzelm@9436
   510
wenzelm@9436
   511
Goal "(Suc m - n) - Suc k = m - n - k";
wenzelm@9436
   512
by (simp_tac (simpset() addsimps [diff_diff_left]) 1);
wenzelm@9436
   513
qed "Suc_diff_diff";
wenzelm@9436
   514
Addsimps [Suc_diff_diff];
wenzelm@9436
   515
wenzelm@9436
   516
Goal "0<n ==> n - Suc i < n";
wenzelm@9436
   517
by (case_tac "n" 1);
wenzelm@9436
   518
by Safe_tac;
wenzelm@9436
   519
by (asm_simp_tac (simpset() addsimps le_simps) 1);
wenzelm@9436
   520
qed "diff_Suc_less";
wenzelm@9436
   521
Addsimps [diff_Suc_less];
wenzelm@9436
   522
wenzelm@9436
   523
(*This and the next few suggested by Florian Kammueller*)
wenzelm@9436
   524
Goal "!!i::nat. i-j-k = i-k-j";
wenzelm@9436
   525
by (simp_tac (simpset() addsimps [diff_diff_left, add_commute]) 1);
wenzelm@9436
   526
qed "diff_commute";
wenzelm@9436
   527
wenzelm@9436
   528
Goal "k <= (j::nat) --> (i + j) - k = i + (j - k)";
wenzelm@9436
   529
by (res_inst_tac [("m","j"),("n","k")] diff_induct 1);
wenzelm@9436
   530
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   531
qed_spec_mp "diff_add_assoc";
wenzelm@9436
   532
wenzelm@9436
   533
Goal "k <= (j::nat) --> (j + i) - k = (j - k) + i";
wenzelm@9436
   534
by (asm_simp_tac (simpset() addsimps [add_commute, diff_add_assoc]) 1);
wenzelm@9436
   535
qed_spec_mp "diff_add_assoc2";
wenzelm@9436
   536
wenzelm@9436
   537
Goal "(n+m) - n = (m::nat)";
wenzelm@9436
   538
by (induct_tac "n" 1);
wenzelm@9436
   539
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   540
qed "diff_add_inverse";
wenzelm@9436
   541
wenzelm@9436
   542
Goal "(m+n) - n = (m::nat)";
wenzelm@9436
   543
by (simp_tac (simpset() addsimps [diff_add_assoc]) 1);
wenzelm@9436
   544
qed "diff_add_inverse2";
wenzelm@9436
   545
wenzelm@9436
   546
Goal "i <= (j::nat) ==> (j-i=k) = (j=k+i)";
wenzelm@9436
   547
by Safe_tac;
wenzelm@9436
   548
by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_add_inverse2])));
wenzelm@9436
   549
qed "le_imp_diff_is_add";
wenzelm@9436
   550
wenzelm@9436
   551
Goal "!!m::nat. (m-n = 0) = (m <= n)";
wenzelm@9436
   552
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
wenzelm@9436
   553
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   554
qed "diff_is_0_eq";
wenzelm@9436
   555
wenzelm@9436
   556
Goal "!!m::nat. (0 = m-n) = (m <= n)";
wenzelm@9436
   557
by (stac (diff_is_0_eq RS sym) 1);
wenzelm@9436
   558
by (rtac eq_sym_conv 1);
wenzelm@9436
   559
qed "zero_is_diff_eq";
wenzelm@9436
   560
Addsimps [diff_is_0_eq, zero_is_diff_eq];
wenzelm@9436
   561
wenzelm@9436
   562
Goal "!!m::nat. (0<n-m) = (m<n)";
wenzelm@9436
   563
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
wenzelm@9436
   564
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   565
qed "zero_less_diff";
wenzelm@9436
   566
Addsimps [zero_less_diff];
wenzelm@9436
   567
wenzelm@9436
   568
Goal "i < j  ==> EX k::nat. 0<k & i+k = j";
wenzelm@9436
   569
by (res_inst_tac [("x","j - i")] exI 1);
wenzelm@9436
   570
by (asm_simp_tac (simpset() addsimps [add_diff_inverse, less_not_sym]) 1);
wenzelm@9436
   571
qed "less_imp_add_positive";
wenzelm@9436
   572
wenzelm@9436
   573
Goal "P(k) --> (ALL n. P(Suc(n))--> P(n)) --> P(k-i)";
wenzelm@9436
   574
by (res_inst_tac [("m","k"),("n","i")] diff_induct 1);
wenzelm@9436
   575
by (ALLGOALS (Clarify_tac THEN' Simp_tac THEN' TRY o Blast_tac));
wenzelm@9436
   576
qed "zero_induct_lemma";
wenzelm@9436
   577
wenzelm@9436
   578
val prems = Goal "[| P(k);  !!n. P(Suc(n)) ==> P(n) |] ==> P(0)";
wenzelm@9436
   579
by (rtac (diff_self_eq_0 RS subst) 1);
wenzelm@9436
   580
by (rtac (zero_induct_lemma RS mp RS mp) 1);
wenzelm@9436
   581
by (REPEAT (ares_tac ([impI,allI]@prems) 1));
wenzelm@9436
   582
qed "zero_induct";
wenzelm@9436
   583
wenzelm@9436
   584
Goal "(k+m) - (k+n) = m - (n::nat)";
wenzelm@9436
   585
by (induct_tac "k" 1);
wenzelm@9436
   586
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   587
qed "diff_cancel";
wenzelm@9436
   588
wenzelm@9436
   589
Goal "(m+k) - (n+k) = m - (n::nat)";
wenzelm@9436
   590
by (asm_simp_tac
wenzelm@9436
   591
    (simpset() addsimps [diff_cancel, inst "n" "k" add_commute]) 1);
wenzelm@9436
   592
qed "diff_cancel2";
wenzelm@9436
   593
wenzelm@9436
   594
Goal "n - (n+m) = (0::nat)";
wenzelm@9436
   595
by (induct_tac "n" 1);
wenzelm@9436
   596
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   597
qed "diff_add_0";
wenzelm@9436
   598
wenzelm@9436
   599
wenzelm@9436
   600
(** Difference distributes over multiplication **)
wenzelm@9436
   601
wenzelm@9436
   602
Goal "!!m::nat. (m - n) * k = (m * k) - (n * k)";
wenzelm@9436
   603
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
wenzelm@9436
   604
by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_cancel])));
wenzelm@9436
   605
qed "diff_mult_distrib" ;
wenzelm@9436
   606
wenzelm@9436
   607
Goal "!!m::nat. k * (m - n) = (k * m) - (k * n)";
wenzelm@9436
   608
val mult_commute_k = read_instantiate [("m","k")] mult_commute;
wenzelm@9436
   609
by (simp_tac (simpset() addsimps [diff_mult_distrib, mult_commute_k]) 1);
wenzelm@9436
   610
qed "diff_mult_distrib2" ;
wenzelm@9436
   611
(*NOT added as rewrites, since sometimes they are used from right-to-left*)
wenzelm@9436
   612
wenzelm@9436
   613
wenzelm@9436
   614
(*** Monotonicity of Multiplication ***)
wenzelm@9436
   615
wenzelm@9436
   616
Goal "i <= (j::nat) ==> i*k<=j*k";
wenzelm@9436
   617
by (induct_tac "k" 1);
wenzelm@9436
   618
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_le_mono])));
wenzelm@9436
   619
qed "mult_le_mono1";
wenzelm@9436
   620
wenzelm@9436
   621
Goal "i <= (j::nat) ==> k*i <= k*j";
wenzelm@9436
   622
by (dtac mult_le_mono1 1);
wenzelm@9436
   623
by (asm_simp_tac (simpset() addsimps [mult_commute]) 1);
wenzelm@9436
   624
qed "mult_le_mono2";
wenzelm@9436
   625
wenzelm@9436
   626
(* <= monotonicity, BOTH arguments*)
wenzelm@9436
   627
Goal "[| i <= (j::nat); k <= l |] ==> i*k <= j*l";
wenzelm@9436
   628
by (etac (mult_le_mono1 RS le_trans) 1);
wenzelm@9436
   629
by (etac mult_le_mono2 1);
wenzelm@9436
   630
qed "mult_le_mono";
wenzelm@9436
   631
wenzelm@9436
   632
(*strict, in 1st argument; proof is by induction on k>0*)
wenzelm@9436
   633
Goal "!!i::nat. [| i<j; 0<k |] ==> k*i < k*j";
wenzelm@9436
   634
by (eres_inst_tac [("m1","0")] (less_eq_Suc_add RS exE) 1);
wenzelm@9436
   635
by (Asm_simp_tac 1);
wenzelm@9436
   636
by (induct_tac "x" 1);
wenzelm@9436
   637
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_less_mono])));
wenzelm@9436
   638
qed "mult_less_mono2";
wenzelm@9436
   639
wenzelm@9436
   640
Goal "!!i::nat. [| i<j; 0<k |] ==> i*k < j*k";
wenzelm@9436
   641
by (dtac mult_less_mono2 1);
wenzelm@9436
   642
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [mult_commute])));
wenzelm@9436
   643
qed "mult_less_mono1";
wenzelm@9436
   644
wenzelm@9436
   645
Goal "!!m::nat. (0 < m*n) = (0<m & 0<n)";
wenzelm@9436
   646
by (induct_tac "m" 1);
wenzelm@9436
   647
by (case_tac "n" 2);
wenzelm@9436
   648
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   649
qed "zero_less_mult_iff";
wenzelm@9436
   650
Addsimps [zero_less_mult_iff];
wenzelm@9436
   651
wenzelm@9436
   652
Goal "(1 <= m*n) = (1<=m & 1<=n)";
wenzelm@9436
   653
by (induct_tac "m" 1);
wenzelm@9436
   654
by (case_tac "n" 2);
wenzelm@9436
   655
by (ALLGOALS Asm_simp_tac);
wenzelm@9436
   656
qed "one_le_mult_iff";
wenzelm@9436
   657
Addsimps [one_le_mult_iff];
wenzelm@9436
   658
wenzelm@9436
   659
Goal "(m*n = 1) = (m=1 & n=1)";
wenzelm@9436
   660
by (induct_tac "m" 1);
wenzelm@9436
   661
by (Simp_tac 1);
wenzelm@9436
   662
by (induct_tac "n" 1);
wenzelm@9436
   663
by (Simp_tac 1);
wenzelm@9436
   664
by (fast_tac (claset() addss simpset()) 1);
wenzelm@9436
   665
qed "mult_eq_1_iff";
wenzelm@9436
   666
Addsimps [mult_eq_1_iff];
wenzelm@9436
   667
paulson@9637
   668
Goal "!!m::nat. (m*k < n*k) = (0<k & m<n)";
wenzelm@9436
   669
by (safe_tac (claset() addSIs [mult_less_mono1]));
paulson@9637
   670
by (case_tac "k" 1);
paulson@9637
   671
by Auto_tac;  
paulson@9637
   672
by (full_simp_tac (simpset() delsimps [le_0_eq]
paulson@9637
   673
			     addsimps [linorder_not_le RS sym]) 1);
paulson@9637
   674
by (blast_tac (claset() addIs [mult_le_mono1]) 1); 
wenzelm@9436
   675
qed "mult_less_cancel2";
wenzelm@9436
   676
paulson@9637
   677
Goal "!!m::nat. (k*m < k*n) = (0<k & m<n)";
paulson@9637
   678
by (simp_tac (simpset() addsimps [mult_less_cancel2, 
paulson@9637
   679
                                  inst "m" "k" mult_commute]) 1);
wenzelm@9436
   680
qed "mult_less_cancel1";
wenzelm@9436
   681
Addsimps [mult_less_cancel1, mult_less_cancel2];
wenzelm@9436
   682
paulson@9637
   683
Goal "!!m::nat. (m*k <= n*k) = (0<k --> m<=n)";
paulson@9637
   684
by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
paulson@9637
   685
by Auto_tac;  
wenzelm@9436
   686
qed "mult_le_cancel2";
wenzelm@9436
   687
paulson@9637
   688
Goal "!!m::nat. (k*m <= k*n) = (0<k --> m<=n)";
paulson@9637
   689
by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
paulson@9637
   690
by Auto_tac;  
wenzelm@9436
   691
qed "mult_le_cancel1";
wenzelm@9436
   692
Addsimps [mult_le_cancel1, mult_le_cancel2];
wenzelm@9436
   693
paulson@9637
   694
Goal "(m*k = n*k) = (m=n | (k = (0::nat)))";
wenzelm@9436
   695
by (cut_facts_tac [less_linear] 1);
wenzelm@9436
   696
by Safe_tac;
paulson@9637
   697
by Auto_tac; 	
wenzelm@9436
   698
by (ALLGOALS (dtac mult_less_mono1 THEN' assume_tac));
wenzelm@9436
   699
by (ALLGOALS Asm_full_simp_tac);
wenzelm@9436
   700
qed "mult_cancel2";
wenzelm@9436
   701
paulson@9637
   702
Goal "(k*m = k*n) = (m=n | (k = (0::nat)))";
paulson@9637
   703
by (simp_tac (simpset() addsimps [mult_cancel2, inst "m" "k" mult_commute]) 1);
wenzelm@9436
   704
qed "mult_cancel1";
wenzelm@9436
   705
Addsimps [mult_cancel1, mult_cancel2];
wenzelm@9436
   706
paulson@9637
   707
Goal "(Suc k * m < Suc k * n) = (m < n)";
paulson@9637
   708
by (stac mult_less_cancel1 1);
paulson@9637
   709
by (Simp_tac 1);
paulson@9637
   710
qed "Suc_mult_less_cancel1";
paulson@9637
   711
paulson@9637
   712
Goal "(Suc k * m <= Suc k * n) = (m <= n)";
paulson@9637
   713
by (stac mult_le_cancel1 1);
paulson@9637
   714
by (Simp_tac 1);
paulson@9637
   715
qed "Suc_mult_le_cancel1";
paulson@9637
   716
wenzelm@9436
   717
Goal "(Suc k * m = Suc k * n) = (m = n)";
paulson@9637
   718
by (stac mult_cancel1 1);
wenzelm@9436
   719
by (Simp_tac 1);
wenzelm@9436
   720
qed "Suc_mult_cancel1";
wenzelm@9436
   721
wenzelm@9436
   722
wenzelm@9436
   723
(*Lemma for gcd*)
wenzelm@9436
   724
Goal "!!m::nat. m = m*n ==> n=1 | m=0";
wenzelm@9436
   725
by (dtac sym 1);
wenzelm@9436
   726
by (rtac disjCI 1);
wenzelm@9436
   727
by (rtac nat_less_cases 1 THEN assume_tac 2);
wenzelm@9436
   728
by (fast_tac (claset() addSEs [less_SucE] addss simpset()) 1);
wenzelm@9436
   729
by (best_tac (claset() addDs [mult_less_mono2] addss simpset()) 1);
wenzelm@9436
   730
qed "mult_eq_self_implies_10";