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.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.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.65 +
1.67 +    "[| m:nat;  n:nat |] ==> m #+ n : nat"
1.68 + (fn prems=> [ (typechk_tac (prems@nat_typechecks@ZF_typechecks)) ]);
1.69 +
1.71 +    "0 #+ n = n"
1.72 + (fn _ => [ (rtac rec_0 1) ]);
1.73 +
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.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.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.140 +
1.142 +
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.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.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.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.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.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.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.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.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.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.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.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.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.336 +val mod_div_equality = result();
1.337 +
1.338 +
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.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));