src/ZF/Arith.ML
author paulson
Fri Jan 29 17:08:20 1999 +0100 (1999-01-29)
changeset 6163 be8234f37e48
parent 6153 bff90585cce5
child 7499 23e090051cb8
permissions -rw-r--r--
expandshort
paulson@1793
     1
(*  Title:      ZF/Arith.ML
clasohm@0
     2
    ID:         $Id$
clasohm@1461
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1992  University of Cambridge
clasohm@0
     5
paulson@1609
     6
Arithmetic operators and their definitions
clasohm@0
     7
clasohm@0
     8
Proofs about elementary arithmetic: addition, multiplication, etc.
clasohm@0
     9
*)
clasohm@0
    10
clasohm@0
    11
(*"Difference" is subtraction of natural numbers.
clasohm@0
    12
  There are no negative numbers; we have
clasohm@0
    13
     m #- n = 0  iff  m<=n   and     m #- n = succ(k) iff m>n.
clasohm@0
    14
  Also, rec(m, 0, %z w.z) is pred(m).   
clasohm@0
    15
*)
clasohm@0
    16
paulson@2469
    17
Addsimps [rec_type, nat_0_le, nat_le_refl];
lcp@25
    18
val nat_typechecks = [rec_type, nat_0I, nat_1I, nat_succI, Ord_nat];
clasohm@0
    19
paulson@5137
    20
Goal "[| 0<k; k: nat |] ==> EX j: nat. k = succ(j)";
paulson@1708
    21
by (etac rev_mp 1);
paulson@6070
    22
by (induct_tac "k" 1);
paulson@2469
    23
by (Simp_tac 1);
paulson@3016
    24
by (Blast_tac 1);
paulson@1708
    25
val lemma = result();
paulson@1708
    26
paulson@1708
    27
(* [| 0 < k; k: nat; !!j. [| j: nat; k = succ(j) |] ==> Q |] ==> Q *)
paulson@1708
    28
bind_thm ("zero_lt_natE", lemma RS bexE);
paulson@1708
    29
paulson@1708
    30
clasohm@0
    31
(** Addition **)
clasohm@0
    32
paulson@6070
    33
Goal "[| m:nat;  n:nat |] ==> m #+ n : nat";
paulson@6070
    34
by (induct_tac "m" 1);
paulson@6070
    35
by Auto_tac;
paulson@6070
    36
qed "add_type";
paulson@6070
    37
Addsimps [add_type];
paulson@6153
    38
AddTCs [add_type];
paulson@2469
    39
clasohm@0
    40
(** Multiplication **)
clasohm@0
    41
paulson@6070
    42
Goal "[| m:nat;  n:nat |] ==> m #* n : nat";
paulson@6070
    43
by (induct_tac "m" 1);
paulson@6070
    44
by Auto_tac;
paulson@6070
    45
qed "mult_type";
paulson@6070
    46
Addsimps [mult_type];
paulson@6153
    47
AddTCs [mult_type];
clasohm@0
    48
paulson@2469
    49
clasohm@0
    50
(** Difference **)
clasohm@0
    51
paulson@6070
    52
Goal "[| m:nat;  n:nat |] ==> m #- n : nat";
paulson@6070
    53
by (induct_tac "n" 1);
paulson@6070
    54
by Auto_tac;
paulson@6070
    55
by (fast_tac (claset() addIs [nat_case_type]) 1);
paulson@6070
    56
qed "diff_type";
paulson@6070
    57
Addsimps [diff_type];
paulson@6153
    58
AddTCs [diff_type];
clasohm@0
    59
paulson@6070
    60
Goal "n:nat ==> 0 #- n = 0";
paulson@6070
    61
by (induct_tac "n" 1);
paulson@6070
    62
by Auto_tac;
paulson@6070
    63
qed "diff_0_eq_0";
clasohm@0
    64
paulson@6070
    65
(*Must simplify BEFORE the induction: else we get a critical pair*)
paulson@6070
    66
Goal "[| m:nat;  n:nat |] ==> succ(m) #- succ(n) = m #- n";
paulson@6070
    67
by (Asm_simp_tac 1);
paulson@6070
    68
by (induct_tac "n" 1);
paulson@6070
    69
by Auto_tac;
paulson@6070
    70
qed "diff_succ_succ";
clasohm@0
    71
paulson@6070
    72
Addsimps [diff_0_eq_0, diff_succ_succ];
paulson@2469
    73
paulson@6070
    74
(*This defining property is no longer wanted*)
paulson@6070
    75
Delsimps [diff_SUCC];  
clasohm@0
    76
clasohm@0
    77
val prems = goal Arith.thy 
lcp@25
    78
    "[| m:nat;  n:nat |] ==> m #- n le m";
lcp@25
    79
by (rtac (prems MRS diff_induct) 1);
lcp@25
    80
by (etac leE 3);
clasohm@0
    81
by (ALLGOALS
paulson@5529
    82
    (asm_simp_tac (simpset() addsimps prems @ [le_iff, nat_into_Ord])));
clasohm@760
    83
qed "diff_le_self";
clasohm@0
    84
clasohm@0
    85
(*** Simplification over add, mult, diff ***)
clasohm@0
    86
clasohm@0
    87
val arith_typechecks = [add_type, mult_type, diff_type];
clasohm@0
    88
clasohm@0
    89
clasohm@0
    90
(*** Addition ***)
clasohm@0
    91
clasohm@0
    92
(*Associative law for addition*)
paulson@6070
    93
Goal "m:nat ==> (m #+ n) #+ k = m #+ (n #+ k)";
paulson@6070
    94
by (induct_tac "m" 1);
paulson@6070
    95
by Auto_tac;
paulson@6070
    96
qed "add_assoc";
clasohm@0
    97
clasohm@0
    98
(*The following two lemmas are used for add_commute and sometimes
clasohm@0
    99
  elsewhere, since they are safe for rewriting.*)
paulson@6070
   100
Goal "m:nat ==> m #+ 0 = m";
paulson@6070
   101
by (induct_tac "m" 1);
paulson@6070
   102
by Auto_tac;
paulson@6070
   103
qed "add_0_right";
clasohm@0
   104
paulson@6070
   105
Goal "m:nat ==> m #+ succ(n) = succ(m #+ n)";
paulson@6070
   106
by (induct_tac "m" 1);
paulson@6070
   107
by Auto_tac;
paulson@6070
   108
qed "add_succ_right";
paulson@2469
   109
paulson@2469
   110
Addsimps [add_0_right, add_succ_right];
clasohm@0
   111
clasohm@0
   112
(*Commutative law for addition*)  
paulson@6070
   113
Goal "[| m:nat;  n:nat |] ==> m #+ n = n #+ m";
paulson@6070
   114
by (induct_tac "n" 1);
paulson@6070
   115
by Auto_tac;
paulson@6070
   116
qed "add_commute";
lcp@435
   117
lcp@437
   118
(*for a/c rewriting*)
paulson@6070
   119
Goal "[| m:nat;  n:nat |] ==> m#+(n#+k)=n#+(m#+k)";
paulson@6070
   120
by (asm_simp_tac (simpset() addsimps [add_assoc RS sym, add_commute]) 1);
paulson@6070
   121
qed "add_left_commute";
lcp@435
   122
lcp@435
   123
(*Addition is an AC-operator*)
lcp@435
   124
val add_ac = [add_assoc, add_commute, add_left_commute];
clasohm@0
   125
clasohm@0
   126
(*Cancellation law on the left*)
paulson@6070
   127
Goal "[| k #+ m = k #+ n;  k:nat |] ==> m=n";
paulson@6070
   128
by (etac rev_mp 1);
paulson@6070
   129
by (induct_tac "k" 1);
paulson@6070
   130
by Auto_tac;
clasohm@760
   131
qed "add_left_cancel";
clasohm@0
   132
clasohm@0
   133
(*** Multiplication ***)
clasohm@0
   134
clasohm@0
   135
(*right annihilation in product*)
paulson@6070
   136
Goal "m:nat ==> m #* 0 = 0";
paulson@6070
   137
by (induct_tac "m" 1);
paulson@6070
   138
by Auto_tac;
paulson@6070
   139
qed "mult_0_right";
clasohm@0
   140
clasohm@0
   141
(*right successor law for multiplication*)
paulson@6070
   142
Goal "[| m:nat;  n:nat |] ==> m #* succ(n) = m #+ (m #* n)";
paulson@6070
   143
by (induct_tac "m" 1);
paulson@6070
   144
by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac)));
paulson@6070
   145
qed "mult_succ_right";
paulson@2469
   146
paulson@2469
   147
Addsimps [mult_0_right, mult_succ_right];
clasohm@0
   148
paulson@5137
   149
Goal "n:nat ==> 1 #* n = n";
paulson@2469
   150
by (Asm_simp_tac 1);
paulson@1793
   151
qed "mult_1";
paulson@1793
   152
paulson@5137
   153
Goal "n:nat ==> n #* 1 = n";
paulson@2469
   154
by (Asm_simp_tac 1);
paulson@1793
   155
qed "mult_1_right";
paulson@1793
   156
paulson@6070
   157
Addsimps [mult_1, mult_1_right];
paulson@6070
   158
clasohm@0
   159
(*Commutative law for multiplication*)
paulson@6070
   160
Goal "[| m:nat;  n:nat |] ==> m #* n = n #* m";
paulson@6070
   161
by (induct_tac "m" 1);
paulson@6070
   162
by Auto_tac;
paulson@6070
   163
qed "mult_commute";
clasohm@0
   164
clasohm@0
   165
(*addition distributes over multiplication*)
paulson@6070
   166
Goal "[| m:nat;  k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)";
paulson@6070
   167
by (induct_tac "m" 1);
paulson@6070
   168
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_assoc RS sym])));
paulson@6070
   169
qed "add_mult_distrib";
clasohm@0
   170
clasohm@0
   171
(*Distributive law on the left; requires an extra typing premise*)
paulson@6070
   172
Goal "[| m:nat;  n:nat;  k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)";
paulson@6070
   173
by (induct_tac "m" 1);
paulson@6070
   174
by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac)));
paulson@6070
   175
qed "add_mult_distrib_left";
clasohm@0
   176
clasohm@0
   177
(*Associative law for multiplication*)
paulson@6070
   178
Goal "[| m:nat;  n:nat;  k:nat |] ==> (m #* n) #* k = m #* (n #* k)";
paulson@6070
   179
by (induct_tac "m" 1);
paulson@6070
   180
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_mult_distrib])));
paulson@6070
   181
qed "mult_assoc";
clasohm@0
   182
lcp@437
   183
(*for a/c rewriting*)
paulson@6070
   184
Goal "[| m:nat;  n:nat;  k:nat |] ==> m #* (n #* k) = n #* (m #* k)";
paulson@6070
   185
by (rtac (mult_commute RS trans) 1);
paulson@6070
   186
by (rtac (mult_assoc RS trans) 3);
paulson@6070
   187
by (rtac (mult_commute RS subst_context) 6);
paulson@6070
   188
by (REPEAT (ares_tac [mult_type] 1));
paulson@6070
   189
qed "mult_left_commute";
lcp@437
   190
lcp@437
   191
val mult_ac = [mult_assoc,mult_commute,mult_left_commute];
lcp@437
   192
clasohm@0
   193
clasohm@0
   194
(*** Difference ***)
clasohm@0
   195
paulson@6070
   196
Goal "m:nat ==> m #- m = 0";
paulson@6070
   197
by (induct_tac "m" 1);
paulson@6070
   198
by Auto_tac;
paulson@6070
   199
qed "diff_self_eq_0";
clasohm@0
   200
lcp@25
   201
(*Addition is the inverse of subtraction*)
paulson@5137
   202
Goal "[| n le m;  m:nat |] ==> n #+ (m#-n) = m";
lcp@25
   203
by (forward_tac [lt_nat_in_nat] 1);
lcp@127
   204
by (etac nat_succI 1);
lcp@25
   205
by (etac rev_mp 1);
clasohm@0
   206
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
paulson@2469
   207
by (ALLGOALS Asm_simp_tac);
clasohm@760
   208
qed "add_diff_inverse";
clasohm@0
   209
paulson@5504
   210
Goal "[| n le m;  m:nat |] ==> (m#-n) #+ n = m";
paulson@5504
   211
by (forward_tac [lt_nat_in_nat] 1);
paulson@5504
   212
by (etac nat_succI 1);
paulson@5504
   213
by (asm_simp_tac (simpset() addsimps [add_commute, add_diff_inverse]) 1);
paulson@5504
   214
qed "add_diff_inverse2";
paulson@5504
   215
paulson@1609
   216
(*Proof is IDENTICAL to that above*)
paulson@5137
   217
Goal "[| n le m;  m:nat |] ==> succ(m) #- n = succ(m#-n)";
paulson@1609
   218
by (forward_tac [lt_nat_in_nat] 1);
paulson@1609
   219
by (etac nat_succI 1);
paulson@1609
   220
by (etac rev_mp 1);
paulson@1609
   221
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
paulson@2469
   222
by (ALLGOALS Asm_simp_tac);
paulson@1609
   223
qed "diff_succ";
paulson@1609
   224
paulson@5341
   225
Goal "[| m: nat; n: nat |] ==> 0 < n #- m  <->  m<n";
paulson@5341
   226
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
paulson@5341
   227
by (ALLGOALS Asm_simp_tac);
paulson@5341
   228
qed "zero_less_diff";
paulson@5341
   229
Addsimps [zero_less_diff];
paulson@5341
   230
paulson@5341
   231
paulson@1708
   232
(** Subtraction is the inverse of addition. **)
paulson@1708
   233
paulson@6070
   234
Goal "[| m:nat;  n:nat |] ==> (n#+m) #- n = m";
paulson@6070
   235
by (induct_tac "n" 1);
paulson@6070
   236
by Auto_tac;
clasohm@760
   237
qed "diff_add_inverse";
clasohm@0
   238
paulson@5137
   239
Goal "[| m:nat;  n:nat |] ==> (m#+n) #- n = m";
lcp@437
   240
by (res_inst_tac [("m1","m")] (add_commute RS ssubst) 1);
lcp@437
   241
by (REPEAT (ares_tac [diff_add_inverse] 1));
clasohm@760
   242
qed "diff_add_inverse2";
lcp@437
   243
paulson@5137
   244
Goal "[| k:nat; m: nat; n: nat |] ==> (k#+m) #- (k#+n) = m #- n";
paulson@6070
   245
by (induct_tac "k" 1);
paulson@2469
   246
by (ALLGOALS Asm_simp_tac);
paulson@1708
   247
qed "diff_cancel";
paulson@1708
   248
paulson@5137
   249
Goal "[| k:nat; m: nat; n: nat |] ==> (m#+k) #- (n#+k) = m #- n";
paulson@1708
   250
val add_commute_k = read_instantiate [("n","k")] add_commute;
wenzelm@4091
   251
by (asm_simp_tac (simpset() addsimps [add_commute_k, diff_cancel]) 1);
paulson@1708
   252
qed "diff_cancel2";
paulson@1708
   253
paulson@6070
   254
Goal "[| m:nat;  n:nat |] ==> n #- (n#+m) = 0";
paulson@6070
   255
by (induct_tac "n" 1);
paulson@6070
   256
by Auto_tac;
clasohm@760
   257
qed "diff_add_0";
clasohm@0
   258
paulson@1708
   259
(** Difference distributes over multiplication **)
paulson@1708
   260
paulson@5137
   261
Goal "[| m:nat; n: nat; k:nat |] ==> (m #- n) #* k = (m #* k) #- (n #* k)";
paulson@1708
   262
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
wenzelm@4091
   263
by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_cancel])));
paulson@1708
   264
qed "diff_mult_distrib" ;
paulson@1708
   265
paulson@5137
   266
Goal "[| m:nat; n: nat; k:nat |] ==> k #* (m #- n) = (k #* m) #- (k #* n)";
paulson@1708
   267
val mult_commute_k = read_instantiate [("m","k")] mult_commute;
wenzelm@4091
   268
by (asm_simp_tac (simpset() addsimps 
paulson@1793
   269
                  [mult_commute_k, diff_mult_distrib]) 1);
paulson@1708
   270
qed "diff_mult_distrib2" ;
paulson@1708
   271
clasohm@0
   272
(*** Remainder ***)
clasohm@0
   273
paulson@5137
   274
Goal "[| 0<n;  n le m;  m:nat |] ==> m #- n < m";
lcp@25
   275
by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1);
clasohm@0
   276
by (etac rev_mp 1);
clasohm@0
   277
by (etac rev_mp 1);
clasohm@0
   278
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
paulson@6070
   279
by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_le_self])));
clasohm@760
   280
qed "div_termination";
clasohm@0
   281
clasohm@1461
   282
val div_rls =   (*for mod and div*)
lcp@25
   283
    nat_typechecks @
lcp@25
   284
    [Ord_transrec_type, apply_type, div_termination RS ltD, if_type,
lcp@435
   285
     nat_into_Ord, not_lt_iff_le RS iffD1];
lcp@25
   286
paulson@6070
   287
val div_ss = simpset() addsimps [nat_into_Ord, div_termination RS ltD,
paulson@6070
   288
				 not_lt_iff_le RS iffD2];
clasohm@0
   289
clasohm@0
   290
(*Type checking depends upon termination!*)
paulson@5137
   291
Goalw [mod_def] "[| 0<n;  m:nat;  n:nat |] ==> m mod n : nat";
lcp@25
   292
by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1));
clasohm@760
   293
qed "mod_type";
paulson@6153
   294
AddTCs [mod_type];
clasohm@0
   295
paulson@5137
   296
Goal "[| 0<n;  m<n |] ==> m mod n = m";
clasohm@0
   297
by (rtac (mod_def RS def_transrec RS trans) 1);
lcp@25
   298
by (asm_simp_tac div_ss 1);
clasohm@760
   299
qed "mod_less";
clasohm@0
   300
paulson@5137
   301
Goal "[| 0<n;  n le m;  m:nat |] ==> m mod n = (m#-n) mod n";
lcp@25
   302
by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1);
clasohm@0
   303
by (rtac (mod_def RS def_transrec RS trans) 1);
lcp@25
   304
by (asm_simp_tac div_ss 1);
clasohm@760
   305
qed "mod_geq";
clasohm@0
   306
paulson@2469
   307
Addsimps [mod_type, mod_less, mod_geq];
paulson@2469
   308
clasohm@0
   309
(*** Quotient ***)
clasohm@0
   310
clasohm@0
   311
(*Type checking depends upon termination!*)
wenzelm@5067
   312
Goalw [div_def]
paulson@5147
   313
    "[| 0<n;  m:nat;  n:nat |] ==> m div n : nat";
lcp@25
   314
by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1));
clasohm@760
   315
qed "div_type";
paulson@6153
   316
AddTCs [div_type];
clasohm@0
   317
paulson@5137
   318
Goal "[| 0<n;  m<n |] ==> m div n = 0";
clasohm@0
   319
by (rtac (div_def RS def_transrec RS trans) 1);
lcp@25
   320
by (asm_simp_tac div_ss 1);
clasohm@760
   321
qed "div_less";
clasohm@0
   322
paulson@5137
   323
Goal "[| 0<n;  n le m;  m:nat |] ==> m div n = succ((m#-n) div n)";
lcp@25
   324
by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1);
clasohm@0
   325
by (rtac (div_def RS def_transrec RS trans) 1);
lcp@25
   326
by (asm_simp_tac div_ss 1);
clasohm@760
   327
qed "div_geq";
clasohm@0
   328
paulson@2469
   329
Addsimps [div_type, div_less, div_geq];
paulson@2469
   330
paulson@1609
   331
(*A key result*)
paulson@5137
   332
Goal "[| 0<n;  m:nat;  n:nat |] ==> (m div n)#*n #+ m mod n = m";
lcp@25
   333
by (etac complete_induct 1);
lcp@437
   334
by (excluded_middle_tac "x<n" 1);
lcp@25
   335
(*case x<n*)
paulson@2469
   336
by (Asm_simp_tac 2);
lcp@25
   337
(*case n le x*)
lcp@25
   338
by (asm_full_simp_tac
wenzelm@4091
   339
     (simpset() addsimps [not_lt_iff_le, nat_into_Ord, add_assoc,
clasohm@1461
   340
                         div_termination RS ltD, add_diff_inverse]) 1);
clasohm@760
   341
qed "mod_div_equality";
clasohm@0
   342
paulson@6068
   343
paulson@6068
   344
(*** Further facts about mod (mainly for mutilated chess board) ***)
paulson@1609
   345
paulson@6068
   346
Goal "[| 0<n;  m:nat;  n:nat |] \
paulson@6068
   347
\     ==> succ(m) mod n = (if succ(m mod n) = n then 0 else succ(m mod n))";
paulson@1609
   348
by (etac complete_induct 1);
paulson@1609
   349
by (excluded_middle_tac "succ(x)<n" 1);
paulson@1623
   350
(* case succ(x) < n *)
wenzelm@4091
   351
by (asm_simp_tac (simpset() addsimps [mod_less, nat_le_refl RS lt_trans,
paulson@1623
   352
                                     succ_neq_self]) 2);
wenzelm@4091
   353
by (asm_simp_tac (simpset() addsimps [ltD RS mem_imp_not_eq]) 2);
paulson@1623
   354
(* case n le succ(x) *)
paulson@1609
   355
by (asm_full_simp_tac
wenzelm@4091
   356
     (simpset() addsimps [not_lt_iff_le, nat_into_Ord, mod_geq]) 1);
paulson@1623
   357
by (etac leE 1);
wenzelm@4091
   358
by (asm_simp_tac (simpset() addsimps [div_termination RS ltD, diff_succ, 
paulson@1623
   359
                                     mod_geq]) 1);
wenzelm@4091
   360
by (asm_simp_tac (simpset() addsimps [mod_less, diff_self_eq_0]) 1);
paulson@1609
   361
qed "mod_succ";
paulson@1609
   362
paulson@5137
   363
Goal "[| 0<n;  m:nat;  n:nat |] ==> m mod n < n";
paulson@1609
   364
by (etac complete_induct 1);
paulson@1609
   365
by (excluded_middle_tac "x<n" 1);
paulson@1609
   366
(*case x<n*)
wenzelm@4091
   367
by (asm_simp_tac (simpset() addsimps [mod_less]) 2);
paulson@1609
   368
(*case n le x*)
paulson@1609
   369
by (asm_full_simp_tac
wenzelm@4091
   370
     (simpset() addsimps [not_lt_iff_le, nat_into_Ord,
paulson@1609
   371
                         mod_geq, div_termination RS ltD]) 1);
paulson@1609
   372
qed "mod_less_divisor";
paulson@1609
   373
paulson@1609
   374
paulson@6068
   375
Goal "[| k: nat; b<2 |] ==> k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)";
paulson@1609
   376
by (subgoal_tac "k mod 2: 2" 1);
wenzelm@4091
   377
by (asm_simp_tac (simpset() addsimps [mod_less_divisor RS ltD]) 2);
paulson@1623
   378
by (dtac ltD 1);
paulson@5137
   379
by Auto_tac;
paulson@1609
   380
qed "mod2_cases";
paulson@1609
   381
paulson@5137
   382
Goal "m:nat ==> succ(succ(m)) mod 2 = m mod 2";
paulson@1609
   383
by (subgoal_tac "m mod 2: 2" 1);
wenzelm@4091
   384
by (asm_simp_tac (simpset() addsimps [mod_less_divisor RS ltD]) 2);
wenzelm@4091
   385
by (asm_simp_tac (simpset() addsimps [mod_succ] setloop Step_tac) 1);
paulson@1609
   386
qed "mod2_succ_succ";
paulson@1609
   387
paulson@5137
   388
Goal "m:nat ==> (m#+m) mod 2 = 0";
paulson@6070
   389
by (induct_tac "m" 1);
wenzelm@4091
   390
by (simp_tac (simpset() addsimps [mod_less]) 1);
wenzelm@4091
   391
by (asm_simp_tac (simpset() addsimps [mod2_succ_succ, add_succ_right]) 1);
paulson@1609
   392
qed "mod2_add_self";
paulson@1609
   393
clasohm@0
   394
lcp@25
   395
(**** Additional theorems about "le" ****)
clasohm@0
   396
paulson@5137
   397
Goal "[| m:nat;  n:nat |] ==> m le m #+ n";
paulson@6070
   398
by (induct_tac "m" 1);
paulson@2469
   399
by (ALLGOALS Asm_simp_tac);
clasohm@760
   400
qed "add_le_self";
lcp@14
   401
paulson@5137
   402
Goal "[| m:nat;  n:nat |] ==> m le n #+ m";
paulson@2033
   403
by (stac add_commute 1);
lcp@25
   404
by (REPEAT (ares_tac [add_le_self] 1));
clasohm@760
   405
qed "add_le_self2";
lcp@14
   406
paulson@1708
   407
(*** Monotonicity of Addition ***)
lcp@14
   408
paulson@1708
   409
(*strict, in 1st argument; proof is by rule induction on 'less than'*)
paulson@5137
   410
Goal "[| i<j; j:nat; k:nat |] ==> i#+k < j#+k";
lcp@25
   411
by (forward_tac [lt_nat_in_nat] 1);
lcp@127
   412
by (assume_tac 1);
lcp@25
   413
by (etac succ_lt_induct 1);
wenzelm@4091
   414
by (ALLGOALS (asm_simp_tac (simpset() addsimps [leI])));
clasohm@760
   415
qed "add_lt_mono1";
lcp@14
   416
lcp@14
   417
(*strict, in both arguments*)
paulson@5137
   418
Goal "[| i<j; k<l; j:nat; l:nat |] ==> i#+k < j#+l";
lcp@25
   419
by (rtac (add_lt_mono1 RS lt_trans) 1);
lcp@25
   420
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1));
paulson@2033
   421
by (EVERY [stac add_commute 1,
paulson@2033
   422
           stac add_commute 3,
clasohm@1461
   423
           rtac add_lt_mono1 5]);
lcp@25
   424
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1));
clasohm@760
   425
qed "add_lt_mono";
lcp@14
   426
lcp@25
   427
(*A [clumsy] way of lifting < monotonicity to le monotonicity *)
paulson@5325
   428
val lt_mono::ford::prems = Goal
clasohm@1461
   429
     "[| !!i j. [| i<j; j:k |] ==> f(i) < f(j); \
clasohm@1461
   430
\        !!i. i:k ==> Ord(f(i));                \
clasohm@1461
   431
\        i le j;  j:k                           \
lcp@25
   432
\     |] ==> f(i) le f(j)";
lcp@14
   433
by (cut_facts_tac prems 1);
paulson@3016
   434
by (blast_tac (le_cs addSIs [lt_mono,ford] addSEs [leE]) 1);
clasohm@760
   435
qed "Ord_lt_mono_imp_le_mono";
lcp@14
   436
lcp@25
   437
(*le monotonicity, 1st argument*)
paulson@5137
   438
Goal "[| i le j; j:nat; k:nat |] ==> i#+k le j#+k";
wenzelm@3840
   439
by (res_inst_tac [("f", "%j. j#+k")] Ord_lt_mono_imp_le_mono 1);
lcp@435
   440
by (REPEAT (ares_tac [add_lt_mono1, add_type RS nat_into_Ord] 1));
clasohm@760
   441
qed "add_le_mono1";
lcp@14
   442
lcp@25
   443
(* le monotonicity, BOTH arguments*)
paulson@5137
   444
Goal "[| i le j; k le l; j:nat; l:nat |] ==> i#+k le j#+l";
lcp@25
   445
by (rtac (add_le_mono1 RS le_trans) 1);
lcp@25
   446
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
paulson@2033
   447
by (EVERY [stac add_commute 1,
paulson@2033
   448
           stac add_commute 3,
clasohm@1461
   449
           rtac add_le_mono1 5]);
lcp@25
   450
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
clasohm@760
   451
qed "add_le_mono";
paulson@1609
   452
paulson@1708
   453
(*** Monotonicity of Multiplication ***)
paulson@1708
   454
paulson@5137
   455
Goal "[| i le j; j:nat; k:nat |] ==> i#*k le j#*k";
paulson@1708
   456
by (forward_tac [lt_nat_in_nat] 1);
paulson@6070
   457
by (induct_tac "k" 2);
wenzelm@4091
   458
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_le_mono])));
paulson@1708
   459
qed "mult_le_mono1";
paulson@1708
   460
paulson@1708
   461
(* le monotonicity, BOTH arguments*)
paulson@5137
   462
Goal "[| i le j; k le l; j:nat; l:nat |] ==> i#*k le j#*l";
paulson@1708
   463
by (rtac (mult_le_mono1 RS le_trans) 1);
paulson@1708
   464
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
paulson@2033
   465
by (EVERY [stac mult_commute 1,
paulson@2033
   466
           stac mult_commute 3,
paulson@1708
   467
           rtac mult_le_mono1 5]);
paulson@1708
   468
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
paulson@1708
   469
qed "mult_le_mono";
paulson@1708
   470
paulson@1708
   471
(*strict, in 1st argument; proof is by induction on k>0*)
paulson@5137
   472
Goal "[| i<j; 0<k; j:nat; k:nat |] ==> k#*i < k#*j";
paulson@1793
   473
by (etac zero_lt_natE 1);
paulson@1708
   474
by (forward_tac [lt_nat_in_nat] 2);
paulson@2469
   475
by (ALLGOALS Asm_simp_tac);
paulson@6070
   476
by (induct_tac "x" 1);
wenzelm@4091
   477
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_lt_mono])));
paulson@1708
   478
qed "mult_lt_mono2";
paulson@1708
   479
paulson@5137
   480
Goal "[| i<j; 0<c; i:nat; j:nat; c:nat |] ==> i#*c < j#*c";
paulson@4839
   481
by (asm_simp_tac (simpset() addsimps [mult_lt_mono2, mult_commute]) 1);
paulson@4839
   482
qed "mult_lt_mono1";
paulson@4839
   483
paulson@5137
   484
Goal "[| m: nat; n: nat |] ==> 0 < m#*n <-> 0<m & 0<n";
wenzelm@4091
   485
by (best_tac (claset() addEs [natE] addss (simpset())) 1);
paulson@1708
   486
qed "zero_lt_mult_iff";
paulson@1708
   487
paulson@5137
   488
Goal "[| m: nat; n: nat |] ==> m#*n = 1 <-> m=1 & n=1";
wenzelm@4091
   489
by (best_tac (claset() addEs [natE] addss (simpset())) 1);
paulson@1793
   490
qed "mult_eq_1_iff";
paulson@1793
   491
paulson@1708
   492
(*Cancellation law for division*)
paulson@5137
   493
Goal "[| 0<n; 0<k; k:nat; m:nat; n:nat |] ==> (k#*m) div (k#*n) = m div n";
paulson@1708
   494
by (eres_inst_tac [("i","m")] complete_induct 1);
paulson@1708
   495
by (excluded_middle_tac "x<n" 1);
wenzelm@4091
   496
by (asm_simp_tac (simpset() addsimps [div_less, zero_lt_mult_iff, 
paulson@1793
   497
                                     mult_lt_mono2]) 2);
paulson@1708
   498
by (asm_full_simp_tac
wenzelm@4091
   499
     (simpset() addsimps [not_lt_iff_le, nat_into_Ord,
paulson@1708
   500
                         zero_lt_mult_iff, le_refl RS mult_le_mono, div_geq,
paulson@1708
   501
                         diff_mult_distrib2 RS sym,
paulson@1793
   502
                         div_termination RS ltD]) 1);
paulson@1708
   503
qed "div_cancel";
paulson@1708
   504
paulson@5137
   505
Goal "[| 0<n; 0<k; k:nat; m:nat; n:nat |] ==> \
paulson@1708
   506
\        (k#*m) mod (k#*n) = k #* (m mod n)";
paulson@1708
   507
by (eres_inst_tac [("i","m")] complete_induct 1);
paulson@1708
   508
by (excluded_middle_tac "x<n" 1);
wenzelm@4091
   509
by (asm_simp_tac (simpset() addsimps [mod_less, zero_lt_mult_iff, 
paulson@1793
   510
                                     mult_lt_mono2]) 2);
paulson@1708
   511
by (asm_full_simp_tac
wenzelm@4091
   512
     (simpset() addsimps [not_lt_iff_le, nat_into_Ord,
paulson@1708
   513
                         zero_lt_mult_iff, le_refl RS mult_le_mono, mod_geq,
paulson@1708
   514
                         diff_mult_distrib2 RS sym,
paulson@1793
   515
                         div_termination RS ltD]) 1);
paulson@1708
   516
qed "mult_mod_distrib";
paulson@1708
   517
paulson@6070
   518
(*Lemma for gcd*)
paulson@5137
   519
Goal "[| m = m#*n; m: nat; n: nat |] ==> n=1 | m=0";
paulson@1793
   520
by (rtac disjCI 1);
paulson@1793
   521
by (dtac sym 1);
paulson@1793
   522
by (rtac Ord_linear_lt 1 THEN REPEAT_SOME (ares_tac [nat_into_Ord,nat_1I]));
paulson@6070
   523
by (dtac (nat_into_Ord RS Ord_0_lt RSN (2,mult_lt_mono2)) 2);
paulson@6070
   524
by Auto_tac;
paulson@1793
   525
qed "mult_eq_self_implies_10";
paulson@1708
   526
paulson@2469
   527
(*Thanks to Sten Agerholm*)
paulson@5504
   528
Goal "[|m#+n le m#+k; m:nat; n:nat; k:nat|] ==> n le k";
paulson@2493
   529
by (etac rev_mp 1);
paulson@6070
   530
by (induct_tac "m" 1);
paulson@2469
   531
by (Asm_simp_tac 1);
paulson@3736
   532
by Safe_tac;
wenzelm@4091
   533
by (asm_full_simp_tac (simpset() addsimps [not_le_iff_lt,nat_into_Ord]) 1);
paulson@2469
   534
qed "add_le_elim1";
paulson@2469
   535
paulson@5504
   536
Goal "[| m<n; n: nat |] ==> EX k: nat. n = succ(m#+k)";
paulson@5504
   537
by (forward_tac [lt_nat_in_nat] 1 THEN assume_tac 1);
paulson@6163
   538
by (etac rev_mp 1);
paulson@6070
   539
by (induct_tac "n" 1);
paulson@5504
   540
by (ALLGOALS (simp_tac (simpset() addsimps [le_iff])));
paulson@5504
   541
by (blast_tac (claset() addSEs [leE] 
paulson@5504
   542
                        addSIs [add_0_right RS sym, add_succ_right RS sym]) 1);
paulson@5504
   543
qed_spec_mp "less_imp_Suc_add";