(* -*- holl -*- *)

(* SEMINARIO DI GEOMETRIA - LE  BASI DI UNO SPAZIO TOPOLOGICO E LA TOPOLOGIA GENERATA    *)
(* Autore: Emanuele Frandi                                                               *)

(* ABSTRACT: Molte interessanti proprietà degli spazi topologici si possono esprimere    *)
(* vedendo gli spazi stessi come generati da "basi". In questo script, partendo dalle    *)
(* nozioni e dai teoremi di topologia formalizzati in HOL durante il corso, si cerca di  *)
(* definire il concetto di base e dimostrare con HOL alcune semplici proprietà delle     *)
(* basi di spazi topologici.                                                             *)

(*--- Carichiamo anzitutto la libreria di topologia generale realizzata nelle lezioni ---*)

loadt "topology.ml";;

(* 1 - TOPOLOGIA GENERATA                                                                *)

(*------- Definiamo la topologia generata e dimostriamone una proprietà basilare  -------*)

let GENERATED_TOPOLOGY = new_definition
  `!X G. GENERATED_TOPOLOGY X G = INTERS {E | E IN TOPOLOGY X /\ G SUBSET E}`;;

g `!X G. G SUBSET GENERATED_TOPOLOGY X G`;;
e (REPEAT GEN_TAC);;
e (REWRITE_TAC[GENERATED_TOPOLOGY; SUBSET_INTERS]);;
e (REPEAT STRIP_TAC);;
e (SET_TAC[]);;
let GENERATED_TOPOLOGY_SUBSET=top_thm();;

(*--- Vogliamo dimostrare che l'intersezione di una famiglia non vuota di topologie è ---*)
(*--- una topologia ---------------------------------------------------------------------*)

g `!X:A->bool U. (!G. G IN U ==> G IN TOPOLOGY X) /\ ~(U = {}) ==> INTERS U IN TOPOLOGY X`;;
e (REPEAT STRIP_TAC);;
e (REWRITE_TAC[IN_TOPOLOGY; IN_INTERS; SUBSET_INTERS]);;
e (REPEAT CONJ_TAC);;
  e (REWRITE_TAC [EXTENSION; IN_UNIONS]);;
  e (SUBGOAL_THEN `X:A->bool IN INTERS U` ASSUME_TAC);;
   e (REWRITE_TAC [IN_INTERS]);;
   e (REPEAT STRIP_TAC);;
   e (ASM_MESON_TAC [OPEN_ALL]);;
  e (GEN_TAC);;
  e EQ_TAC;;
   e (STRIP_TAC);;
   e (SUBGOAL_THEN `t:A->bool SUBSET X` ASSUME_TAC);;
    e (SUBGOAL_THEN `?G:(A->bool)->bool. G IN U` STRIP_ASSUME_TAC);;
     e (SET_TAC[]);;
    e (SUBGOAL_THEN `t:A->bool IN G` ASSUME_TAC);;
     e (SET_TAC[]);;
    e (ASM_MESON_TAC[TOPOLOGY_SUBSET]);;
   e (SET_TAC[]);;
  e (SET_TAC[]);;
 e (REPEAT STRIP_TAC);;
 e (ASM_MESON_TAC[OPEN_UNIONS]);;
e (ASM_MESON_TAC[OPEN_INTER]);;
let TOP_INTERS=top_thm();;

(* - Vogliamo provare che la topologia generata da una famiglia di sottoinsiemi di uno --*) 
(* - spazio è una topologia ed è la meno fine tra quelle contenenti la famiglia data. ---*)

g `!X:A->bool G. (!s. s IN G ==> s SUBSET X) ==>  GENERATED_TOPOLOGY X G IN TOPOLOGY X`;;
e (REPEAT STRIP_TAC);;
e (REWRITE_TAC[GENERATED_TOPOLOGY]);;
e (MATCH_MP_TAC TOP_INTERS);;
e CONJ_TAC;;
 e (SET_TAC[]);;
e (SUBGOAL_THEN `DISCRETE_TOPOLOGY (X:A->bool) IN TOPOLOGY X` ASSUME_TAC);;
 e (REWRITE_TAC [DISCRETE_TOPOLOGY_IN_TOPOLOGY]);;
e (SUBGOAL_THEN `G SUBSET DISCRETE_TOPOLOGY (X:A->bool)` ASSUME_TAC);;
 e (REWRITE_TAC[DISCRETE_TOPOLOGY]);;
 e (SET_TAC[]);;
e (SET_TAC[]);;
let GENERATED_TOPOLOGY_IN_TOPOLOGY=top_thm();;

g `!X:A->bool G U.(!s. s IN G ==> s SUBSET X) /\ U IN TOPOLOGY X /\ G SUBSET U ==>
   GENERATED_TOPOLOGY X G SUBSET U`;;
e (REPEAT STRIP_TAC);;
e (REWRITE_TAC[GENERATED_TOPOLOGY]);;
e (SET_TAC[]);;
let GENERATED_TOPOLOGY_COARSEST=top_thm();;

(* 2 - BASI DI UNO SPAZIO TOPOLOGICO: DEFINIZIONE E PROPRIETA'                           *)

(*--- Andiamo a definire una base prima in astratto e poi di uno spazio topologico, -----*)
(*--- assieme a un paio di proprietà elementari per usarne la definizione ---------------*) 

let ABSBASIS = new_definition
`!X B. ABSBASIS X B <=> X = UNIONS B /\ (!u v x.  u IN B /\ v IN B /\ x IN u INTER v ==> 
 (?w. w IN B /\ x IN w /\ w SUBSET u INTER v))`;;

g `!X B. ABSBASIS X B ==> X = UNIONS B`;;
e (SIMP_TAC[ABSBASIS]);;
let ABSBASIS_UNIONS_ALL=top_thm();;

g `!X B. ABSBASIS X B ==> (!u v x. u IN B /\ v IN B /\ x IN u INTER v ==> 
   (?w. w IN B /\ x IN w /\ w SUBSET u INTER v))`;;
e (SIMP_TAC[ABSBASIS]);;
let ABSBASIS_INTER=top_thm();;

let BASIS = new_definition
`! X U B. BASIS X U B <=> U IN TOPOLOGY X /\ B SUBSET U /\ 
 !A. A IN U ==> (? S. S SUBSET B /\ UNIONS S = A)`;;

(*--- Dimostriamo alcune proprietà delle basi astratte che saranno utili in seguito ----*)

g `!X B u v. ABSBASIS X B /\ u IN B /\ v IN B ==> u INTER v = UNIONS {w | w IN B
   /\ w SUBSET u INTER v}`;;
e (REWRITE_TAC[ABSBASIS]);;
e (REPEAT STRIP_TAC);;
e (REWRITE_TAC [EXTENSION]);;
e (GEN_TAC);;
e EQ_TAC;;
 e (REWRITE_TAC[IN_UNIONS; IN_ELIM_THM]);;
 e (ASM_MESON_TAC[]);;
e (SET_TAC[]);;
let ABSBASIS_INTER_EQ=top_thm();;

g `!X B u. ABSBASIS X B /\ u IN B ==> u SUBSET X`;;
e (REWRITE_TAC[ABSBASIS]);;
e (SET_TAC[]);;
let ABSBASIS_SUBSET=top_thm();;

g `!X:A->bool B. ABSBASIS X B ==> {UNIONS f | f SUBSET B} IN TOPOLOGY X`;; 
e (REWRITE_TAC[IN_TOPOLOGY; IN_ELIM_THM]);;
e (REPEAT STRIP_TAC);;
  e (SUBGOAL_THEN `X:A->bool = UNIONS B` ASSUME_TAC);;
   e (MATCH_MP_TAC ABSBASIS_UNIONS_ALL);;
   e (ASM_REWRITE_TAC[]);;
  e (REWRITE_TAC [EXTENSION]);;
  e (ASM_REWRITE_TAC [IN_UNIONS; IN_ELIM_THM]);;
  e (GEN_TAC);;
  e EQ_TAC;;
   e (SET_TAC[]);;
  e (STRIP_TAC);;
  e (EXISTS_TAC `t:A->bool`);;
  e (ASM_REWRITE_TAC[]);;
  e (EXISTS_TAC `{t:A->bool}`);;
  e (SET_TAC[]);;
 e (EXISTS_TAC `UNIONS {g:(A->bool)->bool | g SUBSET B /\ UNIONS g IN a}`);;
 e CONJ_TAC;;
  e (REWRITE_TAC[UNIONS_SUBSET; IN_ELIM_THM]);;
  e (SET_TAC[]);;
 e (REWRITE_TAC[EXTENSION; IN_UNIONS; IN_ELIM_THM]);;
 e (GEN_TAC);;
 e EQ_TAC;;
  e (DISCH_THEN (X_CHOOSE_TAC `u:A->bool`));;
  e (SUBGOAL_THEN `?h. u:A->bool = UNIONS h /\ h SUBSET B` STRIP_ASSUME_TAC);;
   e (SUBGOAL_THEN `u:A->bool IN {UNIONS f | f SUBSET B}` MP_TAC);;
    e (SET_TAC[]);;    
   e (REWRITE_TAC[IN_ELIM_THM]);;     
   e (MESON_TAC[]);;
  e (SUBGOAL_THEN `?s. s IN h /\ x:A IN s` STRIP_ASSUME_TAC);;
   e (SET_TAC[]);;
  e (EXISTS_TAC `s:A->bool`);; 
  e (ASM_REWRITE_TAC[]);;
  e (EXISTS_TAC `h:(A->bool)->bool`);;
  e (ASM_REWRITE_TAC[]);;
  e (ASM_MESON_TAC[]);;
 e (DISCH_THEN (X_CHOOSE_THEN `s:A->bool` STRIP_ASSUME_TAC));;
 e (EXISTS_TAC `UNIONS t:A->bool`);;
 e (SET_TAC[]);;
 e (ASM_REWRITE_TAC[]);;
 e (EXISTS_TAC `{w | w IN B /\  w SUBSET u INTER v :A->bool}`);;
 e CONJ_TAC;;
  e (SET_TAC[]);;
 e (REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ]);;
 e CONJ_TAC;;
  e (GEN_REWRITE_TAC I [SUBSET]);;
  e (REWRITE_TAC[IN_UNIONS; IN_ELIM_THM]);;
  e (REPEAT STRIP_TAC);;
  e (RULE_ASSUM_TAC (REWRITE_RULE [ABSBASIS]));;
  e (SUBGOAL_THEN `?w. w IN f /\ x:A IN w /\ w SUBSET u` STRIP_ASSUME_TAC);;
   e (SET_TAC[]);;
  e (SUBGOAL_THEN `?w'. w' IN f' /\ x:A IN w' /\ w' SUBSET v` STRIP_ASSUME_TAC);;
   e (SET_TAC[]);;
  e (SUBGOAL_THEN `w:A->bool IN B` ASSUME_TAC);;
   e (SET_TAC[]);;
  e (SUBGOAL_THEN `w':A->bool IN B` ASSUME_TAC);;
   e (SET_TAC[]);;
  e (SUBGOAL_THEN `x:A IN w INTER w'` ASSUME_TAC);;
   e (SET_TAC[]);;
  e (SUBGOAL_THEN `?z. z IN B /\ x:A IN z /\ z SUBSET w INTER w'` STRIP_ASSUME_TAC);;
   e (ASM_MESON_TAC[]);;
  e (SET_TAC[]);;
 e (SET_TAC[]);;
e (SET_TAC[]);; 
let ABSBASIS_TOP=top_thm();; 

g `!X:A->bool B. ABSBASIS X B ==> GENERATED_TOPOLOGY X B = {UNIONS f | f SUBSET B}`;; 
e (REPEAT STRIP_TAC);;
e (SUBGOAL_THEN `{UNIONS f | f SUBSET B}:(A->bool)->bool IN TOPOLOGY X` ASSUME_TAC);;
 e (ASM_MESON_TAC[ABSBASIS_TOP]);;
e (MATCH_MP_TAC SUBSET_ANTISYM);;
e CONJ_TAC;;
 e (MATCH_MP_TAC GENERATED_TOPOLOGY_COARSEST);;
 e (REPEAT CONJ_TAC);;
   e (ASM_MESON_TAC[ABSBASIS_SUBSET]);;
  e (ASM_REWRITE_TAC[]);;
 e (REWRITE_TAC[SUBSET]);;
 e (REPEAT STRIP_TAC);;
 e (REWRITE_TAC[IN_ELIM_THM]);;
 e (EXISTS_TAC `{x:A->bool}`);;
 e CONJ_TAC;;
  e (SET_TAC[]);;
 e (SET_TAC[]);;
e (REWRITE_TAC [SUBSET; GENERATED_TOPOLOGY]);;
e (REPEAT STRIP_TAC);;
e (REWRITE_TAC[IN_INTERS]);;
e (REPEAT STRIP_TAC);;
e (SUBGOAL_THEN `?f. x:A->bool = UNIONS f /\ (!y. y IN f ==> y IN B)` STRIP_ASSUME_TAC);;
 e (RULE_ASSUM_TAC (REWRITE_RULE [IN_ELIM_THM]));;
 e (ASM_MESON_TAC[]);;
e (SUBGOAL_THEN `?E. t:(A->bool)->bool = E /\ E IN TOPOLOGY X /\ (!x. x IN B ==> x IN E)`
   STRIP_ASSUME_TAC);;
 e (SET_TAC[]);;
e (SUBGOAL_THEN `f SUBSET E:(A->bool)->bool` ASSUME_TAC);;
 e (SET_TAC[]);;
e (RULE_ASSUM_TAC (REWRITE_RULE [IN_TOPOLOGY]));;
e (SET_TAC[]);;
let GENERATED_TOPOLOGY_UNIONS=top_thm();;

(*--- Dimostriamo che la famiglia dei singoletti è una base per la topologia discreta ---*)

g `! X. BASIS X (DISCRETE_TOPOLOGY X) {{x:A} | x IN X}`;;
e (REWRITE_TAC [BASIS; IN_TOPOLOGY; DISCRETE_TOPOLOGY]);;
e (REPEAT STRIP_TAC);; 
    e (SET_TAC []);;
   e (SET_TAC []);;
  e (SET_TAC []);; 
 e (REWRITE_TAC [SUBSET; IN_ELIM_THM]);;
 e (X_GEN_TAC `y:A->bool`);; 
 e (REPEAT STRIP_TAC);;
 e (SET_TAC []);;
e (EXISTS_TAC `{{x:A} | x IN A}`);;
e (CONJ_TAC);;
 e (SET_TAC []);;
e (REWRITE_TAC [EXTENSION; IN_UNIONS; IN_ELIM_THM]);;
e (X_GEN_TAC `y:A`);;
e EQ_TAC;;
 e (REPEAT STRIP_TAC);;
 e (SET_TAC []);;
e (REPEAT STRIP_TAC);;
e (EXISTS_TAC `{y:A}`);;
e (REWRITE_TAC [IN_SING]);;
e (EXISTS_TAC `y:A`);;
e (SET_TAC []);;
let DISCRETE_BASIS = top_thm();;


(*--------- Dimostriamo che l'intero spazio è una base per la topologia banale ----------*)

(* Premettiamo un "lemma" tecnico: si dimostra che, se s è sottoinsieme di {x} U t,      *)
(* allora o s è sottoinsieme di t oppure c'è un sottoinsieme r di s t.c. s = {x} U r.    *)
(* Ci serviremo di questa proprietà nella dimostrazione del teorema.                     *)

g `!s t x:A. s SUBSET x INSERT t <=> s SUBSET t \/ (?r. r SUBSET t /\ s = x INSERT r)`;;
e (REPEAT GEN_TAC);;
e EQ_TAC;;
 e (ASM_CASES_TAC `x:A IN s`);;
  e (DISCH_TAC);;
  e DISJ2_TAC;;
  e (EXISTS_TAC `s INTER t :A->bool`);;
  e (SET_TAC []);;
 e (DISCH_TAC);;
 e DISJ1_TAC;;
 e (SET_TAC []);;
e (SET_TAC []);;
let SUBSET_INSERT_LEMMA = top_thm();;

(* Veniamo ora alla dimostrazione del teorema *)

g `! X:A->bool. BASIS X (COARSE_TOPOLOGY X) {X}`;;
e (REWRITE_TAC [BASIS; IN_TOPOLOGY; COARSE_TOPOLOGY]);;
e (REPEAT STRIP_TAC);;
    e (REWRITE_TAC [EXTENSION; IN_UNIONS]);;
    e (STRIP_TAC);;
    e (REWRITE_TAC [IN_INSERT; NOT_IN_EMPTY]);;
    e (SET_TAC []);;
   e (RULE_ASSUM_TAC (REWRITE_RULE [SUBSET_INSERT_LEMMA]));;
   e (POP_ASSUM MP_TAC);;
   e (REWRITE_TAC [SUBSET_EMPTY]);;
   e (STRIP_TAC);;
      e (ASM_REWRITE_TAC [UNIONS_0; IN_INSERT]);;
     e (ASM_REWRITE_TAC [UNIONS_1; IN_INSERT]);;
    e (ASM_REWRITE_TAC [UNIONS_1; IN_INSERT]);;
   e (ASM_REWRITE_TAC [UNIONS_2; IN_INSERT]);;
   e (REWRITE_TAC [UNION_EMPTY]);;
  e (POP_ASSUM MP_TAC);;
  e (POP_ASSUM MP_TAC);;
  e (REWRITE_TAC [IN_INSERT; NOT_IN_EMPTY]);;
  e (SET_TAC []);;
 e (SET_TAC []);;
e (POP_ASSUM MP_TAC);;
e (REWRITE_TAC [IN_INSERT; NOT_IN_EMPTY]);;
e (STRIP_TAC);;
 e (EXISTS_TAC `{}:(A->bool)->bool`);;
 e (SET_TAC []);;
e (EXISTS_TAC `{X}:(A->bool)->bool`);;
e (SET_TAC []);;
let COARSE_BASIS = top_thm();;

(* OSSERVAZIONE: In alcuni casi tra le proprietà delle basi si menziona anche il fatto   *)
(* che una base debba necessariamente contenere l'insieme vuoto. Da un punto di vista    *)
(* formale in realtà tale richiesta non è necessaria, in quanto dalla definizione si     *)
(* capisce che l'insieme vuoto è semplicemente scrivibile come "unione vuota" senza      *)
(* doverne imporre la presenza all'interno della base. Questo aspetto, sebbene in        *)
(* apparenza controintuitivo, viene evidenziato in modo naturale lavorando in HOL: ad    *)
(* esempio proprio il teorema appena dimostrato ne fornisce una prova.                   *)


(* 3 - ULTERIORI PROPRIETA'                                                              *)

(*----- Dimostriamo un altro paio di proprietà sulle basi di uno spazio topologico: -----*)

(*----- (i) Gli elementi di una base ricoprono l'intero spazio --------------------------*)

g `!X:A->bool U B. BASIS X U B ==> UNIONS B = X`;;
e (REPEAT GEN_TAC);;
e (REWRITE_TAC [BASIS; IN_UNIONS; IN_TOPOLOGY]);;
e (REPEAT STRIP_TAC);;
e (SUBGOAL_THEN `UNIONS B:A->bool SUBSET X` ASSUME_TAC);;
 e (SET_TAC[]);; 
e (SUBGOAL_THEN `X:A->bool SUBSET UNIONS B` ASSUME_TAC);;
 e (REWRITE_TAC[SUBSET]);;
 e (REPEAT STRIP_TAC);;
 e (SUBGOAL_THEN `?A. A IN U /\ x:A IN A` STRIP_ASSUME_TAC);;
  e (SET_TAC[]);;
 e (SUBGOAL_THEN `?S. S SUBSET B /\ A:A->bool = UNIONS S` STRIP_ASSUME_TAC);;
  e (ASM_MESON_TAC[]);;
 e (SUBGOAL_THEN `?s. s IN S /\ x:A IN s` STRIP_ASSUME_TAC);;
  e (SET_TAC[]);;
 e (SET_TAC[]);;
e (ASM_MESON_TAC[SUBSET_ANTISYM_EQ]);;
let BASIS_COVER = top_thm();;

(*---- (ii) Comunque presi due elementi della base B1, B2 e un punto x della loro -------*)
(*----      intersezione, esiste un elemento della base che contiene x ed è -------------*)
(*----      contenuto nell'intersezione di B1 e B2 --------------------------------------*)

g `!X:A->bool U B B1 B2 x. BASIS X U B /\ B1 IN B /\ B2 IN B /\ x IN B1 INTER B2 ==>
   ?B3. B3 IN B /\ x IN B3 /\ B3 SUBSET B1 INTER B2`;;
e (REPEAT GEN_TAC);;
e (REWRITE_TAC [BASIS; IN_TOPOLOGY]);;
e (REPEAT STRIP_TAC);;
e (SUBGOAL_THEN `B1:A->bool IN U` ASSUME_TAC);;
 e (SET_TAC[]);;
e (SUBGOAL_THEN `B2:A->bool IN U` ASSUME_TAC);;
 e (SET_TAC[]);;
e (SUBGOAL_THEN `B1:A->bool INTER B2 IN U` ASSUME_TAC);;
 e (SET_TAC[]);;
e (SUBGOAL_THEN `?S. S SUBSET B:(A->bool)->bool /\ UNIONS S = B1 INTER B2` STRIP_ASSUME_TAC);;
 e (ASM_MESON_TAC[]);;
e (SUBGOAL_THEN `x:A IN UNIONS S` ASSUME_TAC);;
 e (ASM_MESON_TAC[]);;
e (SUBGOAL_THEN `?P. P IN S /\ P IN B /\ x:A IN P` STRIP_ASSUME_TAC);;
 e (SET_TAC[]);;
e (SUBGOAL_THEN `P:A->bool SUBSET UNIONS S` ASSUME_TAC);;
 e (SET_TAC[]);;
e (EXISTS_TAC `P:A->bool`);;
e (ASM_MESON_TAC[]);;
let BASIS_INTER = top_thm();;

(*-- Per concludere dimostriamo che, se U è una famiglia che soddisfa le due proprietà --*)
(*-- precedenti, allora U è una base per la topologia generata da U ---------------------*)

g `!X U:(A->bool)->bool. UNIONS U = X /\ (!U1 U2 x. U1 IN U /\ U2 IN U /\ x IN U1 INTER U2 ==>
   (?U3. U3 IN U /\ x IN U3 /\ U3 SUBSET U1 INTER U2)) ==> 
   BASIS X (GENERATED_TOPOLOGY X U) U`;;
e (REPEAT GEN_TAC);;
e (REWRITE_TAC[BASIS]);;
e (REPEAT STRIP_TAC);;
  e (SUBGOAL_THEN `ABSBASIS X (U:(A->bool)->bool)` ASSUME_TAC);;
   e (REWRITE_TAC[ABSBASIS]);;
   e (ASM_MESON_TAC[]);;
  e (SUBGOAL_THEN `!s. s IN U:(A->bool)->bool ==> s SUBSET X` ASSUME_TAC);;
   e (REPEAT STRIP_TAC);;
   e (SET_TAC[]);;
  e (ASM_MESON_TAC[GENERATED_TOPOLOGY_IN_TOPOLOGY]);;
 e (ASM_MESON_TAC[GENERATED_TOPOLOGY_SUBSET]);;
e (SUBGOAL_THEN `ABSBASIS X (U:(A->bool)->bool)` ASSUME_TAC);;
 e (REWRITE_TAC[ABSBASIS]);;
 e (ASM_MESON_TAC[]);;
e (SUBGOAL_THEN `GENERATED_TOPOLOGY (X:A->bool) U = {UNIONS f | f SUBSET U}` ASSUME_TAC);;
 e (ASM_MESON_TAC[GENERATED_TOPOLOGY_UNIONS]);;
e (SUBGOAL_THEN `A:A->bool IN {UNIONS f | f SUBSET U}` ASSUME_TAC);;
 e (ASM_MESON_TAC[]);;
e (RULE_ASSUM_TAC (REWRITE_RULE [IN_ELIM_THM]));;
e (ASM_MESON_TAC[]);;  
let GEN_BASIS = top_thm();;