1 (* Exponential representation of natural numbers *)
\r
4 needs "../formal_lp/arith/nat.hl";;
\r
7 module Num_exp_theory = struct
\r
12 let base_const = mk_small_numeral base;;
\r
14 (* num_exp definition *)
\r
15 let num_exp_tm = mk_eq (`(num_exp:num->num->num) n e`,
\r
16 mk_binop `( * ):num->num->num` `n:num` (mk_binop `EXP` base_const `e:num`));;
\r
17 (* let num_exp = new_definition `num_exp n e = n * 2 EXP e`;; *)
\r
18 let num_exp = new_definition num_exp_tm;;
\r
20 (**********************************)
\r
23 let NUM_EXP_EXP = prove(`!n e1 e2. num_exp (num_exp n e1) e2 = num_exp n (e1 + e2)`,
\r
25 REWRITE_TAC[num_exp; EXP_ADD] THEN
\r
29 let NUM_EXP_SUM = prove(`!n e1 e2. num_exp n (e1 + e2) = num_exp n e1 * num_exp 1 e2`,
\r
31 REWRITE_TAC[num_exp; EXP_ADD] THEN
\r
35 let NUM_EXP_SUM1 = prove(`!n e1 e2. num_exp n (e1 + e2) = num_exp 1 e1 * num_exp n e2`,
\r
36 REPEAT GEN_TAC THEN REWRITE_TAC[num_exp; EXP_ADD] THEN ARITH_TAC);;
\r
38 let NUM_EXP_0 = prove(`!n. n = num_exp n 0`,
\r
39 GEN_TAC THEN REWRITE_TAC[num_exp; EXP; MULT_CLAUSES]);;
\r
41 let NUM_EXP_LE = prove(`!m n e. m <= n ==> num_exp m e <= num_exp n e`,
\r
42 SIMP_TAC[num_exp; LE_MULT_RCANCEL]);;
\r
44 let NUM_EXP_LT = prove(`!m n e. m < n ==> num_exp m e < num_exp n e`,
\r
45 SIMP_TAC[num_exp; LT_MULT_RCANCEL; EXP_EQ_0] THEN
\r
48 let NUM_EXP_EQ_0 = prove(`!n e. num_exp n e = 0 <=> n = 0`,
\r
49 REPEAT STRIP_TAC THEN
\r
50 ASM_REWRITE_TAC[num_exp; MULT_EQ_0; EXP_EQ_0] THEN
\r
53 let NUM_EXP_MUL = prove(`!n1 e1 n2 e2. num_exp n1 e1 * num_exp n2 e2 = num_exp (n1 * n2) (e1 + e2)`,
\r
54 REWRITE_TAC[num_exp; EXP_ADD] THEN ARITH_TAC);;
\r
56 let NUM_EXP_ADD = prove(`!n1 e1 n2 e2. e1 <= e2 ==>
\r
57 num_exp n1 e1 + num_exp n2 e2 = num_exp (n1 + num_exp n2 (e2 - e1)) e1`,
\r
58 REPEAT STRIP_TAC THEN
\r
59 REWRITE_TAC[num_exp] THEN
\r
60 REWRITE_TAC[ARITH_RULE `(a + b * c) * d = a * d + b * (c * d):num`] THEN
\r
61 REWRITE_TAC[GSYM EXP_ADD] THEN
\r
62 ASM_SIMP_TAC[ARITH_RULE `e1 <= e2 ==> e2 - e1 + e1 = e2:num`]);;
\r
64 let NUM_EXP_SUB2 = prove(`!n1 e1 n2 e2 r. e1 <= e2 /\ e2 - e1 = r ==>
\r
65 num_exp n1 e1 - num_exp n2 e2 = num_exp (n1 - num_exp n2 r) e1`,
\r
66 REPEAT STRIP_TAC THEN
\r
67 POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
\r
68 REWRITE_TAC[num_exp] THEN
\r
69 MP_TAC (ARITH_RULE `e1 <= e2 ==> e2 = (e2 - e1) + e1:num`) THEN
\r
70 ASM_REWRITE_TAC[] THEN
\r
71 DISCH_THEN (fun th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th]) THEN
\r
72 REWRITE_TAC[EXP_ADD; MULT_ASSOC] THEN
\r
73 REWRITE_TAC[GSYM RIGHT_SUB_DISTRIB]);;
\r
75 let NUM_EXP_SUB1 = prove(`!n1 e1 n2 e2 r. e2 <= e1 /\ e1 - e2 = r ==>
\r
76 num_exp n1 e1 - num_exp n2 e2 = num_exp (num_exp n1 r - n2) e2`,
\r
77 REPEAT STRIP_TAC THEN
\r
78 POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
\r
79 REWRITE_TAC[num_exp] THEN
\r
80 MP_TAC (ARITH_RULE `e2 <= e1 ==> e1 = (e1 - e2) + e2:num`) THEN
\r
81 ASM_REWRITE_TAC[] THEN
\r
82 DISCH_THEN (fun th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th]) THEN
\r
83 REWRITE_TAC[EXP_ADD; MULT_ASSOC] THEN
\r
84 REWRITE_TAC[GSYM RIGHT_SUB_DISTRIB]);;
\r
88 let NUM_EXP_LE1 = prove(`!n1 e1 n2 e2 r. e2 <= e1 /\ e1 - e2 = r /\ n2 <= num_exp n1 r
\r
89 ==> num_exp n2 e2 <= num_exp n1 e1`,
\r
90 REPEAT GEN_TAC THEN REWRITE_TAC[num_exp] THEN
\r
92 POP_ASSUM MP_TAC THEN POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN DISCH_TAC THEN
\r
93 MP_TAC (ARITH_RULE `e2 <= e1 ==> e1 = (e1 - e2) + e2:num`) THEN
\r
94 ASM_REWRITE_TAC[] THEN
\r
95 DISCH_THEN(fun th -> ONCE_REWRITE_TAC[th]) THEN
\r
96 REWRITE_TAC[EXP_ADD; MULT_ASSOC] THEN
\r
97 ASM_REWRITE_TAC[LE_MULT_RCANCEL]);;
\r
99 let NUM_EXP_LE2 = prove(`!n1 e1 n2 e2 r. e1 <= e2 /\ e2 - e1 = r /\ num_exp n2 r <= n1
\r
100 ==> num_exp n2 e2 <= num_exp n1 e1`,
\r
101 REPEAT GEN_TAC THEN REWRITE_TAC[num_exp] THEN
\r
103 POP_ASSUM MP_TAC THEN POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN DISCH_TAC THEN
\r
104 MP_TAC (ARITH_RULE `e1 <= e2 ==> e2 = (e2 - e1) + e1:num`) THEN
\r
105 ASM_REWRITE_TAC[] THEN
\r
106 DISCH_THEN(fun th -> ONCE_REWRITE_TAC[th]) THEN
\r
107 REWRITE_TAC[EXP_ADD; MULT_ASSOC] THEN
\r
108 ASM_REWRITE_TAC[LE_MULT_RCANCEL]);;
\r
110 let NUM_EXP_LE1_EQ = prove(`!n1 e1 n2 e2 r x. e2 <= e1 /\ e1 - e2 = r /\ num_exp n1 r = x ==>
\r
111 (num_exp n1 e1 <= num_exp n2 e2 <=> x <= n2)`,
\r
112 REPEAT GEN_TAC THEN REWRITE_TAC[num_exp] THEN
\r
114 REPLICATE_TAC 2 (POP_ASSUM (fun th -> REWRITE_TAC[SYM th])) THEN
\r
115 MP_TAC (ARITH_RULE `e2 <= e1 ==> e1 = (e1 - e2) + e2:num`) THEN
\r
116 ASM_REWRITE_TAC[] THEN
\r
117 DISCH_THEN (fun th -> GEN_REWRITE_TAC (LAND_CONV o DEPTH_CONV) [th]) THEN
\r
118 REWRITE_TAC[EXP_ADD; MULT_ASSOC] THEN
\r
119 ASM_REWRITE_TAC[LE_MULT_RCANCEL; EXP_EQ_0; ARITH_EQ]);;
\r
121 let NUM_EXP_LE2_EQ = prove(`!n1 e1 n2 e2 r x. e1 <= e2 /\ e2 - e1 = r /\ num_exp n2 r = x ==>
\r
122 (num_exp n1 e1 <= num_exp n2 e2 <=> n1 <= x)`,
\r
123 REPEAT GEN_TAC THEN REWRITE_TAC[num_exp] THEN
\r
125 REPLICATE_TAC 2 (POP_ASSUM (fun th -> REWRITE_TAC[SYM th])) THEN
\r
126 MP_TAC (ARITH_RULE `e1 <= e2 ==> e2 = (e2 - e1) + e1:num`) THEN
\r
127 ASM_REWRITE_TAC[] THEN
\r
128 DISCH_THEN (fun th -> GEN_REWRITE_TAC (LAND_CONV o DEPTH_CONV) [th]) THEN
\r
129 REWRITE_TAC[EXP_ADD; MULT_ASSOC] THEN
\r
130 ASM_REWRITE_TAC[LE_MULT_RCANCEL; EXP_EQ_0; ARITH_EQ]);;
\r
134 let NUM_EXP_LT1 = prove(`!n1 e1 n2 e2 r. e2 <= e1 /\ e1 - e2 = r /\ n2 < num_exp n1 r
\r
135 ==> num_exp n2 e2 < num_exp n1 e1`,
\r
136 REPEAT GEN_TAC THEN REWRITE_TAC[num_exp] THEN
\r
138 POP_ASSUM MP_TAC THEN POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN DISCH_TAC THEN
\r
139 MP_TAC (ARITH_RULE `e2 <= e1 ==> e1 = (e1 - e2) + e2:num`) THEN
\r
140 ASM_REWRITE_TAC[] THEN
\r
141 DISCH_THEN (fun th -> ONCE_REWRITE_TAC[th]) THEN
\r
142 REWRITE_TAC[EXP_ADD; MULT_ASSOC] THEN
\r
143 ASM_REWRITE_TAC[LT_MULT_RCANCEL; EXP_EQ_0; ARITH_EQ]);;
\r
147 let NUM_EXP_LT2 = prove(`!n1 e1 n2 e2 r. e1 <= e2 /\ e2 - e1 = r /\ num_exp n2 r < n1
\r
148 ==> num_exp n2 e2 < num_exp n1 e1`,
\r
149 REPEAT GEN_TAC THEN REWRITE_TAC[num_exp] THEN
\r
151 POP_ASSUM MP_TAC THEN POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN DISCH_TAC THEN
\r
152 MP_TAC (ARITH_RULE `e1 <= e2 ==> e2 = (e2 - e1) + e1:num`) THEN
\r
153 ASM_REWRITE_TAC[] THEN
\r
154 DISCH_THEN (fun th -> ONCE_REWRITE_TAC[th]) THEN
\r
155 REWRITE_TAC[EXP_ADD; MULT_ASSOC] THEN
\r
156 ASM_REWRITE_TAC[LT_MULT_RCANCEL; EXP_EQ_0; ARITH_EQ]);;
\r
160 let NUM_EXP_LT1_EQ = prove(`!n1 e1 n2 e2 r x. e2 <= e1 /\ e1 - e2 = r /\ num_exp n1 r = x ==>
\r
161 (num_exp n1 e1 < num_exp n2 e2 <=> x < n2)`,
\r
162 REPEAT GEN_TAC THEN REWRITE_TAC[num_exp] THEN
\r
164 REPLICATE_TAC 2 (POP_ASSUM (fun th -> REWRITE_TAC[SYM th])) THEN
\r
165 MP_TAC (ARITH_RULE `e2 <= e1 ==> e1 = (e1 - e2) + e2:num`) THEN
\r
166 ASM_REWRITE_TAC[] THEN
\r
167 DISCH_THEN (fun th -> GEN_REWRITE_TAC (LAND_CONV o DEPTH_CONV) [th]) THEN
\r
168 REWRITE_TAC[EXP_ADD; MULT_ASSOC] THEN
\r
169 ASM_REWRITE_TAC[LT_MULT_RCANCEL; EXP_EQ_0; ARITH_EQ]);;
\r
173 let NUM_EXP_LT2_EQ = prove(`!n1 e1 n2 e2 r x. e1 <= e2 /\ e2 - e1 = r /\ num_exp n2 r = x ==>
\r
174 (num_exp n1 e1 < num_exp n2 e2 <=> n1 < x)`,
\r
175 REPEAT GEN_TAC THEN REWRITE_TAC[num_exp] THEN
\r
177 REPLICATE_TAC 2 (POP_ASSUM (fun th -> REWRITE_TAC[SYM th])) THEN
\r
178 MP_TAC (ARITH_RULE `e1 <= e2 ==> e2 = (e2 - e1) + e1:num`) THEN
\r
179 ASM_REWRITE_TAC[] THEN
\r
180 DISCH_THEN (fun th -> GEN_REWRITE_TAC (LAND_CONV o DEPTH_CONV) [th]) THEN
\r
181 REWRITE_TAC[EXP_ADD; MULT_ASSOC] THEN
\r
182 ASM_REWRITE_TAC[LT_MULT_RCANCEL; EXP_EQ_0; ARITH_EQ]);;
\r