12116Sjkh(*---------------------------------------------------------------------------*) 22116Sjkh(* An efficient divide-and-conquer-style exponentiation function. *) 32116Sjkh(*---------------------------------------------------------------------------*) 42116Sjkh 52116Sjkhload "numLib"; 62116Sjkhopen arithmeticTheory numLib; 72116Sjkh 88870Srgrimesval exp_def = 92116Sjkh Define 102116Sjkh `(exp x 0 = 1) /\ 112116Sjkh (exp x n = if EVEN n then 122116Sjkh let k = exp x (n DIV 2) in k * k 13176451Sdas else x * exp x (n-1))`; 14176451Sdas 152116Sjkhval exp_ind = fetch "-" "exp_ind"; 162116Sjkh 172116Sjkh(*---------------------------------------------------------------------------*) 182116Sjkh(* A form of correctness: exp is equal to the prim. rec defn. of EXP *) 192116Sjkh(* given by: *) 202116Sjkh(* *) 212116Sjkh(* m EXP 0 = 1 *) 222116Sjkh(* m EXP (SUC n) = m * m EXP n *) 232116Sjkh(* *) 242116Sjkh(*---------------------------------------------------------------------------*) 252116Sjkh 26175309Sdasval EXP_eq_exp = Q.prove 27175309Sdas(`!x m. x EXP m = exp x m`, 282116Sjkh recInduct exp_ind 292116Sjkh THEN RW_TAC arith_ss [EXP, exp_def, LET_THM, EVEN_MOD2] 302116Sjkh THEN POP_ASSUM (SUBST1_TAC o SYM) 31153043Sbde THEN RW_TAC arith_ss [GSYM EXP_ADD,GSYM EXP_EXP_MULT] 322116Sjkh THEN METIS_TAC [DIVISION, DECIDE ``0<2``, ADD_0, MULT_SYM, EXP]); 332116Sjkh 342116Sjkh 352116Sjkh(*---------------------------------------------------------------------------*) 362116Sjkh(* Some computations with exp. We first have to come up with a version of *) 3797413Salfred(* exp where SUC constructors are not on the lhs of the recursion equation. *) 38117912Speter(*---------------------------------------------------------------------------*) 392116Sjkh 402116Sjkhval alt_exp_eqns = Q.prove 412116Sjkh(`exp x n = 422116Sjkh if n=0 then 1 else 432116Sjkh if n=1 then x else 442116Sjkh if EVEN n 452116Sjkh then let v = exp x (n DIV 2) in v * v 462116Sjkh else x * exp x (n-1)`, 478870Srgrimes Cases_on `n` THENL [ALL_TAC, Cases_on `n'`] THEN 482116Sjkh RW_TAC arith_ss [exp_def]); 492116Sjkh 502116Sjkhval _ = computeLib.add_funs [alt_exp_eqns]; 512116Sjkh 522116SjkhEVAL ``exp 2 1``; 53175480SbdeEVAL ``exp 2 4 * exp 4 2``; 542116SjkhEVAL ``exp 2 10``; 552116SjkhEVAL ``exp 2 16``; 562116SjkhEVAL ``exp 2 100``; 572116Sjkh 582116Sjkh(*--------------------------------------------------------------------------- 592116Sjkh REDUCE_CONV is faster than EVAL for exp because of how numerals 602116Sjkh are represented. 612116Sjkh ---------------------------------------------------------------------------*) 622116Sjkh 63153042SbdeCount.apply EVAL ``exp 2 500``; 64153042SbdeCount.apply REDUCE_CONV ``2 EXP 500``; 65153042Sbde