src/ZF/Arith.ML
author lcp
Fri Sep 17 16:16:38 1993 +0200 (1993-09-17)
changeset 6 8ce8c4d13d4d
parent 0 a5a9c433f639
child 14 1c0926788772
permissions -rw-r--r--
Installation of new simplifier for ZF. Deleted all congruence rules not
involving local assumptions. NB the congruence rules for Sigma and Pi
(dependent type constructions) cause difficulties and are not used by
default.
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
val rec_ss = ZF_ss 
lcp@6
    32
      addsimps [nat_case_succ, nat_succI];
clasohm@0
    33
by (rtac rec_trans 1);
lcp@6
    34
by (simp_tac rec_ss 1);
clasohm@0
    35
val rec_succ = result();
clasohm@0
    36
clasohm@0
    37
val major::prems = goal Arith.thy
clasohm@0
    38
    "[| n: nat;  \
clasohm@0
    39
\       a: C(0);  \
clasohm@0
    40
\       !!m z. [| m: nat;  z: C(m) |] ==> b(m,z): C(succ(m))  \
clasohm@0
    41
\    |] ==> rec(n,a,b) : C(n)";
clasohm@0
    42
by (rtac (major RS nat_induct) 1);
clasohm@0
    43
by (ALLGOALS
lcp@6
    44
    (asm_simp_tac (ZF_ss addsimps (prems@[rec_0,rec_succ]))));
clasohm@0
    45
val rec_type = result();
clasohm@0
    46
clasohm@0
    47
val nat_typechecks = [rec_type,nat_0I,nat_1I,nat_succI,Ord_nat];
clasohm@0
    48
lcp@6
    49
val nat_ss = ZF_ss addsimps ([rec_0,rec_succ] @ nat_typechecks);
clasohm@0
    50
clasohm@0
    51
clasohm@0
    52
(** Addition **)
clasohm@0
    53
clasohm@0
    54
val add_type = prove_goalw Arith.thy [add_def]
clasohm@0
    55
    "[| m:nat;  n:nat |] ==> m #+ n : nat"
clasohm@0
    56
 (fn prems=> [ (typechk_tac (prems@nat_typechecks@ZF_typechecks)) ]);
clasohm@0
    57
clasohm@0
    58
val add_0 = prove_goalw Arith.thy [add_def]
clasohm@0
    59
    "0 #+ n = n"
clasohm@0
    60
 (fn _ => [ (rtac rec_0 1) ]);
clasohm@0
    61
clasohm@0
    62
val add_succ = prove_goalw Arith.thy [add_def]
clasohm@0
    63
    "succ(m) #+ n = succ(m #+ n)"
clasohm@0
    64
 (fn _=> [ (rtac rec_succ 1) ]); 
clasohm@0
    65
clasohm@0
    66
(** Multiplication **)
clasohm@0
    67
clasohm@0
    68
val mult_type = prove_goalw Arith.thy [mult_def]
clasohm@0
    69
    "[| m:nat;  n:nat |] ==> m #* n : nat"
clasohm@0
    70
 (fn prems=>
clasohm@0
    71
  [ (typechk_tac (prems@[add_type]@nat_typechecks@ZF_typechecks)) ]);
clasohm@0
    72
clasohm@0
    73
val mult_0 = prove_goalw Arith.thy [mult_def]
clasohm@0
    74
    "0 #* n = 0"
clasohm@0
    75
 (fn _ => [ (rtac rec_0 1) ]);
clasohm@0
    76
clasohm@0
    77
val mult_succ = prove_goalw Arith.thy [mult_def]
clasohm@0
    78
    "succ(m) #* n = n #+ (m #* n)"
clasohm@0
    79
 (fn _ => [ (rtac rec_succ 1) ]); 
clasohm@0
    80
clasohm@0
    81
(** Difference **)
clasohm@0
    82
clasohm@0
    83
val diff_type = prove_goalw Arith.thy [diff_def]
clasohm@0
    84
    "[| m:nat;  n:nat |] ==> m #- n : nat"
clasohm@0
    85
 (fn prems=> [ (typechk_tac (prems@nat_typechecks@ZF_typechecks)) ]);
clasohm@0
    86
clasohm@0
    87
val diff_0 = prove_goalw Arith.thy [diff_def]
clasohm@0
    88
    "m #- 0 = m"
clasohm@0
    89
 (fn _ => [ (rtac rec_0 1) ]);
clasohm@0
    90
clasohm@0
    91
val diff_0_eq_0 = prove_goalw Arith.thy [diff_def]
clasohm@0
    92
    "n:nat ==> 0 #- n = 0"
clasohm@0
    93
 (fn [prem]=>
clasohm@0
    94
  [ (rtac (prem RS nat_induct) 1),
lcp@6
    95
    (ALLGOALS (asm_simp_tac nat_ss)) ]);
clasohm@0
    96
clasohm@0
    97
(*Must simplify BEFORE the induction!!  (Else we get a critical pair)
clasohm@0
    98
  succ(m) #- succ(n)   rewrites to   pred(succ(m) #- n)  *)
clasohm@0
    99
val diff_succ_succ = prove_goalw Arith.thy [diff_def]
clasohm@0
   100
    "[| m:nat;  n:nat |] ==> succ(m) #- succ(n) = m #- n"
clasohm@0
   101
 (fn prems=>
lcp@6
   102
  [ (asm_simp_tac (nat_ss addsimps prems) 1),
clasohm@0
   103
    (nat_ind_tac "n" prems 1),
lcp@6
   104
    (ALLGOALS (asm_simp_tac (nat_ss addsimps prems))) ]);
clasohm@0
   105
clasohm@0
   106
val prems = goal Arith.thy 
clasohm@0
   107
    "[| m:nat;  n:nat |] ==> m #- n : succ(m)";
clasohm@0
   108
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
clasohm@0
   109
by (resolve_tac prems 1);
clasohm@0
   110
by (resolve_tac prems 1);
clasohm@0
   111
by (etac succE 3);
clasohm@0
   112
by (ALLGOALS
lcp@6
   113
    (asm_simp_tac
lcp@6
   114
     (nat_ss addsimps (prems@[diff_0,diff_0_eq_0,diff_succ_succ]))));
clasohm@0
   115
val diff_leq = result();
clasohm@0
   116
clasohm@0
   117
(*** Simplification over add, mult, diff ***)
clasohm@0
   118
clasohm@0
   119
val arith_typechecks = [add_type, mult_type, diff_type];
clasohm@0
   120
val arith_rews = [add_0, add_succ,
clasohm@0
   121
		  mult_0, mult_succ,
clasohm@0
   122
		  diff_0, diff_0_eq_0, diff_succ_succ];
clasohm@0
   123
lcp@6
   124
val arith_ss = nat_ss addsimps (arith_rews@arith_typechecks);
clasohm@0
   125
clasohm@0
   126
(*** Addition ***)
clasohm@0
   127
clasohm@0
   128
(*Associative law for addition*)
clasohm@0
   129
val add_assoc = prove_goal Arith.thy 
clasohm@0
   130
    "m:nat ==> (m #+ n) #+ k = m #+ (n #+ k)"
clasohm@0
   131
 (fn prems=>
clasohm@0
   132
  [ (nat_ind_tac "m" prems 1),
lcp@6
   133
    (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
clasohm@0
   134
clasohm@0
   135
(*The following two lemmas are used for add_commute and sometimes
clasohm@0
   136
  elsewhere, since they are safe for rewriting.*)
clasohm@0
   137
val add_0_right = prove_goal Arith.thy
clasohm@0
   138
    "m:nat ==> m #+ 0 = m"
clasohm@0
   139
 (fn prems=>
clasohm@0
   140
  [ (nat_ind_tac "m" prems 1),
lcp@6
   141
    (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); 
clasohm@0
   142
clasohm@0
   143
val add_succ_right = prove_goal Arith.thy
clasohm@0
   144
    "m:nat ==> m #+ succ(n) = succ(m #+ n)"
clasohm@0
   145
 (fn prems=>
clasohm@0
   146
  [ (nat_ind_tac "m" prems 1),
lcp@6
   147
    (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); 
clasohm@0
   148
clasohm@0
   149
(*Commutative law for addition*)  
clasohm@0
   150
val add_commute = prove_goal Arith.thy 
clasohm@0
   151
    "[| m:nat;  n:nat |] ==> m #+ n = n #+ m"
clasohm@0
   152
 (fn prems=>
clasohm@0
   153
  [ (nat_ind_tac "n" prems 1),
clasohm@0
   154
    (ALLGOALS
lcp@6
   155
     (asm_simp_tac
lcp@6
   156
      (arith_ss addsimps (prems@[add_0_right, add_succ_right])))) ]);
clasohm@0
   157
clasohm@0
   158
(*Cancellation law on the left*)
clasohm@0
   159
val [knat,eqn] = goal Arith.thy 
clasohm@0
   160
    "[| k:nat;  k #+ m = k #+ n |] ==> m=n";
clasohm@0
   161
by (rtac (eqn RS rev_mp) 1);
clasohm@0
   162
by (nat_ind_tac "k" [knat] 1);
lcp@6
   163
by (ALLGOALS (simp_tac arith_ss));
clasohm@0
   164
by (fast_tac ZF_cs 1);
clasohm@0
   165
val add_left_cancel = result();
clasohm@0
   166
clasohm@0
   167
(*** Multiplication ***)
clasohm@0
   168
clasohm@0
   169
(*right annihilation in product*)
clasohm@0
   170
val mult_0_right = prove_goal Arith.thy 
clasohm@0
   171
    "m:nat ==> m #* 0 = 0"
clasohm@0
   172
 (fn prems=>
clasohm@0
   173
  [ (nat_ind_tac "m" prems 1),
lcp@6
   174
    (ALLGOALS (asm_simp_tac (arith_ss addsimps prems)))  ]);
clasohm@0
   175
clasohm@0
   176
(*right successor law for multiplication*)
clasohm@0
   177
val mult_succ_right = prove_goal Arith.thy 
lcp@6
   178
    "!!m n. [| m:nat;  n:nat |] ==> m #* succ(n) = m #+ (m #* n)"
lcp@6
   179
 (fn _=>
lcp@6
   180
  [ (nat_ind_tac "m" [] 1),
lcp@6
   181
    (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]))),
clasohm@0
   182
       (*The final goal requires the commutative law for addition*)
lcp@6
   183
    (rtac (add_commute RS subst_context) 1),
lcp@6
   184
    (REPEAT (assume_tac 1))  ]);
clasohm@0
   185
clasohm@0
   186
(*Commutative law for multiplication*)
clasohm@0
   187
val mult_commute = prove_goal Arith.thy 
clasohm@0
   188
    "[| m:nat;  n:nat |] ==> m #* n = n #* m"
clasohm@0
   189
 (fn prems=>
clasohm@0
   190
  [ (nat_ind_tac "m" prems 1),
lcp@6
   191
    (ALLGOALS (asm_simp_tac
lcp@6
   192
	     (arith_ss addsimps (prems@[mult_0_right, mult_succ_right])))) ]);
clasohm@0
   193
clasohm@0
   194
(*addition distributes over multiplication*)
clasohm@0
   195
val add_mult_distrib = prove_goal Arith.thy 
clasohm@0
   196
    "[| m:nat;  k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)"
clasohm@0
   197
 (fn prems=>
clasohm@0
   198
  [ (nat_ind_tac "m" prems 1),
lcp@6
   199
    (ALLGOALS (asm_simp_tac (arith_ss addsimps ([add_assoc RS sym]@prems)))) ]);
clasohm@0
   200
clasohm@0
   201
(*Distributive law on the left; requires an extra typing premise*)
clasohm@0
   202
val add_mult_distrib_left = prove_goal Arith.thy 
clasohm@0
   203
    "[| m:nat;  n:nat;  k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)"
clasohm@0
   204
 (fn prems=>
clasohm@0
   205
      let val mult_commute' = read_instantiate [("m","k")] mult_commute
lcp@6
   206
          val ss = arith_ss addsimps ([mult_commute',add_mult_distrib]@prems)
lcp@6
   207
      in [ (simp_tac ss 1) ]
clasohm@0
   208
      end);
clasohm@0
   209
clasohm@0
   210
(*Associative law for multiplication*)
clasohm@0
   211
val mult_assoc = prove_goal Arith.thy 
clasohm@0
   212
    "[| m:nat;  n:nat;  k:nat |] ==> (m #* n) #* k = m #* (n #* k)"
clasohm@0
   213
 (fn prems=>
clasohm@0
   214
  [ (nat_ind_tac "m" prems 1),
lcp@6
   215
    (ALLGOALS (asm_simp_tac (arith_ss addsimps (prems@[add_mult_distrib])))) ]);
clasohm@0
   216
clasohm@0
   217
clasohm@0
   218
(*** Difference ***)
clasohm@0
   219
clasohm@0
   220
val diff_self_eq_0 = prove_goal Arith.thy 
clasohm@0
   221
    "m:nat ==> m #- m = 0"
clasohm@0
   222
 (fn prems=>
clasohm@0
   223
  [ (nat_ind_tac "m" prems 1),
lcp@6
   224
    (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
clasohm@0
   225
clasohm@0
   226
(*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
clasohm@0
   227
val notless::prems = goal Arith.thy
clasohm@0
   228
    "[| ~m:n;  m:nat;  n:nat |] ==> n #+ (m#-n) = m";
clasohm@0
   229
by (rtac (notless RS rev_mp) 1);
clasohm@0
   230
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
clasohm@0
   231
by (resolve_tac prems 1);
clasohm@0
   232
by (resolve_tac prems 1);
lcp@6
   233
by (ALLGOALS (asm_simp_tac
lcp@6
   234
	      (arith_ss addsimps (prems@[succ_mem_succ_iff, Ord_0_mem_succ, 
clasohm@0
   235
				  naturals_are_ordinals]))));
clasohm@0
   236
val add_diff_inverse = result();
clasohm@0
   237
clasohm@0
   238
clasohm@0
   239
(*Subtraction is the inverse of addition. *)
clasohm@0
   240
val [mnat,nnat] = goal Arith.thy
clasohm@0
   241
    "[| m:nat;  n:nat |] ==> (n#+m) #-n = m";
clasohm@0
   242
by (rtac (nnat RS nat_induct) 1);
lcp@6
   243
by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat])));
clasohm@0
   244
val diff_add_inverse = result();
clasohm@0
   245
clasohm@0
   246
val [mnat,nnat] = goal Arith.thy
clasohm@0
   247
    "[| m:nat;  n:nat |] ==> n #- (n#+m) = 0";
clasohm@0
   248
by (rtac (nnat RS nat_induct) 1);
lcp@6
   249
by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat])));
clasohm@0
   250
val diff_add_0 = result();
clasohm@0
   251
clasohm@0
   252
clasohm@0
   253
(*** Remainder ***)
clasohm@0
   254
clasohm@0
   255
(*In ordinary notation: if 0<n and n<=m then m-n < m *)
lcp@6
   256
goal Arith.thy "!!m n. [| 0:n; ~ m:n;  m:nat;  n:nat |] ==> m #- n : m";
clasohm@0
   257
by (etac rev_mp 1);
clasohm@0
   258
by (etac rev_mp 1);
clasohm@0
   259
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
lcp@6
   260
by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_leq,diff_succ_succ])));
clasohm@0
   261
val div_termination = result();
clasohm@0
   262
clasohm@0
   263
val div_rls =
clasohm@0
   264
    [Ord_transrec_type, apply_type, div_termination, if_type] @ 
clasohm@0
   265
    nat_typechecks;
clasohm@0
   266
clasohm@0
   267
(*Type checking depends upon termination!*)
clasohm@0
   268
val prems = goalw Arith.thy [mod_def]
clasohm@0
   269
    "[| 0:n;  m:nat;  n:nat |] ==> m mod n : nat";
clasohm@0
   270
by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1));
clasohm@0
   271
val mod_type = result();
clasohm@0
   272
lcp@6
   273
val div_ss = ZF_ss addsimps [naturals_are_ordinals,div_termination];
clasohm@0
   274
clasohm@0
   275
val prems = goal Arith.thy "[| 0:n;  m:n;  m:nat;  n:nat |] ==> m mod n = m";
clasohm@0
   276
by (rtac (mod_def RS def_transrec RS trans) 1);
lcp@6
   277
by (simp_tac (div_ss addsimps prems) 1);
clasohm@0
   278
val mod_less = result();
clasohm@0
   279
clasohm@0
   280
val prems = goal Arith.thy
clasohm@0
   281
    "[| 0:n;  ~m:n;  m:nat;  n:nat |] ==> m mod n = (m#-n) mod n";
clasohm@0
   282
by (rtac (mod_def RS def_transrec RS trans) 1);
lcp@6
   283
by (simp_tac (div_ss addsimps prems) 1);
clasohm@0
   284
val mod_geq = result();
clasohm@0
   285
clasohm@0
   286
(*** Quotient ***)
clasohm@0
   287
clasohm@0
   288
(*Type checking depends upon termination!*)
clasohm@0
   289
val prems = goalw Arith.thy [div_def]
clasohm@0
   290
    "[| 0:n;  m:nat;  n:nat |] ==> m div n : nat";
clasohm@0
   291
by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1));
clasohm@0
   292
val div_type = result();
clasohm@0
   293
clasohm@0
   294
val prems = goal Arith.thy
clasohm@0
   295
    "[| 0:n;  m:n;  m:nat;  n:nat |] ==> m div n = 0";
clasohm@0
   296
by (rtac (div_def RS def_transrec RS trans) 1);
lcp@6
   297
by (simp_tac (div_ss addsimps prems) 1);
clasohm@0
   298
val div_less = result();
clasohm@0
   299
clasohm@0
   300
val prems = goal Arith.thy
clasohm@0
   301
    "[| 0:n;  ~m:n;  m:nat;  n:nat |] ==> m div n = succ((m#-n) div n)";
clasohm@0
   302
by (rtac (div_def RS def_transrec RS trans) 1);
lcp@6
   303
by (simp_tac (div_ss addsimps prems) 1);
clasohm@0
   304
val div_geq = result();
clasohm@0
   305
clasohm@0
   306
(*Main Result.*)
clasohm@0
   307
val prems = goal Arith.thy
clasohm@0
   308
    "[| 0:n;  m:nat;  n:nat |] ==> (m div n)#*n #+ m mod n = m";
clasohm@0
   309
by (res_inst_tac [("i","m")] complete_induct 1);
clasohm@0
   310
by (resolve_tac prems 1);
clasohm@0
   311
by (res_inst_tac [("Q","x:n")] (excluded_middle RS disjE) 1);
clasohm@0
   312
by (ALLGOALS 
lcp@6
   313
    (asm_simp_tac
lcp@6
   314
     (arith_ss addsimps ([mod_type,div_type] @ prems @
clasohm@0
   315
        [mod_less,mod_geq, div_less, div_geq,
clasohm@0
   316
	 add_assoc, add_diff_inverse, div_termination]))));
clasohm@0
   317
val mod_div_equality = result();
clasohm@0
   318
clasohm@0
   319
clasohm@0
   320
(**** Additional theorems about "less than" ****)
clasohm@0
   321
clasohm@0
   322
val [mnat,nnat] = goal Arith.thy
clasohm@0
   323
    "[| m:nat;  n:nat |] ==> ~ (m #+ n) : n";
clasohm@0
   324
by (rtac (mnat RS nat_induct) 1);
lcp@6
   325
by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mem_not_refl])));
clasohm@0
   326
by (rtac notI 1);
clasohm@0
   327
by (etac notE 1);
clasohm@0
   328
by (etac (succI1 RS Ord_trans) 1);
clasohm@0
   329
by (rtac (nnat RS naturals_are_ordinals) 1);
clasohm@0
   330
val add_not_less_self = result();
clasohm@0
   331
clasohm@0
   332
val [mnat,nnat] = goal Arith.thy
clasohm@0
   333
    "[| m:nat;  n:nat |] ==> m : succ(m #+ n)";
clasohm@0
   334
by (rtac (mnat RS nat_induct) 1);
clasohm@0
   335
(*May not simplify even with ZF_ss because it would expand m:succ(...) *)
clasohm@0
   336
by (rtac (add_0 RS ssubst) 1);
clasohm@0
   337
by (rtac (add_succ RS ssubst) 2);
clasohm@0
   338
by (REPEAT (ares_tac [nnat, Ord_0_mem_succ, succ_mem_succI, 
clasohm@0
   339
		      naturals_are_ordinals, nat_succI, add_type] 1));
clasohm@0
   340
val add_less_succ_self = result();