release 1.30.0

SKolodynski · May 26, 2024 · ea33786 · ea33786
1 parent 6f7ff74
commit ea33786
Show file tree

Hide file tree

Showing 114 changed files with 11,727 additions and 9,770 deletions.
diff --git a/Dockerfile b/Dockerfile
@@ -1,6 +1,6 @@
 ## Dockerfile for IsarMathLib
 
-FROM slawekkol/isarmathlib:isabelle-zf-2023
+FROM slawekkol/isarmathlib:isabelle-zf-2024
 
 COPY IsarMathLib /home/isabelle/IsarMathLib
 

diff --git a/IsarMathLib/IntModule_ZF.thy b/IsarMathLib/IntModule_ZF.thy
@@ -1054,8 +1054,8 @@ proof(rule nat_induct[of z2 "\<lambda>t. Fold(P,\<one>,(z1#*t)\<times>{g}) = Fol
   }
 qed
 
-text\<open>Multiplying 2 int_of natural numbers, is the same as multiplying the natural
-numbers and then applying int_of\<close>
+text\<open>Multiplying 2 int\_of natural numbers, is the same as multiplying the natural
+numbers and then applying int\_of\<close>
 
 lemma int_of_mult:
   assumes "nr:nat" "ns:nat"
@@ -1257,17 +1257,19 @@ sublocale abelian_group_int_action < int_action:module0 ints IntegerAddition Int
   using groupAssum apply simp using isAbelian apply simp using group_action_int
   unfolding IsLeftModule_def apply simp done
 
-text\<open>
+(*
 lemma (in abelian_group_int) one_one:
   shows "\<one> = TheNeutralElement(ints,IntegerMultiplication)"
 
 cannot be interpreted. First the unit integer.
-\<close>
+\<close>*)
 
 abbreviation (in abelian_group_int_action) zone ("\<one>\<^sub>\<int>") where
 "\<one>\<^sub>\<int> \<equiv> ione"
 
 text\<open>Then, the unit in the abelian group\<close>
 
 abbreviation (in abelian_group_int_action) gone ("\<one>\<^sub>G") where
-"\<one>\<^sub>G \<equiv> neut"
+"\<one>\<^sub>G \<equiv> neut"
+
+end
diff --git a/IsarMathLib/document/root.tex b/IsarMathLib/document/root.tex
@@ -66,8 +66,8 @@
 \maketitle
 
 \begin{abstract}
-This is the proof document of the IsarMathLib project version 1.29.0. 
-IsarMathLib is a library of formalized mathematics for Isabelle2023 (ZF logic). 
+This is the proof document of the IsarMathLib project version 1.30.0. 
+IsarMathLib is a library of formalized mathematics for Isabelle2024 (ZF logic). 
 
 \end{abstract}
 

diff --git a/README.md b/README.md
@@ -10,7 +10,7 @@ IsarMathLib is a library of formalized mathematics for Isabelle/ZF.
 [Isabelle](https://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html) is a theorem proving environment developed at Cambridge University and TU Munich.
 Isabelle needs to be installed on the machine before you can generate IsarMathLib proof documents or verify the proofs. The Isabelle site provides the installation instructions. IsarMathLib is always tested only with the version of Isabelle that is current at the time of IsarMathLib release.
 
-IsarMathLib needs Isabelle/ZF logic that is not shipped precompiled in the Isabelle distribution bundle. To build the ZF heap go to the directory where you have unpacked Isabelle and type "./bin/isabelle build -b ZF". Alternatively, one can change the default logic in the etc/settings file from HOL to ZF and then start Isabelle environment with the main `Isabelle2023` executable script. This should start with building the ZF heap image.
+IsarMathLib needs Isabelle/ZF logic that is not shipped precompiled in the Isabelle distribution bundle. To build the ZF heap go to the directory where you have unpacked Isabelle and type "./bin/isabelle build -b ZF". Alternatively, one can change the default logic in the etc/settings file from HOL to ZF and then start Isabelle environment with the main `Isabelle2024` executable script. This should start with building the ZF heap image.
 
 Before processing the IsarMathLib project theories, make sure you have LaTeX installed (including extras, for example in Ubuntu run "apt-get install texlive-latex-extras").
 

diff --git a/docs/IsarMathLib/AbelianGroup_ZF.html b/docs/IsarMathLib/AbelianGroup_ZF.html
diff --git a/docs/IsarMathLib/Cardinal_ZF.html b/docs/IsarMathLib/Cardinal_ZF.html
diff --git a/docs/IsarMathLib/CommutativeSemigroup_ZF.html b/docs/IsarMathLib/CommutativeSemigroup_ZF.html
diff --git a/docs/IsarMathLib/Complex_ZF.html b/docs/IsarMathLib/Complex_ZF.html
diff --git a/docs/IsarMathLib/DirectProduct_ZF.html b/docs/IsarMathLib/DirectProduct_ZF.html
diff --git a/docs/IsarMathLib/Enumeration_ZF.html b/docs/IsarMathLib/Enumeration_ZF.html
diff --git a/docs/IsarMathLib/EquivClass1.html b/docs/IsarMathLib/EquivClass1.html
diff --git a/docs/IsarMathLib/Field_ZF.html b/docs/IsarMathLib/Field_ZF.html
diff --git a/docs/IsarMathLib/FinOrd_ZF.html b/docs/IsarMathLib/FinOrd_ZF.html
diff --git a/docs/IsarMathLib/Finite1.html b/docs/IsarMathLib/Finite1.html
diff --git a/docs/IsarMathLib/FiniteSeq_ZF.html b/docs/IsarMathLib/FiniteSeq_ZF.html
diff --git a/docs/IsarMathLib/Finite_State_Machines_ZF.html b/docs/IsarMathLib/Finite_State_Machines_ZF.html
diff --git a/docs/IsarMathLib/Finite_ZF.html b/docs/IsarMathLib/Finite_ZF.html
diff --git a/docs/IsarMathLib/Finite_ZF_1.html b/docs/IsarMathLib/Finite_ZF_1.html
diff --git a/docs/IsarMathLib/Fol1.html b/docs/IsarMathLib/Fol1.html
diff --git a/docs/IsarMathLib/Fold_ZF.html b/docs/IsarMathLib/Fold_ZF.html
diff --git a/docs/IsarMathLib/Generalization_ZF.html b/docs/IsarMathLib/Generalization_ZF.html
diff --git a/docs/IsarMathLib/Group_ZF.html b/docs/IsarMathLib/Group_ZF.html
diff --git a/docs/IsarMathLib/Group_ZF_1.html b/docs/IsarMathLib/Group_ZF_1.html
diff --git a/docs/IsarMathLib/Group_ZF_1b.html b/docs/IsarMathLib/Group_ZF_1b.html
diff --git a/docs/IsarMathLib/Group_ZF_2.html b/docs/IsarMathLib/Group_ZF_2.html
diff --git a/docs/IsarMathLib/Group_ZF_3.html b/docs/IsarMathLib/Group_ZF_3.html
diff --git a/docs/IsarMathLib/Group_ZF_4.html b/docs/IsarMathLib/Group_ZF_4.html
diff --git a/docs/IsarMathLib/Group_ZF_5.html b/docs/IsarMathLib/Group_ZF_5.html
diff --git a/docs/IsarMathLib/InductiveSeq_ZF.html b/docs/IsarMathLib/InductiveSeq_ZF.html
diff --git a/docs/IsarMathLib/IntDiv_ZF_IML.html b/docs/IsarMathLib/IntDiv_ZF_IML.html
diff --git a/docs/IsarMathLib/IntModule_ZF.html b/docs/IsarMathLib/IntModule_ZF.html
diff --git a/docs/IsarMathLib/Int_ZF_1.html b/docs/IsarMathLib/Int_ZF_1.html
diff --git a/docs/IsarMathLib/Int_ZF_2.html b/docs/IsarMathLib/Int_ZF_2.html
diff --git a/docs/IsarMathLib/Int_ZF_3.html b/docs/IsarMathLib/Int_ZF_3.html
diff --git a/docs/IsarMathLib/Int_ZF_IML.html b/docs/IsarMathLib/Int_ZF_IML.html
diff --git a/docs/IsarMathLib/Introduction.html b/docs/IsarMathLib/Introduction.html
diff --git a/docs/IsarMathLib/Lattice_ZF.html b/docs/IsarMathLib/Lattice_ZF.html
diff --git a/docs/IsarMathLib/Loop_ZF.html b/docs/IsarMathLib/Loop_ZF.html
diff --git a/docs/IsarMathLib/MMI_Complex_ZF.html b/docs/IsarMathLib/MMI_Complex_ZF.html
diff --git a/docs/IsarMathLib/MMI_Complex_ZF_1.html b/docs/IsarMathLib/MMI_Complex_ZF_1.html
diff --git a/docs/IsarMathLib/MMI_Complex_ZF_2.html b/docs/IsarMathLib/MMI_Complex_ZF_2.html
diff --git a/docs/IsarMathLib/MMI_examples.html b/docs/IsarMathLib/MMI_examples.html
@@ -12,7 +12,7 @@
 <h1>Theory MMI_examples</h1>
 </div>
 
-<pre class="source"><span class="comment1"><span>(</span><span>*</span><span> 
+<pre class="source"><span class="comment1"><span>(* 
     This file is a part of MMIsar - a translation of Metamath's set.mm to Isabelle 2005 (ZF logic).
 
     Copyright (C) 2006  Slawomir Kolodynski
@@ -37,22 +37,22 @@ <h1>Theory MMI_examples</h1>
 STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE
 USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 
-</span><span>*</span><span>)</span></span><span>
+*)</span></span><span>
 
-</span><span class="keyword1"><span class="command"><span>section</span></span></span><span> </span><span class="quoted"><span class="plain_text"><span>‹</span><span>Metamath examples</span><span>›</span></span></span><span>
+</span><span class="keyword1"><span class="command"><span>section</span></span></span><span> </span><span class="quoted"><span class="plain_text"><span>‹Metamath examples›</span></span></span><span>
 
 </span><span class="keyword1"><span class="command"><span>theory</span></span></span><span> </span><a href="MMI_examples.html"><span>MMI_examples</span></a><span> </span><span class="keyword2"><span class="keyword"><span>imports</span></span></span><span> </span><a href="MMI_Complex_ZF.html"><span>MMI_Complex_ZF</span></a><span>
 
 </span><span class="keyword2"><span class="keyword"><span>begin</span></span></span><span> 
 
-</span><span class="keyword1"><span class="command"><span>text</span></span></span><span class="quoted"><span class="plain_text"><span>‹</span><span>This theory contains 10 theorems translated from 
-</span><span>  Metamath (with proofs). It is included
-</span><span>  in the proof document as an illustration of how a translated
-</span><span>  Metamath proof looks like. The "known\_theorems.txt"
-</span><span>  file included in the IsarMathLib distribution provides
-</span><span>  a list of all translated facts.</span><span>›</span></span></span><span>
+</span><span class="keyword1"><span class="command"><span>text</span></span></span><span class="quoted"><span class="plain_text"><span>‹This theory contains 10 theorems translated from 
+  Metamath (with proofs). It is included
+  in the proof document as an illustration of how a translated
+  Metamath proof looks like. The "known\_theorems.txt"
+  file included in the IsarMathLib distribution provides
+  a list of all translated facts.›</span></span></span><span>
 
-</span><span class="comment1"><span>(</span><span>*</span><span>*****201-210***************************</span><span>*</span><span>)</span></span><span>
+</span><span class="comment1"><span>(******201-210****************************)</span></span><span>
 
 </span><span class="keyword1"><span class="command"><span>lemma</span></span></span><span> </span><span class="main"><span>(</span></span><span class="keyword2"><span class="keyword"><span>in</span></span></span><span> </span><a class="entity_ref" href="MMI_prelude.html#MMI_prelude.MMIsar0|locale"><span>MMIsar0</span></a><span class="main"><span>)</span></span><span> </span><span class="entity_def" id="MMI_examples.MMIsar0.MMI_dividt|fact"><span class="entity_def" id="MMI_examples.MMIsar0.MMI_dividt|thm"><span>MMI_dividt</span></span></span><span class="main"><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> </span><span class="free"><span>A</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="main"><span class="free"><span>ℂ</span></span></span><span> </span><span class="main"><a class="entity_ref" href="../../FOL/ZF/IFOL.html#IFOL.conj|const"><span>∧</span></a></span><span> </span><span class="free"><span>A</span></span><span> </span><span class="main"><a class="entity_ref" href="../../FOL/ZF/IFOL.html#IFOL.not_equal|const"><span>≠</span></a></span><span> </span><span class="main"><span class="free"><span>𝟬</span></span></span><span> </span><span class="main"><span>)</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> </span><span class="free"><span>A</span></span><span> </span><span class="main"><span class="free"><span>\&lt;cdiv&gt;</span></span></span><span> </span><span class="free"><span>A</span></span><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="main"><span class="free"><span>𝟭</span></span></span><span>"</span></span></span><span>