src/ZF/Arith.ML
author lcp
Thu Nov 18 14:57:05 1993 +0100 (1993-11-18)
changeset 127 eec6bb9c58ea
parent 25 3ac1c0c0016e
child 435 ca5356bd315a
permissions -rw-r--r--
Misc modifs such as expandshort
clasohm@0
     1
(*  Title: 	ZF/arith.ML
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1992  University of Cambridge
clasohm@0
     5
clasohm@0
     6
For arith.thy.  Arithmetic operators and their definitions
clasohm@0
     7
clasohm@0
     8
Proofs about elementary arithmetic: addition, multiplication, etc.
clasohm@0
     9
clasohm@0
    10
Could prove def_rec_0, def_rec_succ...
clasohm@0
    11
*)
clasohm@0
    12
clasohm@0
    13
open Arith;
clasohm@0
    14
clasohm@0
    15
(*"Difference" is subtraction of natural numbers.
clasohm@0
    16
  There are no negative numbers; we have
clasohm@0
    17
     m #- n = 0  iff  m<=n   and     m #- n = succ(k) iff m>n.
clasohm@0
    18
  Also, rec(m, 0, %z w.z) is pred(m).   
clasohm@0
    19
*)
clasohm@0
    20
clasohm@0
    21
(** rec -- better than nat_rec; the succ case has no type requirement! **)
clasohm@0
    22
clasohm@0
    23
val rec_trans = rec_def RS def_transrec RS trans;
clasohm@0
    24
clasohm@0
    25
goal Arith.thy "rec(0,a,b) = a";
clasohm@0
    26
by (rtac rec_trans 1);
clasohm@0
    27
by (rtac nat_case_0 1);
clasohm@0
    28
val rec_0 = result();
clasohm@0
    29
clasohm@0
    30
goal Arith.thy "rec(succ(m),a,b) = b(m, rec(m,a,b))";
clasohm@0
    31
by (rtac rec_trans 1);
lcp@14
    32
by (simp_tac (ZF_ss addsimps [nat_case_succ, nat_succI]) 1);
clasohm@0
    33
val rec_succ = result();
clasohm@0
    34
clasohm@0
    35
val major::prems = goal Arith.thy
clasohm@0
    36
    "[| n: nat;  \
clasohm@0
    37
\       a: C(0);  \
clasohm@0
    38
\       !!m z. [| m: nat;  z: C(m) |] ==> b(m,z): C(succ(m))  \
clasohm@0
    39
\    |] ==> rec(n,a,b) : C(n)";
clasohm@0
    40
by (rtac (major RS nat_induct) 1);
clasohm@0
    41
by (ALLGOALS
lcp@6
    42
    (asm_simp_tac (ZF_ss addsimps (prems@[rec_0,rec_succ]))));
clasohm@0
    43
val rec_type = result();
clasohm@0
    44
lcp@25
    45
val nat_le_refl = naturals_are_ordinals RS le_refl;
lcp@25
    46
lcp@25
    47
val nat_typechecks = [rec_type, nat_0I, nat_1I, nat_succI, Ord_nat];
clasohm@0
    48
lcp@25
    49
val nat_simps = [rec_0, rec_succ, not_lt0, nat_0_le, le0_iff, succ_le_iff,
lcp@25
    50
		 nat_le_refl];
lcp@25
    51
lcp@25
    52
val nat_ss = ZF_ss addsimps (nat_simps @ nat_typechecks);
clasohm@0
    53
clasohm@0
    54
clasohm@0
    55
(** Addition **)
clasohm@0
    56
clasohm@0
    57
val add_type = prove_goalw Arith.thy [add_def]
clasohm@0
    58
    "[| m:nat;  n:nat |] ==> m #+ n : nat"
clasohm@0
    59
 (fn prems=> [ (typechk_tac (prems@nat_typechecks@ZF_typechecks)) ]);
clasohm@0
    60
clasohm@0
    61
val add_0 = prove_goalw Arith.thy [add_def]
clasohm@0
    62
    "0 #+ n = n"
clasohm@0
    63
 (fn _ => [ (rtac rec_0 1) ]);
clasohm@0
    64
clasohm@0
    65
val add_succ = prove_goalw Arith.thy [add_def]
clasohm@0
    66
    "succ(m) #+ n = succ(m #+ n)"
clasohm@0
    67
 (fn _=> [ (rtac rec_succ 1) ]); 
clasohm@0
    68
clasohm@0
    69
(** Multiplication **)
clasohm@0
    70
clasohm@0
    71
val mult_type = prove_goalw Arith.thy [mult_def]
clasohm@0
    72
    "[| m:nat;  n:nat |] ==> m #* n : nat"
clasohm@0
    73
 (fn prems=>
clasohm@0
    74
  [ (typechk_tac (prems@[add_type]@nat_typechecks@ZF_typechecks)) ]);
clasohm@0
    75
clasohm@0
    76
val mult_0 = prove_goalw Arith.thy [mult_def]
clasohm@0
    77
    "0 #* n = 0"
clasohm@0
    78
 (fn _ => [ (rtac rec_0 1) ]);
clasohm@0
    79
clasohm@0
    80
val mult_succ = prove_goalw Arith.thy [mult_def]
clasohm@0
    81
    "succ(m) #* n = n #+ (m #* n)"
clasohm@0
    82
 (fn _ => [ (rtac rec_succ 1) ]); 
clasohm@0
    83
clasohm@0
    84
(** Difference **)
clasohm@0
    85
clasohm@0
    86
val diff_type = prove_goalw Arith.thy [diff_def]
clasohm@0
    87
    "[| m:nat;  n:nat |] ==> m #- n : nat"
clasohm@0
    88
 (fn prems=> [ (typechk_tac (prems@nat_typechecks@ZF_typechecks)) ]);
clasohm@0
    89
clasohm@0
    90
val diff_0 = prove_goalw Arith.thy [diff_def]
clasohm@0
    91
    "m #- 0 = m"
clasohm@0
    92
 (fn _ => [ (rtac rec_0 1) ]);
clasohm@0
    93
clasohm@0
    94
val diff_0_eq_0 = prove_goalw Arith.thy [diff_def]
clasohm@0
    95
    "n:nat ==> 0 #- n = 0"
clasohm@0
    96
 (fn [prem]=>
clasohm@0
    97
  [ (rtac (prem RS nat_induct) 1),
lcp@6
    98
    (ALLGOALS (asm_simp_tac nat_ss)) ]);
clasohm@0
    99
clasohm@0
   100
(*Must simplify BEFORE the induction!!  (Else we get a critical pair)
clasohm@0
   101
  succ(m) #- succ(n)   rewrites to   pred(succ(m) #- n)  *)
clasohm@0
   102
val diff_succ_succ = prove_goalw Arith.thy [diff_def]
clasohm@0
   103
    "[| m:nat;  n:nat |] ==> succ(m) #- succ(n) = m #- n"
clasohm@0
   104
 (fn prems=>
lcp@6
   105
  [ (asm_simp_tac (nat_ss addsimps prems) 1),
clasohm@0
   106
    (nat_ind_tac "n" prems 1),
lcp@6
   107
    (ALLGOALS (asm_simp_tac (nat_ss addsimps prems))) ]);
clasohm@0
   108
clasohm@0
   109
val prems = goal Arith.thy 
lcp@25
   110
    "[| m:nat;  n:nat |] ==> m #- n le m";
lcp@25
   111
by (rtac (prems MRS diff_induct) 1);
lcp@25
   112
by (etac leE 3);
clasohm@0
   113
by (ALLGOALS
lcp@6
   114
    (asm_simp_tac
lcp@25
   115
     (nat_ss addsimps (prems @ [le_iff, diff_0, diff_0_eq_0, 
lcp@25
   116
				diff_succ_succ, naturals_are_ordinals]))));
lcp@25
   117
val diff_le_self = result();
clasohm@0
   118
clasohm@0
   119
(*** Simplification over add, mult, diff ***)
clasohm@0
   120
clasohm@0
   121
val arith_typechecks = [add_type, mult_type, diff_type];
lcp@25
   122
val arith_simps = [add_0, add_succ,
lcp@25
   123
		   mult_0, mult_succ,
lcp@25
   124
		   diff_0, diff_0_eq_0, diff_succ_succ];
clasohm@0
   125
lcp@25
   126
val arith_ss = nat_ss addsimps (arith_simps@arith_typechecks);
clasohm@0
   127
clasohm@0
   128
(*** Addition ***)
clasohm@0
   129
clasohm@0
   130
(*Associative law for addition*)
clasohm@0
   131
val add_assoc = prove_goal Arith.thy 
clasohm@0
   132
    "m:nat ==> (m #+ n) #+ k = m #+ (n #+ k)"
clasohm@0
   133
 (fn prems=>
clasohm@0
   134
  [ (nat_ind_tac "m" prems 1),
lcp@6
   135
    (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
clasohm@0
   136
clasohm@0
   137
(*The following two lemmas are used for add_commute and sometimes
clasohm@0
   138
  elsewhere, since they are safe for rewriting.*)
clasohm@0
   139
val add_0_right = prove_goal Arith.thy
clasohm@0
   140
    "m:nat ==> m #+ 0 = m"
clasohm@0
   141
 (fn prems=>
clasohm@0
   142
  [ (nat_ind_tac "m" prems 1),
lcp@6
   143
    (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); 
clasohm@0
   144
clasohm@0
   145
val add_succ_right = prove_goal Arith.thy
clasohm@0
   146
    "m:nat ==> m #+ succ(n) = succ(m #+ n)"
clasohm@0
   147
 (fn prems=>
clasohm@0
   148
  [ (nat_ind_tac "m" prems 1),
lcp@6
   149
    (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); 
clasohm@0
   150
clasohm@0
   151
(*Commutative law for addition*)  
clasohm@0
   152
val add_commute = prove_goal Arith.thy 
clasohm@0
   153
    "[| m:nat;  n:nat |] ==> m #+ n = n #+ m"
clasohm@0
   154
 (fn prems=>
clasohm@0
   155
  [ (nat_ind_tac "n" prems 1),
clasohm@0
   156
    (ALLGOALS
lcp@6
   157
     (asm_simp_tac
lcp@6
   158
      (arith_ss addsimps (prems@[add_0_right, add_succ_right])))) ]);
clasohm@0
   159
clasohm@0
   160
(*Cancellation law on the left*)
clasohm@0
   161
val [knat,eqn] = goal Arith.thy 
clasohm@0
   162
    "[| k:nat;  k #+ m = k #+ n |] ==> m=n";
clasohm@0
   163
by (rtac (eqn RS rev_mp) 1);
clasohm@0
   164
by (nat_ind_tac "k" [knat] 1);
lcp@6
   165
by (ALLGOALS (simp_tac arith_ss));
clasohm@0
   166
by (fast_tac ZF_cs 1);
clasohm@0
   167
val add_left_cancel = result();
clasohm@0
   168
clasohm@0
   169
(*** Multiplication ***)
clasohm@0
   170
clasohm@0
   171
(*right annihilation in product*)
clasohm@0
   172
val mult_0_right = prove_goal Arith.thy 
clasohm@0
   173
    "m:nat ==> m #* 0 = 0"
clasohm@0
   174
 (fn prems=>
clasohm@0
   175
  [ (nat_ind_tac "m" prems 1),
lcp@6
   176
    (ALLGOALS (asm_simp_tac (arith_ss addsimps prems)))  ]);
clasohm@0
   177
clasohm@0
   178
(*right successor law for multiplication*)
clasohm@0
   179
val mult_succ_right = prove_goal Arith.thy 
lcp@6
   180
    "!!m n. [| m:nat;  n:nat |] ==> m #* succ(n) = m #+ (m #* n)"
lcp@6
   181
 (fn _=>
lcp@6
   182
  [ (nat_ind_tac "m" [] 1),
lcp@6
   183
    (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]))),
clasohm@0
   184
       (*The final goal requires the commutative law for addition*)
lcp@6
   185
    (rtac (add_commute RS subst_context) 1),
lcp@6
   186
    (REPEAT (assume_tac 1))  ]);
clasohm@0
   187
clasohm@0
   188
(*Commutative law for multiplication*)
clasohm@0
   189
val mult_commute = prove_goal Arith.thy 
clasohm@0
   190
    "[| m:nat;  n:nat |] ==> m #* n = n #* m"
clasohm@0
   191
 (fn prems=>
clasohm@0
   192
  [ (nat_ind_tac "m" prems 1),
lcp@6
   193
    (ALLGOALS (asm_simp_tac
lcp@6
   194
	     (arith_ss addsimps (prems@[mult_0_right, mult_succ_right])))) ]);
clasohm@0
   195
clasohm@0
   196
(*addition distributes over multiplication*)
clasohm@0
   197
val add_mult_distrib = prove_goal Arith.thy 
lcp@14
   198
    "!!m n. [| m:nat;  k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)"
lcp@14
   199
 (fn _=>
lcp@14
   200
  [ (etac nat_induct 1),
lcp@14
   201
    (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]))) ]);
clasohm@0
   202
clasohm@0
   203
(*Distributive law on the left; requires an extra typing premise*)
clasohm@0
   204
val add_mult_distrib_left = prove_goal Arith.thy 
clasohm@0
   205
    "[| m:nat;  n:nat;  k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)"
clasohm@0
   206
 (fn prems=>
clasohm@0
   207
      let val mult_commute' = read_instantiate [("m","k")] mult_commute
lcp@6
   208
          val ss = arith_ss addsimps ([mult_commute',add_mult_distrib]@prems)
lcp@6
   209
      in [ (simp_tac ss 1) ]
clasohm@0
   210
      end);
clasohm@0
   211
clasohm@0
   212
(*Associative law for multiplication*)
clasohm@0
   213
val mult_assoc = prove_goal Arith.thy 
lcp@14
   214
    "!!m n k. [| m:nat;  n:nat;  k:nat |] ==> (m #* n) #* k = m #* (n #* k)"
lcp@14
   215
 (fn _=>
lcp@14
   216
  [ (etac nat_induct 1),
lcp@14
   217
    (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_mult_distrib]))) ]);
clasohm@0
   218
clasohm@0
   219
clasohm@0
   220
(*** Difference ***)
clasohm@0
   221
clasohm@0
   222
val diff_self_eq_0 = prove_goal Arith.thy 
clasohm@0
   223
    "m:nat ==> m #- m = 0"
clasohm@0
   224
 (fn prems=>
clasohm@0
   225
  [ (nat_ind_tac "m" prems 1),
lcp@6
   226
    (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
clasohm@0
   227
lcp@25
   228
(*Addition is the inverse of subtraction*)
lcp@25
   229
goal Arith.thy "!!m n. [| n le m;  m:nat |] ==> n #+ (m#-n) = m";
lcp@25
   230
by (forward_tac [lt_nat_in_nat] 1);
lcp@127
   231
by (etac nat_succI 1);
lcp@25
   232
by (etac rev_mp 1);
clasohm@0
   233
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
lcp@25
   234
by (ALLGOALS (asm_simp_tac arith_ss));
clasohm@0
   235
val add_diff_inverse = result();
clasohm@0
   236
clasohm@0
   237
(*Subtraction is the inverse of addition. *)
clasohm@0
   238
val [mnat,nnat] = goal Arith.thy
clasohm@0
   239
    "[| m:nat;  n:nat |] ==> (n#+m) #-n = m";
clasohm@0
   240
by (rtac (nnat RS nat_induct) 1);
lcp@6
   241
by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat])));
clasohm@0
   242
val diff_add_inverse = result();
clasohm@0
   243
clasohm@0
   244
val [mnat,nnat] = goal Arith.thy
clasohm@0
   245
    "[| m:nat;  n:nat |] ==> n #- (n#+m) = 0";
clasohm@0
   246
by (rtac (nnat RS nat_induct) 1);
lcp@6
   247
by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat])));
clasohm@0
   248
val diff_add_0 = result();
clasohm@0
   249
clasohm@0
   250
clasohm@0
   251
(*** Remainder ***)
clasohm@0
   252
lcp@25
   253
goal Arith.thy "!!m n. [| 0<n;  n le m;  m:nat |] ==> m #- n < m";
lcp@25
   254
by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1);
clasohm@0
   255
by (etac rev_mp 1);
clasohm@0
   256
by (etac rev_mp 1);
clasohm@0
   257
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
lcp@25
   258
by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_le_self,diff_succ_succ])));
clasohm@0
   259
val div_termination = result();
clasohm@0
   260
lcp@25
   261
val div_rls =	(*for mod and div*)
lcp@25
   262
    nat_typechecks @
lcp@25
   263
    [Ord_transrec_type, apply_type, div_termination RS ltD, if_type,
lcp@25
   264
     naturals_are_ordinals, not_lt_iff_le RS iffD1];
lcp@25
   265
lcp@25
   266
val div_ss = ZF_ss addsimps [naturals_are_ordinals, div_termination RS ltD,
lcp@25
   267
			     not_lt_iff_le RS iffD2];
clasohm@0
   268
clasohm@0
   269
(*Type checking depends upon termination!*)
lcp@25
   270
goalw Arith.thy [mod_def] "!!m n. [| 0<n;  m:nat;  n:nat |] ==> m mod n : nat";
lcp@25
   271
by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1));
clasohm@0
   272
val mod_type = result();
clasohm@0
   273
lcp@25
   274
goal Arith.thy "!!m n. [| 0<n;  m<n |] ==> m mod n = m";
clasohm@0
   275
by (rtac (mod_def RS def_transrec RS trans) 1);
lcp@25
   276
by (asm_simp_tac div_ss 1);
clasohm@0
   277
val mod_less = result();
clasohm@0
   278
lcp@25
   279
goal Arith.thy "!!m n. [| 0<n;  n le m;  m:nat |] ==> m mod n = (m#-n) mod n";
lcp@25
   280
by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1);
clasohm@0
   281
by (rtac (mod_def RS def_transrec RS trans) 1);
lcp@25
   282
by (asm_simp_tac div_ss 1);
clasohm@0
   283
val mod_geq = result();
clasohm@0
   284
clasohm@0
   285
(*** Quotient ***)
clasohm@0
   286
clasohm@0
   287
(*Type checking depends upon termination!*)
lcp@25
   288
goalw Arith.thy [div_def]
lcp@25
   289
    "!!m n. [| 0<n;  m:nat;  n:nat |] ==> m div n : nat";
lcp@25
   290
by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1));
clasohm@0
   291
val div_type = result();
clasohm@0
   292
lcp@25
   293
goal Arith.thy "!!m n. [| 0<n;  m<n |] ==> m div n = 0";
clasohm@0
   294
by (rtac (div_def RS def_transrec RS trans) 1);
lcp@25
   295
by (asm_simp_tac div_ss 1);
clasohm@0
   296
val div_less = result();
clasohm@0
   297
lcp@25
   298
goal Arith.thy
lcp@25
   299
 "!!m n. [| 0<n;  n le m;  m:nat |] ==> m div n = succ((m#-n) div n)";
lcp@25
   300
by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1);
clasohm@0
   301
by (rtac (div_def RS def_transrec RS trans) 1);
lcp@25
   302
by (asm_simp_tac div_ss 1);
clasohm@0
   303
val div_geq = result();
clasohm@0
   304
clasohm@0
   305
(*Main Result.*)
lcp@25
   306
goal Arith.thy
lcp@25
   307
    "!!m n. [| 0<n;  m:nat;  n:nat |] ==> (m div n)#*n #+ m mod n = m";
lcp@25
   308
by (etac complete_induct 1);
lcp@25
   309
by (res_inst_tac [("Q","x<n")] (excluded_middle RS disjE) 1);
lcp@25
   310
(*case x<n*)
lcp@25
   311
by (asm_simp_tac (arith_ss addsimps [mod_less, div_less]) 2);
lcp@25
   312
(*case n le x*)
lcp@25
   313
by (asm_full_simp_tac
lcp@25
   314
     (arith_ss addsimps [not_lt_iff_le, naturals_are_ordinals,
lcp@25
   315
			 mod_geq, div_geq, add_assoc,
lcp@25
   316
			 div_termination RS ltD, add_diff_inverse]) 1);
clasohm@0
   317
val mod_div_equality = result();
clasohm@0
   318
clasohm@0
   319
lcp@25
   320
(**** Additional theorems about "le" ****)
clasohm@0
   321
lcp@25
   322
goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m le m #+ n";
lcp@25
   323
by (etac nat_induct 1);
lcp@25
   324
by (ALLGOALS (asm_simp_tac arith_ss));
lcp@25
   325
val add_le_self = result();
lcp@14
   326
lcp@25
   327
goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m le n #+ m";
lcp@14
   328
by (rtac (add_commute RS ssubst) 1);
lcp@25
   329
by (REPEAT (ares_tac [add_le_self] 1));
lcp@25
   330
val add_le_self2 = result();
lcp@14
   331
lcp@14
   332
(** Monotonicity of addition **)
lcp@14
   333
lcp@14
   334
(*strict, in 1st argument*)
lcp@25
   335
goal Arith.thy "!!i j k. [| i<j; j:nat; k:nat |] ==> i#+k < j#+k";
lcp@25
   336
by (forward_tac [lt_nat_in_nat] 1);
lcp@127
   337
by (assume_tac 1);
lcp@25
   338
by (etac succ_lt_induct 1);
lcp@25
   339
by (ALLGOALS (asm_simp_tac (arith_ss addsimps [leI])));
lcp@25
   340
val add_lt_mono1 = result();
lcp@14
   341
lcp@14
   342
(*strict, in both arguments*)
lcp@25
   343
goal Arith.thy "!!i j k l. [| i<j; k<l; j:nat; l:nat |] ==> i#+k < j#+l";
lcp@25
   344
by (rtac (add_lt_mono1 RS lt_trans) 1);
lcp@25
   345
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1));
lcp@14
   346
by (EVERY [rtac (add_commute RS ssubst) 1,
lcp@14
   347
	   rtac (add_commute RS ssubst) 3,
lcp@25
   348
	   rtac add_lt_mono1 5]);
lcp@25
   349
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1));
lcp@25
   350
val add_lt_mono = result();
lcp@14
   351
lcp@25
   352
(*A [clumsy] way of lifting < monotonicity to le monotonicity *)
lcp@25
   353
val lt_mono::ford::prems = goal Ord.thy
lcp@25
   354
     "[| !!i j. [| i<j; j:k |] ==> f(i) < f(j);	\
lcp@25
   355
\        !!i. i:k ==> Ord(f(i));		\
lcp@25
   356
\        i le j;  j:k				\
lcp@25
   357
\     |] ==> f(i) le f(j)";
lcp@14
   358
by (cut_facts_tac prems 1);
lcp@25
   359
by (fast_tac (lt_cs addSIs [lt_mono,ford] addSEs [leE]) 1);
lcp@25
   360
val Ord_lt_mono_imp_le_mono = result();
lcp@14
   361
lcp@25
   362
(*le monotonicity, 1st argument*)
lcp@14
   363
goal Arith.thy
lcp@25
   364
    "!!i j k. [| i le j; j:nat; k:nat |] ==> i#+k le j#+k";
lcp@25
   365
by (res_inst_tac [("f", "%j.j#+k")] Ord_lt_mono_imp_le_mono 1);
lcp@25
   366
by (REPEAT (ares_tac [add_lt_mono1, add_type RS naturals_are_ordinals] 1));
lcp@25
   367
val add_le_mono1 = result();
lcp@14
   368
lcp@25
   369
(* le monotonicity, BOTH arguments*)
lcp@14
   370
goal Arith.thy
lcp@25
   371
    "!!i j k. [| i le j; k le l; j:nat; l:nat |] ==> i#+k le j#+l";
lcp@25
   372
by (rtac (add_le_mono1 RS le_trans) 1);
lcp@25
   373
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
lcp@14
   374
by (EVERY [rtac (add_commute RS ssubst) 1,
lcp@14
   375
	   rtac (add_commute RS ssubst) 3,
lcp@25
   376
	   rtac add_le_mono1 5]);
lcp@25
   377
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
lcp@25
   378
val add_le_mono = result();