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