theory MMI_prelude imports Order_ZF_1
begin
Metamath's set.mm features a large (over 8000) collection of theorems proven in the ZFC set theory. This theory is part of an attempt to translate those theorems to Isar so that they are available for Isabelle/ZF users. A total of about 1200 assertions have been translated, 600 of that with proofs (the rest was proven automatically by Isabelle). The translation was done with the support of the mmisar tool, whose source is included in the IsarMathLib distributions prior to version 1.6.4. The translation tool was doing about 99 percent of work involved, with the rest mostly related to the difference between Isabelle/ZF and Metamath metalogics. Metamath uses Tarski-Megill metalogic that does not have a notion of bound variables (see \( http://planetx.\ cc.\ vt.\ edu/AsteroidMeta/Distinctors\_vs\_binders \) for details and discussion). The translation project is closed now as I decided that it was too boring and tedious even with the support of mmisar software. Also, the translated proofs are not as readable as native Isar proofs which goes against IsarMathLib philosophy.
Importing from Metamath - how is it done
We are interested in importing the theorems about complex numbers that start from the "recnt" theorem on. This is done mostly automatically by the mmisar tool that is included in the IsarMathLib distributions prior to version 1.6.4. The tool works as follows:
First it reads the list of (Metamath) names of theorems that are already imported to IsarMathlib ("known theorems") and the list of theorems that are intended to be imported in this session ("new theorems"). The new theorems are consecutive theorems about complex numbers as they appear in the Metamath database. Then mmisar creates a "Metamath script" that contains Metamath commands that open a log file and put the statements and proofs of the new theorems in that file in a readable format. The tool writes this script to a disk file and executes metamath with standard input redirected from that file. Then the log file is read and its contents converted to the Isar format. In Metamath, the proofs of theorems about complex numbers depend only on 28 axioms of complex numbers and some basic logic and set theory theorems. The tool finds which of these dependencies are not known yet and repeats the process of getting their statements from Metamath as with the new theorems. As a result of this process mmisar creates files new\_theorems.thy, new\_deps.thy and new\_known\_theorems.txt. The file new\_theorems.thy contains the theorems (with proofs) imported from Metamath in this session. These theorems are added (by hand) to the current MMI_Complex_ZF_x.thy file. The file new\_deps.thy contains the statements of new dependencies with generic proofs "by auto". These are added to the MMI_logic_and_sets.thy. Most of the dependencies can be proven automatically by Isabelle. However, some manual work has to be done for the dependencies that Isabelle can not prove by itself and to correct problems related to the fact that Metamath uses a metalogic based on distinct variable constraints (Tarski-Megill metalogic), rather than an explicit notion of free and bound variables.
The old list of known theorems is replaced by the new list and mmisar is ready to convert the next batch of new theorems. Of course this rarely works in practice without tweaking the mmisar source files every time a new batch is processed.
The context for Metamath theorems
We list the Metamth's axioms of complex numbers and define notation here.
The next definition is what Metamath \(X\in V\) is translated to. I am not sure why it works, probably because Isabelle does a type inference and the "=" sign indicates that both sides are sets.
definition
\( X \text{ is a set } \equiv X = X \)
The next locale sets up the context to which Metamath theorems about complex numbers are imported. It assumes the axioms of complex numbers and defines the notation used for complex numbers. One of the problems with importing theorems from Metamath is that Metamath allows direct infix notation for binary operations so that the notation \(a f b\) is allowed where \(f\) is a function (that is, a set of pairs). To my knowledge, Isar allows only notation \( f\langle a,b\rangle \) with a possibility of defining a syntax say \( a + b \) to mean the same as \( f\langle a,b\rangle \) (please correct me if I am wrong here). This is why we have two objects for addition: one called caddset that represents the binary function, and the second one called ca which defines the \( a + b \) notation for \( caddset\langle a,b\rangle \). The same applies to multiplication of real numbers. Another difficulty is that Metamath allows to define sets with syntax \(\{ x | p\}\) where \(p\) is some formula that (usually) depends on \(x\). Isabelle allows the set comprehension like this only as a subset of another set i.e. \(\{x\in A . p(x)\}\). This forces us to have a sligtly different definition of (complex) natural numbers, requiring explicitly that natural numbers is a subset of reals. Because of that, the proofs of Metamath theorems that reference the definition directly can not be imported.
locale MMIsar0
defines \( a + b \equiv + \langle a,b\rangle \)
defines \( a \cdot b \equiv \cdot \langle a,b\rangle \)
defines \( a - b \equiv \bigcup \{ x \in \mathbb{C} .\ b + x = a \} \)
defines \( - a \equiv 0 - a \)
defines \( a / b \equiv \bigcup \{ x \in \mathbb{C} .\ b \cdot x = a \} \)
defines \( +\infty \equiv \mathbb{C} \)
defines \( -\infty \equiv \{\mathbb{C} \} \)
defines \( \mathbb{R} ^* \equiv \mathbb{R} \cup \{+\infty ,-\infty \} \)
defines \( \mathbb{N} \equiv \bigcap \{N \in Pow(\mathbb{R} ).\ 1 \in N \wedge (\forall n.\ n\in N \longrightarrow n + 1 \in N)\} \)
defines \( a \lt _{\mathbb{R}} b \equiv \langle a,b\rangle \in \lt _{\mathbb{R}} \)
defines \( \lt \equiv ( \lt _{\mathbb{R}} \cap \mathbb{R} \times \mathbb{R} ) \cup \{\langle -\infty ,+\infty \rangle \} \cup \) \( (\mathbb{R} \times \{+\infty \}) \cup (\{-\infty \}\times \mathbb{R} ) \)
defines \( a \lt b \equiv \langle a,b\rangle \in \lt \)
defines \( a > b \equiv \langle a,b\rangle \in converse( \lt ) \)
defines \( a \leq b \equiv \neg (b \lt a) \)
defines \( 2 \equiv 1 + 1 \)
defines \( 3 \equiv 2 + 1 \)
defines \( 4 \equiv 3 + 1 \)
defines \( 5 \equiv 4 + 1 \)
defines \( 6 \equiv 5 + 1 \)
defines \( 7 \equiv 6 + 1 \)
defines \( 8 \equiv 7 + 1 \)
defines \( 9 \equiv 8 + 1 \)
assumes MMI_pre_axlttri: \( A \in \mathbb{R} \wedge B \in \mathbb{R} \longrightarrow (A \lt _{\mathbb{R}} B \longleftrightarrow \neg (A=B \vee B \lt _{\mathbb{R}} A)) \)
assumes MMI_pre_axlttrn: \( A \in \mathbb{R} \wedge B \in \mathbb{R} \wedge C \in \mathbb{R} \longrightarrow ((A \lt _{\mathbb{R}} B \wedge B \lt _{\mathbb{R}} C) \longrightarrow A \lt _{\mathbb{R}} C) \)
assumes MMI_pre_axltadd: \( A \in \mathbb{R} \wedge B \in \mathbb{R} \wedge C \in \mathbb{R} \longrightarrow (A \lt _{\mathbb{R}} B \longrightarrow C + A \lt _{\mathbb{R}} C + B) \)
assumes MMI_pre_axmulgt0: \( A \in \mathbb{R} \wedge B \in \mathbb{R} \longrightarrow ( 0 \lt _{\mathbb{R}} A \wedge 0 \lt _{\mathbb{R}} B \longrightarrow 0 \lt _{\mathbb{R}} A\cdot B) \)
assumes MMI_pre_axsup: \( A \subseteq \mathbb{R} \wedge A \neq 0 \wedge (\exists x\in \mathbb{R} .\ \forall y\in A.\ y \lt _{\mathbb{R}} x) \longrightarrow \) \( (\exists x\in \mathbb{R} .\ (\forall y\in A.\ \neg (x \lt _{\mathbb{R}} y)) \wedge (\forall y\in \mathbb{R} .\ (y \lt _{\mathbb{R}} x \longrightarrow (\exists z\in A.\ y \lt _{\mathbb{R}} z)))) \)
assumes MMI_axresscn: \( \mathbb{R} \subseteq \mathbb{C} \)
assumes MMI_ax1ne0: \( 1 \neq 0 \)
assumes MMI_axcnex: \( \mathbb{C} \text{ is a set } \)
assumes MMI_axaddopr: \( + : ( \mathbb{C} \times \mathbb{C} ) \rightarrow \mathbb{C} \)
assumes MMI_axmulopr: \( \cdot : ( \mathbb{C} \times \mathbb{C} ) \rightarrow \mathbb{C} \)
assumes MMI_axmulcom: \( A \in \mathbb{C} \wedge B \in \mathbb{C} \longrightarrow A \cdot B = B \cdot A \)
assumes MMI_axaddcl: \( A \in \mathbb{C} \wedge B \in \mathbb{C} \longrightarrow A + B \in \mathbb{C} \)
assumes MMI_axmulcl: \( A \in \mathbb{C} \wedge B \in \mathbb{C} \longrightarrow A \cdot B \in \mathbb{C} \)
assumes MMI_axdistr: \( A \in \mathbb{C} \wedge B \in \mathbb{C} \wedge C \in \mathbb{C} \longrightarrow A\cdot (B + C) = A\cdot B + A\cdot C \)
assumes MMI_axaddcom: \( A \in \mathbb{C} \wedge B \in \mathbb{C} \longrightarrow A + B = B + A \)
assumes MMI_axaddass: \( A \in \mathbb{C} \wedge B \in \mathbb{C} \wedge C \in \mathbb{C} \longrightarrow A + B + C = A + (B + C) \)
assumes MMI_axmulass: \( A \in \mathbb{C} \wedge B \in \mathbb{C} \wedge C \in \mathbb{C} \longrightarrow A \cdot B \cdot C = A \cdot (B \cdot C) \)
assumes MMI_ax1re: \( 1 \in \mathbb{R} \)
assumes MMI_axi2m1: \( \imath \cdot \imath + 1 = 0 \)
assumes MMI_ax0id: \( A \in \mathbb{C} \longrightarrow A + 0 = A \)
assumes MMI_axicn: \( \imath \in \mathbb{C} \)
assumes MMI_axnegex: \( A \in \mathbb{C} \longrightarrow ( \exists x \in \mathbb{C} .\ ( A + x ) = 0 ) \)
assumes MMI_axrecex: \( A \in \mathbb{C} \wedge A \neq 0 \longrightarrow ( \exists x \in \mathbb{C} .\ A \cdot x = 1 ) \)
assumes MMI_ax1id: \( A \in \mathbb{C} \longrightarrow A \cdot 1 = A \)
assumes MMI_axaddrcl: \( A \in \mathbb{R} \wedge B \in \mathbb{R} \longrightarrow A + B \in \mathbb{R} \)
assumes MMI_axmulrcl: \( A \in \mathbb{R} \wedge B \in \mathbb{R} \longrightarrow A \cdot B \in \mathbb{R} \)
assumes MMI_axrnegex: \( A \in \mathbb{R} \longrightarrow ( \exists x \in \mathbb{R} .\ A + x = 0 ) \)
assumes MMI_axrrecex: \( A \in \mathbb{R} \wedge A \neq 0 \longrightarrow ( \exists x \in \mathbb{R} .\ A \cdot x = 1 ) \)
end
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8