100/cantor.ml

   1 (* ========================================================================= *)
   2 (* Cantor's theorem.                                                         *)
   3 (* ========================================================================= *)
   4
   5 (* ------------------------------------------------------------------------- *)
   6 (* Ad hoc version for whole type.                                            *)
   7 (* ------------------------------------------------------------------------- *)
   8
   9 let CANTOR_THM_INJ = prove
  10  (`~(?f:(A->bool)->A. (!x y. f(x) = f(y) ==> x = y))`,
  11   REWRITE_TAC[INJECTIVE_LEFT_INVERSE; NOT_EXISTS_THM] THEN
  12   MAP_EVERY X_GEN_TAC [`f:(A->bool)->A`; `g:A->(A->bool)`] THEN
  13   DISCH_THEN(MP_TAC o SPEC `\x:A. ~(g x x)`) THEN MESON_TAC[]);;
  14
  15 let CANTOR_THM_SURJ = prove
  16  (`~(?f:A->(A->bool). !s. ?x. f x = s)`,
  17   REWRITE_TAC[SURJECTIVE_RIGHT_INVERSE; NOT_EXISTS_THM] THEN
  18   MAP_EVERY X_GEN_TAC [`g:A->(A->bool)`; `f:(A->bool)->A`] THEN
  19   DISCH_THEN(MP_TAC o SPEC `\x:A. ~(g x x)`) THEN MESON_TAC[]);;
  20
  21 (* ------------------------------------------------------------------------- *)
  22 (* Proper version for any set, in terms of cardinality operators.            *)
  23 (* ------------------------------------------------------------------------- *)
  24
  25 let CANTOR = prove
  26  (`!s:A->bool. s <_c {t | t SUBSET s}`,
  27   GEN_TAC THEN REWRITE_TAC[lt_c] THEN CONJ_TAC THENL
  28    [REWRITE_TAC[le_c] THEN EXISTS_TAC `(=):A->A->bool` THEN
  29     REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM; SUBSET; IN] THEN MESON_TAC[];
  30     REWRITE_TAC[LE_C; IN_ELIM_THM; SURJECTIVE_RIGHT_INVERSE] THEN
  31     REWRITE_TAC[NOT_EXISTS_THM] THEN X_GEN_TAC `g:A->(A->bool)` THEN
  32     DISCH_THEN(MP_TAC o SPEC `\x:A. s(x) /\ ~(g x x)`) THEN
  33     REWRITE_TAC[SUBSET; IN; FUN_EQ_THM] THEN MESON_TAC[]]);;
  34
  35 (* ------------------------------------------------------------------------- *)
  36 (* More explicit "injective" version as in Paul Taylor's book.               *)
  37 (* ------------------------------------------------------------------------- *)
  38
  39 let CANTOR_THM_INJ' = prove
  40  (`~(?f:(A->bool)->A. (!x y. f(x) = f(y) ==> x = y))`,
  41   STRIP_TAC THEN
  42   ABBREV_TAC `(g:A->A->bool) = \a. { b | !s. f(s) = a ==> b IN s}` THEN
  43   MP_TAC(ISPEC `g:A->A->bool`
  44    (REWRITE_RULE[NOT_EXISTS_THM] CANTOR_THM_SURJ)) THEN
  45   FIRST_X_ASSUM(SUBST_ALL_TAC o SYM) THEN
  46   ASM_REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
  47   ASM_MESON_TAC[]);;
  48
  49 (* ------------------------------------------------------------------------- *)
  50 (* Another sequence of versions (Lawvere, Cantor, Taylor) taken from         *)
  51 (* http://ncatlab.org/nlab/show/Cantor%27s+theorem.                          *)
  52 (* ------------------------------------------------------------------------- *)
  53
  54 let CANTOR_LAWVERE = prove
  55  (`!h:A->(A->B).
  56         (!f:A->B. ?x:A. h(x) = f) ==> !n:B->B. ?x. n(x) = x`,
  57   REPEAT STRIP_TAC THEN
  58   ABBREV_TAC `g:A->B = \a. (n:B->B) (h a a)` THEN
  59   RULE_ASSUM_TAC(REWRITE_RULE[FUN_EQ_THM]) THEN
  60   ASM_MESON_TAC[]);;
  61
  62 let CANTOR = prove
  63  (`!f:A->(A->bool). ~(!s. ?x. f x = s)`,
  64   GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP CANTOR_LAWVERE) THEN
  65   DISCH_THEN(MP_TAC o SPEC `(~)`) THEN MESON_TAC[]);;
  66
  67 let CANTOR_TAYLOR = prove
  68  (`!f:(A->bool)->A. ~(!x y. f(x) = f(y) ==> x = y)`,
  69   REPEAT STRIP_TAC THEN
  70   MP_TAC(ISPEC `\a:A.  { b:A | !s. f(s) = a ==> b IN s}`
  71    (REWRITE_RULE[NOT_EXISTS_THM] CANTOR)) THEN
  72   REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
  73   ASM_MESON_TAC[]);;
  74
  75 let SURJECTIVE_COMPOSE = prove
  76  (`(!y. ?x. f(x) = y) /\ (!z. ?y. g(y) = z)
  77    ==> (!z. ?x. (g o f) x = z)`,
  78   MESON_TAC[o_THM]);;
  79
  80 let INJECTIVE_SURJECTIVE_PREIMAGE = prove
  81  (`!f:A->B. (!x y. f(x) = f(y) ==> x = y) ==> !t. ?s. {x | f(x) IN s} = t`,
  82   REPEAT STRIP_TAC THEN
  83   EXISTS_TAC `IMAGE (f:A->B) t` THEN
  84   REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_IMAGE] THEN
  85   ASM_MESON_TAC[]);;
  86
  87 let CANTOR_JOHNSTONE = prove
  88  (`!i:B->S f:B->S->bool.
  89         ~((!x y. i(x) = i(y) ==> x = y) /\ (!s. ?z. f(z) = s))`,
  90   REPEAT STRIP_TAC THEN
  91   MP_TAC(ISPEC
  92    `(IMAGE (f:B->S->bool)) o (\s:S->bool. {x | i(x) IN s})`
  93     (REWRITE_RULE[NOT_EXISTS_THM] CANTOR)) THEN
  94   REWRITE_TAC[] THEN MATCH_MP_TAC SURJECTIVE_COMPOSE THEN
  95   ASM_REWRITE_TAC[SURJECTIVE_IMAGE] THEN
  96   MATCH_MP_TAC INJECTIVE_SURJECTIVE_PREIMAGE THEN
  97   ASM_REWRITE_TAC[]);;