(* ========================================================================= *)
(* Binary expansions as a bijection between numbers and finite sets.         *)
(* ========================================================================= *)


let BINARY_INDUCT = 
prove
 (`!P. P 0 /\ (!n. P n ==> P(2 * n) /\ P(2 * n + 1)) ==> !n. P n`,

  GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC num_WF THEN GEN_TAC THEN
  STRIP_ASSUME_TAC(ARITH_RULE
   `n = 0 \/ n DIV 2 < n /\ (n = 2 * n DIV 2 \/ n = 2 * n DIV 2 + 1)`) THEN
  ASM_MESON_TAC[]);;


let BOUNDED_FINITE = 
prove
 (`!s. (!x:num. x IN s ==> x <= n) ==> FINITE s`,

  REPEAT STRIP_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `0..n` THEN
  ASM_SIMP_TAC[SUBSET; IN_NUMSEG; FINITE_NUMSEG; LE_0]);;


let EVEN_NSUM = 
prove
 (`!s. FINITE s /\ (!i. i IN s ==> EVEN(f i)) ==> EVEN(nsum s f)`,

  REWRITE_TAC[IMP_CONJ] THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
  ASM_SIMP_TAC[NSUM_CLAUSES; ARITH; EVEN_ADD; IN_INSERT]);;

(* ------------------------------------------------------------------------- *)
(* The basic bijections.                                                     *)
(* ------------------------------------------------------------------------- *)


let bitset = new_definition
 `bitset n = {i | ODD(n DIV (2 EXP i))}`;;


let binarysum = new_definition
 `binarysum s = nsum s (\i. 2 EXP i)`;;

(* ------------------------------------------------------------------------- *)
(* Inverse property in one direction.                                        *)
(* ------------------------------------------------------------------------- *)


let BITSET_BOUND_LEMMA = 
prove
 (`!n i. i IN (bitset n) ==> 2 EXP i <= n`,

  REWRITE_TAC[bitset; IN_ELIM_THM] THEN MESON_TAC[DIV_LT; ODD; NOT_LE]);;


let BITSET_BOUND_WEAK = 
prove
 (`!n i. i IN (bitset n) ==> i < n`,


let FINITE_BITSET = 
prove
 (`!n. FINITE(bitset n)`,

  GEN_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `0..n` THEN
  REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG; LE_0; SUBSET] THEN
  MESON_TAC[LT_IMP_LE; BITSET_BOUND_WEAK]);;


let BITSET_0 = 
prove
 (`bitset 0 = {}`,

  REWRITE_TAC[bitset; EXTENSION; NOT_IN_EMPTY; IN_ELIM_THM] THEN
  SIMP_TAC[DIV_0; EXP_EQ_0; ARITH]);;


let BITSET_STEP = 
prove
 (`(!n. bitset(2 * n) = IMAGE SUC (bitset n)) /\
   (!n. bitset(2 * n + 1) = 0 INSERT (IMAGE SUC (bitset n)))`,

  MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN CONJ_TAC THENL
   [ALL_TAC; DISCH_THEN(fun th -> REWRITE_TAC[GSYM th])] THEN
  REWRITE_TAC[bitset; EXTENSION; IN_INSERT; IN_ELIM_THM; IN_IMAGE] THEN
  GEN_TAC THEN MATCH_MP_TAC num_INDUCTION THEN
  REWRITE_TAC[ARITH; ODD_MULT; DIV_1; NOT_SUC; ODD_ADD] THEN
  GEN_TAC THEN DISCH_THEN(K ALL_TAC) THEN
  REWRITE_TAC[SUC_INJ; UNWIND_THM1; EXP] THEN
  SIMP_TAC[CONV_RULE(RAND_CONV SYM_CONV) (SPEC_ALL DIV_DIV);
           MULT_EQ_0; EXP_EQ_0; ARITH] THEN
  REWRITE_TAC[ARITH_RULE `(2 * n + 1) DIV 2 = n /\ (2 * n) DIV 2 = n`]);;


let BINARYSUM_BITSET = 
prove
 (`!n. binarysum (bitset n) = n`,

  CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN REWRITE_TAC[binarysum] THEN
  MATCH_MP_TAC BINARY_INDUCT THEN REWRITE_TAC[BITSET_0; NSUM_CLAUSES] THEN
  SIMP_TAC[BITSET_STEP; NSUM_IMAGE; SUC_INJ; ADD1; FINITE_BITSET; ARITH;
  NSUM_CLAUSES; FINITE_IMAGE; IN_IMAGE; ARITH_RULE `~(0 = x + 1)`] THEN
  REWRITE_TAC[o_DEF; EXP; NSUM_LMUL] THEN
  ASM_MESON_TAC[ADD_SYM; ARITH_RULE `~(2 * m = 0) ==> m < 2 * m`;
                ARITH_RULE `m < SUC(2 * m)`]);;


let BITSET_EQ = 
prove
 (`!m n. bitset m = bitset n <=> m = n`,

  MESON_TAC[BINARYSUM_BITSET]);;


let BITSET_EQ_EMPTY = 
prove
 (`!n. bitset n = {} <=> n = 0`,

  MESON_TAC[BITSET_EQ; BITSET_0]);;

(* ------------------------------------------------------------------------- *)
(* Inverse property in the other direction.                                  *)
(* ------------------------------------------------------------------------- *)


let BINARYSUM_BOUND_LEMMA = 
prove
 (`!k s. (!i. i IN s ==> i < k) ==> nsum s (\i. 2 EXP i) < 2 EXP k`,

  INDUCT_TAC THEN
  SIMP_TAC[LT; GSYM NOT_EXISTS_THM; MEMBER_NOT_EMPTY; NSUM_CLAUSES; ARITH] THEN
  REPEAT STRIP_TAC THEN SUBGOAL_THEN `FINITE(s:num->bool)` ASSUME_TAC THENL
   [ASM_MESON_TAC[BOUNDED_FINITE; LE_LT]; ALL_TAC] THEN
  MATCH_MP_TAC LET_TRANS THEN
  EXISTS_TAC `nsum (k INSERT (s DELETE k)) (\i. 2 EXP i)` THEN CONJ_TAC THENL
   [MATCH_MP_TAC NSUM_SUBSET THEN SIMP_TAC[FINITE_INSERT; FINITE_DELETE];
    ASM_SIMP_TAC[NSUM_CLAUSES; FINITE_DELETE; IN_DELETE] THEN
    REWRITE_TAC[EXP; ARITH_RULE `a + b < 2 * a <=> b < a `] THEN
    FIRST_X_ASSUM MATCH_MP_TAC] THEN
  ASM SET_TAC[]);;


let BINARYSUM_DIV_DIVISIBLE = 
prove
 (`!s k. FINITE s /\ (!i. i IN s ==> k <= i)
         ==> nsum s (\i. 2 EXP i) = 2 EXP k * nsum s (\i. 2 EXP (i - k))`,

  REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
  MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
  SIMP_TAC[NSUM_CLAUSES; DIV_0; EXP_EQ_0; ARITH_EQ; MULT_CLAUSES] THEN
  SIMP_TAC[IN_INSERT; ADD_ASSOC; EQ_ADD_RCANCEL; LEFT_ADD_DISTRIB] THEN
  SIMP_TAC[GSYM EXP_ADD; ARITH_RULE `i <= k:num ==> i + k - i = k`]);;


let BINARYSUM_DIV = 
prove
 (`!k s. FINITE s
         ==> (nsum s (\j. 2 EXP j)) DIV (2 EXP k) =
             nsum s (\j. if j < k then 0 else 2 EXP (j - k))`,

  REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
  EXISTS_TAC `(nsum {i | i < k /\ i IN s} (\j. 2 EXP j) +
               nsum {i | k <= i /\ i IN s} (\j. 2 EXP j)) DIV (2 EXP k)` THEN
  CONJ_TAC THENL
   [AP_THM_TAC THEN AP_TERM_TAC THEN CONV_TAC SYM_CONV THEN
    MATCH_MP_TAC NSUM_UNION_EQ THEN
    ASM_SIMP_TAC[EXTENSION; IN_INTER; IN_UNION; IN_ELIM_THM; NOT_IN_EMPTY] THEN
    CONJ_TAC THEN X_GEN_TAC `i:num` THEN
    ASM_CASES_TAC `(i:num) IN s` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC;
    ALL_TAC] THEN
  MATCH_MP_TAC DIV_UNIQ THEN
  EXISTS_TAC `nsum {i | i < k /\ i IN s} (\j. 2 EXP j)` THEN
  SIMP_TAC[BINARYSUM_BOUND_LEMMA; IN_ELIM_THM] THEN
  REWRITE_TAC[ARITH_RULE `a + x:num = y + a <=> x = y`] THEN
  MATCH_MP_TAC EQ_TRANS THEN
  EXISTS_TAC `2 EXP k * nsum {i | k <= i /\ i IN s} (\i. 2 EXP (i - k))` THEN
  CONJ_TAC THENL
   [MATCH_MP_TAC BINARYSUM_DIV_DIVISIBLE THEN SIMP_TAC[IN_ELIM_THM] THEN
    MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `s:num->bool` THEN
    ASM_SIMP_TAC[SUBSET; IN_ELIM_THM];
    ALL_TAC] THEN
  GEN_REWRITE_TAC RAND_CONV [MULT_SYM] THEN
  REWRITE_TAC[EQ_MULT_LCANCEL; EXP_EQ_0; ARITH_EQ] THEN
  ONCE_REWRITE_TAC[GSYM NSUM_SUPPORT] THEN
  REWRITE_TAC[support; NEUTRAL_ADD; EXP_EQ_0; ARITH; IN_ELIM_THM] THEN
  REWRITE_TAC[ARITH_RULE `(if p then 0 else q) = 0 <=> ~p ==> q = 0`] THEN
  REWRITE_TAC[EXP_EQ_0; ARITH; NOT_LT; CONJ_ACI] THEN
  MATCH_MP_TAC NSUM_EQ THEN
  SIMP_TAC[IN_ELIM_THM; ARITH_RULE `k <= j:num ==> ~(j < k)`]);;


let BITSET_BINARYSUM = 
prove
 (`!s. FINITE s ==> bitset (binarysum s) = s`,

  GEN_TAC THEN DISCH_TAC THEN
  REWRITE_TAC[bitset; binarysum; EXTENSION; IN_ELIM_THM] THEN
  X_GEN_TAC `i:num` THEN ASM_SIMP_TAC[BINARYSUM_DIV] THEN
  ASM_CASES_TAC `(i:num) IN s` THEN ASM_REWRITE_TAC[] THENL
   [FIRST_ASSUM(SUBST1_TAC o MATCH_MP (SET_RULE
     `i IN s ==> s = i INSERT (s DELETE i)`)) THEN
    ASM_SIMP_TAC[NSUM_CLAUSES; FINITE_DELETE; IN_DELETE] THEN
    REWRITE_TAC[LT_REFL; SUB_REFL; ARITH; ODD_ADD];
    ALL_TAC] THEN
  REWRITE_TAC[NOT_ODD] THEN MATCH_MP_TAC EVEN_NSUM THEN
  ASM_REWRITE_TAC[FINITE_DELETE; IN_DELETE] THEN
  ONCE_REWRITE_TAC[COND_RAND] THEN SIMP_TAC[ARITH; EVEN_EXP; SUB_EQ_0] THEN
  REPEAT STRIP_TAC THEN COND_CASES_TAC THEN ASM_MESON_TAC[LE_LT]);;

(* ------------------------------------------------------------------------- *)
(* Also, bijections between restricted segments.                             *)
(* ------------------------------------------------------------------------- *)


let BINARYSUM_BOUND = 
prove
 (`!k s. (!i. i IN s ==> i < k) ==> binarysum s < 2 EXP k`,

  REWRITE_TAC[BINARYSUM_BOUND_LEMMA; binarysum]);;


let BITSET_BOUND = 
prove
 (`!n i k. n < 2 EXP k /\ i IN bitset n ==> i < k`,

  REPEAT STRIP_TAC THEN SUBGOAL_THEN `2 EXP i < 2 EXP k` MP_TAC THENL
   [ASM_MESON_TAC[BITSET_BOUND_LEMMA; LET_TRANS];
    REWRITE_TAC[LT_EXP; ARITH]]);;


let BITSET_BOUND_EQ = 
prove
 (`!n k. n < 2 EXP k <=> (!i. i IN bitset n ==> i < k)`,


let BINARYSUM_BOUND_EQ = 
prove
 (`!s k. FINITE s ==> (binarysum s < 2 EXP k <=> (!i. i IN s ==> i < k))`,