development/thales/examples/sierpinski.hl

   1
   2
   3 flyspeck_needs "general/tactics.hl";;
   4
   5 module Sierpinski:sig
   6
   7   val INFINITE_CRIT:thm
   8
   9   val INFINITE_EXISTS:thm
  10
  11   val num_seq_type:thm
  12
  13   val sierpinski:thm
  14
  15 end =
  16
  17 struct
  18
  19 let SELECT_TAC= Tactics.SELECT_TAC;;
  20 let EVERY_PAT_ASSUM = Tactics.EVERY_PAT_ASSUM;;
  21
  22 (* Sierpinski's theorem *)
  23
  24 (* start 3:36 July 3 *)
  25
  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]
  29 );;
  30
  31 (*
  32 let INFINITE_EXISTS = prove_by_refinement (
  33 `!x P. INFINITE { (x:A) | P x } ==> (?x. P x)`,
  34 [
  35 REWRITE_TAC[INFINITE];
  36 REPEAT STRIP_TAC;
  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];
  40 MESON_TAC[];
  41 ]);;
  42 *)
  43
  44 let INFINITE_EXISTS = prove_by_refinement (
  45 `!x P. INFINITE { (x:A) | P x } ==> (?x. P x)`,
  46 [
  47 REWRITE_TAC[INFINITE];
  48 REPEAT STRIP_TAC;
  49 ASM_CASES_TAC `({(x:A) | P x} = {})` ;
  50 ASM_MESON_TAC[FINITE_EMPTY];
  51 POP_ASSUM MP_TAC;
  52 SET_TAC[];
  53 ]);;
  54
  55 let numm0 = prove_by_refinement(`{n | n > 0 } = (:num) DIFF {0}`,
  56 [
  57 REWRITE_TAC[DIFF;FUN_EQ_THM;IN_ELIM_THM;IN_SING;SET_RULE `x IN (:num)`];
  58 ARITH_TAC;
  59 ]);;
  60
  61 let inf_pos_y = prove_by_refinement(
  62   `!y N. INFINITE N ==> INFINITE { (n:num) | n > y /\ n IN N }`,
  63 [
  64 REPEAT STRIP_TAC;
  65 MATCH_MP_TAC INFINITE_CRIT; (* strategy *)
  66 ASM_MESON_TAC[num_y;FINITE_NUMSEG_LE]; (* terminator *)
  67 ]);;
  68
  69 let inf_pos = prove_by_refinement(
  70 `INFINITE { n | n > 0 }`,
  71 [
  72 MATCH_MP_TAC INFINITE_CRIT;
  73 MESON_TAC[numm0;FINITE_SING;num_INFINITE];
  74 ]);;
  75
  76
  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)`,
  80 [
  81  EXISTS_TAC `(\n:num. &0), { n | n > 0}`;
  82  REWRITE_TAC[FST;SND;IN_ELIM_THM;inf_pos]
  83 ]);;
  84
  85 let num_seq_type = new_type_definition
  86   "num_seq" ("mk_num_seq","dest_num_seq") num_seq_exists;;
  87
  88 let num_seq_axiom = `(?f:real->num_seq.  ONTO f)`;;
  89
  90 let phin = new_definition `phin = @(f:real->num_seq). ONTO f`;;
  91
  92 let phi_domain = new_definition
  93   `phi_domain b = SND (dest_num_seq (phin b))`;;
  94
  95 let phi = new_definition
  96   `phi b = FST (dest_num_seq (phin b))`;;
  97
  98 let phin_ONTO = prove_by_refinement(
  99   `(?f: real->num_seq. ONTO f) ==> (!ns. ?b. phin b = ns)`,
 100 [
 101 REWRITE_TAC[phin];
 102 SELECT_ELIM_TAC;
 103 MESON_TAC[ONTO]
 104 ]);;
 105
 106 let h_b = define
 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))`;;
 108
 109
 110 let num_y = prove_by_refinement(
 111   `{(n:num) | n > y /\ n IN N} = N DIFF {n | n <= y}`,
 112 [
 113 REWRITE_TAC[DIFF;FUN_EQ_THM;IN_ELIM_THM;IN_SING];
 114 GEN_TAC;
 115 MATCH_MP_TAC (TAUT` (x = y) ==>  (x /\ a <=> a /\ y) `);
 116 ARITH_TAC;
 117 ]);;
 118
 119 let inf_ex = prove_by_refinement(  `!y. INFINITE N ==> ?(n:num). n > y /\ n IN N`,
 120 [
 121 REPEAT STRIP_TAC;
 122 MATCH_MP_TAC INFINITE_EXISTS;
 123 MATCH_MP_TAC inf_pos_y;
 124 ASM_REWRITE_TAC[]
 125 ]);;
 126
 127 let h_b_inc = prove_by_refinement(
 128 `(!i. INFINITE (N i)) ==> (!i.  (h_b N i  <  h_b N (SUC i) ))`,
 129 [
 130 (* unpack *)
 131 REWRITE_TAC[h_b];
 132 DISCH_TAC;
 133 GEN_TAC;
 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));
 137 (* resolve *)
 138 SELECT_TAC;
 139 POP_ASSUM MP_TAC THEN ARITH_TAC;
 140 ASM_MESON_TAC[IN];
 141 ]);;
 142
 143 let lemma_inc_injective = Hypermap.lemma_inc_injective;;
 144
 145 let h_b_inj = prove(
 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]);;
 148
 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))`;;
 152
 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))))`,
 156 [
 157 REWRITE_TAC[continuum_family];
 158 MESON_TAC[COUNTABLE_AS_INJECTIVE_IMAGE]
 159 ]);;
 160
 161 (* Harrison's lemma *)
 162 let WELLDEFINED_FUNCTION_1 = Tactics.WELLDEFINED_FUNCTION_1;;
 163
 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))))`,
 169 [
 170 REPEAT STRIP_TAC;
 171 MP_TAC (ISPEC `s:A->bool` COUNTABLE_AS_INJECTIVE_IMAGE);
 172 ASM_REWRITE_TAC[];
 173 REPEAT STRIP_TAC;
 174 EXISTS_TAC `f:num->A`;
 175 ASM_REWRITE_TAC[];
 176 SUBGOAL_THEN  `?g:A->num. (!n. g (f n) = n)` MP_TAC;
 177 ASM_REWRITE_TAC[WELLDEFINED_FUNCTION_1];
 178 REPEAT STRIP_TAC;
 179 EXISTS_TAC `g:A->num`;
 180 ASM_REWRITE_TAC[IN_IMAGE];
 181 ASM_MESON_TAC[];
 182 ]);;
 183
 184
 185 let h_b_IN = prove_by_refinement(
 186   `(!i. INFINITE (N i)) ==> (!i. (h_b N i IN N i))`,
 187 [
 188 REPEAT STRIP_TAC;
 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
 192 SELECT_ELIM_TAC THEN
 193 REPEAT STRIP_TAC THEN
 194 ASM_MESON_TAC[inf_ex;IN];
 195 ]);;
 196
 197 let phi_domain_inf = prove_by_refinement(
 198  `(?b:real->num_seq.  ONTO b) ==>
 199     (!x. INFINITE (phi_domain x))`,
 200 [
 201 REWRITE_TAC[phi_domain;phin];
 202 DISCH_TAC;
 203 SELECT_ELIM_TAC;
 204 REPEAT STRIP_TAC;
 205 ASM_MESON_TAC[num_seq_type]
 206 ]);;
 207
 208 let lemma1 =  prove_by_refinement
 209  (`(?b:real->num_seq.  ONTO b) ==> (!A x. continuum_family A ==>
 210     (?h.  (
 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)))`,
 213 [
 214 (* unpack *)
 215 REWRITE_TAC[continuum_family];
 216 REPEAT STRIP_TAC;
 217 (* fact gathering *)
 218 MP_TAC (ISPEC `(A:real->real->bool) x` countable_bij);
 219 ASM_REWRITE_TAC[];
 220 REPEAT STRIP_TAC;
 221 SUBGOAL_THEN `!a. a IN (A:real->real->bool) x ==> (phi_domain a) = (phi_domain o (f:num->real)) (g a) ` ASSUME_TAC;
 222 REWRITE_TAC[o_THM];
 223 ASM_MESON_TAC[IN];
 224 SUBGOAL_THEN `!i:num. INFINITE ((phi_domain o f) i)` ASSUME_TAC;
 225 REWRITE_TAC[o_THM];
 226 ASM_MESON_TAC[phi_domain_inf];
 227 (* hit the goal *)
 228 EXISTS_TAC `\(y:real).  if A (x:real) y then h_b (phi_domain o f) (g y) else 0`;
 229 BETA_TAC;
 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];
 235 ]);;
 236
 237 let lem = REWRITE_RULE [RIGHT_IMP_EXISTS_THM;SKOLEM_THM]
 238   lemma1;;
 239
 240 let hx = new_specification ["hx"] lem;;
 241
 242 let WELLDEFINED_FUNCTION_2b = Tactics.WELLDEFINED_FUNCTION_2b;;
 243
 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))`,
 248 [
 249 REPEAT STRIP_TAC; (* unpack *)
 250 REWRITE_TAC[WELLDEFINED_FUNCTION_2b;PAIR_EQ]; (* strategy *)
 251 REPEAT STRIP_TAC;
 252 SUBGOAL_THEN `(y:real) = y'`  ASSUME_TAC ;
 253 ASM_MESON_TAC[hx];
 254 ASM_REWRITE_TAC[]
 255 ]);;
 256
 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))`,
 261 [
 262 REPEAT STRIP_TAC;
 263 MP_TAC (ISPECL [`A:real->real->bool`; `b:real->num_seq`] f_ex);
 264 ASM_REWRITE_TAC[];
 265 STRIP_TAC;
 266 EXISTS_TAC `\ n x . (f:num#real->real) (n,x)`;
 267 BETA_TAC;
 268 ASM_REWRITE_TAC[];
 269 ]);;
 270
 271 let fd_ex = prove_by_refinement(
 272  `?f. !A. (continuum_family A) /\ (?(b:real->num_seq). ONTO b)
 273    ==>
 274    (!x y. A x y ==> f A (hx A x y) x = phi y (hx A x y))`,
 275 [
 276 REWRITE_TAC[GSYM SKOLEM_THM];
 277 ASM_MESON_TAC[fc_ex]
 278 ]);;
 279
 280 let fd = new_specification[ "fd"] fd_ex;;
 281
 282
 283 let r_exists = prove_by_refinement(
 284   `!X (b:real->num_seq). INFINITE { n | ~((X n) = (:real)) } /\  (ONTO b)  ==>
 285   (?r.
 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)))`,
 288 [
 289 REPEAT GEN_TAC;
 290 ABBREV_TAC `N = { n:num | ~(X n = (:real) ) }`;
 291 STRIP_TAC;
 292 FIRST_RULE_ASSUM (MATCH_MP (ISPEC `0` inf_pos_y)) ASSUME_TAC;
 293 (* intro ph, N0  *)
 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];
 298 REPEAT STRIP_TAC;
 299 (* *)
 300 SUBGOAL_THEN `dest_num_seq (mk_num_seq (ph,N0)) = (ph,N0)` ASSUME_TAC;
 301 ASM_REWRITE_TAC[GSYM num_seq_type];
 302 CONJ_TAC;
 303 ASM_MESON_TAC[IN];
 304 EXPAND_TAC "N0";
 305 REWRITE_TAC[IN_ELIM_THM;TAUT `a /\ b ==> a`];
 306 (* intro r *)
 307 SUBGOAL_THEN `?(r:real). phin r = mk_num_seq (ph,N0)` MP_TAC;
 308 ASM_MESON_TAC[ONTO;phin];
 309 REPEAT STRIP_TAC;
 310 (*  *)
 311 SUBGOAL_THEN `(phi_domain r = N0) /\ (phi r = ph)`   MP_TAC;
 312 ASM_REWRITE_TAC[phi_domain;phi];
 313 REPEAT STRIP_TAC;
 314 EXISTS_TAC `r:real`;
 315 ASM_REWRITE_TAC[];
 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));
 318 EXPAND_TAC"N0";
 319 EXPAND_TAC"N";
 320 REWRITE_TAC[IN_ELIM_THM];
 321 ]
 322 );;
 323
 324
 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)`,
 328 [
 329 (* unpack *)
 330 REPEAT STRIP_TAC;
 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);
 333 BETA_TAC;
 334 ASM_REWRITE_TAC[];
 335 REPEAT STRIP_TAC;
 336 (* unpack continuum family *)
 337 UNDISCH_THEN `continuum_family A` (fun t -> ASSUME_TAC t THEN MP_TAC (REWRITE_RULE[continuum_family] t));
 338 REPEAT STRIP_TAC;
 339 (* unpack goal *)
 340 MATCH_MP_TAC COUNTABLE_SUBSET; (* strategy *)
 341 EXISTS_TAC `(A:real->real->bool) r`;
 342 ASM_REWRITE_TAC[SUBSET];
 343 REPEAT STRIP_TAC;
 344 REFUTE_THEN ASSUME_TAC;
 345 (* *)
 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]];
 348 (*  *)
 349 SUBGOAL_THEN `hx A x r IN phi_domain r` ASSUME_TAC;
 350 ASM_MESON_TAC[hx;IN];
 351 (* *)
 352 SUBGOAL_THEN `~(phi r (hx A x r) IN IMAGE (fd A (hx A x r)) s)` MP_TAC;
 353 ASM_MESON_TAC[];
 354 REWRITE_TAC[IN_IMAGE];
 355 EXISTS_TAC`x:real`;
 356 ASM_REWRITE_TAC[];
 357 ]);;
 358
 359
 360
 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)) }))`,
 365 [
 366 REPEAT STRIP_TAC;
 367 EXISTS_TAC`fd A`;
 368 REPEAT STRIP_TAC;
 369 MP_TAC (ISPECL[`A:real->real->bool`;`b:real->num_seq`;`s:real->bool`] countable_s);
 370 ASM_REWRITE_TAC[INFINITE];
 371 ]);;
 372
 373 (* complete at 1:25 pm July 4, 2010.  *)
 374
 375 end;;