refactor with explicit metric topology definition

IsarMathLib/MetricSpace_ZF.thy

@@ -65,18 +65,25 @@ text\<open>A disk is defined as set of points located less than the radius from
 
 definition "Disk(X,d,r,c,R) \<equiv> {x\<in>X. \<langle>d`\<langle>c,x\<rangle>,R\<rangle> \<in> StrictVersion(r)}"
 
+text\<open>We define a metric topology as consisting of unions of open disks.\<close>
+
+definition
+  "MetricTopology(X,L,A,r,d) \<equiv> {\<Union>A. A \<in> Pow(\<Union>c\<in>X. {Disk(X,d,r,c,R). R\<in>PositiveSet(L,A,r)})}"
+
 text\<open>Next we define notation for metric spaces. We will reuse the additive notation defined in 
   the \<open>loop1\<close> locale adding only the assumption about $d$ being a pseudometric and notation
   for a disk centered at $c$ with radius $R$.
   Since for many theorems it is sufficient to assume the pseudometric axioms we will
-  assume in this context that the sets $d,X,L,A,r$ form a pseudometric raher than a metric.\<close>
+  assume in this context that the sets $d,X,L,A,r$ form a pseudometric raher than a metric.
+  In the \<open>pmetric_space\<close> context $\tau$ denotes the topology defined by the metric $d$. \<close>
 
 locale pmetric_space =  loop1 +
   fixes d and X 
   assumes pmetricAssum: "IsApseudoMetric(d,X,L,A,r)"
   fixes disk
   defines disk_def [simp]: "disk(c,R) \<equiv> Disk(X,d,r,c,R)"
-
+  fixes pmettop ("\<tau>") 
+  defines pmettop [simp]: "\<tau> \<equiv> MetricTopology(X,L,A,r,d)"
 
 text\<open> The next lemma shows the definition of the pseudometric in the notation used in the 
   \<open>metric_space\<close> context.\<close>
@@ -186,7 +193,8 @@ proof -
 qed
 
 text\<open>Disks centered at points farther away than the sum of radii do not overlap. \<close>
-lemma (in pmetric_space) far_disks: 
+
+lemma (in pmetric_space) far_disks:
   assumes "x\<in>X" "y\<in>X"  "r\<^sub>x\<ra>r\<^sub>y \<lsq> d`\<langle>x,y\<rangle>"
   shows "disk(x,r\<^sub>x)\<inter>disk(y,r\<^sub>y) = 0"
 proof -
@@ -218,17 +226,29 @@ proof -
     using loop_ord_refl far_disks by simp
 qed
 
-text\<open>Unions of disks form a topology, hence (pseudo)metric spaces are topological spaces. \<close>
+text\<open>The definition of metric topology written in notation of \<open>pmetric_space\<close> context:\<close>
+
+lemma (in pmetric_space) metric_top_def_alt:
+  defines "B \<equiv> \<Union>c\<in>X. {disk(c,R). R\<in>L\<^sub>+}"
+  shows "\<tau> = {\<Union>A. A \<in> Pow(B)}"
+proof -
+  from assms have "MetricTopology(X,L,A,r,d) =  {\<Union>A. A \<in> Pow(B)}"
+    unfolding MetricTopology_def by simp
+  thus ?thesis by simp
+qed
+
+text\<open>Unions of disks form a topology, hence (pseudo)metric spaces are topological spaces.
+  Recall that in the \<open>pmetric_space\<close> context $\tau$ is the metric topology (i.e. set of unions
+  of open disks. \<close>
 
 theorem (in pmetric_space) pmetric_is_top: 
   assumes  "r {down-directs} L\<^sub>+" 
   defines "B \<equiv> \<Union>c\<in>X. {disk(c,R). R\<in>L\<^sub>+}" 
-  defines "T \<equiv> {\<Union>A. A \<in> Pow(B)}"
-  shows "T {is a topology}"  "B {is a base for} T"  "\<Union>T = X"
+  shows "\<tau> {is a topology}"  "B {is a base for} \<tau>"  "\<Union>\<tau> = X"
 proof -
-  from assms  show  "T {is a topology}"  "B {is a base for} T" 
-    using disks_form_base Top_1_2_T1 by auto
-  then have "\<Union>T = \<Union>B" using Top_1_2_L5 by simp
+  from assms show  "\<tau> {is a topology}"  "B {is a base for} \<tau>" 
+    using disks_form_base Top_1_2_T1 metric_top_def_alt by auto
+  then have "\<Union>\<tau> = \<Union>B" using Top_1_2_L5 by simp
   moreover have "\<Union>B = X"
   proof
     from assms(2) show "\<Union>B \<subseteq> X" using disk_definition by auto
@@ -237,7 +257,7 @@ proof -
       with assms(2) \<open>x\<in>X\<close> have "x \<in> \<Union>B" using center_in_disk by auto
     } thus "X \<subseteq> \<Union>B" by auto
   qed 
-  ultimately show "\<Union>T = X" by simp
+  ultimately show "\<Union>\<tau> = X" by simp
 qed
 
 text\<open>To define the \<open>metric_space\<close> locale we take the \<open>pmetric_space\<close> and add 
@@ -268,17 +288,19 @@ text\<open>An ordered loop valued metric space is $T_2$ (i.e. Hausdorff).\<close
 theorem (in metric_space) metric_space_T2:
     assumes "r {down-directs} L\<^sub>+"
     defines "B \<equiv> \<Union>c\<in>X. {disk(c,R). R\<in>L\<^sub>+}" 
-    defines "T \<equiv> {\<Union>A. A \<in> Pow(B)}"
-    shows "T {is T\<^sub>2}"
+    shows "\<tau> {is T\<^sub>2}"
 proof -
-  { fix x y assume "x\<in>\<Union>T" "y\<in>\<Union>T" "x\<noteq>y"
-    from assms have "B\<subseteq>T" using pmetric_is_top(2) base_sets_open by auto
+  { fix x y assume "x\<in>\<Union>\<tau>" "y\<in>\<Union>\<tau>" "x\<noteq>y"
+    from assms have "B\<subseteq>\<tau>" 
+      using pmetric_is_top(2) base_sets_open metric_top_def_alt 
+      by auto
     moreover have "\<exists>U\<in>B. \<exists>V\<in>B. x\<in>U \<and> y\<in>V \<and> U\<inter>V = 0"
     proof -
-      let ?R = "d`\<langle>x,y\<rangle>"
-      from assms have "\<Union>T = X" using pmetric_is_top(3) by simp
-      with \<open>x\<in>\<Union>T\<close> \<open>y\<in>\<Union>T\<close> have "x\<in>X" "y\<in>X" by auto
-      with \<open>x\<noteq>y\<close> have "?R\<in>L\<^sub>+" using dist_pos by simp
+      let ?R = "d`\<langle>x,y\<rangle>" 
+      from assms have "\<Union>\<tau> = X" using pmetric_is_top(3) by simp
+      with \<open>x\<in>\<Union>\<tau>\<close> have "x\<in>X" by blast
+      from \<open>\<Union>\<tau> = X\<close> \<open>y\<in>\<Union>\<tau>\<close> have "y\<in>X" by blast
+      with \<open>x\<noteq>y\<close> \<open>x\<in>X\<close> have "?R\<in>L\<^sub>+" using dist_pos by simp
       with assms(2) \<open>x\<in>X\<close> \<open>y\<in>X\<close> have "disk(x,?R) \<in> B" and "disk(y,?R) \<in> B"
         by auto
       { assume "disk(x,?R) \<inter> disk(y,?R) = 0"
@@ -314,7 +336,7 @@ proof -
       }
       ultimately show ?thesis by auto
     qed
-    ultimately have "\<exists>U\<in>T. \<exists>V\<in>T. x\<in>U \<and> y\<in>V \<and> U\<inter>V = 0" by auto
+    ultimately have "\<exists>U\<in>\<tau>. \<exists>V\<in>\<tau>. x\<in>U \<and> y\<in>V \<and> U\<inter>V = 0" by auto
   } then show ?thesis unfolding isT2_def by simp
 qed
 
@@ -490,5 +512,4 @@ theorem (in pmetric_space) metric_gauge_base:
     uniform_top_is_top
   unfolding IsUniformityBaseOn_def by simp_all
 
-
 end

IsarMathLib/MetricSpace_ZF_1.thy

@@ -46,6 +46,8 @@ text\<open> The \<open>reals\<close> context (locale) defined in the \<open>Real
 text\<open>The \<open>pmetric_space1\<close> locale extends the \<open>reals\<close> locale, adding the carrier $X$ 
   of the metric space and the metric $\mathcal{d}$ to the context, together with the assumption
   that $\mathcal{d}:X\times X \rightarrow \mathbb{R}^+$ is a pseudo metric.
+  As in the \<open>pmetric_space\<close> locale we define the $\tau$ to be the metric topology, i.e.
+  the topology induced by the pseudometric $\mathcal{d}$.
   An alternative would be to define the \<open>pmetric_space1\<close> as an extension of the \<open>pmetric_space1\<close>
   context, but that is in turn an extension of the \<open>loop1\<close> locale that defines notation
   for left and right division which which do not want in the context of real numbers. \<close>
@@ -55,6 +57,8 @@ locale pmetric_space1 = reals +
   assumes pmetricAssum: "IsApseudoMetric(\<d>,X,\<real>,Add,ROrd)"
   fixes ball
   defines ball_def [simp]: "ball(c,r) \<equiv> Disk(X,\<d>,ROrd,c,r)"
+  fixes pmettop ("\<tau>") 
+  defines pmettop [simp]: "\<tau> \<equiv> MetricTopology(X,\<real>,Add,ROrd,\<d>)"
 
 text\<open>The propositions proven in the \<open>pmetric_space\<close> context defined in \<open>Metric_Space_ZF\<close> theory 
   are valid in the \<open>pmetric_space1\<close> context. \<close>
@@ -104,16 +108,16 @@ text\<open>Since in the \<open>pmetric_space1\<close> context $\mathfrak{d}$ is
 
 theorem (in pmetric_space1) rpmetric_is_top:
   shows 
-    "Metric_Topology {is a topology}"
-    "Open_Balls {is a base for} Metric_Topology"
-    "\<Union> Metric_Topology = X"
+    "\<tau> {is a topology}"
+    "Open_Balls {is a base for} \<tau>"
+    "\<Union>\<tau> = X"
   unfolding Open_Balls_def Metric_Topology_def
   using rord_down_directs pmetric_space_pmetric_space1_valid 
     pmetric_space.pmetric_is_top by simp_all
 
 text\<open>The topology generated by a metric is Hausdorff (i.e. $T_2$). \<close>
 
-theorem (in metric_space1) rmetric_space_T2: shows "Metric_Topology {is T\<^sub>2}"
+theorem (in metric_space1) rmetric_space_T2: shows "\<tau> {is T\<^sub>2}"
   unfolding Open_Balls_def Metric_Topology_def
   using rord_down_directs metric_space_metric_space1_valid
     metric_space.metric_space_T2 by simp

IsarMathLib/Real_ZF_2.thy

@@ -256,18 +256,24 @@ lemma (in reals) rord_down_directs: shows "ROrd {down-directs} \<real>\<^sub>+"
   using pos_is_lattice(3) pos_non_empty meet_down_directs down_dir_mono
   unfolding IsAlattice_def by blast
 
-text\<open> We define the topology on reals as one consisting of the unions of open disks. \<close>
+text\<open> We define the topology on reals as the metric topology
+  coming from the \<open>dist\<close> metric (i.e. consisting of the unions of open disks). \<close>
 
-definition (in reals) RealTopology ("\<tau>\<^sub>\<real>") 
-  where "\<tau>\<^sub>\<real> \<equiv> {\<Union>A. A \<in> Pow(\<Union>c\<in>\<real>.{disk(c,r). r \<in> \<real>\<^sub>+})}"
+definition (in reals) RealTopology ("\<tau>\<^sub>\<real>")
+  where "\<tau>\<^sub>\<real> \<equiv> MetricTopology(\<real>,\<real>,Add,ROrd,dist)"
+
+text\<open>A more explicit definition of the real topology in notation used in the \<open>reals\<close> context. \<close>
+
+lemma (in reals) real_toplology_def_alt: 
+  shows "\<tau>\<^sub>\<real> = {\<Union>A. A \<in> Pow(\<Union>c\<in>\<real>.{disk(c,r). r \<in> \<real>\<^sub>+})}"
+  unfolding MetricTopology_def RealTopology_def by simp
 
 text\<open>Real numbers form a Hausdorff topological space with topology generated by open disks. \<close>
 
 theorem (in reals) reals_is_top: 
   shows "\<tau>\<^sub>\<real> {is a topology}" "\<Union>\<tau>\<^sub>\<real> = \<real>" "\<tau>\<^sub>\<real> {is T\<^sub>2}"
   using rord_down_directs metric_space_valid pmetric_space_valid 
     pmetric_space.pmetric_is_top  metric_space.metric_space_T2
-  unfolding RealTopology_def
-    by simp_all
+  unfolding RealTopology_def by simp_all
 
 end