Library/binary.ml

   1 (* ========================================================================= *)
   2 (* Binary expansions as a bijection between numbers and finite sets.         *)
   3 (* ========================================================================= *)
   4
   5 let BINARY_INDUCT = prove
   6  (`!P. P 0 /\ (!n. P n ==> P(2 * n) /\ P(2 * n + 1)) ==> !n. P n`,
   7   GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC num_WF THEN GEN_TAC THEN
   8   STRIP_ASSUME_TAC(ARITH_RULE
   9    `n = 0 \/ n DIV 2 < n /\ (n = 2 * n DIV 2 \/ n = 2 * n DIV 2 + 1)`) THEN
  10   ASM_MESON_TAC[]);;
  11
  12 let BOUNDED_FINITE = prove
  13  (`!s. (!x:num. x IN s ==> x <= n) ==> FINITE s`,
  14   REPEAT STRIP_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `0..n` THEN
  15   ASM_SIMP_TAC[SUBSET; IN_NUMSEG; FINITE_NUMSEG; LE_0]);;
  16
  17 let EVEN_NSUM = prove
  18  (`!s. FINITE s /\ (!i. i IN s ==> EVEN(f i)) ==> EVEN(nsum s f)`,
  19   REWRITE_TAC[IMP_CONJ] THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
  20   ASM_SIMP_TAC[NSUM_CLAUSES; ARITH; EVEN_ADD; IN_INSERT]);;
  21
  22 (* ------------------------------------------------------------------------- *)
  23 (* The basic bijections.                                                     *)
  24 (* ------------------------------------------------------------------------- *)
  25
  26 let bitset = new_definition
  27  `bitset n = {i | ODD(n DIV (2 EXP i))}`;;
  28
  29 let binarysum = new_definition
  30  `binarysum s = nsum s (\i. 2 EXP i)`;;
  31
  32 (* ------------------------------------------------------------------------- *)
  33 (* Inverse property in one direction.                                        *)
  34 (* ------------------------------------------------------------------------- *)
  35
  36 let BITSET_BOUND_LEMMA = prove
  37  (`!n i. i IN (bitset n) ==> 2 EXP i <= n`,
  38   REWRITE_TAC[bitset; IN_ELIM_THM] THEN MESON_TAC[DIV_LT; ODD; NOT_LE]);;
  39
  40 let BITSET_BOUND_WEAK = prove
  41  (`!n i. i IN (bitset n) ==> i < n`,
  42   MESON_TAC[BITSET_BOUND_LEMMA; LT_POW2_REFL; LTE_TRANS]);;
  43
  44 let FINITE_BITSET = prove
  45  (`!n. FINITE(bitset n)`,
  46   GEN_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `0..n` THEN
  47   REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG; LE_0; SUBSET] THEN
  48   MESON_TAC[LT_IMP_LE; BITSET_BOUND_WEAK]);;
  49
  50 let BITSET_0 = prove
  51  (`bitset 0 = {}`,
  52   REWRITE_TAC[bitset; EXTENSION; NOT_IN_EMPTY; IN_ELIM_THM] THEN
  53   SIMP_TAC[DIV_0; EXP_EQ_0; ARITH]);;
  54
  55 let BITSET_STEP = prove
  56  (`(!n. bitset(2 * n) = IMAGE SUC (bitset n)) /\
  57    (!n. bitset(2 * n + 1) = 0 INSERT (IMAGE SUC (bitset n)))`,
  58   MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN CONJ_TAC THENL
  59    [ALL_TAC; DISCH_THEN(fun th -> REWRITE_TAC[GSYM th])] THEN
  60   REWRITE_TAC[bitset; EXTENSION; IN_INSERT; IN_ELIM_THM; IN_IMAGE] THEN
  61   GEN_TAC THEN MATCH_MP_TAC num_INDUCTION THEN
  62   REWRITE_TAC[ARITH; ODD_MULT; DIV_1; NOT_SUC; ODD_ADD] THEN
  63   GEN_TAC THEN DISCH_THEN(K ALL_TAC) THEN
  64   REWRITE_TAC[SUC_INJ; UNWIND_THM1; EXP] THEN
  65   SIMP_TAC[CONV_RULE(RAND_CONV SYM_CONV) (SPEC_ALL DIV_DIV);
  66            MULT_EQ_0; EXP_EQ_0; ARITH] THEN
  67   REWRITE_TAC[ARITH_RULE `(2 * n + 1) DIV 2 = n /\ (2 * n) DIV 2 = n`]);;
  68
  69 let BINARYSUM_BITSET = prove
  70  (`!n. binarysum (bitset n) = n`,
  71   CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN REWRITE_TAC[binarysum] THEN
  72   MATCH_MP_TAC BINARY_INDUCT THEN REWRITE_TAC[BITSET_0; NSUM_CLAUSES] THEN
  73   SIMP_TAC[BITSET_STEP; NSUM_IMAGE; SUC_INJ; ADD1; FINITE_BITSET; ARITH;
  74   NSUM_CLAUSES; FINITE_IMAGE; IN_IMAGE; ARITH_RULE `~(0 = x + 1)`] THEN
  75   REWRITE_TAC[o_DEF; EXP; NSUM_LMUL] THEN
  76   ASM_MESON_TAC[ADD_SYM; ARITH_RULE `~(2 * m = 0) ==> m < 2 * m`;
  77                 ARITH_RULE `m < SUC(2 * m)`]);;
  78
  79 let BITSET_EQ = prove
  80  (`!m n. bitset m = bitset n <=> m = n`,
  81   MESON_TAC[BINARYSUM_BITSET]);;
  82
  83 let BITSET_EQ_EMPTY = prove
  84  (`!n. bitset n = {} <=> n = 0`,
  85   MESON_TAC[BITSET_EQ; BITSET_0]);;
  86
  87 (* ------------------------------------------------------------------------- *)
  88 (* Inverse property in the other direction.                                  *)
  89 (* ------------------------------------------------------------------------- *)
  90
  91 let BINARYSUM_BOUND_LEMMA = prove
  92  (`!k s. (!i. i IN s ==> i < k) ==> nsum s (\i. 2 EXP i) < 2 EXP k`,
  93   INDUCT_TAC THEN
  94   SIMP_TAC[LT; GSYM NOT_EXISTS_THM; MEMBER_NOT_EMPTY; NSUM_CLAUSES; ARITH] THEN
  95   REPEAT STRIP_TAC THEN SUBGOAL_THEN `FINITE(s:num->bool)` ASSUME_TAC THENL
  96    [ASM_MESON_TAC[BOUNDED_FINITE; LE_LT]; ALL_TAC] THEN
  97   MATCH_MP_TAC LET_TRANS THEN
  98   EXISTS_TAC `nsum (k INSERT (s DELETE k)) (\i. 2 EXP i)` THEN CONJ_TAC THENL
  99    [MATCH_MP_TAC NSUM_SUBSET THEN SIMP_TAC[FINITE_INSERT; FINITE_DELETE];
 100     ASM_SIMP_TAC[NSUM_CLAUSES; FINITE_DELETE; IN_DELETE] THEN
 101     REWRITE_TAC[EXP; ARITH_RULE `a + b < 2 * a <=> b < a `] THEN
 102     FIRST_X_ASSUM MATCH_MP_TAC] THEN
 103   ASM SET_TAC[]);;
 104
 105 let BINARYSUM_DIV_DIVISIBLE = prove
 106  (`!s k. FINITE s /\ (!i. i IN s ==> k <= i)
 107          ==> nsum s (\i. 2 EXP i) = 2 EXP k * nsum s (\i. 2 EXP (i - k))`,
 108   REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
 109   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 110   SIMP_TAC[NSUM_CLAUSES; DIV_0; EXP_EQ_0; ARITH_EQ; MULT_CLAUSES] THEN
 111   SIMP_TAC[IN_INSERT; ADD_ASSOC; EQ_ADD_RCANCEL; LEFT_ADD_DISTRIB] THEN
 112   SIMP_TAC[GSYM EXP_ADD; ARITH_RULE `i <= k:num ==> i + k - i = k`]);;
 113
 114 let BINARYSUM_DIV = prove
 115  (`!k s. FINITE s
 116          ==> (nsum s (\j. 2 EXP j)) DIV (2 EXP k) =
 117              nsum s (\j. if j < k then 0 else 2 EXP (j - k))`,
 118   REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
 119   EXISTS_TAC `(nsum {i | i < k /\ i IN s} (\j. 2 EXP j) +
 120                nsum {i | k <= i /\ i IN s} (\j. 2 EXP j)) DIV (2 EXP k)` THEN
 121   CONJ_TAC THENL
 122    [AP_THM_TAC THEN AP_TERM_TAC THEN CONV_TAC SYM_CONV THEN
 123     MATCH_MP_TAC NSUM_UNION_EQ THEN
 124     ASM_SIMP_TAC[EXTENSION; IN_INTER; IN_UNION; IN_ELIM_THM; NOT_IN_EMPTY] THEN
 125     CONJ_TAC THEN X_GEN_TAC `i:num` THEN
 126     ASM_CASES_TAC `(i:num) IN s` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC;
 127     ALL_TAC] THEN
 128   MATCH_MP_TAC DIV_UNIQ THEN
 129   EXISTS_TAC `nsum {i | i < k /\ i IN s} (\j. 2 EXP j)` THEN
 130   SIMP_TAC[BINARYSUM_BOUND_LEMMA; IN_ELIM_THM] THEN
 131   REWRITE_TAC[ARITH_RULE `a + x:num = y + a <=> x = y`] THEN
 132   MATCH_MP_TAC EQ_TRANS THEN
 133   EXISTS_TAC `2 EXP k * nsum {i | k <= i /\ i IN s} (\i. 2 EXP (i - k))` THEN
 134   CONJ_TAC THENL
 135    [MATCH_MP_TAC BINARYSUM_DIV_DIVISIBLE THEN SIMP_TAC[IN_ELIM_THM] THEN
 136     MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `s:num->bool` THEN
 137     ASM_SIMP_TAC[SUBSET; IN_ELIM_THM];
 138     ALL_TAC] THEN
 139   GEN_REWRITE_TAC RAND_CONV [MULT_SYM] THEN
 140   REWRITE_TAC[EQ_MULT_LCANCEL; EXP_EQ_0; ARITH_EQ] THEN
 141   ONCE_REWRITE_TAC[GSYM NSUM_SUPPORT] THEN
 142   REWRITE_TAC[support; NEUTRAL_ADD; EXP_EQ_0; ARITH; IN_ELIM_THM] THEN
 143   REWRITE_TAC[ARITH_RULE `(if p then 0 else q) = 0 <=> ~p ==> q = 0`] THEN
 144   REWRITE_TAC[EXP_EQ_0; ARITH; NOT_LT; CONJ_ACI] THEN
 145   MATCH_MP_TAC NSUM_EQ THEN
 146   SIMP_TAC[IN_ELIM_THM; ARITH_RULE `k <= j:num ==> ~(j < k)`]);;
 147
 148 let BITSET_BINARYSUM = prove
 149  (`!s. FINITE s ==> bitset (binarysum s) = s`,
 150   GEN_TAC THEN DISCH_TAC THEN
 151   REWRITE_TAC[bitset; binarysum; EXTENSION; IN_ELIM_THM] THEN
 152   X_GEN_TAC `i:num` THEN ASM_SIMP_TAC[BINARYSUM_DIV] THEN
 153   ASM_CASES_TAC `(i:num) IN s` THEN ASM_REWRITE_TAC[] THENL
 154    [FIRST_ASSUM(SUBST1_TAC o MATCH_MP (SET_RULE
 155      `i IN s ==> s = i INSERT (s DELETE i)`)) THEN
 156     ASM_SIMP_TAC[NSUM_CLAUSES; FINITE_DELETE; IN_DELETE] THEN
 157     REWRITE_TAC[LT_REFL; SUB_REFL; ARITH; ODD_ADD];
 158     ALL_TAC] THEN
 159   REWRITE_TAC[NOT_ODD] THEN MATCH_MP_TAC EVEN_NSUM THEN
 160   ASM_REWRITE_TAC[FINITE_DELETE; IN_DELETE] THEN
 161   ONCE_REWRITE_TAC[COND_RAND] THEN SIMP_TAC[ARITH; EVEN_EXP; SUB_EQ_0] THEN
 162   REPEAT STRIP_TAC THEN COND_CASES_TAC THEN ASM_MESON_TAC[LE_LT]);;
 163
 164 (* ------------------------------------------------------------------------- *)
 165 (* Also, bijections between restricted segments.                             *)
 166 (* ------------------------------------------------------------------------- *)
 167
 168 let BINARYSUM_BOUND = prove
 169  (`!k s. (!i. i IN s ==> i < k) ==> binarysum s < 2 EXP k`,
 170   REWRITE_TAC[BINARYSUM_BOUND_LEMMA; binarysum]);;
 171
 172 let BITSET_BOUND = prove
 173  (`!n i k. n < 2 EXP k /\ i IN bitset n ==> i < k`,
 174   REPEAT STRIP_TAC THEN SUBGOAL_THEN `2 EXP i < 2 EXP k` MP_TAC THENL
 175    [ASM_MESON_TAC[BITSET_BOUND_LEMMA; LET_TRANS];
 176     REWRITE_TAC[LT_EXP; ARITH]]);;
 177
 178 let BITSET_BOUND_EQ = prove
 179  (`!n k. n < 2 EXP k <=> (!i. i IN bitset n ==> i < k)`,
 180   MESON_TAC[BINARYSUM_BOUND; BITSET_BOUND; BINARYSUM_BITSET]);;
 181
 182 let BINARYSUM_BOUND_EQ = prove
 183  (`!s k. FINITE s ==> (binarysum s < 2 EXP k <=> (!i. i IN s ==> i < k))`,
 184   MESON_TAC[BINARYSUM_BOUND; BITSET_BOUND; BITSET_BINARYSUM]);;