src/ZF/Arith.ML
changeset 0 a5a9c433f639
child 6 8ce8c4d13d4d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/Arith.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,356 @@
     1.4 +(*  Title: 	ZF/arith.ML
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1992  University of Cambridge
     1.8 +
     1.9 +For arith.thy.  Arithmetic operators and their definitions
    1.10 +
    1.11 +Proofs about elementary arithmetic: addition, multiplication, etc.
    1.12 +
    1.13 +Could prove def_rec_0, def_rec_succ...
    1.14 +*)
    1.15 +
    1.16 +open Arith;
    1.17 +
    1.18 +(*"Difference" is subtraction of natural numbers.
    1.19 +  There are no negative numbers; we have
    1.20 +     m #- n = 0  iff  m<=n   and     m #- n = succ(k) iff m>n.
    1.21 +  Also, rec(m, 0, %z w.z) is pred(m).   
    1.22 +*)
    1.23 +
    1.24 +(** rec -- better than nat_rec; the succ case has no type requirement! **)
    1.25 +
    1.26 +val rec_trans = rec_def RS def_transrec RS trans;
    1.27 +
    1.28 +goal Arith.thy "rec(0,a,b) = a";
    1.29 +by (rtac rec_trans 1);
    1.30 +by (rtac nat_case_0 1);
    1.31 +val rec_0 = result();
    1.32 +
    1.33 +goal Arith.thy "rec(succ(m),a,b) = b(m, rec(m,a,b))";
    1.34 +val rec_ss = ZF_ss 
    1.35 +      addcongs (mk_typed_congs Arith.thy [("b", "[i,i]=>i")])
    1.36 +      addrews [nat_case_succ, nat_succI];
    1.37 +by (rtac rec_trans 1);
    1.38 +by (SIMP_TAC rec_ss 1);
    1.39 +val rec_succ = result();
    1.40 +
    1.41 +val major::prems = goal Arith.thy
    1.42 +    "[| n: nat;  \
    1.43 +\       a: C(0);  \
    1.44 +\       !!m z. [| m: nat;  z: C(m) |] ==> b(m,z): C(succ(m))  \
    1.45 +\    |] ==> rec(n,a,b) : C(n)";
    1.46 +by (rtac (major RS nat_induct) 1);
    1.47 +by (ALLGOALS
    1.48 +    (ASM_SIMP_TAC (ZF_ss addrews (prems@[rec_0,rec_succ]))));
    1.49 +val rec_type = result();
    1.50 +
    1.51 +val prems = goalw Arith.thy [rec_def]
    1.52 +    "[| n=n';  a=a';  !!m z. b(m,z)=b'(m,z)  \
    1.53 +\    |] ==> rec(n,a,b)=rec(n',a',b')";
    1.54 +by (SIMP_TAC (ZF_ss addcongs [transrec_cong,nat_case_cong] 
    1.55 +		    addrews (prems RL [sym])) 1);
    1.56 +val rec_cong = result();
    1.57 +
    1.58 +val nat_typechecks = [rec_type,nat_0I,nat_1I,nat_succI,Ord_nat];
    1.59 +
    1.60 +val nat_ss = ZF_ss addcongs [nat_case_cong,rec_cong]
    1.61 +	       	   addrews ([rec_0,rec_succ] @ nat_typechecks);
    1.62 +
    1.63 +
    1.64 +(** Addition **)
    1.65 +
    1.66 +val add_type = prove_goalw Arith.thy [add_def]
    1.67 +    "[| m:nat;  n:nat |] ==> m #+ n : nat"
    1.68 + (fn prems=> [ (typechk_tac (prems@nat_typechecks@ZF_typechecks)) ]);
    1.69 +
    1.70 +val add_0 = prove_goalw Arith.thy [add_def]
    1.71 +    "0 #+ n = n"
    1.72 + (fn _ => [ (rtac rec_0 1) ]);
    1.73 +
    1.74 +val add_succ = prove_goalw Arith.thy [add_def]
    1.75 +    "succ(m) #+ n = succ(m #+ n)"
    1.76 + (fn _=> [ (rtac rec_succ 1) ]); 
    1.77 +
    1.78 +(** Multiplication **)
    1.79 +
    1.80 +val mult_type = prove_goalw Arith.thy [mult_def]
    1.81 +    "[| m:nat;  n:nat |] ==> m #* n : nat"
    1.82 + (fn prems=>
    1.83 +  [ (typechk_tac (prems@[add_type]@nat_typechecks@ZF_typechecks)) ]);
    1.84 +
    1.85 +val mult_0 = prove_goalw Arith.thy [mult_def]
    1.86 +    "0 #* n = 0"
    1.87 + (fn _ => [ (rtac rec_0 1) ]);
    1.88 +
    1.89 +val mult_succ = prove_goalw Arith.thy [mult_def]
    1.90 +    "succ(m) #* n = n #+ (m #* n)"
    1.91 + (fn _ => [ (rtac rec_succ 1) ]); 
    1.92 +
    1.93 +(** Difference **)
    1.94 +
    1.95 +val diff_type = prove_goalw Arith.thy [diff_def]
    1.96 +    "[| m:nat;  n:nat |] ==> m #- n : nat"
    1.97 + (fn prems=> [ (typechk_tac (prems@nat_typechecks@ZF_typechecks)) ]);
    1.98 +
    1.99 +val diff_0 = prove_goalw Arith.thy [diff_def]
   1.100 +    "m #- 0 = m"
   1.101 + (fn _ => [ (rtac rec_0 1) ]);
   1.102 +
   1.103 +val diff_0_eq_0 = prove_goalw Arith.thy [diff_def]
   1.104 +    "n:nat ==> 0 #- n = 0"
   1.105 + (fn [prem]=>
   1.106 +  [ (rtac (prem RS nat_induct) 1),
   1.107 +    (ALLGOALS (ASM_SIMP_TAC nat_ss)) ]);
   1.108 +
   1.109 +(*Must simplify BEFORE the induction!!  (Else we get a critical pair)
   1.110 +  succ(m) #- succ(n)   rewrites to   pred(succ(m) #- n)  *)
   1.111 +val diff_succ_succ = prove_goalw Arith.thy [diff_def]
   1.112 +    "[| m:nat;  n:nat |] ==> succ(m) #- succ(n) = m #- n"
   1.113 + (fn prems=>
   1.114 +  [ (ASM_SIMP_TAC (nat_ss addrews prems) 1),
   1.115 +    (nat_ind_tac "n" prems 1),
   1.116 +    (ALLGOALS (ASM_SIMP_TAC (nat_ss addrews prems))) ]);
   1.117 +
   1.118 +val prems = goal Arith.thy 
   1.119 +    "[| m:nat;  n:nat |] ==> m #- n : succ(m)";
   1.120 +by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.121 +by (resolve_tac prems 1);
   1.122 +by (resolve_tac prems 1);
   1.123 +by (etac succE 3);
   1.124 +by (ALLGOALS
   1.125 +    (ASM_SIMP_TAC
   1.126 +     (nat_ss addrews (prems@[diff_0,diff_0_eq_0,diff_succ_succ]))));
   1.127 +val diff_leq = result();
   1.128 +
   1.129 +(*** Simplification over add, mult, diff ***)
   1.130 +
   1.131 +val arith_typechecks = [add_type, mult_type, diff_type];
   1.132 +val arith_rews = [add_0, add_succ,
   1.133 +		  mult_0, mult_succ,
   1.134 +		  diff_0, diff_0_eq_0, diff_succ_succ];
   1.135 +
   1.136 +val arith_congs = mk_congs Arith.thy ["op #+", "op #-", "op #*"];
   1.137 +
   1.138 +val arith_ss = nat_ss addcongs arith_congs
   1.139 +                      addrews  (arith_rews@arith_typechecks);
   1.140 +
   1.141 +(*** Addition ***)
   1.142 +
   1.143 +(*Associative law for addition*)
   1.144 +val add_assoc = prove_goal Arith.thy 
   1.145 +    "m:nat ==> (m #+ n) #+ k = m #+ (n #+ k)"
   1.146 + (fn prems=>
   1.147 +  [ (nat_ind_tac "m" prems 1),
   1.148 +    (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
   1.149 +
   1.150 +(*The following two lemmas are used for add_commute and sometimes
   1.151 +  elsewhere, since they are safe for rewriting.*)
   1.152 +val add_0_right = prove_goal Arith.thy
   1.153 +    "m:nat ==> m #+ 0 = m"
   1.154 + (fn prems=>
   1.155 +  [ (nat_ind_tac "m" prems 1),
   1.156 +    (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]); 
   1.157 +
   1.158 +val add_succ_right = prove_goal Arith.thy
   1.159 +    "m:nat ==> m #+ succ(n) = succ(m #+ n)"
   1.160 + (fn prems=>
   1.161 +  [ (nat_ind_tac "m" prems 1),
   1.162 +    (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]); 
   1.163 +
   1.164 +(*Commutative law for addition*)  
   1.165 +val add_commute = prove_goal Arith.thy 
   1.166 +    "[| m:nat;  n:nat |] ==> m #+ n = n #+ m"
   1.167 + (fn prems=>
   1.168 +  [ (nat_ind_tac "n" prems 1),
   1.169 +    (ALLGOALS
   1.170 +     (ASM_SIMP_TAC
   1.171 +      (arith_ss addrews (prems@[add_0_right, add_succ_right])))) ]);
   1.172 +
   1.173 +(*Cancellation law on the left*)
   1.174 +val [knat,eqn] = goal Arith.thy 
   1.175 +    "[| k:nat;  k #+ m = k #+ n |] ==> m=n";
   1.176 +by (rtac (eqn RS rev_mp) 1);
   1.177 +by (nat_ind_tac "k" [knat] 1);
   1.178 +by (ALLGOALS (SIMP_TAC arith_ss));
   1.179 +by (fast_tac ZF_cs 1);
   1.180 +val add_left_cancel = result();
   1.181 +
   1.182 +(*** Multiplication ***)
   1.183 +
   1.184 +(*right annihilation in product*)
   1.185 +val mult_0_right = prove_goal Arith.thy 
   1.186 +    "m:nat ==> m #* 0 = 0"
   1.187 + (fn prems=>
   1.188 +  [ (nat_ind_tac "m" prems 1),
   1.189 +    (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems)))  ]);
   1.190 +
   1.191 +(*right successor law for multiplication*)
   1.192 +val mult_succ_right = prove_goal Arith.thy 
   1.193 +    "[| m:nat;  n:nat |] ==> m #* succ(n) = m #+ (m #* n)"
   1.194 + (fn prems=>
   1.195 +  [ (nat_ind_tac "m" prems 1),
   1.196 +    (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews ([add_assoc RS sym]@prems)))),
   1.197 +       (*The final goal requires the commutative law for addition*)
   1.198 +    (REPEAT (ares_tac (prems@[refl,add_commute]@ZF_congs@arith_congs) 1))  ]);
   1.199 +
   1.200 +(*Commutative law for multiplication*)
   1.201 +val mult_commute = prove_goal Arith.thy 
   1.202 +    "[| m:nat;  n:nat |] ==> m #* n = n #* m"
   1.203 + (fn prems=>
   1.204 +  [ (nat_ind_tac "m" prems 1),
   1.205 +    (ALLGOALS (ASM_SIMP_TAC
   1.206 +	       (arith_ss addrews (prems@[mult_0_right, mult_succ_right])))) ]);
   1.207 +
   1.208 +(*addition distributes over multiplication*)
   1.209 +val add_mult_distrib = prove_goal Arith.thy 
   1.210 +    "[| m:nat;  k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)"
   1.211 + (fn prems=>
   1.212 +  [ (nat_ind_tac "m" prems 1),
   1.213 +    (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews ([add_assoc RS sym]@prems)))) ]);
   1.214 +
   1.215 +(*Distributive law on the left; requires an extra typing premise*)
   1.216 +val add_mult_distrib_left = prove_goal Arith.thy 
   1.217 +    "[| m:nat;  n:nat;  k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)"
   1.218 + (fn prems=>
   1.219 +      let val mult_commute' = read_instantiate [("m","k")] mult_commute
   1.220 +          val ss = arith_ss addrews ([mult_commute',add_mult_distrib]@prems)
   1.221 +      in [ (SIMP_TAC ss 1) ]
   1.222 +      end);
   1.223 +
   1.224 +(*Associative law for multiplication*)
   1.225 +val mult_assoc = prove_goal Arith.thy 
   1.226 +    "[| m:nat;  n:nat;  k:nat |] ==> (m #* n) #* k = m #* (n #* k)"
   1.227 + (fn prems=>
   1.228 +  [ (nat_ind_tac "m" prems 1),
   1.229 +    (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews (prems@[add_mult_distrib])))) ]);
   1.230 +
   1.231 +
   1.232 +(*** Difference ***)
   1.233 +
   1.234 +val diff_self_eq_0 = prove_goal Arith.thy 
   1.235 +    "m:nat ==> m #- m = 0"
   1.236 + (fn prems=>
   1.237 +  [ (nat_ind_tac "m" prems 1),
   1.238 +    (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
   1.239 +
   1.240 +(*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
   1.241 +val notless::prems = goal Arith.thy
   1.242 +    "[| ~m:n;  m:nat;  n:nat |] ==> n #+ (m#-n) = m";
   1.243 +by (rtac (notless RS rev_mp) 1);
   1.244 +by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.245 +by (resolve_tac prems 1);
   1.246 +by (resolve_tac prems 1);
   1.247 +by (ALLGOALS (ASM_SIMP_TAC
   1.248 +	      (arith_ss addrews (prems@[succ_mem_succ_iff, Ord_0_mem_succ, 
   1.249 +				  naturals_are_ordinals]))));
   1.250 +val add_diff_inverse = result();
   1.251 +
   1.252 +
   1.253 +(*Subtraction is the inverse of addition. *)
   1.254 +val [mnat,nnat] = goal Arith.thy
   1.255 +    "[| m:nat;  n:nat |] ==> (n#+m) #-n = m";
   1.256 +by (rtac (nnat RS nat_induct) 1);
   1.257 +by (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews [mnat])));
   1.258 +val diff_add_inverse = result();
   1.259 +
   1.260 +val [mnat,nnat] = goal Arith.thy
   1.261 +    "[| m:nat;  n:nat |] ==> n #- (n#+m) = 0";
   1.262 +by (rtac (nnat RS nat_induct) 1);
   1.263 +by (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews [mnat])));
   1.264 +val diff_add_0 = result();
   1.265 +
   1.266 +
   1.267 +(*** Remainder ***)
   1.268 +
   1.269 +(*In ordinary notation: if 0<n and n<=m then m-n < m *)
   1.270 +val prems = goal Arith.thy
   1.271 +    "[| 0:n; ~ m:n;  m:nat;  n:nat |] ==> m #- n : m";
   1.272 +by (cut_facts_tac prems 1);
   1.273 +by (etac rev_mp 1);
   1.274 +by (etac rev_mp 1);
   1.275 +by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.276 +by (resolve_tac prems 1);
   1.277 +by (resolve_tac prems 1);
   1.278 +by (ALLGOALS (ASM_SIMP_TAC
   1.279 +	      (nat_ss addrews (prems@[diff_leq,diff_succ_succ]))));
   1.280 +val div_termination = result();
   1.281 +
   1.282 +val div_rls =
   1.283 +    [Ord_transrec_type, apply_type, div_termination, if_type] @ 
   1.284 +    nat_typechecks;
   1.285 +
   1.286 +(*Type checking depends upon termination!*)
   1.287 +val prems = goalw Arith.thy [mod_def]
   1.288 +    "[| 0:n;  m:nat;  n:nat |] ==> m mod n : nat";
   1.289 +by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1));
   1.290 +val mod_type = result();
   1.291 +
   1.292 +val div_ss = ZF_ss addrews [naturals_are_ordinals,div_termination];
   1.293 +
   1.294 +val prems = goal Arith.thy "[| 0:n;  m:n;  m:nat;  n:nat |] ==> m mod n = m";
   1.295 +by (rtac (mod_def RS def_transrec RS trans) 1);
   1.296 +by (SIMP_TAC (div_ss addrews prems) 1);
   1.297 +val mod_less = result();
   1.298 +
   1.299 +val prems = goal Arith.thy
   1.300 +    "[| 0:n;  ~m:n;  m:nat;  n:nat |] ==> m mod n = (m#-n) mod n";
   1.301 +by (rtac (mod_def RS def_transrec RS trans) 1);
   1.302 +by (SIMP_TAC (div_ss addrews prems) 1);
   1.303 +val mod_geq = result();
   1.304 +
   1.305 +(*** Quotient ***)
   1.306 +
   1.307 +(*Type checking depends upon termination!*)
   1.308 +val prems = goalw Arith.thy [div_def]
   1.309 +    "[| 0:n;  m:nat;  n:nat |] ==> m div n : nat";
   1.310 +by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1));
   1.311 +val div_type = result();
   1.312 +
   1.313 +val prems = goal Arith.thy
   1.314 +    "[| 0:n;  m:n;  m:nat;  n:nat |] ==> m div n = 0";
   1.315 +by (rtac (div_def RS def_transrec RS trans) 1);
   1.316 +by (SIMP_TAC (div_ss addrews prems) 1);
   1.317 +val div_less = result();
   1.318 +
   1.319 +val prems = goal Arith.thy
   1.320 +    "[| 0:n;  ~m:n;  m:nat;  n:nat |] ==> m div n = succ((m#-n) div n)";
   1.321 +by (rtac (div_def RS def_transrec RS trans) 1);
   1.322 +by (SIMP_TAC (div_ss addrews prems) 1);
   1.323 +val div_geq = result();
   1.324 +
   1.325 +(*Main Result.*)
   1.326 +val prems = goal Arith.thy
   1.327 +    "[| 0:n;  m:nat;  n:nat |] ==> (m div n)#*n #+ m mod n = m";
   1.328 +by (res_inst_tac [("i","m")] complete_induct 1);
   1.329 +by (resolve_tac prems 1);
   1.330 +by (res_inst_tac [("Q","x:n")] (excluded_middle RS disjE) 1);
   1.331 +by (ALLGOALS 
   1.332 +    (ASM_SIMP_TAC
   1.333 +     (arith_ss addrews ([mod_type,div_type] @ prems @
   1.334 +        [mod_less,mod_geq, div_less, div_geq,
   1.335 +	 add_assoc, add_diff_inverse, div_termination]))));
   1.336 +val mod_div_equality = result();
   1.337 +
   1.338 +
   1.339 +(**** Additional theorems about "less than" ****)
   1.340 +
   1.341 +val [mnat,nnat] = goal Arith.thy
   1.342 +    "[| m:nat;  n:nat |] ==> ~ (m #+ n) : n";
   1.343 +by (rtac (mnat RS nat_induct) 1);
   1.344 +by (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews [mem_not_refl])));
   1.345 +by (rtac notI 1);
   1.346 +by (etac notE 1);
   1.347 +by (etac (succI1 RS Ord_trans) 1);
   1.348 +by (rtac (nnat RS naturals_are_ordinals) 1);
   1.349 +val add_not_less_self = result();
   1.350 +
   1.351 +val [mnat,nnat] = goal Arith.thy
   1.352 +    "[| m:nat;  n:nat |] ==> m : succ(m #+ n)";
   1.353 +by (rtac (mnat RS nat_induct) 1);
   1.354 +(*May not simplify even with ZF_ss because it would expand m:succ(...) *)
   1.355 +by (rtac (add_0 RS ssubst) 1);
   1.356 +by (rtac (add_succ RS ssubst) 2);
   1.357 +by (REPEAT (ares_tac [nnat, Ord_0_mem_succ, succ_mem_succI, 
   1.358 +		      naturals_are_ordinals, nat_succI, add_type] 1));
   1.359 +val add_less_succ_self = result();