This theory does not contain any formalized mathematics used in other theories, but is an introduction to IsarMathLib project.

Isar (the Isabelle's formal proof language) was designed to be similar to the standard language of mathematics. Any person able to read proofs in a typical mathematical paper should be able to read and understand Isar proofs without having to learn a special proof language. However, Isar is a formal proof language and as such it does contain a couple of constructs whose meaning is hard to guess. In this tutorial we will define a notion and prove an example theorem about that notion, explaining Isar syntax along the way. This tutorial may also serve as a style guide for IsarMathLib contributors. Note that this tutorial aims to help in reading the presentation of the Isar language that is used in IsarMathLib proof document and HTML rendering on the FormalMath.org site, but does not teach how to write proofs that can be verified by Isabelle. This presentation is different than the source processed by Isabelle (the concept that the source and presentation look different should be familiar to any LaTeX user). To learn how to write Isar proofs one needs to study the source of this tutorial as well.

The first thing that mathematicians typically do is to define
notions. In Isar this is done with the *definition* keyword.
In our case we define a notion of two
sets being disjoint. We will use the infix notation, i.e. the string
\( \text{ is disjoint with } \) put between two sets to denote our notion
of disjointness.
The left side of the \( \equiv \) symbol is the notion
being defined, the right side says how we define it. In Isabelle *0*
is used to denote both zero (of natural numbers) and the empty set, which is
not surprising as those two things are the same in set theory.

** Definition **

\( A \text{ is disjoint with } B \equiv A \cap B = 0 \)

We are ready to prove a theorem. Here we show that the relation of being disjoint is symmetric. We start with one of the keywords ''theorem'', ''lemma'' or ''corollary''. In Isar they are synonymous. Then we provide a name for the theorem. In standard mathematics theorems are numbered. In Isar we can do that too, but it is considered better to give theorems meaningful names. After the ''shows'' keyword we give the statement to show. The \( \longleftrightarrow \) symbol denotes the equivalence in Isabelle/ZF. Here we want to show that "A is disjoint with B iff and only if B is disjoint with A". To prove this fact we show two implications - the first one that \( A \text{ is disjoint with } B \) implies \( B \text{ is disjoint with } A \) and then the converse one. Each of these implications is formulated as a statement to be proved and then proved in a subproof like a mini-theorem. Each subproof uses a proof block to show the implication. Proof blocks are delimited with curly brackets in Isar. Proof block is one of the constructs that does not exist in informal mathematics, so it may be confusing. When reading a proof containing a proof block I suggest to focus first on what is that we are proving in it. This can be done by looking at the first line or two of the block and then at the last statement. In our case the block starts with "assume \( A \text{ is disjoint with } B \) and the last statement is "then have \( B \text{ is disjoint with } A \)". It is a typical pattern when someone needs to prove an implication: one assumes the antecedent and then shows that the consequent follows from this assumption. Implications are denoted with the \( \longrightarrow \) symbol in Isabelle. After we prove both implications we collect them using the ''moreover'' construct. The keyword ''ultimately'' indicates that what follows is the conclusion of the statements collected with ''moreover''. The ''show'' keyword is like ''have'', except that it indicates that we have arrived at the claim of the theorem (or a subproof).

** theorem ** disjointness_symmetric:

{
** assume **\( A \text{ is disjoint with } B \)
** then **** have ** \( A \cap B = 0 \)** using ** AreDisjoint_def
** hence ** \( B \cap A = 0 \)
** then **** have ** \( B \text{ is disjoint with } A \)** using ** AreDisjoint_def
** } **
** thus ** \( thesis \)
** qed **

{
** assume **\( B \text{ is disjoint with } A \)
** then **** have ** \( B \cap A = 0 \)** using ** AreDisjoint_def
** hence ** \( A \cap B = 0 \)
** then **** have ** \( A \text{ is disjoint with } B \)** using ** AreDisjoint_def
** } **
** thus ** \( thesis \)
** qed **

The *Fol1*, * ZF1* and *Nat_ZF_IML* theory
files contain some background material that is needed for
the remaining theories.

*Order_ZF* and *Order_ZF_1a* reformulate
material from standard Isabelle's
*Order* theory in terms of non-strict (less-or-equal)
order relations.
*Order_ZF_1* on the other hand directly continues the *Order*
theory file using strict order relations (less and not equal). This is useful
for translating theorems from Metamath.

In *NatOrder_ZF* we prove that the usual order on natural numbers
is linear.
The *func1* theory provides basic facts about functions.
*func_ZF* continues this development with more advanced
topics that relate to algebraic properties of binary operations,
like lifting a binary operation to a function space,
associative, commutative and distributive operations and properties
of functions related to order relations. *func_ZF_1* is
about properties of functions related to order relations.

The standard Isabelle's *Finite* theory defines the finite
powerset of a set as a certain "datatype" (?) with some recursive
properties. IsarMathLib's *Finite1*
and *Finite_ZF_1* theories develop more facts about this notion.
These two theories are obsolete now.
They will be gradually replaced by an approach based on set theory
rather than tools specific to Isabelle. This approach is presented
in *Finite_ZF* theory file.

In *FinOrd_ZF* we talk about ordered finite sets.

The *EquivClass1* theory file is a reformulation of
the material in the standard
Isabelle's *EquivClass* theory in the spirit of ZF set theory.
*FiniteSeq_ZF* discusses the notion of finite sequences
(a.k.a. lists).

*InductiveSeq_ZF* provides the definition and properties of
(what is known in basic calculus as) sequences defined by induction,
i. e. by a formula of the form \(a_0 = x,\ a_{n+1} = f(a_n)\).

*Fold_ZF* shows how the familiar from functional
programming notion of fold can be interpreted in set theory.

*Partitions_ZF* is about splitting a set into non-overlapping
subsets. This is a common trick in proofs.

*Semigroup_ZF* treats the expressions of the form
\(a_0\cdot a_1\cdot .. \cdot a_n\), (i.e. products of finite sequences),
where "\(\cdot\)" is an associative binary operation.

*CommutativeSemigroup_ZF* is another take on a similar subject.
This time we consider the case when the operation is commutative
and the result of depends only on the set of elements we are
summing (additively speaking), but not the order.

The *Topology_ZF* series covers basics of general topology:
interior, closure, boundary, compact sets, separation axioms and
continuous functions.
*Group_ZF*, *Group_ZF_1*, *Group_ZF_1b*
and *Group_ZF_2*
provide basic facts of the group theory. *Group_ZF_3*
considers the notion of almost homomorphisms that is nedeed for the
real numbers construction in *Real_ZF*.

The *TopologicalGroup* connects the *Topology_ZF* and
*Group_ZF* series and starts the subject of topological groups
with some basic definitions and facts.

In *DirectProduct_ZF* we define direct product of groups and show
some its basic properties.

The *OrderedGroup_ZF* theory treats ordered groups.
This is a suprisingly large theory for such relatively obscure topic.
*Ring_ZF* defines rings. *Ring_ZF_1* covers
the properties of rings that are specific to the real numbers construction
in *Real_ZF*.

The *OrderedRing_ZF* theory looks at the consequences of adding
a linear order to the ring algebraic structure.
*Field_ZF* and *OrderedField_ZF* contain basic facts
about (you guessed it) fields and ordered fields.
*Int_ZF_IML* theory considers the integers
as a monoid (multiplication) and an abelian ordered group (addition).
In *Int_ZF_1* we show that integers form a commutative ring.
*Int_ZF_2* contains some facts about slopes (almost homomorphisms
on integers) needed for real numbers construction,
used in *Real_ZF_1*.

In the *IntDiv_ZF_IML* theory translates some properties of the
integer quotient and reminder functions studied in the standard Isabelle's
*IntDiv_ZF* theory to the notation used in IsarMathLib.
The *Real_ZF* and *Real_ZF_1* theories
contain the construction of real numbers based on the paper \cite{Arthan2004}
by R. D. Arthan (not Cauchy sequences, not Dedekind sections).
The heavy lifting
is done mostly in *Group_ZF_3*, *Ring_ZF_1*
and *Int_ZF_2*. *Real_ZF* contains
the part of the construction that can be done
starting from generic abelian groups (rather than additive group of integers).
This allows to show that real numbers form a ring.
*Real_ZF_1* continues the construction using properties specific
to the integers and showing that real numbers constructed this way
form a complete ordered field.

In *Complex_ZF* we construct complex numbers starting from
a complete ordered field (a model of real numbers). We also define
the notation for writing about complex numbers and prove that the
structure of complex numbers constructed there satisfies the axioms
of complex numbers used in Metamath.

*MMI_prelude* defines the *mmisar0* context in which
most theorems translated from Metamath are proven. It also contains a
chapter explaining how the translation works.

In the *Metamath_interface* theory we prove a theorem
that the *mmisar0* context is valid (can be used)
in the *complex0* context.
All theories using the translated results will import the
*Metamath_interface* theory. The *Metamath_sampler*
theory provides some examples of using the translated theorems
in the *complex0* context.

The theories *MMI_logic_and_sets*, *MMI_Complex*,
*MMI_Complex_1* and *MMI_Complex_2*
contain the theorems imported from the
Metamath's set.mm database. As the translated proofs are rather verbose
these theories are not printed in this proof document.
The full list of translated facts can be found in the
*Metamath_theorems.txt* file included in the
IsarMathLib distribution.
The *MMI_examples* provides some theorems imported from Metamath
that are printed in this proof document as examples of how translated
proofs look like.

Definition of AreDisjoint:
\( A \text{ is disjoint with } B \equiv A \cap B = 0 \)