flyspeck_needs "general/tactics.hl";;

module Sierpinski:sig

  val INFINITE_CRIT:thm

  val INFINITE_EXISTS:thm

  val num_seq_type:thm

  val sierpinski:thm

end = 

struct

let SELECT_TAC= Tactics.SELECT_TAC;;
let EVERY_PAT_ASSUM = Tactics.EVERY_PAT_ASSUM;;

(* Sierpinski's theorem *)

(* start 3:36 July 3 *)

let INFINITE_CRIT = 
prove( 
 `!X Y Z. INFINITE X /\ FINITE Y /\ (Z = X DIFF Y) ==> INFINITE Z`,

MESON_TAC[INFINITE_DIFF_FINITE]
);;
(*
let INFINITE_EXISTS = prove_by_refinement (
`!x P. INFINITE { (x:A) | P x } ==> (?x. P x)`,
[
REWRITE_TAC[INFINITE];
REPEAT STRIP_TAC;
SUBGOAL_THEN `~({(x:A) | P x} = {})` MP_TAC;
ASM_MESON_TAC[FINITE_EMPTY];
REWRITE_TAC[EXTENSION;NOT_IN_EMPTY;IN_ELIM_THM];
MESON_TAC[];
]);;
*)

let INFINITE_EXISTS = 
prove_by_refinement (
`!x P. INFINITE { (x:A) | P x } ==> (?x. P x)`,

[
REWRITE_TAC[INFINITE];
REPEAT STRIP_TAC;
ASM_CASES_TAC `({(x:A) | P x} = {})` ;
ASM_MESON_TAC[FINITE_EMPTY];
POP_ASSUM MP_TAC;
SET_TAC[];
]);;
let numm0 = 
prove_by_refinement(`{n | n > 0 } = (:num) DIFF {0}`,

[
REWRITE_TAC[DIFF;FUN_EQ_THM;IN_ELIM_THM;IN_SING;SET_RULE `x IN (:num)`];
ARITH_TAC;
]);;
let inf_pos_y = 
prove_by_refinement( 
  `!y N. INFINITE N ==> INFINITE { (n:num) | n > y /\ n IN N }`,

[
REPEAT STRIP_TAC;
MATCH_MP_TAC INFINITE_CRIT; (* strategy *)
ASM_MESON_TAC[num_y;FINITE_NUMSEG_LE]; (* terminator *)
]);;
let inf_pos = 
prove_by_refinement( 
`INFINITE { n | n > 0 }`,

[
MATCH_MP_TAC INFINITE_CRIT; 
MESON_TAC[numm0;FINITE_SING;num_INFINITE];
]);;

let num_seq_exists = 
prove_by_refinement( 
`?x.  (!n. ~(SND x n) ==> (FST x n =  &0)) /\
    INFINITE (SND x) /\ (!n.  n IN SND x  ==> n >0)`,

[
 EXISTS_TAC `(\n:num. &0), { n | n > 0}`;
 REWRITE_TAC[FST;SND;IN_ELIM_THM;inf_pos]
]);;
let num_seq_type = new_type_definition 
  "num_seq" ("mk_num_seq","dest_num_seq") num_seq_exists;;

let num_seq_axiom = `(?f:real->num_seq.  ONTO f)`;;

let phin = new_definition `phin = @(f:real->num_seq). ONTO f`;;
let phi_domain = new_definition 
  `phi_domain b = SND (dest_num_seq (phin b))`;;
let phi = new_definition 
  `phi b = FST (dest_num_seq (phin b))`;;
let phin_ONTO = 
prove_by_refinement(
  `(?f: real->num_seq. ONTO f) ==> (!ns. ?b. phin b = ns)`,

[
REWRITE_TAC[phin];
SELECT_ELIM_TAC;
MESON_TAC[ONTO]
]);;
let h_b = define 
 `(h_b N 0 = @(n:num). N 0 n) /\ (h_b N (SUC i) = @n. (N  (SUC i) n /\ n > h_b N i))`;;

let num_y = 
prove_by_refinement(
  `{(n:num) | n > y /\ n IN N} = N DIFF {n | n <= y}`,

[
REWRITE_TAC[DIFF;FUN_EQ_THM;IN_ELIM_THM;IN_SING];
GEN_TAC;
MATCH_MP_TAC (TAUT` (x = y) ==>  (x /\ a <=> a /\ y) `);
ARITH_TAC;
]);;
let inf_ex = 
prove_by_refinement(  `!y. INFINITE N ==> ?(n:num). n > y /\ n IN N`,

[
REPEAT STRIP_TAC;
MATCH_MP_TAC INFINITE_EXISTS; 
MATCH_MP_TAC inf_pos_y;
ASM_REWRITE_TAC[]
]);;
let h_b_inc = 
prove_by_refinement(
`(!i. INFINITE (N i)) ==> (!i.  (h_b N i  <  h_b N (SUC i) ))`,

[
(* unpack *)
REWRITE_TAC[h_b];
DISCH_TAC;
GEN_TAC;
(* prep assumptions *)
FIRST_X_ASSUM (ASSUME_TAC o (ISPEC `SUC i:num`));
FIRST_X_ASSUM (ASSUME_TAC o (MATCH_MP inf_ex));
(* resolve *)
SELECT_TAC;
POP_ASSUM MP_TAC THEN ARITH_TAC;
ASM_MESON_TAC[IN];
]);;
let lemma_inc_injective = Hypermap.lemma_inc_injective;;

let h_b_inj = 
prove(
  `(!i. INFINITE (N i)) ==> (!i j. (i = j) <=> (h_b N i = h_b N j))`,

   MESON_TAC [h_b_inc;lemma_inc_injective]);;
let continuum_family = new_definition `continuum_family A =
    ((!(x:real). INFINITE(A x) /\ (COUNTABLE (A x))) /\ 
    (!x y. x IN A y \/ y IN A x))`;;
let continuum_bij = 
prove_by_refinement( 
  `continuum_family A ==> (!x. (?b.  (A x = IMAGE b (:num)) /\
			     (!m n. (b m = b n) ==> (m = n))))`,

[
REWRITE_TAC[continuum_family];
MESON_TAC[COUNTABLE_AS_INJECTIVE_IMAGE]
]);;
(* Harrison's lemma *)
let WELLDEFINED_FUNCTION_1 = Tactics.WELLDEFINED_FUNCTION_1;;

let countable_bij = 
prove_by_refinement( 
  `!s. (COUNTABLE (s:A->bool)) /\ (INFINITE s) ==> (?f g. 
        (s = IMAGE f (:num) /\ (!m n. f m = f n ==> m = n) /\
        (!n. g (f n) = n) /\ (!a. a IN s ==> f (g a) = a) /\ 
        (!a b. a IN s /\ b IN s /\ (g a = g b) ==> (a = b))))`,

[
REPEAT STRIP_TAC;
MP_TAC (ISPEC `s:A->bool` COUNTABLE_AS_INJECTIVE_IMAGE);
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
EXISTS_TAC `f:num->A`;
ASM_REWRITE_TAC[];
SUBGOAL_THEN  `?g:A->num. (!n. g (f n) = n)` MP_TAC;
ASM_REWRITE_TAC[WELLDEFINED_FUNCTION_1];
REPEAT STRIP_TAC;
EXISTS_TAC `g:A->num`;
ASM_REWRITE_TAC[IN_IMAGE];
ASM_MESON_TAC[];
]);;

let h_b_IN = 
prove_by_refinement(
  `(!i. INFINITE (N i)) ==> (!i. (h_b N i IN N i))`,

[
REPEAT STRIP_TAC;
DISJ_CASES_TAC (SPEC `i:num` num_CASES) THEN
TRY(FIRST_X_ASSUM MP_TAC) THEN REPEAT STRIP_TAC THEN
ASM_REWRITE_TAC[h_b;IN] THEN
SELECT_ELIM_TAC THEN
REPEAT STRIP_TAC THEN
ASM_MESON_TAC[inf_ex;IN];
]);;
let phi_domain_inf = 
prove_by_refinement( 
 `(?b:real->num_seq.  ONTO b) ==> 
    (!x. INFINITE (phi_domain x))`,

[
REWRITE_TAC[phi_domain;phin];
DISCH_TAC;
SELECT_ELIM_TAC;
REPEAT STRIP_TAC;
ASM_MESON_TAC[num_seq_type]
]);;
let lemma1 = 
prove_by_refinement 
 (`(?b:real->num_seq.  ONTO b) ==> (!A x. continuum_family A ==>
    (?h.  (
         (! y z. A x y /\ A x z /\ (h y = h z) ==> (y = z))) /\
             (!y. A x y ==> h y IN phi_domain y) /\ (!y. ~(A x y) ==> h y = 0)))`,

[
(* unpack *)
REWRITE_TAC[continuum_family];
REPEAT STRIP_TAC;
(* fact gathering *)
MP_TAC (ISPEC `(A:real->real->bool) x` countable_bij);
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
SUBGOAL_THEN `!a. a IN (A:real->real->bool) x ==> (phi_domain a) = (phi_domain o (f:num->real)) (g a) ` ASSUME_TAC;
REWRITE_TAC[o_THM];
ASM_MESON_TAC[IN];
SUBGOAL_THEN `!i:num. INFINITE ((phi_domain o f) i)` ASSUME_TAC;
REWRITE_TAC[o_THM];
ASM_MESON_TAC[phi_domain_inf];
(* hit the goal *)
EXISTS_TAC `\(y:real).  if A (x:real) y then h_b (phi_domain o f) (g y) else 0`;
BETA_TAC;
REPEAT CONJ_TAC THEN REPEAT STRIP_TAC THEN
(* terminate every subgoal *)
TRY(FIRST_X_ASSUM MP_TAC) THEN
ASM_REWRITE_TAC[] THEN
ASM_MESON_TAC[IN;h_b_inj;h_b_IN];
]);;
let lem = REWRITE_RULE [RIGHT_IMP_EXISTS_THM;SKOLEM_THM]
  lemma1;;

let hx = new_specification ["hx"] lem;;
let WELLDEFINED_FUNCTION_2b = Tactics.WELLDEFINED_FUNCTION_2b;;

(* next existence of f *)
let f_ex = 
prove_by_refinement 
(`!A (b:real->num_seq).   (continuum_family A) /\ (ONTO b) ==>
   (?(f:(num#real) -> real). !x y. A x y ==> f ((hx A x y), x) = phi y (hx A x y))`,

[
REPEAT STRIP_TAC; (* unpack *)
REWRITE_TAC[WELLDEFINED_FUNCTION_2b;PAIR_EQ]; (* strategy *)
REPEAT STRIP_TAC;
SUBGOAL_THEN `(y:real) = y'`  ASSUME_TAC ;
ASM_MESON_TAC[hx];
ASM_REWRITE_TAC[]
]);;
let fc_ex = 
prove_by_refinement(
 `!A (b:real->num_seq).   (continuum_family A) /\ (ONTO b) ==>
   (?(f:num->real -> real). !x y. A x y ==> 
  f (hx A x y) x = phi y (hx A x y))`,

[
REPEAT STRIP_TAC;
MP_TAC (ISPECL [`A:real->real->bool`; `b:real->num_seq`] f_ex);
ASM_REWRITE_TAC[];
STRIP_TAC;
EXISTS_TAC `\ n x . (f:num#real->real) (n,x)`;
BETA_TAC;
ASM_REWRITE_TAC[];
]);;
let fd_ex = 
prove_by_refinement(
 `?f. !A. (continuum_family A) /\ (?(b:real->num_seq). ONTO b) 
   ==>
   (!x y. A x y ==> f A (hx A x y) x = phi y (hx A x y))`,

[
REWRITE_TAC[GSYM SKOLEM_THM];
ASM_MESON_TAC[fc_ex]
]);;
let fd = new_specification[ "fd"] fd_ex;;

let r_exists = 
prove_by_refinement(
  `!X (b:real->num_seq). INFINITE { n | ~((X n) = (:real)) } /\  (ONTO b)  ==>
  (?r. 
  (phi_domain r =  {n | n > 0 /\ (~((X n) = (:real))) } ) /\ 
  (!n. if n IN phi_domain r then ~(phi r n IN X n) else (phi r n = &0)))`,

[
REPEAT GEN_TAC;
ABBREV_TAC `N = { n:num | ~(X n = (:real) ) }`;
STRIP_TAC;
FIRST_RULE_ASSUM (MATCH_MP (ISPEC `0` inf_pos_y)) ASSUME_TAC; 
(* intro ph, N0  *)
ABBREV_TAC `N0 = {n | n > 0 /\ n IN N}`;
SUBGOAL_THEN `?ph. !(n:num). if (n IN N0) then (~(ph n IN X n)) else (ph n= &0)` MP_TAC;
REWRITE_TAC[GSYM SKOLEM_THM];
ASM SET_TAC[IN_ELIM_THM];
REPEAT STRIP_TAC;
(* *)
SUBGOAL_THEN `dest_num_seq (mk_num_seq (ph,N0)) = (ph,N0)` ASSUME_TAC;
ASM_REWRITE_TAC[GSYM num_seq_type];
CONJ_TAC;
ASM_MESON_TAC[IN];
EXPAND_TAC "N0";
REWRITE_TAC[IN_ELIM_THM;TAUT `a /\ b ==> a`];
(* intro r *)
SUBGOAL_THEN `?(r:real). phin r = mk_num_seq (ph,N0)` MP_TAC;
ASM_MESON_TAC[ONTO;phin];
REPEAT STRIP_TAC;
(*  *)
SUBGOAL_THEN `(phi_domain r = N0) /\ (phi r = ph)`   MP_TAC;
ASM_REWRITE_TAC[phi_domain;phi];
REPEAT STRIP_TAC;
EXISTS_TAC `r:real`;
ASM_REWRITE_TAC[];
EVERY_PAT_ASSUM [`ph:num->real`] (fun t-> UNDISCH_THEN (concl t) (K ALL_TAC));
EVERY_PAT_ASSUM [`phi_domain`] (fun t-> UNDISCH_THEN (concl t) (K ALL_TAC));
EXPAND_TAC"N0";
EXPAND_TAC"N";
REWRITE_TAC[IN_ELIM_THM];
]
);;


let countable_s = 
prove_by_refinement(
  `!A (b:real->num_seq) s. (continuum_family A) /\ (ONTO b) /\
    (INFINITE { n | ~(IMAGE (fd A n) s = (:real) ) }) ==> (COUNTABLE s)`,

[
(* unpack *)
REPEAT STRIP_TAC;
ABBREV_TAC `N = { n | ~(IMAGE (fd A n) s = (:real) ) }`;
MP_TAC (ISPECL [`\n. IMAGE (fd A n) s`;`b:real->num_seq`] r_exists);
BETA_TAC;
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
(* unpack continuum family *)
UNDISCH_THEN `continuum_family A` (fun t -> ASSUME_TAC t THEN MP_TAC (REWRITE_RULE[continuum_family] t));
REPEAT STRIP_TAC;
(* unpack goal *)
MATCH_MP_TAC COUNTABLE_SUBSET; (* strategy *)
EXISTS_TAC `(A:real->real->bool) r`;
ASM_REWRITE_TAC[SUBSET];
REPEAT STRIP_TAC;
REFUTE_THEN ASSUME_TAC;
(* *)
SUBGOAL_TAC "A" `r IN (A:real->real -> bool) x` [ASM_MESON_TAC[]];
SUBGOAL_TAC "B" `fd A  (hx A x r) x = phi r (hx A x r)` [ASM_MESON_TAC[IN;fd]];
(*  *)
SUBGOAL_THEN `hx A x r IN phi_domain r` ASSUME_TAC;
ASM_MESON_TAC[hx;IN];
(* *)
SUBGOAL_THEN `~(phi r (hx A x r) IN IMAGE (fd A (hx A x r)) s)` MP_TAC;
ASM_MESON_TAC[];
REWRITE_TAC[IN_IMAGE];
EXISTS_TAC`x:real`;
ASM_REWRITE_TAC[];
]);;


let sierpinski = 
prove_by_refinement
(`!A (b:real->num_seq).   (continuum_family A) /\ (ONTO b) ==>
     (?(f:num->real->real). !s. 
           (~(COUNTABLE s) ==> FINITE { n | ~(IMAGE (f n) s = (:real)) }))`,

[
REPEAT STRIP_TAC;
EXISTS_TAC`fd A`;
REPEAT STRIP_TAC;
MP_TAC (ISPECL[`A:real->real->bool`;`b:real->num_seq`;`s:real->bool`] countable_s);
ASM_REWRITE_TAC[INFINITE];
]);;
(* complete at 1:25 pm July 4, 2010.  *)

end;;