formal_lp/old/arith/num_exp_theory.hl

   1 (* Exponential representation of natural numbers *)\r
   2 \r
   3 (* Dependencies *)\r
   4 needs "../formal_lp/arith/nat.hl";;\r
   5 \r
   6 \r
   7 module Num_exp_theory = struct\r
   8 \r
   9 open Arith_options;;\r
  10 \r
  11 \r
  12 let base_const = mk_small_numeral base;;\r
  13 \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
  19 \r
  20 (**********************************)\r
  21 (* Theorems *)\r
  22 \r
  23 let NUM_EXP_EXP = prove(`!n e1 e2. num_exp (num_exp n e1) e2 = num_exp n (e1 + e2)`,\r
  24    REPEAT GEN_TAC THEN\r
  25      REWRITE_TAC[num_exp; EXP_ADD] THEN\r
  26      ARITH_TAC);;\r
  27 \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 \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
  37 \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
  40 \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
  43 \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
  46                          ARITH_TAC);;\r
  47 \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
  51      ARITH_TAC);;\r
  52 \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
  55 \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
  63 \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
  74 \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
  85 \r
  86 (* NUM_EXP_LE *)\r
  87 \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
  91      STRIP_TAC 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
  98 \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
 102      STRIP_TAC 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
 109 \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
 113      STRIP_TAC 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
 120 \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
 124      STRIP_TAC 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
 131 \r
 132 (* NUM_EXP_LT *)\r
 133 \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
 137      STRIP_TAC 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
 144 \r
 145 \r
 146 \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
 150      STRIP_TAC 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
 157 \r
 158      \r
 159      \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
 163      STRIP_TAC 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
 170 \r
 171 \r
 172 \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
 176      STRIP_TAC 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
 183 \r
 184 end;;\r