Skip to content

Commit

Permalink
release 1.31.0
Browse files Browse the repository at this point in the history
  • Loading branch information
@SKolodynski
SKolodynski committed Jul 26, 2024
1 parent 74ce652 commit 65b26be
Show file tree
Hide file tree
Showing 18 changed files with 2,085 additions and 1,399 deletions.
30 changes: 15 additions & 15 deletions IsarMathLib/MetricSpace_ZF.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ 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>
text\<open>We define \<open>metric topology\<close> 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)})}"
Expand Down Expand Up @@ -94,7 +94,7 @@ locale pmetric_space = loop1 +


text\<open> The next lemma shows the definition of the pseudometric in the notation used in the
\<open>metric_space\<close> context.\<close>
\<open>pmetric_space\<close> context.\<close>

lemma (in pmetric_space) pmetric_properties: shows
"d: X\<times>X \<rightarrow> L\<^sup>+"
Expand All @@ -104,7 +104,7 @@ lemma (in pmetric_space) pmetric_properties: shows
using pmetricAssum unfolding IsApseudoMetric_def by auto

text\<open>The values of the metric are in the in the nonnegative set of the loop,
hence in the loop. /\<close>
hence in the loop.\<close>

lemma (in pmetric_space) pmetric_loop_valued: assumes "x\<in>X" "y\<in>X"
shows "d`\<langle>x,y\<rangle> \<in> L\<^sup>+" "d`\<langle>x,y\<rangle> \<in> L"
Expand Down Expand Up @@ -231,9 +231,9 @@ text\<open>Disks centered at points farther away than the sum of radii do not ov

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"
shows "disk(x,r\<^sub>x)\<inter>disk(y,r\<^sub>y) = \<emptyset>"
proof -
{ assume "disk(x,r\<^sub>x)\<inter>disk(y,r\<^sub>y) \<noteq> 0"
{ assume "disk(x,r\<^sub>x)\<inter>disk(y,r\<^sub>y) \<noteq> \<emptyset>"
then obtain z where "z \<in> disk(x,r\<^sub>x)\<inter>disk(y,r\<^sub>y)" by auto
then have "z\<in>X" and "d`\<langle>x,z\<rangle> \<ra> d`\<langle>y,z\<rangle> \<ls> r\<^sub>x\<ra>r\<^sub>y"
using disk_definition add_ineq_strict by auto
Expand Down Expand Up @@ -272,9 +272,9 @@ proof -
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>
text\<open>If the order of the loop down-directs its set of positive elements
then the metric topology defined as collection of unions of (open) disks is indeed a topology.
Recall that in the \<open>pmetric_space\<close> context $\tau$ denotes the metric topology. \<close>

theorem (in pmetric_space) pmetric_is_top:
assumes "r {down-directs} L\<^sub>+"
Expand All @@ -290,7 +290,7 @@ theorem (in pmetric_space) disks_are_base:
shows "B {is a base for} \<tau>"
using assms disks_form_base Top_1_2_T1 metric_top_def_alt by simp

text\<open>$X$ is the carrier of metric topology.\<close>
text\<open>If $r$ down-directs $L_+$ then $X$ is the carrier of metric topology.\<close>

theorem (in pmetric_space) metric_top_carrier:
assumes "r {down-directs} L\<^sub>+" shows "\<Union>\<tau> = X"
Expand All @@ -315,7 +315,7 @@ lemma (in pmetric_space) topology0_valid_in_pmetric_space:
shows "topology0(\<tau>)"
using assms pmetric_is_top unfolding topology0_def by simp

text\<open>Disks are open in the metric topology.\<close>
text\<open>If $r$ down-directs $L_+$ then disks are open in the metric topology.\<close>

lemma (in pmetric_space) disks_open:
assumes "c\<in>X" "R\<in>L\<^sub>+" "r {down-directs} L\<^sub>+"
Expand Down Expand Up @@ -346,7 +346,7 @@ proof -
using ident_indisc posset_definition posset_definition1 by auto
qed

text\<open>An ordered loop valued metric space is $T_2$ (i.e. Hausdorff).\<close>
text\<open>If $r$ down-directs $L_+$ then the 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>+"
Expand Down Expand Up @@ -444,9 +444,8 @@ lemma (in pmetric_space) gauge_members:
by simp

text\<open>Suppose $b\in L^+$ (i.e. b is an element of the loop that is greater than the neutral element)
and $x\in X$. Then the set $B=\{ d^{-1}(\{c\in L^+: c\leq b\}$ is a relation on $X$ and
the image of the singleton set $\{ x\}$ by that relation is the set
$\{ y\in X:d\langle x,y\rangle \leq b\}$,
and $x\in X$. Then the image of the singleton set $\{ x\}$ by the relation
$B=\{ d^{-1}(\{c\in L^+: c\leq b\}$ is the set $\{ y\in X:d\langle x,y\rangle \leq b\}$,
i.e. the closed disk with center $x$ and radius $b$. Hence the the image $B\{ x\}$ contains
the open disk with center $x$ and radius $b$. \<close>

Expand Down Expand Up @@ -518,7 +517,8 @@ corollary (in pmetric_space) gauge_3rd_cond:
assumes "B\<^sub>1\<in>\<BB>" shows "\<exists>B\<^sub>2\<in>\<BB>. B\<^sub>2 \<subseteq> converse(B\<^sub>1)"
using assms gauge_symmetric by auto

text\<open>The sets of the form $d^{-1}([0,b])$ are subsets of $X\times X$. \<close>
text\<open>The collection of sets of the form $d^{-1}([0,b])$ for $b\in L_+$
is contained of the powerset of $X\times X$.\<close>

lemma (in pmetric_space) gauge_5thCond: shows "\<BB>\<subseteq>Pow(X\<times>X)"
using uniform_gauge_def_alt pmetric_properties(1) func1_1_L3 by force
Expand Down
2 changes: 1 addition & 1 deletion IsarMathLib/document/root.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -66,7 +66,7 @@
\maketitle

\begin{abstract}
This is the proof document of the IsarMathLib project version 1.30.0.
This is the proof document of the IsarMathLib project version 1.31.0.
IsarMathLib is a library of formalized mathematics for Isabelle2024 (ZF logic).

\end{abstract}
Expand Down
12 changes: 6 additions & 6 deletions docs/IsarMathLib/Fol1.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -193,20 +193,20 @@ <h1>Theory Fol1</h1>
</span><span class="keyword1"><span class="command"><span>using</span></span></span><span> </span><a class="entity_ref" href="Fol1.html#Fol1.Xor_def|fact"><span>Xor_def</span></a><span> </span><span class="keyword1"><span class="command"><span>by</span></span></span><span> </span><a class="entity_ref" href="../../FOL/ZF/ISABELLE_HOME/src/Provers/clasimp.ML.html#FOL.auto|method"><span class="operator"><span>auto</span></span></a><span>

</span><span class="keyword1"><span class="command"><span>text</span></span></span><span class="quoted"><span class="plain_text"><span>‹Constructions from the same sets are the same.
It is suprising but we do have to use this as a rule in rarte cases.›</span></span></span><span>
It is suprising but we do have to use this as a rule in rare cases.›</span></span></span><span>

</span><span class="keyword1"><span class="command"><span class="entity_def" id="offset_6078..6083">lemma</span></span></span><span> </span><span class="entity_def" id="Fol1.same_constr|fact"><span class="entity_def" id="Fol1.same_constr|thm"><span>same_constr</span></span></span><span class="main"><span>:</span></span><span> </span><span class="keyword2"><span class="keyword"><span>assumes</span></span></span><span> </span><span class="quoted"><span class="quoted"><span>"</span><span class="free"><span>x</span></span><span class="main"><a class="entity_ref" href="../../FOL/ZF/IFOL.html#IFOL.eq|const"><span>=</span></a></span><span class="free"><span>y</span></span><span>"</span></span></span><span> </span><span class="keyword2"><span class="keyword"><span>shows</span></span></span><span> </span><span class="quoted"><span class="quoted"><span>"</span><span class="free"><span>P</span></span><span class="main"><span>(</span></span><span class="free"><span>x</span></span><span class="main"><span>)</span></span><span> </span><span class="main"><a class="entity_ref" href="../../FOL/ZF/IFOL.html#IFOL.eq|const"><span>=</span></a></span><span> </span><span class="free"><span>P</span></span><span class="main"><span>(</span></span><span class="free"><span>y</span></span><span class="main"><span>)</span></span><span>"</span></span></span><span>
</span><span class="keyword1"><span class="command"><span>using</span></span></span><span> </span><a class="entity_ref" href="Fol1.html#offset_6078..6083"><span>assms</span></a><span> </span><span class="keyword1"><span class="command"><span>by</span></span></span><span> </span><span class="operator"><span>simp</span></span><span>
</span><span class="keyword1"><span class="command"><span class="entity_def" id="offset_6077..6082">lemma</span></span></span><span> </span><span class="entity_def" id="Fol1.same_constr|fact"><span class="entity_def" id="Fol1.same_constr|thm"><span>same_constr</span></span></span><span class="main"><span>:</span></span><span> </span><span class="keyword2"><span class="keyword"><span>assumes</span></span></span><span> </span><span class="quoted"><span class="quoted"><span>"</span><span class="free"><span>x</span></span><span class="main"><a class="entity_ref" href="../../FOL/ZF/IFOL.html#IFOL.eq|const"><span>=</span></a></span><span class="free"><span>y</span></span><span>"</span></span></span><span> </span><span class="keyword2"><span class="keyword"><span>shows</span></span></span><span> </span><span class="quoted"><span class="quoted"><span>"</span><span class="free"><span>P</span></span><span class="main"><span>(</span></span><span class="free"><span>x</span></span><span class="main"><span>)</span></span><span> </span><span class="main"><a class="entity_ref" href="../../FOL/ZF/IFOL.html#IFOL.eq|const"><span>=</span></a></span><span> </span><span class="free"><span>P</span></span><span class="main"><span>(</span></span><span class="free"><span>y</span></span><span class="main"><span>)</span></span><span>"</span></span></span><span>
</span><span class="keyword1"><span class="command"><span>using</span></span></span><span> </span><a class="entity_ref" href="Fol1.html#offset_6077..6082"><span>assms</span></a><span> </span><span class="keyword1"><span class="command"><span>by</span></span></span><span> </span><span class="operator"><span>simp</span></span><span>

</span><span class="keyword1"><span class="command"><span>text</span></span></span><span class="quoted"><span class="plain_text"><span>‹Equivalence relations are symmetric.›</span></span></span><span>

</span><span class="keyword1"><span class="command"><span>lemma</span></span></span><span> </span><span class="entity_def" id="Fol1.equiv_is_sym|fact"><span class="entity_def" id="Fol1.equiv_is_sym|thm"><span>equiv_is_sym</span></span></span><span class="main"><span>:</span></span><span> </span><span class="keyword2"><span class="keyword"><span>assumes</span></span></span><span> </span><span class="entity_def" id="offset_6226..6228">A1</span><span class="main"><span>:</span></span><span> </span><span class="quoted"><span class="quoted"><span>"</span><a class="entity_ref" href="../../FOL/ZF/Trancl.html#Trancl.equiv|const"><span>equiv</span></a><span class="main"><span>(</span></span><span class="free"><span>X</span></span><span class="main"><span>,</span></span><span class="free"><span>r</span></span><span class="main"><span>)</span></span><span>"</span></span></span><span> </span><span class="keyword2"><span class="keyword"><span>and</span></span></span><span> </span><span class="entity_def" id="offset_6247..6249">A2</span><span class="main"><span>:</span></span><span> </span><span class="quoted"><span class="quoted"><span>"</span><span class="main"><span>⟨</span></span><span class="free"><span>x</span></span><span class="main"><span>,</span></span><span class="free"><span>y</span></span><span class="main"><span>⟩</span></span><span> </span><span class="main"><a class="entity_ref" href="../../FOL/ZF/ZF_Base.html#ZF_Base.mem|const"><span>∈</span></a></span><span> </span><span class="free"><span>r</span></span><span>"</span></span></span><span>
</span><span class="keyword1"><span class="command"><span>lemma</span></span></span><span> </span><span class="entity_def" id="Fol1.equiv_is_sym|fact"><span class="entity_def" id="Fol1.equiv_is_sym|thm"><span>equiv_is_sym</span></span></span><span class="main"><span>:</span></span><span> </span><span class="keyword2"><span class="keyword"><span>assumes</span></span></span><span> </span><span class="entity_def" id="offset_6225..6227">A1</span><span class="main"><span>:</span></span><span> </span><span class="quoted"><span class="quoted"><span>"</span><a class="entity_ref" href="../../FOL/ZF/Trancl.html#Trancl.equiv|const"><span>equiv</span></a><span class="main"><span>(</span></span><span class="free"><span>X</span></span><span class="main"><span>,</span></span><span class="free"><span>r</span></span><span class="main"><span>)</span></span><span>"</span></span></span><span> </span><span class="keyword2"><span class="keyword"><span>and</span></span></span><span> </span><span class="entity_def" id="offset_6246..6248">A2</span><span class="main"><span>:</span></span><span> </span><span class="quoted"><span class="quoted"><span>"</span><span class="main"><span>⟨</span></span><span class="free"><span>x</span></span><span class="main"><span>,</span></span><span class="free"><span>y</span></span><span class="main"><span>⟩</span></span><span> </span><span class="main"><a class="entity_ref" href="../../FOL/ZF/ZF_Base.html#ZF_Base.mem|const"><span>∈</span></a></span><span> </span><span class="free"><span>r</span></span><span>"</span></span></span><span>
</span><span class="keyword2"><span class="keyword"><span>shows</span></span></span><span> </span><span class="quoted"><span class="quoted"><span>"</span><span class="main"><span>⟨</span></span><span class="free"><span>y</span></span><span class="main"><span>,</span></span><span class="free"><span>x</span></span><span class="main"><span>⟩</span></span><span> </span><span class="main"><a class="entity_ref" href="../../FOL/ZF/ZF_Base.html#ZF_Base.mem|const"><span>∈</span></a></span><span> </span><span class="free"><span>r</span></span><span>"</span></span></span><span>
</span><span class="keyword1"><span class="command"><span>proof</span></span></span><span> </span><span class="operator"><span>-</span></span><span>
</span><span class="keyword1"><span class="command"><span>from</span></span></span><span> </span><a class="entity_ref" href="Fol1.html#offset_6226..6228"><span>A1</span></a><span> </span><span class="keyword1"><span class="command"><span>have</span></span></span><span> </span><span class="quoted"><span class="quoted"><span>"</span><a class="entity_ref" href="../../FOL/ZF/Trancl.html#Trancl.sym|const"><span>sym</span></a><span class="main"><span>(</span></span><span class="free"><span>r</span></span><span class="main"><span>)</span></span><span>"</span></span></span><span> </span><span class="keyword1"><span class="command"><span>using</span></span></span><span> </span><a class="entity_ref" href="../../FOL/ZF/Trancl.html#Trancl.equiv_def|fact"><span>equiv_def</span></a><span> </span><span class="keyword1"><span class="command"><span>by</span></span></span><span> </span><span class="operator"><span>simp</span></span><span>
</span><span class="keyword1"><span class="command"><span>from</span></span></span><span> </span><a class="entity_ref" href="Fol1.html#offset_6225..6227"><span>A1</span></a><span> </span><span class="keyword1"><span class="command"><span>have</span></span></span><span> </span><span class="quoted"><span class="quoted"><span>"</span><a class="entity_ref" href="../../FOL/ZF/Trancl.html#Trancl.sym|const"><span>sym</span></a><span class="main"><span>(</span></span><span class="free"><span>r</span></span><span class="main"><span>)</span></span><span>"</span></span></span><span> </span><span class="keyword1"><span class="command"><span>using</span></span></span><span> </span><a class="entity_ref" href="../../FOL/ZF/Trancl.html#Trancl.equiv_def|fact"><span>equiv_def</span></a><span> </span><span class="keyword1"><span class="command"><span>by</span></span></span><span> </span><span class="operator"><span>simp</span></span><span>
</span><span class="keyword1"><span class="command"><span>then</span></span></span><span> </span><span class="keyword1"><span class="command"><span>have</span></span></span><span> </span><span class="quoted"><span class="quoted"><span>"</span><span class="main"><a class="entity_ref" href="../../FOL/ZF/IFOL.html#IFOL.All|const"><span>∀</span></a></span><span class="bound"><span>x</span></span><span> </span><span class="bound"><span>y</span></span><span class="main"><a class="entity_ref" href="../../FOL/ZF/IFOL.html#IFOL.All|const"><span>.</span></a></span><span> </span><span class="main"><span>⟨</span></span><span class="bound"><span>x</span></span><span class="main"><span>,</span></span><span class="bound"><span>y</span></span><span class="main"><span>⟩</span></span><span> </span><span class="main"><a class="entity_ref" href="../../FOL/ZF/ZF_Base.html#ZF_Base.mem|const"><span>∈</span></a></span><span> </span><span class="free"><span>r</span></span><span> </span><span class="main"><a class="entity_ref" href="../../FOL/ZF/IFOL.html#IFOL.imp|const"><span>⟶</span></a></span><span> </span><span class="main"><span>⟨</span></span><span class="bound"><span>y</span></span><span class="main"><span>,</span></span><span class="bound"><span>x</span></span><span class="main"><span>⟩</span></span><span> </span><span class="main"><a class="entity_ref" href="../../FOL/ZF/ZF_Base.html#ZF_Base.mem|const"><span>∈</span></a></span><span> </span><span class="free"><span>r</span></span><span>"</span></span></span><span>
</span><span class="keyword1"><span class="command"><span>unfolding</span></span></span><span> </span><a class="entity_ref" href="../../FOL/ZF/Trancl.html#Trancl.sym_def|fact"><span>sym_def</span></a><span> </span><span class="keyword1"><span class="command"><span>by</span></span></span><span> </span><a class="entity_ref" href="../../FOL/ZF/ISABELLE_HOME/src/Provers/classical.ML.html#FOL.fast|method"><span class="operator"><span>fast</span></span></a><span>
</span><span class="keyword1"><span class="command"><span>with</span></span></span><span> </span><a class="entity_ref" href="Fol1.html#offset_6247..6249"><span>A2</span></a><span> </span><span class="keyword3"><span class="command"><span>show</span></span></span><span> </span><span class="quoted"><span class="quoted"><span>"</span><span class="main"><span>⟨</span></span><span class="free"><span>y</span></span><span class="main"><span>,</span></span><span class="free"><span>x</span></span><span class="main"><span>⟩</span></span><span> </span><span class="main"><a class="entity_ref" href="../../FOL/ZF/ZF_Base.html#ZF_Base.mem|const"><span>∈</span></a></span><span> </span><span class="free"><span>r</span></span><span>"</span></span></span><span> </span><span class="keyword1"><span class="command"><span>by</span></span></span><span> </span><a class="entity_ref" href="../../FOL/ZF/ISABELLE_HOME/src/Provers/blast.ML.html#FOL.blast|method"><span class="operator"><span>blast</span></span></a><span>
</span><span class="keyword1"><span class="command"><span>with</span></span></span><span> </span><a class="entity_ref" href="Fol1.html#offset_6246..6248"><span>A2</span></a><span> </span><span class="keyword3"><span class="command"><span>show</span></span></span><span> </span><span class="quoted"><span class="quoted"><span>"</span><span class="main"><span>⟨</span></span><span class="free"><span>y</span></span><span class="main"><span>,</span></span><span class="free"><span>x</span></span><span class="main"><span>⟩</span></span><span> </span><span class="main"><a class="entity_ref" href="../../FOL/ZF/ZF_Base.html#ZF_Base.mem|const"><span>∈</span></a></span><span> </span><span class="free"><span>r</span></span><span>"</span></span></span><span> </span><span class="keyword1"><span class="command"><span>by</span></span></span><span> </span><a class="entity_ref" href="../../FOL/ZF/ISABELLE_HOME/src/Provers/blast.ML.html#FOL.blast|method"><span class="operator"><span>blast</span></span></a><span>
</span><span class="keyword1"><span class="command"><span>qed</span></span></span><span>

</span><span class="comment1"><span>(* In Isabelle/ZF conjunction associates to the right!.
Expand Down
Loading

0 comments on commit 65b26be

Please sign in to comment.