(* Exponential representation of natural numbers *)

(* Dependencies *)
needs "../formal_lp/arith/nat.hl";;


module Num_exp_theory = struct

open Arith_options;;


let base_const = mk_small_numeral base;;

(* num_exp definition *)
let num_exp_tm = mk_eq (`(num_exp:num->num->num) n e`,
                        mk_binop `( * ):num->num->num` `n:num` (mk_binop `EXP` base_const `e:num`));;
(* let num_exp = new_definition `num_exp n e = n * 2 EXP e`;; *)
let num_exp = new_definition num_exp_tm;;

(**********************************)
(* Theorems *)

let NUM_EXP_EXP = 
prove(`!n e1 e2. num_exp (num_exp n e1) e2 = num_exp n (e1 + e2)`,

   REPEAT GEN_TAC THEN
     REWRITE_TAC[num_exp; EXP_ADD] THEN
     ARITH_TAC);;

	 
let NUM_EXP_SUM = 
prove(`!n e1 e2. num_exp n (e1 + e2) = num_exp n e1 * num_exp 1 e2`,

   REPEAT GEN_TAC THEN
     REWRITE_TAC[num_exp; EXP_ADD] THEN
     ARITH_TAC);;


let NUM_EXP_SUM1 = 
prove(`!n e1 e2. num_exp n (e1 + e2) = num_exp 1 e1 * num_exp n e2`,

                         REPEAT GEN_TAC THEN REWRITE_TAC[num_exp; EXP_ADD] THEN ARITH_TAC);;

let NUM_EXP_0 = 
prove(`!n. n = num_exp n 0`,

                      GEN_TAC THEN REWRITE_TAC[num_exp; EXP; MULT_CLAUSES]);;

let NUM_EXP_LE = 
prove(`!m n e. m <= n ==> num_exp m e <= num_exp n e`,

     SIMP_TAC[num_exp; LE_MULT_RCANCEL]);;

let NUM_EXP_LT = 
prove(`!m n e. m < n ==> num_exp m e < num_exp n e`,

                       SIMP_TAC[num_exp; LT_MULT_RCANCEL; EXP_EQ_0] THEN
                         ARITH_TAC);;

let NUM_EXP_EQ_0 = 
prove(`!n e. num_exp n e = 0 <=> n = 0`,

   REPEAT STRIP_TAC THEN
     ASM_REWRITE_TAC[num_exp; MULT_EQ_0; EXP_EQ_0] THEN
     ARITH_TAC);;

let NUM_EXP_MUL = 
prove(`!n1 e1 n2 e2. num_exp n1 e1 * num_exp n2 e2 = num_exp (n1 * n2) (e1 + e2)`,

                        REWRITE_TAC[num_exp; EXP_ADD] THEN ARITH_TAC);;

let NUM_EXP_ADD = 
prove(`!n1 e1 n2 e2. e1 <= e2 ==>
                          num_exp n1 e1 + num_exp n2 e2 = num_exp (n1 + num_exp n2 (e2 - e1)) e1`,

   REPEAT STRIP_TAC THEN
     REWRITE_TAC[num_exp] THEN
     REWRITE_TAC[ARITH_RULE `(a + b * c) * d = a * d + b * (c * d):num`] THEN
     REWRITE_TAC[GSYM EXP_ADD] THEN
     ASM_SIMP_TAC[ARITH_RULE `e1 <= e2 ==> e2 - e1 + e1 = e2:num`]);;

let NUM_EXP_SUB2 = 
prove(`!n1 e1 n2 e2 r. e1 <= e2 /\ e2 - e1 = r ==>
			   num_exp n1 e1 - num_exp n2 e2 = num_exp (n1 - num_exp n2 r) e1`,

   REPEAT STRIP_TAC THEN
     POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
     REWRITE_TAC[num_exp] THEN
     MP_TAC (ARITH_RULE `e1 <= e2 ==> e2 = (e2 - e1) + e1:num`) THEN
     ASM_REWRITE_TAC[] THEN
     DISCH_THEN (fun th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th]) THEN
     REWRITE_TAC[EXP_ADD; MULT_ASSOC] THEN
     REWRITE_TAC[GSYM RIGHT_SUB_DISTRIB]);;

let NUM_EXP_SUB1 = 
prove(`!n1 e1 n2 e2 r. e2 <= e1 /\ e1 - e2 = r ==>
			   num_exp n1 e1 - num_exp n2 e2 = num_exp (num_exp n1 r - n2) e2`,

   REPEAT STRIP_TAC THEN
     POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
     REWRITE_TAC[num_exp] THEN
     MP_TAC (ARITH_RULE `e2 <= e1 ==> e1 = (e1 - e2) + e2:num`) THEN
     ASM_REWRITE_TAC[] THEN
     DISCH_THEN (fun th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th]) THEN
     REWRITE_TAC[EXP_ADD; MULT_ASSOC] THEN
     REWRITE_TAC[GSYM RIGHT_SUB_DISTRIB]);;

(* NUM_EXP_LE *)

let NUM_EXP_LE1 = 
prove(`!n1 e1 n2 e2 r. e2 <= e1 /\ e1 - e2 = r /\ n2 <= num_exp n1 r
			      ==> num_exp n2 e2 <= num_exp n1 e1`,

   REPEAT GEN_TAC THEN REWRITE_TAC[num_exp] THEN
     STRIP_TAC THEN
     POP_ASSUM MP_TAC THEN POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN DISCH_TAC THEN
     MP_TAC (ARITH_RULE `e2 <= e1 ==> e1 = (e1 - e2) + e2:num`) THEN
     ASM_REWRITE_TAC[] THEN
     DISCH_THEN(fun th -> ONCE_REWRITE_TAC[th]) THEN
     REWRITE_TAC[EXP_ADD; MULT_ASSOC] THEN
     ASM_REWRITE_TAC[LE_MULT_RCANCEL]);;

let NUM_EXP_LE2 = 
prove(`!n1 e1 n2 e2 r. e1 <= e2 /\ e2 - e1 = r /\ num_exp n2 r <= n1
			      ==> num_exp n2 e2 <= num_exp n1 e1`,

   REPEAT GEN_TAC THEN REWRITE_TAC[num_exp] THEN
     STRIP_TAC THEN
     POP_ASSUM MP_TAC THEN POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN DISCH_TAC THEN
     MP_TAC (ARITH_RULE `e1 <= e2 ==> e2 = (e2 - e1) + e1:num`) THEN
     ASM_REWRITE_TAC[] THEN
     DISCH_THEN(fun th -> ONCE_REWRITE_TAC[th]) THEN
     REWRITE_TAC[EXP_ADD; MULT_ASSOC] THEN
     ASM_REWRITE_TAC[LE_MULT_RCANCEL]);;

let NUM_EXP_LE1_EQ = 
prove(`!n1 e1 n2 e2 r x. e2 <= e1 /\ e1 - e2 = r /\ num_exp n1 r = x ==>
			       (num_exp n1 e1 <= num_exp n2 e2 <=> x <= n2)`,

   REPEAT GEN_TAC THEN REWRITE_TAC[num_exp] THEN
     STRIP_TAC THEN
     REPLICATE_TAC 2 (POP_ASSUM (fun th -> REWRITE_TAC[SYM th])) THEN
     MP_TAC (ARITH_RULE `e2 <= e1 ==> e1 = (e1 - e2) + e2:num`) THEN
     ASM_REWRITE_TAC[] THEN
     DISCH_THEN (fun th -> GEN_REWRITE_TAC (LAND_CONV o DEPTH_CONV) [th]) THEN
     REWRITE_TAC[EXP_ADD; MULT_ASSOC] THEN
     ASM_REWRITE_TAC[LE_MULT_RCANCEL; EXP_EQ_0; ARITH_EQ]);;

let NUM_EXP_LE2_EQ = 
prove(`!n1 e1 n2 e2 r x. e1 <= e2 /\ e2 - e1 = r /\ num_exp n2 r = x ==>
			       (num_exp n1 e1 <= num_exp n2 e2 <=> n1 <= x)`,

   REPEAT GEN_TAC THEN REWRITE_TAC[num_exp] THEN
     STRIP_TAC THEN
     REPLICATE_TAC 2 (POP_ASSUM (fun th -> REWRITE_TAC[SYM th])) THEN
     MP_TAC (ARITH_RULE `e1 <= e2 ==> e2 = (e2 - e1) + e1:num`) THEN
     ASM_REWRITE_TAC[] THEN
     DISCH_THEN (fun th -> GEN_REWRITE_TAC (LAND_CONV o DEPTH_CONV) [th]) THEN
     REWRITE_TAC[EXP_ADD; MULT_ASSOC] THEN
     ASM_REWRITE_TAC[LE_MULT_RCANCEL; EXP_EQ_0; ARITH_EQ]);;

(* NUM_EXP_LT *)

let NUM_EXP_LT1 = 
prove(`!n1 e1 n2 e2 r. e2 <= e1 /\ e1 - e2 = r /\ n2 < num_exp n1 r
			    ==> num_exp n2 e2 < num_exp n1 e1`,

   REPEAT GEN_TAC THEN REWRITE_TAC[num_exp] THEN
     STRIP_TAC THEN
     POP_ASSUM MP_TAC THEN POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN DISCH_TAC THEN
     MP_TAC (ARITH_RULE `e2 <= e1 ==> e1 = (e1 - e2) + e2:num`) THEN
     ASM_REWRITE_TAC[] THEN
     DISCH_THEN (fun th -> ONCE_REWRITE_TAC[th]) THEN
     REWRITE_TAC[EXP_ADD; MULT_ASSOC] THEN
     ASM_REWRITE_TAC[LT_MULT_RCANCEL; EXP_EQ_0; ARITH_EQ]);;



let NUM_EXP_LT2 = 
prove(`!n1 e1 n2 e2 r. e1 <= e2 /\ e2 - e1 = r /\ num_exp n2 r < n1
			    ==> num_exp n2 e2 < num_exp n1 e1`,

   REPEAT GEN_TAC THEN REWRITE_TAC[num_exp] THEN
     STRIP_TAC THEN
     POP_ASSUM MP_TAC THEN POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN DISCH_TAC THEN
     MP_TAC (ARITH_RULE `e1 <= e2 ==> e2 = (e2 - e1) + e1:num`) THEN
     ASM_REWRITE_TAC[] THEN
     DISCH_THEN (fun th -> ONCE_REWRITE_TAC[th]) THEN
     REWRITE_TAC[EXP_ADD; MULT_ASSOC] THEN
     ASM_REWRITE_TAC[LT_MULT_RCANCEL; EXP_EQ_0; ARITH_EQ]);;

     
     
let NUM_EXP_LT1_EQ = 
prove(`!n1 e1 n2 e2 r x. e2 <= e1 /\ e1 - e2 = r /\ num_exp n1 r = x ==>
			       (num_exp n1 e1 < num_exp n2 e2 <=> x < n2)`,

   REPEAT GEN_TAC THEN REWRITE_TAC[num_exp] THEN
     STRIP_TAC THEN
     REPLICATE_TAC 2 (POP_ASSUM (fun th -> REWRITE_TAC[SYM th])) THEN
     MP_TAC (ARITH_RULE `e2 <= e1 ==> e1 = (e1 - e2) + e2:num`) THEN
     ASM_REWRITE_TAC[] THEN
     DISCH_THEN (fun th -> GEN_REWRITE_TAC (LAND_CONV o DEPTH_CONV) [th]) THEN
     REWRITE_TAC[EXP_ADD; MULT_ASSOC] THEN
     ASM_REWRITE_TAC[LT_MULT_RCANCEL; EXP_EQ_0; ARITH_EQ]);;



let NUM_EXP_LT2_EQ = 
prove(`!n1 e1 n2 e2 r x. e1 <= e2 /\ e2 - e1 = r /\ num_exp n2 r = x ==>
			       (num_exp n1 e1 < num_exp n2 e2 <=> n1 < x)`,

   REPEAT GEN_TAC THEN REWRITE_TAC[num_exp] THEN
     STRIP_TAC THEN
     REPLICATE_TAC 2 (POP_ASSUM (fun th -> REWRITE_TAC[SYM th])) THEN
     MP_TAC (ARITH_RULE `e1 <= e2 ==> e2 = (e2 - e1) + e1:num`) THEN
     ASM_REWRITE_TAC[] THEN
     DISCH_THEN (fun th -> GEN_REWRITE_TAC (LAND_CONV o DEPTH_CONV) [th]) THEN
     REWRITE_TAC[EXP_ADD; MULT_ASSOC] THEN
     ASM_REWRITE_TAC[LT_MULT_RCANCEL; EXP_EQ_0; ARITH_EQ]);;

end;;