(* -*- holl -*- *)

g `!u s. s SUBSET INTERS u <=> (!t. t IN u ==> s SUBSET t)`;;
e (SET_TAC[]);;
let SUBSET_INTERS = top_thm ();;

let TOPOLOGY = new_definition
  `TOPOLOGY X = { U:(A->bool)->bool |
                  UNIONS U = X /\
     		  (!a. a SUBSET U ==> UNIONS a IN U) /\
       		  (!u v. u IN U /\ v IN U ==> u INTER v IN U) }`;;

g `!U X. U IN TOPOLOGY X <=> 
         UNIONS U = X /\
       	 (!a. a SUBSET U ==> UNIONS a IN U) /\
         (!u v. u IN U /\ v IN U ==> u INTER v IN U)`;;
e (REWRITE_TAC [TOPOLOGY; IN_ELIM_THM]);;
let IN_TOPOLOGY = top_thm ();;

g `!X U. U IN TOPOLOGY X ==> UNIONS U = X`;;
e (SIMP_TAC [IN_TOPOLOGY]);;
let TOPOLOGY_UNIONS_EQ_ALL = top_thm ();;

g `!X U. U IN TOPOLOGY X /\ u IN U ==> u SUBSET X`;;
e (REWRITE_TAC [IN_TOPOLOGY; SUBSET]);;
e (SET_TAC []);;
let TOPOLOGY_SUBSET = top_thm ();;

g `!X U a. U IN TOPOLOGY X /\ a SUBSET U ==> UNIONS a IN U`;;
e (SIMP_TAC [IN_TOPOLOGY]);;
let OPEN_UNIONS = top_thm ();;

g `!X U u v. U IN TOPOLOGY X /\ u IN U /\ v IN U ==> u INTER v IN U`;;
e (SIMP_TAC [IN_TOPOLOGY]);;
let OPEN_INTER = top_thm ();;

g `!(X:A->bool) U. U IN TOPOLOGY X ==> {} IN U`;;
e (REWRITE_TAC [IN_TOPOLOGY]);;
e (REPEAT STRIP_TAC);;
e (FIRST_X_ASSUM (MP_TAC o SPEC `{}:(A->bool)->bool`));;
e (REWRITE_TAC [EMPTY_SUBSET; UNIONS_0]);;
let OPEN_EMPTY = top_thm ();;

g `!X U. U IN TOPOLOGY X ==> X IN U`;;
e (MESON_TAC [OPEN_UNIONS; TOPOLOGY_UNIONS_EQ_ALL; SUBSET_REFL]);;
let OPEN_ALL = top_thm ();;

(* ------------------------------------------------------------------------- *)
(* Topologia discreta.                                                       *)
(* ------------------------------------------------------------------------- *)

let DISCRETE_TOPOLOGY = new_definition
  `!X. DISCRETE_TOPOLOGY X = {u | u SUBSET X}`;;

g `!X. DISCRETE_TOPOLOGY X IN TOPOLOGY X`;;
e (REWRITE_TAC [DISCRETE_TOPOLOGY; IN_TOPOLOGY]);;
e (SET_TAC[]);;
let DISCRETE_TOPOLOGY_IN_TOPOLOGY = top_thm ();;

(* ------------------------------------------------------------------------- *)
(* Topologia banale.                                                         *)
(* ------------------------------------------------------------------------- *)

let COARSE_TOPOLOGY = new_definition
  `!X. COARSE_TOPOLOGY X = {{}, X}`;;

g `!X:A->bool. COARSE_TOPOLOGY X IN TOPOLOGY X`;;
e GEN_TAC;;
e (REWRITE_TAC [IN_TOPOLOGY; COARSE_TOPOLOGY]);;
e CONJ_TAC;;
e (REWRITE_TAC [UNIONS_2; UNION_EMPTY]);;
e CONJ_TAC;;
e (REWRITE_TAC [IN_INSERT; NOT_IN_EMPTY; EMPTY_UNIONS]);;
e GEN_TAC;;
e DISCH_TAC;;
e (SUBGOAL_THEN `a = {} \/ a = {{}} \/ a = {X:A->bool} \/ a = {{}, X}`
     STRIP_ASSUME_TAC);;
e (SET_TAC []);;
e (ASM_REWRITE_TAC []);;
e (SET_TAC []);;
e (ASM_REWRITE_TAC [UNIONS_0; IN_INSERT; NOT_IN_EMPTY]);;
e (SET_TAC []);;
e (ASM_REWRITE_TAC [UNIONS_2]);;
e (SET_TAC []);;
e (REWRITE_TAC [IN_INSERT; NOT_IN_EMPTY]);;
e (SET_TAC []);;
let COARSE_TOPOLOGY_IN_TOPOLOGY = top_thm ();;

(* ------------------------------------------------------------------------- *)
(* Spazi connessi.                                                           *)
(* ------------------------------------------------------------------------- *)

let CONNECTED = new_definition
  `!X U. CONNECTED U X <=>
         U IN TOPOLOGY X /\
 	 (!u v. u IN U /\ v IN U /\ u UNION v = X /\ DISJOINT u v
                ==> u = {} \/ v = {})`;;

g `!X. CONNECTED (COARSE_TOPOLOGY X) X`;;
e GEN_TAC;;
e (REWRITE_TAC [CONNECTED; COARSE_TOPOLOGY_IN_TOPOLOGY]);;
e (REWRITE_TAC [COARSE_TOPOLOGY]);;
e (REWRITE_TAC [IN_INSERT; NOT_IN_EMPTY]);;
e (SET_TAC []);;
let CONNECTED_COARSE_TOPOLOGY = top_thm ();;

(* ------------------------------------------------------------------------- *)
(* Ricoprimenti.                                                             *)
(* ------------------------------------------------------------------------- *)

let COVER = new_definition
  `!X U a. COVER X U a <=> U IN TOPOLOGY X /\ a SUBSET U /\ UNIONS a = X`;;

g `!X U. U IN TOPOLOGY X ==> COVER X U U`;;
e (SIMP_TAC [COVER;SUBSET_REFL;IN_TOPOLOGY]);;
let TRIVIAL_COVER = top_thm();;

g `!(X:A->bool) U. FINITE X /\ U IN TOPOLOGY X ==> FINITE U`;;
e (REWRITE_TAC [IN_TOPOLOGY]);;
e (REPEAT STRIP_TAC);;
e (SUBGOAL_THEN `U SUBSET {t | t SUBSET X:A->bool}`
      ASSUME_TAC);;
e (SET_TAC[]);;
e (ASM_MESON_TAC[FINITE_POWERSET;FINITE_SUBSET]);;
let FINITE_IMP_FINITE_TOPOLOGY = top_thm ();;