1
Preface
1.1
Structure of the book
2
Fundamentals of Isabelle
2.1
Inductive data types
2.2
Functions
2.3
Primitive recursion
2.4
Theorems and proofs
2.4.1
Querying and using proofs
2.4.2
More complex proofs
2.4.3
The thinking process
2.5
Inductive predicates
2.5.1
When to use inductive over recursive
2.6
Type declarations and axiomatization
2.6.1
Sets
2.6.2
Natural numbers
2.6.3
All types are inhabited
2.7
Meta logic
2.7.1
Meta universal quantifier
2.7.2
Meta implication
2.7.3
Meta equality
2.8
Abstraction and representation
2.8.1
Morphisms can be omitted
2.9
Syntactic sugars and Lists
2.10
Type classes and semigroups
2.10.1
List and nat are semigroups
2.10.2
Instantiating natural numbers
2.10.3
Instantiating lists
2.10.4
Restricting type parameters
2.10.5
Type classes with axioms
2.10.6
Proofs that use class axioms
2.11
Quotient types
2.11.1
Integer numbers in mathematics
2.11.2
Equivalence classes
2.11.3
Integer numbers in Isabelle
2.11.4
Lifting
2.12
Main library
2.12.1
Order
2.12.2
Lattices
2.12.3
Top and bottom
2.12.4
Boolean algebra
2.12.5
Sets
2.13
Function sets
2.14
Locales
2.14.1
Semigroups
2.14.2
Monoids
2.14.3
Groups
2.14.4
Group properties
2.14.5
Abelian
2.14.6
Type classes with sublocales
2.15
Archive of formal proofs
3
Set theory
3.1
Maps
3.2
Equivalence classes
4
Abstract Algebra
4.1
Semigroups
4.2
Monoids
4.2.1
Transformations
4.3
Inverse elements
4.4
Groups
4.4.1
Transformations
4.5
Homomorphisms
4.5.1
Isomorphisms
4.5.2
Translations
4.6
Rings
4.7
Fields
5
Topology
5.1
Topological spaces
5.1.1
Topology
5.1.2
Discrete topology
5.1.3
Open, closed and clopen sets
5.1.4
Finite-closed topology
5.1.5
Basis
5.2
Order and separation
5.2.1
Order topology
5.2.2
T0, T1 and T2 spaces
5.2.3
Linear order and separation axioms
5.2.4
Instances of topologies
5.3
Neighborhoods and filters
5.3.1
Filters
5.3.2
Eventually
6
Functional Analysis
7
Measure theory
8
Linear Algebra
9
Real analysis
10
Probability
11
Abstract Algebra II
Learn Mathematics and Computer Science with Isabelle
9
Real analysis