1 (* ========================================================================= *)
2 (* Birthday problem. *)
3 (* ========================================================================= *)
7 (* ------------------------------------------------------------------------- *)
8 (* Restricted function space. *)
9 (* ------------------------------------------------------------------------- *)
11 parse_as_infix("-->",(13,"right"));;
13 let funspace = new_definition
14 `(s --> t) = {f:A->B | (!x. x IN s ==> f(x) IN t) /\
15 (!x. ~(x IN s) ==> f(x) = @y. T)}`;;
17 (* ------------------------------------------------------------------------- *)
19 (* ------------------------------------------------------------------------- *)
21 let FUNSPACE_EMPTY = prove
22 (`({} --> t) = {(\x. @y. T)}`,
23 REWRITE_TAC[EXTENSION; IN_SING; funspace; IN_ELIM_THM; NOT_IN_EMPTY] THEN
24 REWRITE_TAC[FUN_EQ_THM]);;
26 let HAS_SIZE_FUNSPACE = prove
27 (`!s:A->bool t:B->bool m n.
28 s HAS_SIZE m /\ t HAS_SIZE n ==> (s --> t) HAS_SIZE (n EXP m)`,
29 REWRITE_TAC[HAS_SIZE; GSYM CONJ_ASSOC] THEN
30 ONCE_REWRITE_TAC[IMP_CONJ] THEN
31 REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN
32 MATCH_MP_TAC FINITE_INDUCT_STRONG THEN CONJ_TAC THENL
33 [SIMP_TAC[CARD_CLAUSES; FINITE_RULES; FUNSPACE_EMPTY; NOT_IN_EMPTY] THEN
34 REPEAT GEN_TAC THEN DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
35 ASM_REWRITE_TAC[EXP; ARITH];
37 REWRITE_TAC[GSYM HAS_SIZE] THEN REPEAT STRIP_TAC THEN
40 IMAGE (\(y:B,g) u:A. if u = x then y else g(u))
41 {y,g | y IN t /\ g IN s --> t}`
43 [REWRITE_TAC[EXTENSION; IN_IMAGE; funspace; IN_ELIM_THM] THEN
44 ONCE_REWRITE_TAC[TAUT `(a /\ b /\ c) /\ d <=> d /\ a /\ b /\ c`] THEN
45 REWRITE_TAC[PAIR_EQ; EXISTS_PAIR_THM; GSYM CONJ_ASSOC] THEN
46 REWRITE_TAC[RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN
47 CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
48 X_GEN_TAC `f:A->B` THEN EQ_TAC THENL
49 [STRIP_TAC THEN MAP_EVERY EXISTS_TAC
50 [`(f:A->B) x`; `\u. if u = x then @y. T else (f:A->B) u`] THEN
51 REWRITE_TAC[FUN_EQ_THM] THEN ASM_MESON_TAC[IN_INSERT];
52 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
53 MAP_EVERY X_GEN_TAC [`y:B`; `g:A->B`] THEN
54 STRIP_TAC THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN
55 ASM_MESON_TAC[IN_INSERT]];
57 MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN CONJ_TAC THENL
58 [REWRITE_TAC[FORALL_PAIR_THM; IN_ELIM_THM] THEN
59 CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
60 ONCE_REWRITE_TAC[TAUT `(a /\ b) /\ d <=> d /\ a /\ b`] THEN
61 REWRITE_TAC[PAIR_EQ; EXISTS_PAIR_THM; GSYM CONJ_ASSOC] THEN
62 REWRITE_TAC[RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN
63 REWRITE_TAC[FUN_EQ_THM; funspace; IN_ELIM_THM] THEN
64 REPEAT GEN_TAC THEN STRIP_TAC THEN CONJ_TAC THENL
65 [ASM_MESON_TAC[IN_INSERT]; ALL_TAC] THEN
66 X_GEN_TAC `u:A` THEN ASM_CASES_TAC `u:A = x` THEN ASM_MESON_TAC[];
68 FIRST_X_ASSUM(SUBST_ALL_TAC o SYM) THEN ASM_SIMP_TAC[CARD_CLAUSES; EXP] THEN
69 MATCH_MP_TAC HAS_SIZE_PRODUCT THEN ASM_MESON_TAC[]);;
71 (* ------------------------------------------------------------------------- *)
72 (* The restriction to injective functions. *)
73 (* ------------------------------------------------------------------------- *)
75 let FACT_DIVIDES = prove
76 (`!m n. m <= n ==> ?d. FACT(n) = d * FACT(m)`,
77 REWRITE_TAC[LE_EXISTS; LEFT_IMP_EXISTS_THM] THEN
78 X_GEN_TAC `m:num` THEN ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
79 SIMP_TAC[LEFT_FORALL_IMP_THM; EXISTS_REFL] THEN
80 INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; FACT] THEN
81 ASM_MESON_TAC[MULT_AC; MULT_CLAUSES]);;
83 let FACT_DIV_MULT = prove
84 (`!m n. m <= n ==> FACT n = (FACT(n) DIV FACT(m)) * FACT(m)`,
85 REPEAT GEN_TAC THEN DISCH_THEN(STRIP_ASSUME_TAC o MATCH_MP FACT_DIVIDES) THEN
86 ASM_REWRITE_TAC[] THEN
87 GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o ONCE_DEPTH_CONV) [MULT_SYM] THEN
88 ASM_SIMP_TAC[DIV_MULT; GSYM LT_NZ; FACT_LT]);;
90 let HAS_SIZE_FUNSPACE_INJECTIVE = prove
91 (`!s:A->bool t:B->bool m n.
92 s HAS_SIZE m /\ t HAS_SIZE n
93 ==> {f | f IN (s --> t) /\
94 (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y)}
95 HAS_SIZE (if n < m then 0 else (FACT n) DIV (FACT(n - m)))`,
96 REWRITE_TAC[HAS_SIZE; GSYM CONJ_ASSOC] THEN
97 ONCE_REWRITE_TAC[IMP_CONJ] THEN
98 REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN
99 MATCH_MP_TAC FINITE_INDUCT_STRONG THEN CONJ_TAC THENL
100 [SIMP_TAC[CARD_CLAUSES; FINITE_RULES; FUNSPACE_EMPTY; NOT_IN_EMPTY] THEN
101 REPEAT GEN_TAC THEN DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
102 REWRITE_TAC[SET_RULE `{x | x IN s} = s`] THEN
103 ASM_SIMP_TAC[FINITE_RULES; CARD_CLAUSES; FACT] THEN
104 SIMP_TAC[NOT_IN_EMPTY; LT; SUB_0; DIV_REFL; GSYM LT_NZ; FACT_LT] THEN
107 REWRITE_TAC[GSYM HAS_SIZE] THEN REPEAT STRIP_TAC THEN
109 `{f | f IN (x INSERT s) --> t /\
110 (!u v. u IN (x INSERT s) /\ v IN (x INSERT s) /\ f u = f v ==> u = v)} =
111 IMAGE (\(y:B,g) u:A. if u = x then y else g(u))
113 g IN {f | f IN (s --> (t DELETE y)) /\
114 !u v. u IN s /\ v IN s /\ f u = f v ==> u = v}}`
116 [REWRITE_TAC[EXTENSION; IN_IMAGE; funspace; IN_ELIM_THM] THEN
117 ONCE_REWRITE_TAC[TAUT `(a /\ b /\ c) /\ d <=> d /\ a /\ b /\ c`] THEN
118 REWRITE_TAC[PAIR_EQ; EXISTS_PAIR_THM; GSYM CONJ_ASSOC] THEN
119 REWRITE_TAC[RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN
120 CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
121 X_GEN_TAC `f:A->B` THEN EQ_TAC THENL
122 [REWRITE_TAC[IN_INSERT; IN_DELETE] THEN
123 STRIP_TAC THEN MAP_EVERY EXISTS_TAC
124 [`(f:A->B) x`; `\u. if u = x then @y. T else (f:A->B) u`] THEN
125 REWRITE_TAC[FUN_EQ_THM] THEN ASM_MESON_TAC[];
126 REWRITE_TAC[IN_INSERT; IN_DELETE; LEFT_IMP_EXISTS_THM] THEN
127 MAP_EVERY X_GEN_TAC [`y:B`; `g:A->B`] THEN
128 STRIP_TAC THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN
131 MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN CONJ_TAC THENL
132 [REWRITE_TAC[FORALL_PAIR_THM; IN_ELIM_THM] THEN
133 CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
134 ONCE_REWRITE_TAC[TAUT `(a /\ b) /\ d <=> d /\ a /\ b`] THEN
135 REWRITE_TAC[PAIR_EQ; EXISTS_PAIR_THM; GSYM CONJ_ASSOC] THEN
136 REWRITE_TAC[RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN
137 REWRITE_TAC[FUN_EQ_THM; funspace; IN_ELIM_THM; IN_INSERT; IN_DELETE] THEN
138 REPEAT GEN_TAC THEN STRIP_TAC THEN CONJ_TAC THENL
139 [ASM_MESON_TAC[IN_INSERT]; ALL_TAC] THEN
140 X_GEN_TAC `u:A` THEN ASM_CASES_TAC `u:A = x` THEN ASM_MESON_TAC[];
142 FIRST_X_ASSUM(SUBST_ALL_TAC o SYM) THEN ASM_SIMP_TAC[CARD_CLAUSES; EXP] THEN
144 `(if n < SUC (CARD s) then 0 else FACT n DIV FACT (n - SUC (CARD s))) =
145 n * (if (n - 1) < CARD(s:A->bool) then 0
146 else FACT(n - 1) DIV FACT (n - 1 - CARD s))`
148 [ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[MULT_CLAUSES; LT_0] THEN
149 ASM_SIMP_TAC[ARITH_RULE `~(n = 0) ==> (n - 1 < m <=> n < SUC m)`] THEN
150 COND_CASES_TAC THEN ASM_REWRITE_TAC[MULT_CLAUSES] THEN
151 REWRITE_TAC[ARITH_RULE `n - SUC(m) = n - 1 - m`] THEN
152 UNDISCH_TAC `~(n = 0)` THEN SPEC_TAC(`n:num`,`n:num`) THEN
153 INDUCT_TAC THEN REWRITE_TAC[FACT; SUC_SUB1] THEN DISCH_TAC THEN
154 MATCH_MP_TAC DIV_UNIQ THEN EXISTS_TAC `0` THEN
155 REWRITE_TAC[ADD_CLAUSES; FACT_LT; GSYM MULT_ASSOC] THEN
156 AP_TERM_TAC THEN MATCH_MP_TAC FACT_DIV_MULT THEN ARITH_TAC;
157 MATCH_MP_TAC HAS_SIZE_PRODUCT_DEPENDENT THEN ASM_REWRITE_TAC[] THEN
158 X_GEN_TAC `y:B` THEN DISCH_TAC THEN
159 FIRST_X_ASSUM MATCH_MP_TAC THEN
160 RULE_ASSUM_TAC(REWRITE_RULE[HAS_SIZE]) THEN
161 ASM_SIMP_TAC[HAS_SIZE; FINITE_DELETE; CARD_DELETE]]);;
163 (* ------------------------------------------------------------------------- *)
164 (* So the actual birthday result. *)
165 (* ------------------------------------------------------------------------- *)
167 let HAS_SIZE_DIFF = prove
169 s SUBSET t /\ s HAS_SIZE m /\ t HAS_SIZE n
170 ==> (t DIFF s) HAS_SIZE (n - m)`,
171 SIMP_TAC[HAS_SIZE; FINITE_DIFF] THEN
172 REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
173 REPEAT(DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC)) THEN
174 DISCH_THEN(SUBST_ALL_TAC o SYM) THEN FIRST_X_ASSUM(SUBST_ALL_TAC o SYM) THEN
175 FIRST_ASSUM(MP_TAC o MATCH_MP (SET_RULE
176 `s SUBSET t ==> t = s UNION (t DIFF s)`)) THEN
177 DISCH_THEN(fun th -> GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [th]) THEN
178 ASM_SIMP_TAC[CARD_UNION; FINITE_DIFF; ADD_SUB2;
179 SET_RULE `s INTER (t DIFF s) = {}`]);;
181 let BIRTHDAY_THM = prove
182 (`!s:A->bool t:B->bool m n.
183 s HAS_SIZE m /\ t HAS_SIZE n
184 ==> {f | f IN (s --> t) /\
185 ?x y. x IN s /\ y IN s /\ ~(x = y) /\ f(x) = f(y)}
186 HAS_SIZE (if m <= n then (n EXP m) - (FACT n) DIV (FACT(n - m))
188 REPEAT STRIP_TAC THEN
190 `{f:A->B | f IN (s --> t) /\
191 ?x y. x IN s /\ y IN s /\ ~(x = y) /\ f(x) = f(y)} =
193 {f | f IN (s --> t) /\
194 (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y)}`] THEN
195 REWRITE_TAC[ARITH_RULE
196 `(if a <= b then x - y else x) = x - (if b < a then 0 else y)`] THEN
197 MATCH_MP_TAC HAS_SIZE_DIFF THEN
198 ASM_SIMP_TAC[HAS_SIZE_FUNSPACE_INJECTIVE; HAS_SIZE_FUNSPACE] THEN
199 SIMP_TAC[SUBSET; IN_ELIM_THM]);;
201 (* ------------------------------------------------------------------------- *)
202 (* The usual explicit instantiation. *)
203 (* ------------------------------------------------------------------------- *)
205 let FACT_DIV_SIMP = prove
207 ==> (FACT n) DIV (FACT m) = n * FACT(n - 1) DIV FACT(m)`,
208 GEN_TAC THEN REWRITE_TAC[LT_EXISTS; LEFT_IMP_EXISTS_THM] THEN
209 ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
210 SIMP_TAC[LEFT_FORALL_IMP_THM; EXISTS_REFL] THEN
211 REWRITE_TAC[ARITH_RULE `(m + SUC d) - 1 - m = d`] THEN
212 REWRITE_TAC[ARITH_RULE `(m + SUC d) - 1 = m + d`; ADD_SUB2] THEN
213 GEN_TAC THEN MATCH_MP_TAC DIV_UNIQ THEN EXISTS_TAC `0` THEN
214 REWRITE_TAC[FACT_LT; ARITH_RULE `x + 0 = x`] THEN REWRITE_TAC[FACT] THEN
215 SIMP_TAC[GSYM MULT_ASSOC; GSYM FACT_DIV_MULT; LE_ADD] THEN
216 REWRITE_TAC[ADD_CLAUSES; FACT]);;
218 let BIRTHDAY_THM_EXPLICIT = prove
219 (`!s t. s HAS_SIZE 23 /\ t HAS_SIZE 365
220 ==> 2 * CARD {f | f IN (s --> t) /\
221 ?x y. x IN s /\ y IN s /\ ~(x = y) /\ f(x) = f(y)}
223 REPEAT GEN_TAC THEN DISCH_TAC THEN
224 FIRST_ASSUM(MP_TAC o MATCH_MP BIRTHDAY_THM) THEN
225 FIRST_ASSUM(MP_TAC o MATCH_MP HAS_SIZE_FUNSPACE) THEN
226 CONV_TAC(ONCE_DEPTH_CONV NUM_SUB_CONV) THEN
228 (SIMP_TAC[FACT_DIV_SIMP; ARITH_LE; ARITH_LT] THEN
229 CONV_TAC(ONCE_DEPTH_CONV NUM_SUB_CONV))) THEN
230 SIMP_TAC[DIV_REFL; GSYM LT_NZ; FACT_LT] THEN
231 REWRITE_TAC[HAS_SIZE] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
232 CONV_TAC NUM_REDUCE_CONV);;