1 (* ========================================================================= *)
2 (* Binary expansions as a bijection between numbers and finite sets. *)
3 (* ========================================================================= *)
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
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]);;
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]);;
22 (* ------------------------------------------------------------------------- *)
23 (* The basic bijections. *)
24 (* ------------------------------------------------------------------------- *)
26 let bitset = new_definition
27 `bitset n = {i | ODD(n DIV (2 EXP i))}`;;
29 let binarysum = new_definition
30 `binarysum s = nsum s (\i. 2 EXP i)`;;
32 (* ------------------------------------------------------------------------- *)
33 (* Inverse property in one direction. *)
34 (* ------------------------------------------------------------------------- *)
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]);;
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]);;
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]);;
52 REWRITE_TAC[bitset; EXTENSION; NOT_IN_EMPTY; IN_ELIM_THM] THEN
53 SIMP_TAC[DIV_0; EXP_EQ_0; ARITH]);;
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`]);;
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)`]);;
80 (`!m n. bitset m = bitset n <=> m = n`,
81 MESON_TAC[BINARYSUM_BITSET]);;
83 let BITSET_EQ_EMPTY = prove
84 (`!n. bitset n = {} <=> n = 0`,
85 MESON_TAC[BITSET_EQ; BITSET_0]);;
87 (* ------------------------------------------------------------------------- *)
88 (* Inverse property in the other direction. *)
89 (* ------------------------------------------------------------------------- *)
91 let BINARYSUM_BOUND_LEMMA = prove
92 (`!k s. (!i. i IN s ==> i < k) ==> nsum s (\i. 2 EXP i) < 2 EXP k`,
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
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`]);;
114 let BINARYSUM_DIV = prove
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
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;
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
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];
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)`]);;
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];
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]);;
164 (* ------------------------------------------------------------------------- *)
165 (* Also, bijections between restricted segments. *)
166 (* ------------------------------------------------------------------------- *)
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]);;
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]]);;
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]);;
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]);;