atlas.hl

needs "Multivariate/derivatives.ml";;

(* ========================================================================= *)
(* Differential geometry in HOL Light.                                       *)
(* ========================================================================= *)

let INJ_ON = new_definition
  `INJ_ON f s <=> (!x y:A. x IN s /\ y IN s /\ f x:B = f y ==> x = y)`;;

(* ------------------------------------------------------------------------- *)
(* Homeomorphism in the general case (topological spaces).                   *)
(* ------------------------------------------------------------------------- *)

let tophomeomorphism = new_definition
  `!top top' f:A->B.
      tophomeomorphism top top' f <=>
      BIJ f (topspace top) (topspace top') /\
      topcontinuous top top' f /\
      topcontinuous top' top (inverse f)`;;

(* ------------------------------------------------------------------------- *)
(* Hausdorff topological spaces.                                             *)
(* ------------------------------------------------------------------------- *)

let hausdorff = new_definition
  `hausdorff top <=>
   !x y:A. x IN topspace top /\ y IN topspace top /\ ~(x = y)
           ==> (?u v. open_in top u /\ open_in top v /\
                      x IN u /\ y IN v /\ u INTER v = {})`;;

let HAUSDORFF_EUCLIDEAN = prove
 (`hausdorff (euclidean:(real^N)topology)`,
  REWRITE_TAC[hausdorff; TOPSPACE_EUCLIDEAN; IN_UNIV; GSYM OPEN_IN;
              SEPARATION_HAUSDORFF]);;

let HAUSDORFF_SUBTOPOLOGY = prove
 (`!top s:A->bool. hausdorff top ==> hausdorff(subtopology top s)`,
  REPEAT GEN_TAC THEN
  REWRITE_TAC[hausdorff; TOPSPACE_SUBTOPOLOGY; IN_INTER;
              OPEN_IN_SUBTOPOLOGY] THEN
  INTRO_TAC "hp; !x y; (x xINs) (y yINs) neq" THEN
  REMOVE_THEN "hp" (MP_TAC o SPECL[`x:A`;`y:A`]) THEN
  ANTS_TAC THENL [ASM_REWRITE_TAC[]; ALL_TAC] THEN
  INTRO_TAC "@u v. open_u open_v xINu xINv inter" THEN
  MAP_EVERY EXISTS_TAC [`u INTER s:A->bool`;`v INTER s:A->bool`] THEN
  CONJ_TAC THENL [EXISTS_TAC `u:A->bool` THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN
  CONJ_TAC THENL [EXISTS_TAC `v:A->bool` THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN
  ASM_REWRITE_TAC[IN_INTER] THEN REMOVE_THEN "inter" MP_TAC THEN SET_TAC[]);;

let HAUSDORFF_SUBTOPOLOGY_EUCLIDEAN = prove
 (`!s:real^N->bool. hausdorff (subtopology euclidean s)`,
  GEN_TAC THEN MATCH_MP_TAC HAUSDORFF_SUBTOPOLOGY THEN
  MATCH_ACCEPT_TAC HAUSDORFF_EUCLIDEAN);;

(* ------------------------------------------------------------------------- *)
(* Diffeomorphims.                                                           *)
(* ------------------------------------------------------------------------- *)

let diffeomorphism = new_definition
  `diffeomorphism (f:real^M->real^N) s t <=>
   BIJ f s t /\ f differentiable_on s /\ inverse f differentiable_on t`;;

(* ------------------------------------------------------------------------- *)
(* Differentiable atlas.                                                     *)
(* ------------------------------------------------------------------------- *)

parse_as_infix("atlas_on",(12, "right"));;

let atlas_on = new_definition
  `U atlas_on s <=>
   UNIONS {u | u,f | (u,f) IN U} = s /\
   (!u f:A->real^N.
      (u,f) IN U
      ==> u SUBSET s /\ open (IMAGE f u) /\
          f IN EXTENSIONAL u /\ INJ_ON f u) /\
   (!u f v g.
      (u,f) IN U /\ (v,g) IN U
      ==> open (IMAGE f (u INTER v)) /\
          open (IMAGE g (u INTER v)) /\
          diffeomorphism (g o inverse f)
            (IMAGE f (u INTER v)) (IMAGE g (u INTER v)))`;;

let ATLAS_SUPPORT = prove
 (`!s U:(A->bool)#(A->real^N)->bool.
     U atlas_on s ==> UNIONS {u | u,f | u,f:A->real^N IN U} = s`,
  SIMP_TAC[atlas_on]);;

let SUBATLAS = prove
 (`!s U V:(A->bool)#(A->real^N)->bool.
     U atlas_on s /\ V SUBSET U /\ UNIONS {u | u,f | (u,f) IN V} = s
     ==> V atlas_on s`,
  REPEAT GEN_TAC THEN SIMP_TAC[atlas_on] THEN SET_TAC[]);;

(* ------------------------------------------------------------------------- *)
(* Atlas topology.                                                           *)
(* ------------------------------------------------------------------------- *)

let atlas_topology = new_definition
  `atlas_topology U =
   topology {w | w SUBSET UNIONS {u | u,f | u,f:A->real^N IN U}  /\
                 (!u f. u,f IN U ==> open(IMAGE f (w INTER u)))}`;;

let ISTOPOLOGY_ATLAS_TOPOLOGY = prove
 (`!s U.
     U atlas_on s
     ==> istopology {w | w SUBSET UNIONS {u | u,f | u,f:A->real^N IN U}  /\
                         (!u f. u,f IN U ==> open(IMAGE f (w INTER u)))}`,
  INTRO_TAC "!s U; U" THEN REWRITE_TAC[istopology] THEN CONJ_TAC THENL
  [REWRITE_TAC[IN_ELIM_THM; EMPTY_SUBSET; INTER_EMPTY;
               IMAGE_CLAUSES; OPEN_EMPTY];
   ALL_TAC] THEN
  CONJ_TAC THENL
  [REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM; FORALL_IN_GSPEC] THEN
   INTRO_TAC "![v]; v; h1; ![w]; w; h2" THEN REWRITE_TAC[IN_ELIM_THM] THEN
   CONJ_TAC THENL [REMOVE_THEN "v" MP_TAC THEN SET_TAC[]; ALL_TAC] THEN
   INTRO_TAC "!u f; uf" THEN
   (SUBST1_TAC o SET_RULE)
     `(v INTER w) INTER u = (v INTER u) INTER (w INTER u):A->bool` THEN
   HYP_TAC "U -> _ hp _" (REWRITE_RULE[atlas_on]) THEN
   HYP_TAC "hp: +" (SPECL[`u:A->bool`;`f:A->real^N`]) THEN
   ANTS_TAC THENL [ASM_REWRITE_TAC[]; INTRO_TAC "su fu f inj"] THEN
   SUBGOAL_THEN
     `IMAGE (f:A->real^N) ((v INTER u) INTER w INTER u) =
      IMAGE f (v INTER u) INTER IMAGE f (w INTER u)`
     SUBST1_TAC THENL
   [MATCH_MP_TAC IMAGE_INTER_SATURATED_GEN THEN EXISTS_TAC `u:A->bool` THEN
    DISJ1_TAC THEN CONJ_TAC THENL [ALL_TAC; SET_TAC[]] THEN
    HYP_TAC "inj" (REWRITE_RULE[INJ_ON]) THEN HYP SET_TAC "inj" [];
    MATCH_MP_TAC OPEN_INTER THEN ASM_SIMP_TAC[]];
   ALL_TAC] THEN
  INTRO_TAC "!k; k" THEN REWRITE_TAC[IN_ELIM_THM] THEN CONJ_TAC THENL
  [REWRITE_TAC[UNIONS_SUBSET] THEN INTRO_TAC "![v]; v" THEN
   HYP_TAC "k: +" (SPEC `v:A->bool` o GEN_REWRITE_RULE I [SUBSET]) THEN
   ANTS_TAC THENL [ASM_REWRITE_TAC[]; SIMP_TAC[IN_ELIM_THM]];
   ALL_TAC] THEN
  INTRO_TAC "!u f; uf" THEN
  SUBGOAL_THEN `UNIONS k INTER u = UNIONS {w INTER u:A->bool | w IN k}`
               SUBST1_TAC THENL
  [REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ] THEN CONJ_TAC THENL
   [REWRITE_TAC[SUBSET; IN_INTER; IMP_CONJ; FORALL_IN_UNIONS] THEN
    INTRO_TAC "![v] x; v; xv; xu" THEN REWRITE_TAC[IN_UNIONS] THEN
    EXISTS_TAC `v INTER u:A->bool` THEN
    HYP (MP_TAC o CONJ_LIST) "v xv xu" [] THEN SET_TAC[];
    REWRITE_TAC[UNIONS_SUBSET; FORALL_IN_GSPEC] THEN INTRO_TAC "!w; w" THEN 
    HYP_TAC "k: +" (SPEC `w:A->bool` o GEN_REWRITE_RULE I [SUBSET]) THEN
    ANTS_TAC THENL [ASM_REWRITE_TAC[]; SIMP_TAC[IN_ELIM_THM]] THEN
    INTRO_TAC "hp _" THEN REWRITE_TAC[SUBSET; IN_INTER] THEN
    INTRO_TAC "!x; xw xu" THEN ASM_REWRITE_TAC[IN_UNIONS] THEN
    EXISTS_TAC `w:A->bool` THEN ASM_REWRITE_TAC[]];
   ALL_TAC] THEN
  REWRITE_TAC[IMAGE_UNIONS] THEN MATCH_MP_TAC OPEN_UNIONS THEN
  REWRITE_TAC[FORALL_IN_IMAGE; FORALL_IN_GSPEC] THEN INTRO_TAC "!w; w" THEN
  HYP_TAC "k: +" (SPEC `w:A->bool` o GEN_REWRITE_RULE I [SUBSET]) THEN
  ANTS_TAC THENL [ASM_REWRITE_TAC[]; ASM_SIMP_TAC[IN_ELIM_THM]]);;

let OPEN_IN_ATLAS_TOPOLOGY = prove
 (`!s U.
     U atlas_on s
     ==> (!w. open_in (atlas_topology U) w <=>
              w SUBSET s /\
              (!u f:A->real^N. u,f IN U ==> open(IMAGE f (w INTER u))))`,
  INTRO_TAC "!s U; U; !w" THEN REWRITE_TAC[atlas_topology] THEN
  HYP_TAC "U -> hp" (MATCH_MP ISTOPOLOGY_ATLAS_TOPOLOGY) THEN
  HYP_TAC "hp" (REWRITE_RULE[topology_tybij]) THEN
  REMOVE_THEN "hp" SUBST1_TAC THEN GEN_REWRITE_TAC LAND_CONV [GSYM IN] THEN
  REWRITE_TAC[IN_ELIM_THM] THEN HYP_TAC "U" (REWRITE_RULE[atlas_on]) THEN
  ASM_REWRITE_TAC[]);;

(* ------------------------------------------------------------------------- *)
(* Refinement of an atlas.                                                   *)
(* ------------------------------------------------------------------------- *)

let atlas_refinement = new_definition
  `atlas_refinement (s:A->bool) U (V:(A->bool)#(A->real^N)->bool) <=>
   U atlas_on s /\ V atlas_on s /\
   (!u f. u,f IN U
          ==> ?v g. v,g IN V /\ u SUBSET v /\ (!x. x IN u ==> f x = g x))`;;

let ATLAS_REFINEMENT_REFL = prove
 (`!s:A->bool U:(A->bool)#(A->real^N)->bool.
     atlas_refinement s U U <=> U atlas_on s`,
  REWRITE_TAC[atlas_refinement] THEN SET_TAC[]);;

let ATLAS_REFINEMENT_TRANS = prove
 (`!s:A->bool U V W:(A->bool)#(A->real^N)->bool.
     atlas_refinement s U V /\ atlas_refinement s V W
     ==> atlas_refinement s U W`,
  REWRITE_TAC[atlas_refinement] THEN SET_TAC[]);;

(* ------------------------------------------------------------------------- *)
(* Compatibility between two atlas.                                          *)
(* ------------------------------------------------------------------------- *)

let compatible_atlas = new_definition
  `!s U V:(A->bool)#(A->real^N)->bool.
     compatible_atlas s U V <=>
     U atlas_on s /\ V atlas_on s /\ U UNION V atlas_on s`;;

let COMPATIBLE_ATLAS_REFL = prove
 (`!s U:(A->bool)#(A->real^N)->bool.
     compatible_atlas s U U <=> U atlas_on s`,
  REWRITE_TAC[compatible_atlas; UNION_IDEMPOT]);;

let COMPATIBLE_ATLAS_SYM = prove
 (`!s U V:(A->bool)#(A->real^N)->bool.
     compatible_atlas s U V ==> compatible_atlas s V U`,
  SIMP_TAC[compatible_atlas; UNION_COMM]);;

(* TODO. *)
(*
let COMPATIBLE_ATLAS_TRANS = prove
 (`!s U V W:(A->bool)#(A->real^N)->bool.
     compatible_atlas s U V /\ compatible_atlas s V W
     ==> compatible_atlas s U W`,
*)

let differentiable_strucure = new_definition
  `!s U:(A->bool)#(A->real^N)->bool.
     differentiable_strucure s U <=>
     U atlas_on s /\
     (!V. compatible_atlas s U V ==> V SUBSET U)`;;

let maximal_atlas = new_definition
  `!s U:(A->bool)#(A->real^N)->bool.
     maximal_atlas s U = UNIONS {V | compatible_atlas s U V}`;;

(* TODO *)
(*
let MAXIMAL_ATLAS_INC = prove
 (`!s U:(A->bool)#(A->real^N)->bool.
     U SUBSET maximal_atlas s U <=> U atlas_on s`,
*)

(* TODO *)
(*
let DIFFERENTIABLE_STRUCTURE_MAXIMAL_ATLAS = prove
 (`!s U:(A->bool)#(A->real^N)->bool.
     differentiable_strucure s (maximal_atlas s U) <=> U atlas_on s`,
*)

let ATLAS_ON_EMPTY = prove
 (`({}:(A->bool)#(A->real^N)->bool) atlas_on {}`,
  REWRITE_TAC[atlas_on; NOT_IN_EMPTY; EMPTY_GSPEC; UNIONS_0]);;

(* ------------------------------------------------------------------------- *)
(* Example 1: real^N as a differentiable structure                           *)
(* ------------------------------------------------------------------------- *)

let euclidean_atlas = new_definition
  `euclidean_atlas = {((:real^N), \x:real^N.x)}`;;

let UNIONS_SING = SET_RULE `!f:A->(B->bool) a:A. UNIONS { f x | x = a } = f a`;;

let INVERSE_ID = prove (`inverse (\x:A. x) = \x:A. x`, REWRITE_TAC[GSYM I_DEF; INVERSE_I] THEN REWRITE_TAC[I_DEF]);;

let BIJ_ID = prove (`!s:A->bool. BIJ (\x.x) s s`, REWRITE_TAC[BIJ; INJ; SURJ] THEN MESON_TAC[]);;

let SET_PROJ_LEMMA = prove
  (`{ u | u, v | P (u:A ,v:B) } = { FST x | P x }`,
   REWRITE_TAC[EXTENSION] THEN
   GEN_TAC THEN
   REWRITE_TAC[IN_ELIM_THM] THEN
   EQ_TAC THENL
   [
      INTRO_TAC "@u v. h" THEN EXISTS_TAC `u:A, v:B` THEN ASM_REWRITE_TAC[]
      ;
      INTRO_TAC "@y. h" THEN EXISTS_TAC `FST (y:A#B)` THEN EXISTS_TAC `SND (y:A#B)` THEN ASM_REWRITE_TAC[]
   ]
   );;

let EUCLIDEAN_ATLAS = prove
  (`euclidean_atlas atlas_on (:real^N)`,
   REWRITE_TAC[euclidean_atlas; atlas_on; IN_SING] THEN (REPEAT CONJ_TAC) THENL
   [
     REWRITE_TAC[SET_PROJ_LEMMA; UNIONS_SING]
     ;
     REWRITE_TAC[PAIR_EQ] THEN (REPEAT STRIP_TAC) THENL
     [
       SET_TAC[]
       ;
       ASM_REWRITE_TAC[IMAGE_ID; OPEN_UNIV]
       ;
       ASM_REWRITE_TAC[EXTENSIONAL; IN_ELIM_THM] THEN SET_TAC[]
       ;
       ASM_REWRITE_TAC[INJ_ON] THEN SET_TAC[]
     ]
     ;
     REWRITE_TAC[PAIR_EQ] THEN (REPEAT STRIP_TAC) THENL
     [
       ASM_REWRITE_TAC[IMAGE_ID; INTER_UNIV; OPEN_UNIV]
       ;
       ASM_REWRITE_TAC[IMAGE_ID; INTER_UNIV; OPEN_UNIV]
       ;
       ASM_REWRITE_TAC[IMAGE_ID; INTER_UNIV; o_DEF; INVERSE_ID; diffeomorphism; DIFFERENTIABLE_ON_ID; BIJ_ID]
     ]
   ]
  );;