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