3 flyspeck_needs "general/tactics.hl";;
9 val INFINITE_EXISTS:thm
19 let SELECT_TAC= Tactics.SELECT_TAC;;
20 let EVERY_PAT_ASSUM = Tactics.EVERY_PAT_ASSUM;;
22 (* Sierpinski's theorem *)
24 (* start 3:36 July 3 *)
26 let INFINITE_CRIT = prove(
27 `!X Y Z. INFINITE X /\ FINITE Y /\ (Z = X DIFF Y) ==> INFINITE Z`,
28 MESON_TAC[INFINITE_DIFF_FINITE]
32 let INFINITE_EXISTS = prove_by_refinement (
33 `!x P. INFINITE { (x:A) | P x } ==> (?x. P x)`,
35 REWRITE_TAC[INFINITE];
37 SUBGOAL_THEN `~({(x:A) | P x} = {})` MP_TAC;
38 ASM_MESON_TAC[FINITE_EMPTY];
39 REWRITE_TAC[EXTENSION;NOT_IN_EMPTY;IN_ELIM_THM];
44 let INFINITE_EXISTS = prove_by_refinement (
45 `!x P. INFINITE { (x:A) | P x } ==> (?x. P x)`,
47 REWRITE_TAC[INFINITE];
49 ASM_CASES_TAC `({(x:A) | P x} = {})` ;
50 ASM_MESON_TAC[FINITE_EMPTY];
55 let numm0 = prove_by_refinement(`{n | n > 0 } = (:num) DIFF {0}`,
57 REWRITE_TAC[DIFF;FUN_EQ_THM;IN_ELIM_THM;IN_SING;SET_RULE `x IN (:num)`];
61 let inf_pos_y = prove_by_refinement(
62 `!y N. INFINITE N ==> INFINITE { (n:num) | n > y /\ n IN N }`,
65 MATCH_MP_TAC INFINITE_CRIT; (* strategy *)
66 ASM_MESON_TAC[num_y;FINITE_NUMSEG_LE]; (* terminator *)
69 let inf_pos = prove_by_refinement(
70 `INFINITE { n | n > 0 }`,
72 MATCH_MP_TAC INFINITE_CRIT;
73 MESON_TAC[numm0;FINITE_SING;num_INFINITE];
77 let num_seq_exists = prove_by_refinement(
78 `?x. (!n. ~(SND x n) ==> (FST x n = &0)) /\
79 INFINITE (SND x) /\ (!n. n IN SND x ==> n >0)`,
81 EXISTS_TAC `(\n:num. &0), { n | n > 0}`;
82 REWRITE_TAC[FST;SND;IN_ELIM_THM;inf_pos]
85 let num_seq_type = new_type_definition
86 "num_seq" ("mk_num_seq","dest_num_seq") num_seq_exists;;
88 let num_seq_axiom = `(?f:real->num_seq. ONTO f)`;;
90 let phin = new_definition `phin = @(f:real->num_seq). ONTO f`;;
92 let phi_domain = new_definition
93 `phi_domain b = SND (dest_num_seq (phin b))`;;
95 let phi = new_definition
96 `phi b = FST (dest_num_seq (phin b))`;;
98 let phin_ONTO = prove_by_refinement(
99 `(?f: real->num_seq. ONTO f) ==> (!ns. ?b. phin b = ns)`,
107 `(h_b N 0 = @(n:num). N 0 n) /\ (h_b N (SUC i) = @n. (N (SUC i) n /\ n > h_b N i))`;;
110 let num_y = prove_by_refinement(
111 `{(n:num) | n > y /\ n IN N} = N DIFF {n | n <= y}`,
113 REWRITE_TAC[DIFF;FUN_EQ_THM;IN_ELIM_THM;IN_SING];
115 MATCH_MP_TAC (TAUT` (x = y) ==> (x /\ a <=> a /\ y) `);
119 let inf_ex = prove_by_refinement( `!y. INFINITE N ==> ?(n:num). n > y /\ n IN N`,
122 MATCH_MP_TAC INFINITE_EXISTS;
123 MATCH_MP_TAC inf_pos_y;
127 let h_b_inc = prove_by_refinement(
128 `(!i. INFINITE (N i)) ==> (!i. (h_b N i < h_b N (SUC i) ))`,
134 (* prep assumptions *)
135 FIRST_X_ASSUM (ASSUME_TAC o (ISPEC `SUC i:num`));
136 FIRST_X_ASSUM (ASSUME_TAC o (MATCH_MP inf_ex));
139 POP_ASSUM MP_TAC THEN ARITH_TAC;
143 let lemma_inc_injective = Hypermap.lemma_inc_injective;;
146 `(!i. INFINITE (N i)) ==> (!i j. (i = j) <=> (h_b N i = h_b N j))`,
147 MESON_TAC [h_b_inc;lemma_inc_injective]);;
149 let continuum_family = new_definition `continuum_family A =
150 ((!(x:real). INFINITE(A x) /\ (COUNTABLE (A x))) /\
151 (!x y. x IN A y \/ y IN A x))`;;
153 let continuum_bij = prove_by_refinement(
154 `continuum_family A ==> (!x. (?b. (A x = IMAGE b (:num)) /\
155 (!m n. (b m = b n) ==> (m = n))))`,
157 REWRITE_TAC[continuum_family];
158 MESON_TAC[COUNTABLE_AS_INJECTIVE_IMAGE]
161 (* Harrison's lemma *)
162 let WELLDEFINED_FUNCTION_1 = Tactics.WELLDEFINED_FUNCTION_1;;
164 let countable_bij = prove_by_refinement(
165 `!s. (COUNTABLE (s:A->bool)) /\ (INFINITE s) ==> (?f g.
166 (s = IMAGE f (:num) /\ (!m n. f m = f n ==> m = n) /\
167 (!n. g (f n) = n) /\ (!a. a IN s ==> f (g a) = a) /\
168 (!a b. a IN s /\ b IN s /\ (g a = g b) ==> (a = b))))`,
171 MP_TAC (ISPEC `s:A->bool` COUNTABLE_AS_INJECTIVE_IMAGE);
174 EXISTS_TAC `f:num->A`;
176 SUBGOAL_THEN `?g:A->num. (!n. g (f n) = n)` MP_TAC;
177 ASM_REWRITE_TAC[WELLDEFINED_FUNCTION_1];
179 EXISTS_TAC `g:A->num`;
180 ASM_REWRITE_TAC[IN_IMAGE];
185 let h_b_IN = prove_by_refinement(
186 `(!i. INFINITE (N i)) ==> (!i. (h_b N i IN N i))`,
189 DISJ_CASES_TAC (SPEC `i:num` num_CASES) THEN
190 TRY(FIRST_X_ASSUM MP_TAC) THEN REPEAT STRIP_TAC THEN
191 ASM_REWRITE_TAC[h_b;IN] THEN
193 REPEAT STRIP_TAC THEN
194 ASM_MESON_TAC[inf_ex;IN];
197 let phi_domain_inf = prove_by_refinement(
198 `(?b:real->num_seq. ONTO b) ==>
199 (!x. INFINITE (phi_domain x))`,
201 REWRITE_TAC[phi_domain;phin];
205 ASM_MESON_TAC[num_seq_type]
208 let lemma1 = prove_by_refinement
209 (`(?b:real->num_seq. ONTO b) ==> (!A x. continuum_family A ==>
211 (! y z. A x y /\ A x z /\ (h y = h z) ==> (y = z))) /\
212 (!y. A x y ==> h y IN phi_domain y) /\ (!y. ~(A x y) ==> h y = 0)))`,
215 REWRITE_TAC[continuum_family];
218 MP_TAC (ISPEC `(A:real->real->bool) x` countable_bij);
221 SUBGOAL_THEN `!a. a IN (A:real->real->bool) x ==> (phi_domain a) = (phi_domain o (f:num->real)) (g a) ` ASSUME_TAC;
224 SUBGOAL_THEN `!i:num. INFINITE ((phi_domain o f) i)` ASSUME_TAC;
226 ASM_MESON_TAC[phi_domain_inf];
228 EXISTS_TAC `\(y:real). if A (x:real) y then h_b (phi_domain o f) (g y) else 0`;
230 REPEAT CONJ_TAC THEN REPEAT STRIP_TAC THEN
231 (* terminate every subgoal *)
232 TRY(FIRST_X_ASSUM MP_TAC) THEN
233 ASM_REWRITE_TAC[] THEN
234 ASM_MESON_TAC[IN;h_b_inj;h_b_IN];
237 let lem = REWRITE_RULE [RIGHT_IMP_EXISTS_THM;SKOLEM_THM]
240 let hx = new_specification ["hx"] lem;;
242 let WELLDEFINED_FUNCTION_2b = Tactics.WELLDEFINED_FUNCTION_2b;;
244 (* next existence of f *)
245 let f_ex = prove_by_refinement
246 (`!A (b:real->num_seq). (continuum_family A) /\ (ONTO b) ==>
247 (?(f:(num#real) -> real). !x y. A x y ==> f ((hx A x y), x) = phi y (hx A x y))`,
249 REPEAT STRIP_TAC; (* unpack *)
250 REWRITE_TAC[WELLDEFINED_FUNCTION_2b;PAIR_EQ]; (* strategy *)
252 SUBGOAL_THEN `(y:real) = y'` ASSUME_TAC ;
257 let fc_ex = prove_by_refinement(
258 `!A (b:real->num_seq). (continuum_family A) /\ (ONTO b) ==>
259 (?(f:num->real -> real). !x y. A x y ==>
260 f (hx A x y) x = phi y (hx A x y))`,
263 MP_TAC (ISPECL [`A:real->real->bool`; `b:real->num_seq`] f_ex);
266 EXISTS_TAC `\ n x . (f:num#real->real) (n,x)`;
271 let fd_ex = prove_by_refinement(
272 `?f. !A. (continuum_family A) /\ (?(b:real->num_seq). ONTO b)
274 (!x y. A x y ==> f A (hx A x y) x = phi y (hx A x y))`,
276 REWRITE_TAC[GSYM SKOLEM_THM];
280 let fd = new_specification[ "fd"] fd_ex;;
283 let r_exists = prove_by_refinement(
284 `!X (b:real->num_seq). INFINITE { n | ~((X n) = (:real)) } /\ (ONTO b) ==>
286 (phi_domain r = {n | n > 0 /\ (~((X n) = (:real))) } ) /\
287 (!n. if n IN phi_domain r then ~(phi r n IN X n) else (phi r n = &0)))`,
290 ABBREV_TAC `N = { n:num | ~(X n = (:real) ) }`;
292 FIRST_RULE_ASSUM (MATCH_MP (ISPEC `0` inf_pos_y)) ASSUME_TAC;
294 ABBREV_TAC `N0 = {n | n > 0 /\ n IN N}`;
295 SUBGOAL_THEN `?ph. !(n:num). if (n IN N0) then (~(ph n IN X n)) else (ph n= &0)` MP_TAC;
296 REWRITE_TAC[GSYM SKOLEM_THM];
297 ASM SET_TAC[IN_ELIM_THM];
300 SUBGOAL_THEN `dest_num_seq (mk_num_seq (ph,N0)) = (ph,N0)` ASSUME_TAC;
301 ASM_REWRITE_TAC[GSYM num_seq_type];
305 REWRITE_TAC[IN_ELIM_THM;TAUT `a /\ b ==> a`];
307 SUBGOAL_THEN `?(r:real). phin r = mk_num_seq (ph,N0)` MP_TAC;
308 ASM_MESON_TAC[ONTO;phin];
311 SUBGOAL_THEN `(phi_domain r = N0) /\ (phi r = ph)` MP_TAC;
312 ASM_REWRITE_TAC[phi_domain;phi];
316 EVERY_PAT_ASSUM [`ph:num->real`] (fun t-> UNDISCH_THEN (concl t) (K ALL_TAC));
317 EVERY_PAT_ASSUM [`phi_domain`] (fun t-> UNDISCH_THEN (concl t) (K ALL_TAC));
320 REWRITE_TAC[IN_ELIM_THM];
325 let countable_s = prove_by_refinement(
326 `!A (b:real->num_seq) s. (continuum_family A) /\ (ONTO b) /\
327 (INFINITE { n | ~(IMAGE (fd A n) s = (:real) ) }) ==> (COUNTABLE s)`,
331 ABBREV_TAC `N = { n | ~(IMAGE (fd A n) s = (:real) ) }`;
332 MP_TAC (ISPECL [`\n. IMAGE (fd A n) s`;`b:real->num_seq`] r_exists);
336 (* unpack continuum family *)
337 UNDISCH_THEN `continuum_family A` (fun t -> ASSUME_TAC t THEN MP_TAC (REWRITE_RULE[continuum_family] t));
340 MATCH_MP_TAC COUNTABLE_SUBSET; (* strategy *)
341 EXISTS_TAC `(A:real->real->bool) r`;
342 ASM_REWRITE_TAC[SUBSET];
344 REFUTE_THEN ASSUME_TAC;
346 SUBGOAL_TAC "A" `r IN (A:real->real -> bool) x` [ASM_MESON_TAC[]];
347 SUBGOAL_TAC "B" `fd A (hx A x r) x = phi r (hx A x r)` [ASM_MESON_TAC[IN;fd]];
349 SUBGOAL_THEN `hx A x r IN phi_domain r` ASSUME_TAC;
350 ASM_MESON_TAC[hx;IN];
352 SUBGOAL_THEN `~(phi r (hx A x r) IN IMAGE (fd A (hx A x r)) s)` MP_TAC;
354 REWRITE_TAC[IN_IMAGE];
361 let sierpinski = prove_by_refinement
362 (`!A (b:real->num_seq). (continuum_family A) /\ (ONTO b) ==>
363 (?(f:num->real->real). !s.
364 (~(COUNTABLE s) ==> FINITE { n | ~(IMAGE (f n) s = (:real)) }))`,
369 MP_TAC (ISPECL[`A:real->real->bool`;`b:real->num_seq`;`s:real->bool`] countable_s);
370 ASM_REWRITE_TAC[INFINITE];
373 (* complete at 1:25 pm July 4, 2010. *)