formal_ineqs/arith/num_exp_theory.hl

   1 (* =========================================================== *)\r
   2 (* Exponential representation of natural numbers               *)\r
   3 (* Author: Alexey Solovyev                                     *)\r
   4 (* Date: 2012-10-27                                            *)\r
   5 (* =========================================================== *)\r
   6 \r
   7 (* Dependencies *)\r
   8 needs "arith/nat.hl";;\r
   9 \r
  10 \r
  11 module Num_exp_theory = struct\r
  12 \r
  13 let base_const = mk_small_numeral Arith_hash.arith_base;;\r
  14 \r
  15 (* num_exp definition *)\r
  16 let num_exp_tm = mk_eq (`(num_exp:num->num->num) n e`,\r
  17                         mk_binop `( * ):num->num->num` `n:num` (mk_binop `EXP` base_const `e:num`));;\r
  18 (* let num_exp = new_definition `num_exp n e = n * 2 EXP e`;; *)\r
  19 let num_exp = new_definition num_exp_tm;;\r
  20 \r
  21 (**********************************)\r
  22 (* Theorems *)\r
  23 \r
  24 let NUM_EXP_EXP = prove(`!n e1 e2. num_exp (num_exp n e1) e2 = num_exp n (e1 + e2)`,\r
  25    REPEAT GEN_TAC THEN\r
  26      REWRITE_TAC[num_exp; EXP_ADD] THEN\r
  27      ARITH_TAC);;\r
  28 \r
  29 let NUM_EXP_SUM = prove(`!n e1 e2. num_exp n (e1 + e2) = num_exp n e1 * num_exp 1 e2`,\r
  30    REPEAT GEN_TAC THEN\r
  31      REWRITE_TAC[num_exp; EXP_ADD] THEN\r
  32      ARITH_TAC);;\r
  33 \r
  34 let NUM_EXP_SUM1 = prove(`!n e1 e2. num_exp n (e1 + e2) = num_exp 1 e1 * num_exp n e2`,\r
  35                          REPEAT GEN_TAC THEN REWRITE_TAC[num_exp; EXP_ADD] THEN ARITH_TAC);;\r
  36 \r
  37 let NUM_EXP_0 = prove(`!n. n = num_exp n 0`,\r
  38                       GEN_TAC THEN REWRITE_TAC[num_exp; EXP; MULT_CLAUSES]);;\r
  39 \r
  40 let NUM_EXP_LE = prove(`!m n e. m <= n ==> num_exp m e <= num_exp n e`,\r
  41      SIMP_TAC[num_exp; LE_MULT_RCANCEL]);;\r
  42 \r
  43 let NUM_EXP_LT = prove(`!m n e. m < n ==> num_exp m e < num_exp n e`,\r
  44                        SIMP_TAC[num_exp; LT_MULT_RCANCEL; EXP_EQ_0] THEN\r
  45                          ARITH_TAC);;\r
  46 \r
  47 let NUM_EXP_EQ_0 = prove(`!n e. num_exp n e = 0 <=> n = 0`,\r
  48    REPEAT STRIP_TAC THEN\r
  49      ASM_REWRITE_TAC[num_exp; MULT_EQ_0; EXP_EQ_0] THEN\r
  50      ARITH_TAC);;\r
  51 \r
  52 let NUM_EXP_MUL = prove(`!n1 e1 n2 e2. num_exp n1 e1 * num_exp n2 e2 = num_exp (n1 * n2) (e1 + e2)`,\r
  53                         REWRITE_TAC[num_exp; EXP_ADD] THEN ARITH_TAC);;\r
  54 \r
  55 let NUM_EXP_ADD = prove(`!n1 e1 n2 e2. e1 <= e2 ==>\r
  56                           num_exp n1 e1 + num_exp n2 e2 = num_exp (n1 + num_exp n2 (e2 - e1)) e1`,\r
  57    REPEAT STRIP_TAC THEN\r
  58      REWRITE_TAC[num_exp] THEN\r
  59      REWRITE_TAC[ARITH_RULE `(a + b * c) * d = a * d + b * (c * d):num`] THEN\r
  60      REWRITE_TAC[GSYM EXP_ADD] THEN\r
  61      ASM_SIMP_TAC[ARITH_RULE `e1 <= e2 ==> e2 - e1 + e1 = e2:num`]);;\r
  62 \r
  63 let NUM_EXP_SUB2 = prove(`!n1 e1 n2 e2 r. e1 <= e2 /\ e2 - e1 = r ==>\r
  64                            num_exp n1 e1 - num_exp n2 e2 = num_exp (n1 - num_exp n2 r) e1`,\r
  65    REPEAT STRIP_TAC THEN\r
  66      POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN\r
  67      REWRITE_TAC[num_exp] THEN\r
  68      MP_TAC (ARITH_RULE `e1 <= e2 ==> e2 = (e2 - e1) + e1:num`) THEN\r
  69      ASM_REWRITE_TAC[] THEN\r
  70      DISCH_THEN (fun th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th]) THEN\r
  71      REWRITE_TAC[EXP_ADD; MULT_ASSOC] THEN\r
  72      REWRITE_TAC[GSYM RIGHT_SUB_DISTRIB]);;\r
  73 \r
  74 let NUM_EXP_SUB1 = prove(`!n1 e1 n2 e2 r. e2 <= e1 /\ e1 - e2 = r ==>\r
  75                            num_exp n1 e1 - num_exp n2 e2 = num_exp (num_exp n1 r - n2) e2`,\r
  76    REPEAT STRIP_TAC THEN\r
  77      POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN\r
  78      REWRITE_TAC[num_exp] THEN\r
  79      MP_TAC (ARITH_RULE `e2 <= e1 ==> e1 = (e1 - e2) + e2:num`) THEN\r
  80      ASM_REWRITE_TAC[] THEN\r
  81      DISCH_THEN (fun th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th]) THEN\r
  82      REWRITE_TAC[EXP_ADD; MULT_ASSOC] THEN\r
  83      REWRITE_TAC[GSYM RIGHT_SUB_DISTRIB]);;\r
  84 \r
  85 (* NUM_EXP_LE *)\r
  86 \r
  87 let NUM_EXP_LE1 = prove(`!n1 e1 n2 e2 r. e2 <= e1 /\ e1 - e2 = r /\ n2 <= num_exp n1 r\r
  88                               ==> num_exp n2 e2 <= num_exp n1 e1`,\r
  89    REPEAT GEN_TAC THEN REWRITE_TAC[num_exp] THEN\r
  90      STRIP_TAC THEN\r
  91      POP_ASSUM MP_TAC THEN POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN DISCH_TAC THEN\r
  92      MP_TAC (ARITH_RULE `e2 <= e1 ==> e1 = (e1 - e2) + e2:num`) THEN\r
  93      ASM_REWRITE_TAC[] THEN\r
  94      DISCH_THEN(fun th -> ONCE_REWRITE_TAC[th]) THEN\r
  95      REWRITE_TAC[EXP_ADD; MULT_ASSOC] THEN\r
  96      ASM_REWRITE_TAC[LE_MULT_RCANCEL]);;\r
  97 \r
  98 let NUM_EXP_LE2 = prove(`!n1 e1 n2 e2 r. e1 <= e2 /\ e2 - e1 = r /\ num_exp n2 r <= n1\r
  99                               ==> num_exp n2 e2 <= num_exp n1 e1`,\r
 100    REPEAT GEN_TAC THEN REWRITE_TAC[num_exp] THEN\r
 101      STRIP_TAC THEN\r
 102      POP_ASSUM MP_TAC THEN POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN DISCH_TAC THEN\r
 103      MP_TAC (ARITH_RULE `e1 <= e2 ==> e2 = (e2 - e1) + e1:num`) THEN\r
 104      ASM_REWRITE_TAC[] THEN\r
 105      DISCH_THEN(fun th -> ONCE_REWRITE_TAC[th]) THEN\r
 106      REWRITE_TAC[EXP_ADD; MULT_ASSOC] THEN\r
 107      ASM_REWRITE_TAC[LE_MULT_RCANCEL]);;\r
 108 \r
 109 let NUM_EXP_LE1_EQ = prove(`!n1 e1 n2 e2 r x. e2 <= e1 /\ e1 - e2 = r /\ num_exp n1 r = x ==>\r
 110                                (num_exp n1 e1 <= num_exp n2 e2 <=> x <= n2)`,\r
 111    REPEAT GEN_TAC THEN REWRITE_TAC[num_exp] THEN\r
 112      STRIP_TAC THEN\r
 113      REPLICATE_TAC 2 (POP_ASSUM (fun th -> REWRITE_TAC[SYM th])) THEN\r
 114      MP_TAC (ARITH_RULE `e2 <= e1 ==> e1 = (e1 - e2) + e2:num`) THEN\r
 115      ASM_REWRITE_TAC[] THEN\r
 116      DISCH_THEN (fun th -> GEN_REWRITE_TAC (LAND_CONV o DEPTH_CONV) [th]) THEN\r
 117      REWRITE_TAC[EXP_ADD; MULT_ASSOC] THEN\r
 118      ASM_REWRITE_TAC[LE_MULT_RCANCEL; EXP_EQ_0; ARITH_EQ]);;\r
 119 \r
 120 let NUM_EXP_LE2_EQ = prove(`!n1 e1 n2 e2 r x. e1 <= e2 /\ e2 - e1 = r /\ num_exp n2 r = x ==>\r
 121                                (num_exp n1 e1 <= num_exp n2 e2 <=> n1 <= x)`,\r
 122    REPEAT GEN_TAC THEN REWRITE_TAC[num_exp] THEN\r
 123      STRIP_TAC THEN\r
 124      REPLICATE_TAC 2 (POP_ASSUM (fun th -> REWRITE_TAC[SYM th])) THEN\r
 125      MP_TAC (ARITH_RULE `e1 <= e2 ==> e2 = (e2 - e1) + e1:num`) THEN\r
 126      ASM_REWRITE_TAC[] THEN\r
 127      DISCH_THEN (fun th -> GEN_REWRITE_TAC (LAND_CONV o DEPTH_CONV) [th]) THEN\r
 128      REWRITE_TAC[EXP_ADD; MULT_ASSOC] THEN\r
 129      ASM_REWRITE_TAC[LE_MULT_RCANCEL; EXP_EQ_0; ARITH_EQ]);;\r
 130 \r
 131 (* NUM_EXP_LT *)\r
 132 \r
 133 let NUM_EXP_LT1 = prove(`!n1 e1 n2 e2 r. e2 <= e1 /\ e1 - e2 = r /\ n2 < num_exp n1 r\r
 134                             ==> num_exp n2 e2 < num_exp n1 e1`,\r
 135    REPEAT GEN_TAC THEN REWRITE_TAC[num_exp] THEN\r
 136      STRIP_TAC THEN\r
 137      POP_ASSUM MP_TAC THEN POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN DISCH_TAC THEN\r
 138      MP_TAC (ARITH_RULE `e2 <= e1 ==> e1 = (e1 - e2) + e2:num`) THEN\r
 139      ASM_REWRITE_TAC[] THEN\r
 140      DISCH_THEN (fun th -> ONCE_REWRITE_TAC[th]) THEN\r
 141      REWRITE_TAC[EXP_ADD; MULT_ASSOC] THEN\r
 142      ASM_REWRITE_TAC[LT_MULT_RCANCEL; EXP_EQ_0; ARITH_EQ]);;\r
 143 \r
 144 let NUM_EXP_LT2 = prove(`!n1 e1 n2 e2 r. e1 <= e2 /\ e2 - e1 = r /\ num_exp n2 r < n1\r
 145                             ==> num_exp n2 e2 < num_exp n1 e1`,\r
 146    REPEAT GEN_TAC THEN REWRITE_TAC[num_exp] THEN\r
 147      STRIP_TAC THEN\r
 148      POP_ASSUM MP_TAC THEN POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN DISCH_TAC THEN\r
 149      MP_TAC (ARITH_RULE `e1 <= e2 ==> e2 = (e2 - e1) + e1:num`) THEN\r
 150      ASM_REWRITE_TAC[] THEN\r
 151      DISCH_THEN (fun th -> ONCE_REWRITE_TAC[th]) THEN\r
 152      REWRITE_TAC[EXP_ADD; MULT_ASSOC] THEN\r
 153      ASM_REWRITE_TAC[LT_MULT_RCANCEL; EXP_EQ_0; ARITH_EQ]);;\r
 154 \r
 155 let NUM_EXP_LT1_EQ = prove(`!n1 e1 n2 e2 r x. e2 <= e1 /\ e1 - e2 = r /\ num_exp n1 r = x ==>\r
 156                                (num_exp n1 e1 < num_exp n2 e2 <=> x < n2)`,\r
 157    REPEAT GEN_TAC THEN REWRITE_TAC[num_exp] THEN\r
 158      STRIP_TAC THEN\r
 159      REPLICATE_TAC 2 (POP_ASSUM (fun th -> REWRITE_TAC[SYM th])) THEN\r
 160      MP_TAC (ARITH_RULE `e2 <= e1 ==> e1 = (e1 - e2) + e2:num`) THEN\r
 161      ASM_REWRITE_TAC[] THEN\r
 162      DISCH_THEN (fun th -> GEN_REWRITE_TAC (LAND_CONV o DEPTH_CONV) [th]) THEN\r
 163      REWRITE_TAC[EXP_ADD; MULT_ASSOC] THEN\r
 164      ASM_REWRITE_TAC[LT_MULT_RCANCEL; EXP_EQ_0; ARITH_EQ]);;\r
 165 \r
 166 let NUM_EXP_LT2_EQ = prove(`!n1 e1 n2 e2 r x. e1 <= e2 /\ e2 - e1 = r /\ num_exp n2 r = x ==>\r
 167                                (num_exp n1 e1 < num_exp n2 e2 <=> n1 < x)`,\r
 168    REPEAT GEN_TAC THEN REWRITE_TAC[num_exp] THEN\r
 169      STRIP_TAC THEN\r
 170      REPLICATE_TAC 2 (POP_ASSUM (fun th -> REWRITE_TAC[SYM th])) THEN\r
 171      MP_TAC (ARITH_RULE `e1 <= e2 ==> e2 = (e2 - e1) + e1:num`) THEN\r
 172      ASM_REWRITE_TAC[] THEN\r
 173      DISCH_THEN (fun th -> GEN_REWRITE_TAC (LAND_CONV o DEPTH_CONV) [th]) THEN\r
 174      REWRITE_TAC[EXP_ADD; MULT_ASSOC] THEN\r
 175      ASM_REWRITE_TAC[LT_MULT_RCANCEL; EXP_EQ_0; ARITH_EQ]);;\r
 176 \r
 177 (* NUM_EXP_DIV *)\r
 178 \r
 179 let mul_op_num = `( * ):num->num->num`;;\r
 180 \r
 181 let NUM_EXP_DIV1 = prove(`~(n2 = 0) /\ e2 <= e1 ==>\r
 182                            num_exp n1 e1 DIV num_exp n2 e2 = num_exp n1 (e1 - e2) DIV n2`,\r
 183    STRIP_TAC THEN\r
 184      (*`num_exp n1 e1 = 16 EXP e2 * num_exp n1 (e1 - e2)` MP_TAC THENL*)\r
 185      SUBGOAL_THEN (mk_eq(`num_exp n1 e1`, mk_binop mul_op_num (mk_binop `EXP` base_const `e2:num`) `num_exp n1 (e1 - e2)`)) MP_TAC THENL\r
 186      [\r
 187        REWRITE_TAC[num_exp] THEN\r
 188          ONCE_REWRITE_TAC[ARITH_RULE `a * b * c = b * (a * c:num)`] THEN\r
 189          REWRITE_TAC[GSYM EXP_ADD] THEN\r
 190          ASM_SIMP_TAC[ARITH_RULE `e2 <= e1 ==> e2 + e1 - e2 = e1:num`];\r
 191        ALL_TAC\r
 192      ] THEN\r
 193      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN\r
 194      SUBGOAL_THEN (mk_eq(`num_exp n2 e2`, mk_binop mul_op_num (mk_binop `EXP` base_const `e2:num`) `n2:num`)) MP_TAC THENL\r
 195      [\r
 196        REWRITE_TAC[num_exp; MULT_AC];\r
 197        ALL_TAC\r
 198      ] THEN\r
 199      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN\r
 200      MATCH_MP_TAC DIV_MULT2 THEN\r
 201      ASM_REWRITE_TAC[MULT_EQ_0; DE_MORGAN_THM; EXP_EQ_0] THEN\r
 202      ARITH_TAC);;\r
 203          \r
 204 let NUM_EXP_DIV2 = prove(`~(n2 = 0) /\ e1 <= e2 ==>\r
 205                            num_exp n1 e1 DIV num_exp n2 e2 = n1 DIV num_exp n2 (e2 - e1)`,\r
 206    STRIP_TAC THEN\r
 207      (*`num_exp n2 e2 = 16 EXP e1 * num_exp n2 (e2 - e1)` MP_TAC THENL*)\r
 208      SUBGOAL_THEN (mk_eq(`num_exp n2 e2`, mk_binop mul_op_num (mk_binop `EXP` base_const `e1:num`) `num_exp n2 (e2 - e1)`)) MP_TAC THENL\r
 209      [\r
 210        REWRITE_TAC[num_exp] THEN\r
 211          ONCE_REWRITE_TAC[ARITH_RULE `a * b * c = b * (a * c:num)`] THEN\r
 212          REWRITE_TAC[GSYM EXP_ADD] THEN\r
 213          ASM_SIMP_TAC[ARITH_RULE `e1 <= e2 ==> e1 + e2 - e1 = e2:num`];\r
 214        ALL_TAC\r
 215      ] THEN\r
 216      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN\r
 217      SUBGOAL_THEN (mk_eq(`num_exp n1 e1`, mk_binop mul_op_num (mk_binop `EXP` base_const `e1:num`) `n1:num`)) MP_TAC THENL\r
 218      [\r
 219        REWRITE_TAC[num_exp; MULT_AC];\r
 220        ALL_TAC\r
 221      ] THEN\r
 222      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN\r
 223      MATCH_MP_TAC DIV_MULT2 THEN\r
 224      ASM_REWRITE_TAC[num_exp; MULT_EQ_0; DE_MORGAN_THM; EXP_EQ_0] THEN\r
 225      ARITH_TAC);;\r
 226 \r
 227          \r
 228 let EXP_INV_lemma = prove(`!n e1 e2. ~(n = 0) /\ e2 <= e1 ==> &(n EXP (e1 - e2)) =\r
 229                               &(n EXP e1) * inv(&(n EXP e2))`,\r
 230    REPEAT STRIP_TAC THEN\r
 231      REWRITE_TAC[GSYM REAL_OF_NUM_POW] THEN\r
 232      MP_TAC (SPECL [`&n`; `e2:num`; `e1:num`] REAL_POW_SUB) THEN\r
 233      ASM_REWRITE_TAC[REAL_OF_NUM_EQ; real_div]);;\r
 234 \r
 235 let NUM_EXP_SUB_lemma = prove(`!n e1 e2. e2 <= e1 ==> &(num_exp n (e1 - e2)) =\r
 236                                   &(num_exp n e1) * inv(&(num_exp 1 e2))`,\r
 237    REPEAT STRIP_TAC THEN\r
 238      REWRITE_TAC[num_exp] THEN\r
 239      REWRITE_TAC[GSYM REAL_OF_NUM_MUL] THEN\r
 240      MP_TAC (SPECL [base_const; `e1:num`; `e2:num`] EXP_INV_lemma) THEN\r
 241      ANTS_TAC THENL\r
 242      [\r
 243        ASM_REWRITE_TAC[] THEN ARITH_TAC;\r
 244        ALL_TAC\r
 245      ] THEN\r
 246      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN\r
 247      REAL_ARITH_TAC);;\r
 248 \r
 249 \r
 250          \r
 251 end;;\r