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