0

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 
addcongs (mk_typed_congs Arith.thy [("b", "[i,i]=>i")])


33 
addrews [nat_case_succ, nat_succI];


34 
by (rtac rec_trans 1);


35 
by (SIMP_TAC rec_ss 1);


36 
val rec_succ = result();


37 


38 
val major::prems = goal Arith.thy


39 
"[ n: nat; \


40 
\ a: C(0); \


41 
\ !!m z. [ m: nat; z: C(m) ] ==> b(m,z): C(succ(m)) \


42 
\ ] ==> rec(n,a,b) : C(n)";


43 
by (rtac (major RS nat_induct) 1);


44 
by (ALLGOALS


45 
(ASM_SIMP_TAC (ZF_ss addrews (prems@[rec_0,rec_succ]))));


46 
val rec_type = result();


47 


48 
val prems = goalw Arith.thy [rec_def]


49 
"[ n=n'; a=a'; !!m z. b(m,z)=b'(m,z) \


50 
\ ] ==> rec(n,a,b)=rec(n',a',b')";


51 
by (SIMP_TAC (ZF_ss addcongs [transrec_cong,nat_case_cong]


52 
addrews (prems RL [sym])) 1);


53 
val rec_cong = result();


54 


55 
val nat_typechecks = [rec_type,nat_0I,nat_1I,nat_succI,Ord_nat];


56 


57 
val nat_ss = ZF_ss addcongs [nat_case_cong,rec_cong]


58 
addrews ([rec_0,rec_succ] @ nat_typechecks);


59 


60 


61 
(** Addition **)


62 


63 
val add_type = prove_goalw Arith.thy [add_def]


64 
"[ m:nat; n:nat ] ==> m #+ n : nat"


65 
(fn prems=> [ (typechk_tac (prems@nat_typechecks@ZF_typechecks)) ]);


66 


67 
val add_0 = prove_goalw Arith.thy [add_def]


68 
"0 #+ n = n"


69 
(fn _ => [ (rtac rec_0 1) ]);


70 


71 
val add_succ = prove_goalw Arith.thy [add_def]


72 
"succ(m) #+ n = succ(m #+ n)"


73 
(fn _=> [ (rtac rec_succ 1) ]);


74 


75 
(** Multiplication **)


76 


77 
val mult_type = prove_goalw Arith.thy [mult_def]


78 
"[ m:nat; n:nat ] ==> m #* n : nat"


79 
(fn prems=>


80 
[ (typechk_tac (prems@[add_type]@nat_typechecks@ZF_typechecks)) ]);


81 


82 
val mult_0 = prove_goalw Arith.thy [mult_def]


83 
"0 #* n = 0"


84 
(fn _ => [ (rtac rec_0 1) ]);


85 


86 
val mult_succ = prove_goalw Arith.thy [mult_def]


87 
"succ(m) #* n = n #+ (m #* n)"


88 
(fn _ => [ (rtac rec_succ 1) ]);


89 


90 
(** Difference **)


91 


92 
val diff_type = prove_goalw Arith.thy [diff_def]


93 
"[ m:nat; n:nat ] ==> m # n : nat"


94 
(fn prems=> [ (typechk_tac (prems@nat_typechecks@ZF_typechecks)) ]);


95 


96 
val diff_0 = prove_goalw Arith.thy [diff_def]


97 
"m # 0 = m"


98 
(fn _ => [ (rtac rec_0 1) ]);


99 


100 
val diff_0_eq_0 = prove_goalw Arith.thy [diff_def]


101 
"n:nat ==> 0 # n = 0"


102 
(fn [prem]=>


103 
[ (rtac (prem RS nat_induct) 1),


104 
(ALLGOALS (ASM_SIMP_TAC nat_ss)) ]);


105 


106 
(*Must simplify BEFORE the induction!! (Else we get a critical pair)


107 
succ(m) # succ(n) rewrites to pred(succ(m) # n) *)


108 
val diff_succ_succ = prove_goalw Arith.thy [diff_def]


109 
"[ m:nat; n:nat ] ==> succ(m) # succ(n) = m # n"


110 
(fn prems=>


111 
[ (ASM_SIMP_TAC (nat_ss addrews prems) 1),


112 
(nat_ind_tac "n" prems 1),


113 
(ALLGOALS (ASM_SIMP_TAC (nat_ss addrews prems))) ]);


114 


115 
val prems = goal Arith.thy


116 
"[ m:nat; n:nat ] ==> m # n : succ(m)";


117 
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);


118 
by (resolve_tac prems 1);


119 
by (resolve_tac prems 1);


120 
by (etac succE 3);


121 
by (ALLGOALS


122 
(ASM_SIMP_TAC


123 
(nat_ss addrews (prems@[diff_0,diff_0_eq_0,diff_succ_succ]))));


124 
val diff_leq = result();


125 


126 
(*** Simplification over add, mult, diff ***)


127 


128 
val arith_typechecks = [add_type, mult_type, diff_type];


129 
val arith_rews = [add_0, add_succ,


130 
mult_0, mult_succ,


131 
diff_0, diff_0_eq_0, diff_succ_succ];


132 


133 
val arith_congs = mk_congs Arith.thy ["op #+", "op #", "op #*"];


134 


135 
val arith_ss = nat_ss addcongs arith_congs


136 
addrews (arith_rews@arith_typechecks);


137 


138 
(*** Addition ***)


139 


140 
(*Associative law for addition*)


141 
val add_assoc = prove_goal Arith.thy


142 
"m:nat ==> (m #+ n) #+ k = m #+ (n #+ k)"


143 
(fn prems=>


144 
[ (nat_ind_tac "m" prems 1),


145 
(ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);


146 


147 
(*The following two lemmas are used for add_commute and sometimes


148 
elsewhere, since they are safe for rewriting.*)


149 
val add_0_right = prove_goal Arith.thy


150 
"m:nat ==> m #+ 0 = m"


151 
(fn prems=>


152 
[ (nat_ind_tac "m" prems 1),


153 
(ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);


154 


155 
val add_succ_right = prove_goal Arith.thy


156 
"m:nat ==> m #+ succ(n) = succ(m #+ n)"


157 
(fn prems=>


158 
[ (nat_ind_tac "m" prems 1),


159 
(ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);


160 


161 
(*Commutative law for addition*)


162 
val add_commute = prove_goal Arith.thy


163 
"[ m:nat; n:nat ] ==> m #+ n = n #+ m"


164 
(fn prems=>


165 
[ (nat_ind_tac "n" prems 1),


166 
(ALLGOALS


167 
(ASM_SIMP_TAC


168 
(arith_ss addrews (prems@[add_0_right, add_succ_right])))) ]);


169 


170 
(*Cancellation law on the left*)


171 
val [knat,eqn] = goal Arith.thy


172 
"[ k:nat; k #+ m = k #+ n ] ==> m=n";


173 
by (rtac (eqn RS rev_mp) 1);


174 
by (nat_ind_tac "k" [knat] 1);


175 
by (ALLGOALS (SIMP_TAC arith_ss));


176 
by (fast_tac ZF_cs 1);


177 
val add_left_cancel = result();


178 


179 
(*** Multiplication ***)


180 


181 
(*right annihilation in product*)


182 
val mult_0_right = prove_goal Arith.thy


183 
"m:nat ==> m #* 0 = 0"


184 
(fn prems=>


185 
[ (nat_ind_tac "m" prems 1),


186 
(ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);


187 


188 
(*right successor law for multiplication*)


189 
val mult_succ_right = prove_goal Arith.thy


190 
"[ m:nat; n:nat ] ==> m #* succ(n) = m #+ (m #* n)"


191 
(fn prems=>


192 
[ (nat_ind_tac "m" prems 1),


193 
(ALLGOALS (ASM_SIMP_TAC (arith_ss addrews ([add_assoc RS sym]@prems)))),


194 
(*The final goal requires the commutative law for addition*)


195 
(REPEAT (ares_tac (prems@[refl,add_commute]@ZF_congs@arith_congs) 1)) ]);


196 


197 
(*Commutative law for multiplication*)


198 
val mult_commute = prove_goal Arith.thy


199 
"[ m:nat; n:nat ] ==> m #* n = n #* m"


200 
(fn prems=>


201 
[ (nat_ind_tac "m" prems 1),


202 
(ALLGOALS (ASM_SIMP_TAC


203 
(arith_ss addrews (prems@[mult_0_right, mult_succ_right])))) ]);


204 


205 
(*addition distributes over multiplication*)


206 
val add_mult_distrib = prove_goal Arith.thy


207 
"[ m:nat; k:nat ] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)"


208 
(fn prems=>


209 
[ (nat_ind_tac "m" prems 1),


210 
(ALLGOALS (ASM_SIMP_TAC (arith_ss addrews ([add_assoc RS sym]@prems)))) ]);


211 


212 
(*Distributive law on the left; requires an extra typing premise*)


213 
val add_mult_distrib_left = prove_goal Arith.thy


214 
"[ m:nat; n:nat; k:nat ] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)"


215 
(fn prems=>


216 
let val mult_commute' = read_instantiate [("m","k")] mult_commute


217 
val ss = arith_ss addrews ([mult_commute',add_mult_distrib]@prems)


218 
in [ (SIMP_TAC ss 1) ]


219 
end);


220 


221 
(*Associative law for multiplication*)


222 
val mult_assoc = prove_goal Arith.thy


223 
"[ m:nat; n:nat; k:nat ] ==> (m #* n) #* k = m #* (n #* k)"


224 
(fn prems=>


225 
[ (nat_ind_tac "m" prems 1),


226 
(ALLGOALS (ASM_SIMP_TAC (arith_ss addrews (prems@[add_mult_distrib])))) ]);


227 


228 


229 
(*** Difference ***)


230 


231 
val diff_self_eq_0 = prove_goal Arith.thy


232 
"m:nat ==> m # m = 0"


233 
(fn prems=>


234 
[ (nat_ind_tac "m" prems 1),


235 
(ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);


236 


237 
(*Addition is the inverse of subtraction: if n<=m then n+(mn) = m. *)


238 
val notless::prems = goal Arith.thy


239 
"[ ~m:n; m:nat; n:nat ] ==> n #+ (m#n) = m";


240 
by (rtac (notless RS rev_mp) 1);


241 
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);


242 
by (resolve_tac prems 1);


243 
by (resolve_tac prems 1);


244 
by (ALLGOALS (ASM_SIMP_TAC


245 
(arith_ss addrews (prems@[succ_mem_succ_iff, Ord_0_mem_succ,


246 
naturals_are_ordinals]))));


247 
val add_diff_inverse = result();


248 


249 


250 
(*Subtraction is the inverse of addition. *)


251 
val [mnat,nnat] = goal Arith.thy


252 
"[ m:nat; n:nat ] ==> (n#+m) #n = m";


253 
by (rtac (nnat RS nat_induct) 1);


254 
by (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews [mnat])));


255 
val diff_add_inverse = result();


256 


257 
val [mnat,nnat] = goal Arith.thy


258 
"[ m:nat; n:nat ] ==> n # (n#+m) = 0";


259 
by (rtac (nnat RS nat_induct) 1);


260 
by (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews [mnat])));


261 
val diff_add_0 = result();


262 


263 


264 
(*** Remainder ***)


265 


266 
(*In ordinary notation: if 0<n and n<=m then mn < m *)


267 
val prems = goal Arith.thy


268 
"[ 0:n; ~ m:n; m:nat; n:nat ] ==> m # n : m";


269 
by (cut_facts_tac prems 1);


270 
by (etac rev_mp 1);


271 
by (etac rev_mp 1);


272 
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);


273 
by (resolve_tac prems 1);


274 
by (resolve_tac prems 1);


275 
by (ALLGOALS (ASM_SIMP_TAC


276 
(nat_ss addrews (prems@[diff_leq,diff_succ_succ]))));


277 
val div_termination = result();


278 


279 
val div_rls =


280 
[Ord_transrec_type, apply_type, div_termination, if_type] @


281 
nat_typechecks;


282 


283 
(*Type checking depends upon termination!*)


284 
val prems = goalw Arith.thy [mod_def]


285 
"[ 0:n; m:nat; n:nat ] ==> m mod n : nat";


286 
by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1));


287 
val mod_type = result();


288 


289 
val div_ss = ZF_ss addrews [naturals_are_ordinals,div_termination];


290 


291 
val prems = goal Arith.thy "[ 0:n; m:n; m:nat; n:nat ] ==> m mod n = m";


292 
by (rtac (mod_def RS def_transrec RS trans) 1);


293 
by (SIMP_TAC (div_ss addrews prems) 1);


294 
val mod_less = result();


295 


296 
val prems = goal Arith.thy


297 
"[ 0:n; ~m:n; m:nat; n:nat ] ==> m mod n = (m#n) mod n";


298 
by (rtac (mod_def RS def_transrec RS trans) 1);


299 
by (SIMP_TAC (div_ss addrews prems) 1);


300 
val mod_geq = result();


301 


302 
(*** Quotient ***)


303 


304 
(*Type checking depends upon termination!*)


305 
val prems = goalw Arith.thy [div_def]


306 
"[ 0:n; m:nat; n:nat ] ==> m div n : nat";


307 
by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1));


308 
val div_type = result();


309 


310 
val prems = goal Arith.thy


311 
"[ 0:n; m:n; m:nat; n:nat ] ==> m div n = 0";


312 
by (rtac (div_def RS def_transrec RS trans) 1);


313 
by (SIMP_TAC (div_ss addrews prems) 1);


314 
val div_less = result();


315 


316 
val prems = goal Arith.thy


317 
"[ 0:n; ~m:n; m:nat; n:nat ] ==> m div n = succ((m#n) div n)";


318 
by (rtac (div_def RS def_transrec RS trans) 1);


319 
by (SIMP_TAC (div_ss addrews prems) 1);


320 
val div_geq = result();


321 


322 
(*Main Result.*)


323 
val prems = goal Arith.thy


324 
"[ 0:n; m:nat; n:nat ] ==> (m div n)#*n #+ m mod n = m";


325 
by (res_inst_tac [("i","m")] complete_induct 1);


326 
by (resolve_tac prems 1);


327 
by (res_inst_tac [("Q","x:n")] (excluded_middle RS disjE) 1);


328 
by (ALLGOALS


329 
(ASM_SIMP_TAC


330 
(arith_ss addrews ([mod_type,div_type] @ prems @


331 
[mod_less,mod_geq, div_less, div_geq,


332 
add_assoc, add_diff_inverse, div_termination]))));


333 
val mod_div_equality = result();


334 


335 


336 
(**** Additional theorems about "less than" ****)


337 


338 
val [mnat,nnat] = goal Arith.thy


339 
"[ m:nat; n:nat ] ==> ~ (m #+ n) : n";


340 
by (rtac (mnat RS nat_induct) 1);


341 
by (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews [mem_not_refl])));


342 
by (rtac notI 1);


343 
by (etac notE 1);


344 
by (etac (succI1 RS Ord_trans) 1);


345 
by (rtac (nnat RS naturals_are_ordinals) 1);


346 
val add_not_less_self = result();


347 


348 
val [mnat,nnat] = goal Arith.thy


349 
"[ m:nat; n:nat ] ==> m : succ(m #+ n)";


350 
by (rtac (mnat RS nat_induct) 1);


351 
(*May not simplify even with ZF_ss because it would expand m:succ(...) *)


352 
by (rtac (add_0 RS ssubst) 1);


353 
by (rtac (add_succ RS ssubst) 2);


354 
by (REPEAT (ares_tac [nnat, Ord_0_mem_succ, succ_mem_succI,


355 
naturals_are_ordinals, nat_succI, add_type] 1));


356 
val add_less_succ_self = result();
