0

1 
(* Title: CTT/arith


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1991 University of Cambridge


5 


6 
Theorems for arith.thy (Arithmetic operators)


7 


8 
Proofs about elementary arithmetic: addition, multiplication, etc.


9 
Tests definitions and simplifier.


10 
*)


11 


12 
open Arith;


13 
val arith_defs = [add_def, diff_def, absdiff_def, mult_def, mod_def, div_def];


14 


15 


16 
(** Addition *)


17 


18 
(*typing of add: short and long versions*)


19 


20 
val add_typing = prove_goal Arith.thy


21 
"[ a:N; b:N ] ==> a #+ b : N"


22 
(fn prems=>


23 
[ (rewrite_goals_tac arith_defs),


24 
(typechk_tac prems) ]);


25 


26 
val add_typingL = prove_goal Arith.thy


27 
"[ a=c:N; b=d:N ] ==> a #+ b = c #+ d : N"


28 
(fn prems=>


29 
[ (rewrite_goals_tac arith_defs),


30 
(equal_tac prems) ]);


31 


32 


33 
(*computation for add: 0 and successor cases*)


34 


35 
val addC0 = prove_goal Arith.thy


36 
"b:N ==> 0 #+ b = b : N"


37 
(fn prems=>


38 
[ (rewrite_goals_tac arith_defs),


39 
(rew_tac prems) ]);


40 


41 
val addC_succ = prove_goal Arith.thy


42 
"[ a:N; b:N ] ==> succ(a) #+ b = succ(a #+ b) : N"


43 
(fn prems=>


44 
[ (rewrite_goals_tac arith_defs),


45 
(rew_tac prems) ]);


46 


47 


48 
(** Multiplication *)


49 


50 
(*typing of mult: short and long versions*)


51 


52 
val mult_typing = prove_goal Arith.thy


53 
"[ a:N; b:N ] ==> a #* b : N"


54 
(fn prems=>


55 
[ (rewrite_goals_tac arith_defs),


56 
(typechk_tac([add_typing]@prems)) ]);


57 


58 
val mult_typingL = prove_goal Arith.thy


59 
"[ a=c:N; b=d:N ] ==> a #* b = c #* d : N"


60 
(fn prems=>


61 
[ (rewrite_goals_tac arith_defs),


62 
(equal_tac (prems@[add_typingL])) ]);


63 


64 
(*computation for mult: 0 and successor cases*)


65 


66 
val multC0 = prove_goal Arith.thy


67 
"b:N ==> 0 #* b = 0 : N"


68 
(fn prems=>


69 
[ (rewrite_goals_tac arith_defs),


70 
(rew_tac prems) ]);


71 


72 
val multC_succ = prove_goal Arith.thy


73 
"[ a:N; b:N ] ==> succ(a) #* b = b #+ (a #* b) : N"


74 
(fn prems=>


75 
[ (rewrite_goals_tac arith_defs),


76 
(rew_tac prems) ]);


77 


78 


79 
(** Difference *)


80 


81 
(*typing of difference*)


82 


83 
val diff_typing = prove_goal Arith.thy


84 
"[ a:N; b:N ] ==> a  b : N"


85 
(fn prems=>


86 
[ (rewrite_goals_tac arith_defs),


87 
(typechk_tac prems) ]);


88 


89 
val diff_typingL = prove_goal Arith.thy


90 
"[ a=c:N; b=d:N ] ==> a  b = c  d : N"


91 
(fn prems=>


92 
[ (rewrite_goals_tac arith_defs),


93 
(equal_tac prems) ]);


94 


95 


96 


97 
(*computation for difference: 0 and successor cases*)


98 


99 
val diffC0 = prove_goal Arith.thy


100 
"a:N ==> a  0 = a : N"


101 
(fn prems=>


102 
[ (rewrite_goals_tac arith_defs),


103 
(rew_tac prems) ]);


104 


105 
(*Note: rec(a, 0, %z w.z) is pred(a). *)


106 


107 
val diff_0_eq_0 = prove_goal Arith.thy


108 
"b:N ==> 0  b = 0 : N"


109 
(fn prems=>


110 
[ (NE_tac "b" 1),


111 
(rewrite_goals_tac arith_defs),


112 
(hyp_rew_tac prems) ]);


113 


114 


115 
(*Essential to simplify FIRST!! (Else we get a critical pair)


116 
succ(a)  succ(b) rewrites to pred(succ(a)  b) *)


117 
val diff_succ_succ = prove_goal Arith.thy


118 
"[ a:N; b:N ] ==> succ(a)  succ(b) = a  b : N"


119 
(fn prems=>


120 
[ (rewrite_goals_tac arith_defs),


121 
(hyp_rew_tac prems),


122 
(NE_tac "b" 1),


123 
(hyp_rew_tac prems) ]);


124 


125 


126 


127 
(*** Simplification *)


128 


129 
val arith_typing_rls =


130 
[add_typing, mult_typing, diff_typing];


131 


132 
val arith_congr_rls =


133 
[add_typingL, mult_typingL, diff_typingL];


134 


135 
val congr_rls = arith_congr_rls@standard_congr_rls;


136 


137 
val arithC_rls =


138 
[addC0, addC_succ,


139 
multC0, multC_succ,


140 
diffC0, diff_0_eq_0, diff_succ_succ];


141 


142 


143 
structure Arith_simp_data: TSIMP_DATA =


144 
struct


145 
val refl = refl_elem


146 
val sym = sym_elem


147 
val trans = trans_elem


148 
val refl_red = refl_red


149 
val trans_red = trans_red


150 
val red_if_equal = red_if_equal


151 
val default_rls = arithC_rls @ comp_rls


152 
val routine_tac = routine_tac (arith_typing_rls @ routine_rls)


153 
end;


154 


155 
structure Arith_simp = TSimpFun (Arith_simp_data);


156 


157 
fun arith_rew_tac prems = make_rew_tac


158 
(Arith_simp.norm_tac(congr_rls, prems));


159 


160 
fun hyp_arith_rew_tac prems = make_rew_tac


161 
(Arith_simp.cond_norm_tac(prove_cond_tac, congr_rls, prems));


162 


163 


164 
(**********


165 
Addition


166 
**********)


167 


168 
(*Associative law for addition*)


169 
val add_assoc = prove_goal Arith.thy


170 
"[ a:N; b:N; c:N ] ==> (a #+ b) #+ c = a #+ (b #+ c) : N"


171 
(fn prems=>


172 
[ (NE_tac "a" 1),


173 
(hyp_arith_rew_tac prems) ]);


174 


175 


176 
(*Commutative law for addition. Can be proved using three inductions.


177 
Must simplify after first induction! Orientation of rewrites is delicate*)


178 
val add_commute = prove_goal Arith.thy


179 
"[ a:N; b:N ] ==> a #+ b = b #+ a : N"


180 
(fn prems=>


181 
[ (NE_tac "a" 1),


182 
(hyp_arith_rew_tac prems),


183 
(NE_tac "b" 2),


184 
(resolve_tac [sym_elem] 1),


185 
(NE_tac "b" 1),


186 
(hyp_arith_rew_tac prems) ]);


187 


188 


189 
(****************


190 
Multiplication


191 
****************)


192 


193 
(*Commutative law for multiplication


194 
val mult_commute = prove_goal Arith.thy


195 
"[ a:N; b:N ] ==> a #* b = b #* a : N"


196 
(fn prems=>


197 
[ (NE_tac "a" 1),


198 
(hyp_arith_rew_tac prems),


199 
(NE_tac "b" 2),


200 
(resolve_tac [sym_elem] 1),


201 
(NE_tac "b" 1),


202 
(hyp_arith_rew_tac prems) ]); NEEDS COMMUTATIVE MATCHING


203 
***************)


204 


205 
(*right annihilation in product*)


206 
val mult_0_right = prove_goal Arith.thy


207 
"a:N ==> a #* 0 = 0 : N"


208 
(fn prems=>


209 
[ (NE_tac "a" 1),


210 
(hyp_arith_rew_tac prems) ]);


211 


212 
(*right successor law for multiplication*)


213 
val mult_succ_right = prove_goal Arith.thy


214 
"[ a:N; b:N ] ==> a #* succ(b) = a #+ (a #* b) : N"


215 
(fn prems=>


216 
[ (NE_tac "a" 1),


217 
(*swap round the associative law of addition*)


218 
(hyp_arith_rew_tac (prems @ [add_assoc RS sym_elem])),


219 
(*leaves a goal involving a commutative law*)


220 
(REPEAT (assume_tac 1 ORELSE


221 
resolve_tac


222 
(prems@[add_commute,mult_typingL,add_typingL]@


223 
intrL_rls@[refl_elem]) 1)) ]);


224 


225 
(*Commutative law for multiplication*)


226 
val mult_commute = prove_goal Arith.thy


227 
"[ a:N; b:N ] ==> a #* b = b #* a : N"


228 
(fn prems=>


229 
[ (NE_tac "a" 1),


230 
(hyp_arith_rew_tac (prems @ [mult_0_right, mult_succ_right])) ]);


231 


232 
(*addition distributes over multiplication*)


233 
val add_mult_distrib = prove_goal Arith.thy


234 
"[ a:N; b:N; c:N ] ==> (a #+ b) #* c = (a #* c) #+ (b #* c) : N"


235 
(fn prems=>


236 
[ (NE_tac "a" 1),


237 
(*swap round the associative law of addition*)


238 
(hyp_arith_rew_tac (prems @ [add_assoc RS sym_elem])) ]);


239 


240 


241 
(*Associative law for multiplication*)


242 
val mult_assoc = prove_goal Arith.thy


243 
"[ a:N; b:N; c:N ] ==> (a #* b) #* c = a #* (b #* c) : N"


244 
(fn prems=>


245 
[ (NE_tac "a" 1),


246 
(hyp_arith_rew_tac (prems @ [add_mult_distrib])) ]);


247 


248 


249 
(************


250 
Difference


251 
************


252 


253 
Difference on natural numbers, without negative numbers


254 
a  b = 0 iff a<=b a  b = succ(c) iff a>b *)


255 


256 
val diff_self_eq_0 = prove_goal Arith.thy


257 
"a:N ==> a  a = 0 : N"


258 
(fn prems=>


259 
[ (NE_tac "a" 1),


260 
(hyp_arith_rew_tac prems) ]);


261 


262 


263 
(* [ c : N; 0 : N; c : N ] ==> c #+ 0 = c : N *)


264 
val add_0_right = addC0 RSN (3, add_commute RS trans_elem);


265 


266 
(*Addition is the inverse of subtraction: if b<=x then b#+(xb) = x.


267 
An example of induction over a quantified formula (a product).


268 
Uses rewriting with a quantified, implicative inductive hypothesis.*)


269 
val prems =


270 
goal Arith.thy


271 
"b:N ==> ?a : PROD x:N. Eq(N, bx, 0) > Eq(N, b #+ (xb), x)";


272 
by (NE_tac "b" 1);


273 
(*strip one "universal quantifier" but not the "implication"*)


274 
by (resolve_tac intr_rls 3);


275 
(*case analysis on x in


276 
(succ(u) <= x) > (succ(u)#+(xsucc(u)) = x) *)


277 
by (NE_tac "x" 4 THEN assume_tac 4);


278 
(*Prepare for simplification of types  the antecedent succ(u)<=x *)


279 
by (resolve_tac [replace_type] 5);


280 
by (resolve_tac [replace_type] 4);


281 
by (arith_rew_tac prems);


282 
(*Solves first 0 goal, simplifies others. Two sugbgoals remain.


283 
Both follow by rewriting, (2) using quantified induction hyp*)


284 
by (intr_tac[]); (*strips remaining PRODs*)


285 
by (hyp_arith_rew_tac (prems@[add_0_right]));


286 
by (assume_tac 1);


287 
val add_diff_inverse_lemma = result();


288 


289 


290 
(*Version of above with premise ba=0 i.e. a >= b.


291 
Using ProdE does not work  for ?B(?a) is ambiguous.


292 
Instead, add_diff_inverse_lemma states the desired induction scheme;


293 
the use of RS below instantiates Vars in ProdE automatically. *)


294 
val prems =


295 
goal Arith.thy "[ a:N; b:N; ba = 0 : N ] ==> b #+ (ab) = a : N";


296 
by (resolve_tac [EqE] 1);


297 
by (resolve_tac [ add_diff_inverse_lemma RS ProdE RS ProdE ] 1);


298 
by (REPEAT (resolve_tac (prems@[EqI]) 1));


299 
val add_diff_inverse = result();


300 


301 


302 
(********************


303 
Absolute difference


304 
********************)


305 


306 
(*typing of absolute difference: short and long versions*)


307 


308 
val absdiff_typing = prove_goal Arith.thy


309 
"[ a:N; b:N ] ==> a  b : N"


310 
(fn prems=>


311 
[ (rewrite_goals_tac arith_defs),


312 
(typechk_tac prems) ]);


313 


314 
val absdiff_typingL = prove_goal Arith.thy


315 
"[ a=c:N; b=d:N ] ==> a  b = c  d : N"


316 
(fn prems=>


317 
[ (rewrite_goals_tac arith_defs),


318 
(equal_tac prems) ]);


319 


320 
val absdiff_self_eq_0 = prove_goal Arith.thy


321 
"a:N ==> a  a = 0 : N"


322 
(fn prems=>


323 
[ (rewrite_goals_tac [absdiff_def]),


324 
(arith_rew_tac (prems@[diff_self_eq_0])) ]);


325 


326 
val absdiffC0 = prove_goal Arith.thy


327 
"a:N ==> 0  a = a : N"


328 
(fn prems=>


329 
[ (rewrite_goals_tac [absdiff_def]),


330 
(hyp_arith_rew_tac prems) ]);


331 


332 


333 
val absdiff_succ_succ = prove_goal Arith.thy


334 
"[ a:N; b:N ] ==> succ(a)  succ(b) = a  b : N"


335 
(fn prems=>


336 
[ (rewrite_goals_tac [absdiff_def]),


337 
(hyp_arith_rew_tac prems) ]);


338 


339 
(*Note how easy using commutative laws can be? ...not always... *)


340 
val prems = goal Arith.thy "[ a:N; b:N ] ==> a  b = b  a : N";


341 
by (rewrite_goals_tac [absdiff_def]);


342 
by (resolve_tac [add_commute] 1);


343 
by (typechk_tac ([diff_typing]@prems));


344 
val absdiff_commute = result();


345 


346 
(*If a+b=0 then a=0. Surprisingly tedious*)


347 
val prems =


348 
goal Arith.thy "[ a:N; b:N ] ==> ?c : PROD u: Eq(N,a#+b,0) . Eq(N,a,0)";


349 
by (NE_tac "a" 1);


350 
by (resolve_tac [replace_type] 3);


351 
by (arith_rew_tac prems);


352 
by (intr_tac[]); (*strips remaining PRODs*)


353 
by (resolve_tac [ zero_ne_succ RS FE ] 2);


354 
by (etac (EqE RS sym_elem) 3);


355 
by (typechk_tac ([add_typing] @prems));


356 
val add_eq0_lemma = result();


357 


358 
(*Version of above with the premise a+b=0.


359 
Again, resolution instantiates variables in ProdE *)


360 
val prems =


361 
goal Arith.thy "[ a:N; b:N; a #+ b = 0 : N ] ==> a = 0 : N";


362 
by (resolve_tac [EqE] 1);


363 
by (resolve_tac [add_eq0_lemma RS ProdE] 1);


364 
by (resolve_tac [EqI] 3);


365 
by (ALLGOALS (resolve_tac prems));


366 
val add_eq0 = result();


367 


368 
(*Here is a lemma to infer ab=0 and ba=0 from ab=0, below. *)


369 
val prems = goal Arith.thy


370 
"[ a:N; b:N; a  b = 0 : N ] ==> \


371 
\ ?a : SUM v: Eq(N, ab, 0) . Eq(N, ba, 0)";


372 
by (intr_tac[]);


373 
by eqintr_tac;


374 
by (resolve_tac [add_eq0] 2);


375 
by (resolve_tac [add_eq0] 1);


376 
by (resolve_tac [add_commute RS trans_elem] 6);


377 
by (typechk_tac (diff_typing:: map (rewrite_rule [absdiff_def]) prems));


378 
val absdiff_eq0_lem = result();


379 


380 
(*if a  b = 0 then a = b


381 
proof: ab=0 and ba=0, so b = a+(ba) = a+0 = a*)


382 
val prems =


383 
goal Arith.thy "[ a  b = 0 : N; a:N; b:N ] ==> a = b : N";


384 
by (resolve_tac [EqE] 1);


385 
by (resolve_tac [absdiff_eq0_lem RS SumE] 1);


386 
by (TRYALL (resolve_tac prems));


387 
by eqintr_tac;


388 
by (resolve_tac [add_diff_inverse RS sym_elem RS trans_elem] 1);


389 
by (resolve_tac [EqE] 3 THEN assume_tac 3);


390 
by (hyp_arith_rew_tac (prems@[add_0_right]));


391 
val absdiff_eq0 = result();


392 


393 
(***********************


394 
Remainder and Quotient


395 
***********************)


396 


397 
(*typing of remainder: short and long versions*)


398 


399 
val mod_typing = prove_goal Arith.thy


400 
"[ a:N; b:N ] ==> a mod b : N"


401 
(fn prems=>


402 
[ (rewrite_goals_tac [mod_def]),


403 
(typechk_tac (absdiff_typing::prems)) ]);


404 


405 
val mod_typingL = prove_goal Arith.thy


406 
"[ a=c:N; b=d:N ] ==> a mod b = c mod d : N"


407 
(fn prems=>


408 
[ (rewrite_goals_tac [mod_def]),


409 
(equal_tac (prems@[absdiff_typingL])) ]);


410 


411 


412 
(*computation for mod : 0 and successor cases*)


413 


414 
val modC0 = prove_goal Arith.thy "b:N ==> 0 mod b = 0 : N"


415 
(fn prems=>


416 
[ (rewrite_goals_tac [mod_def]),


417 
(rew_tac(absdiff_typing::prems)) ]);


418 


419 
val modC_succ = prove_goal Arith.thy


420 
"[ a:N; b:N ] ==> succ(a) mod b = rec(succ(a mod b)  b, 0, %x y.succ(a mod b)) : N"


421 
(fn prems=>


422 
[ (rewrite_goals_tac [mod_def]),


423 
(rew_tac(absdiff_typing::prems)) ]);


424 


425 


426 
(*typing of quotient: short and long versions*)


427 


428 
val div_typing = prove_goal Arith.thy "[ a:N; b:N ] ==> a div b : N"


429 
(fn prems=>


430 
[ (rewrite_goals_tac [div_def]),


431 
(typechk_tac ([absdiff_typing,mod_typing]@prems)) ]);


432 


433 
val div_typingL = prove_goal Arith.thy


434 
"[ a=c:N; b=d:N ] ==> a div b = c div d : N"


435 
(fn prems=>


436 
[ (rewrite_goals_tac [div_def]),


437 
(equal_tac (prems @ [absdiff_typingL, mod_typingL])) ]);


438 


439 
val div_typing_rls = [mod_typing, div_typing, absdiff_typing];


440 


441 


442 
(*computation for quotient: 0 and successor cases*)


443 


444 
val divC0 = prove_goal Arith.thy "b:N ==> 0 div b = 0 : N"


445 
(fn prems=>


446 
[ (rewrite_goals_tac [div_def]),


447 
(rew_tac([mod_typing, absdiff_typing] @ prems)) ]);


448 


449 
val divC_succ =


450 
prove_goal Arith.thy "[ a:N; b:N ] ==> succ(a) div b = \


451 
\ rec(succ(a) mod b, succ(a div b), %x y. a div b) : N"


452 
(fn prems=>


453 
[ (rewrite_goals_tac [div_def]),


454 
(rew_tac([mod_typing]@prems)) ]);


455 


456 


457 
(*Version of above with same condition as the mod one*)


458 
val divC_succ2 = prove_goal Arith.thy


459 
"[ a:N; b:N ] ==> \


460 
\ succ(a) div b =rec(succ(a mod b)  b, succ(a div b), %x y. a div b) : N"


461 
(fn prems=>


462 
[ (resolve_tac [ divC_succ RS trans_elem ] 1),


463 
(rew_tac(div_typing_rls @ prems @ [modC_succ])),


464 
(NE_tac "succ(a mod b)b" 1),


465 
(rew_tac ([mod_typing, div_typing, absdiff_typing] @prems)) ]);


466 


467 
(*for case analysis on whether a number is 0 or a successor*)


468 
val iszero_decidable = prove_goal Arith.thy


469 
"a:N ==> rec(a, inl(eq), %ka kb.inr(<ka, eq>)) : \


470 
\ Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))"


471 
(fn prems=>


472 
[ (NE_tac "a" 1),


473 
(resolve_tac [PlusI_inr] 3),


474 
(resolve_tac [PlusI_inl] 2),


475 
eqintr_tac,


476 
(equal_tac prems) ]);


477 


478 
(*Main Result. Holds when b is 0 since a mod 0 = a and a div 0 = 0 *)


479 
val prems =


480 
goal Arith.thy "[ a:N; b:N ] ==> a mod b #+ (a div b) #* b = a : N";


481 
by (NE_tac "a" 1);


482 
by (arith_rew_tac (div_typing_rls@prems@[modC0,modC_succ,divC0,divC_succ2]));


483 
by (resolve_tac [EqE] 1);


484 
(*case analysis on succ(u mod b)b *)


485 
by (res_inst_tac [("a1", "succ(u mod b)  b")]


486 
(iszero_decidable RS PlusE) 1);


487 
by (etac SumE 3);


488 
by (hyp_arith_rew_tac (prems @ div_typing_rls @


489 
[modC0,modC_succ, divC0, divC_succ2]));


490 
(*Replace one occurence of b by succ(u mod b). Clumsy!*)


491 
by (resolve_tac [ add_typingL RS trans_elem ] 1);


492 
by (eresolve_tac [EqE RS absdiff_eq0 RS sym_elem] 1);


493 
by (resolve_tac [refl_elem] 3);


494 
by (hyp_arith_rew_tac (prems @ div_typing_rls));


495 
val mod_div_equality = result();


496 


497 
writeln"Reached end of file.";
