Theory Introduction

theory Introduction
imports equalities
(* 
    This file is a part of IsarMathLib - 
    a library of formalized mathematics for Isabelle/Isar.

    Copyright (C) 2008-2014  Slawomir Kolodynski

    This program is free software; Redistribution and use in source and binary forms, 
    with or without modification, are permitted provided that the following conditions are met:

   1. Redistributions of source code must retain the above copyright notice, 
   this list of conditions and the following disclaimer.
   2. Redistributions in binary form must reproduce the above copyright notice, 
   this list of conditions and the following disclaimer in the documentation and/or 
   other materials provided with the distribution.
   3. The name of the author may not be used to endorse or promote products 
   derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED 
WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF 
MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. 
IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, 
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, 
PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; 
OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, 
WHETHER IN CONTRACT, 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.

*)

header{*\isaheader{Introduction.thy}*}

theory Introduction imports equalities

begin

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

section{*How to read IsarMathLib proofs - a tutorial*}

text{*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.
  *}

text{*The first thing that mathematicians typically do is to define
  notions. In Isar this is done with the @{text "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 @{text "≡"} symbol is the notion 
  being defined, the right side says how we define it. In Isabelle @{text "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 
  AreDisjoint (infix "{is disjoint with}" 90) where
  "A {is disjoint with} B ≡ A ∩ B = 0"

text{*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 
  @{text "<->"} 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 
  @{text "A {is disjoint with} B"} implies @{text "B {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 @{text "A {is disjoint with} B"} and the last statement
  is "then have @{text "B {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 
  @{text "-->"} 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: 
  shows "A {is disjoint with} B <-> B {is disjoint with} A"
proof -
  have "A {is disjoint with} B --> B {is disjoint with} A"
  proof -
    { assume "A {is disjoint with} B"
      then have "A ∩ B = 0" using AreDisjoint_def by simp
      hence "B ∩ A = 0" by auto
      then have  "B {is disjoint with} A"
        using AreDisjoint_def by simp
    } thus ?thesis by simp
  qed
  moreover have "B {is disjoint with} A --> A {is disjoint with} B"
  proof -
    { assume "B {is disjoint with} A"
      then have "B ∩ A = 0" using AreDisjoint_def by simp
      hence "A ∩ B = 0" by auto
      then have  "A {is disjoint with} B"
        using AreDisjoint_def by simp
    } thus ?thesis by simp
  qed
  ultimately show ?thesis by blast
qed

section{*Overview of the project*}

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

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

  In @{text "NatOrder_ZF"} we prove that the usual order on natural numbers
  is linear.
  
  The @{text "func1"} theory provides basic facts about functions.
  @{text "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. @{text "func_ZF_1"} is 
  about properties of functions related to order relations.

  The standard Isabelle's @{text "Finite"} theory defines the finite
  powerset of a set as a certain "datatype" (?) with some recursive
  properties. IsarMathLib's @{text "Finite1"} 
  and  @{text "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 @{text "Finite_ZF"} theory file.

  In @{text "FinOrd_ZF"} we talk about ordered finite sets.

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

  @{text "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)$.

  @{text "Fold_ZF"} shows how the familiar from functional 
  programming notion of fold can be interpreted in set theory.

  @{text "Partitions_ZF"} is about splitting a set into non-overlapping
  subsets. This is a common trick in proofs.

  @{text "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.

  @{text "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 @{text "Topology_ZF"} series covers basics of general topology: 
  interior, closure, boundary, compact sets, separation axioms and 
  continuous functions.
  
  @{text "Group_ZF"}, @{text "Group_ZF_1"}, @{text "Group_ZF_1b"} 
  and @{text "Group_ZF_2"}
  provide basic facts of the group theory. @{text "Group_ZF_3"} 
  considers the notion of almost homomorphisms that is nedeed for the 
  real numbers construction in @{text "Real_ZF"}.

  The @{text "TopologicalGroup"} connects the @{text "Topology_ZF"} and 
  @{text "Group_ZF"} series and starts the subject of topological groups
  with some basic definitions and facts.

  In @{text "DirectProduct_ZF"} we define direct product of groups and show
  some its basic properties.

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

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

  In the @{text "IntDiv_ZF_IML"} theory we translate some properties of the 
  integer quotient and reminder functions studied in the standard Isabelle's
  @{text "IntDiv_ZF"} theory to the notation used in IsarMathLib.
  
  The @{text "Real_ZF"} and @{text "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 @{text "Group_ZF_3"}, @{text "Ring_ZF_1"} 
  and @{text "Int_ZF_2"}. @{text "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. 
  @{text "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.

 @{text "Cardinal_ZF"} provides a couple of theorems about cardinals that are mostly used for studying  
 properties of topological properties (yes, this is kind of meta). 
 The main result (proven without AC) is that if two sets can be injectively mapped into an 
 infinite cardinal, then so can be their union. 
 There is also a definition of the Axiom of Choice specific for a given cardinal 
 (so that the choice function exists for families of sets of given cardinality). 
 Some properties are proven for such predicates, like that for finite families of sets the choice 
 function always exists (in ZF) and that the axiom of choice for a larger cardinal implies 
 one for a smaller cardinal.

 @{text "Group_ZF_4"} considers conjugate of subgroup and defines simple groups. 
 A nice theorem here is that endomorphisms of an abelian group form a ring. 
 The first isomorphism theorem (a group homomorphism $h$ induces an isomorphism between the group 
 divided by the kernel of $h$ and the image of $h$) is proven.

 Turns out given a property of a topological space one can define a local version of a property in general. 
 This is studied in the the @{text "Topology_ZF_properties_2"} theory and applied to local 
 versions of the property of being finite or compact or Hausdorff 
 (i.e. locally finite, locally compact, locally Hausdorff).
 There are a couple of nice applications, like one-point compactification that allows to show 
 that every locally compact Hausdorff space is regular. 
 Also there are some results on the interplay between hereditability of a property and local properties.

  For a given surjection $f : X\rightarrow Y$, where $X$ is a topological space one can consider the 
  weakest topology on $Y$ which makes $f$ continuous, let's call it a quotient topology generated by $f$.  
  The quotient topology generated by an equivalence relation r on X is actually a special case 
  of this setup, where $f$ is the natural projection of $X$ on the quotient $X/r$. 
  The properties of these two ways of getting new topologies are studied in @{text "Topology_ZF_8"} 
  theory. The main result is that any quotient topology generated by a function is homeomorphic 
  to a topology given by an equivalence relation, so these two approaches to quotient 
  topologies are kind of equivalent.

  As we all know, automorphisms of a topological space form a group. This fact is proven in @{text "Topology_ZF_9"} 
  and the automorphism groups for co-cardinal, included-set, and excluded-set topologies are identified. 
  For order topologies it is shown that order isomorphisms are homeomorphisms of the topology induced by the order. 
  Properties preserved by continuous functions are studied and as an application it is shown 
  for example that quotient topological spaces of compact (or connected) spaces are compact (or connected, resp.)
 
  The @{text "Topology_ZF_10"} theory is about products of two topological spaces. 
  It is proven that if two spaces are $T_0$ (or $T_1$, $T_2$, regular, connected) then their product is as well.

  Given a total order on a set one can define a natural topology on it generated by taking the rays 
  and intervals as the base. The  @{text "Topology_ZF_11"} theory studies relations between the order 
  and various properties of generated topology. For example one can show that if the order topology 
  is connected, then the order is complete (in the sense that for each set bounded from above the 
  set of upper bounds has a minimum). For a given cardinal $\kappa$ we can consider 
  generalized notion of $\kappa-separability$. Turns out $\kappa$-separability is related to (order) 
  density of sets of cardinality $\kappa$ for order topologies.


  Being a topological group imposes additional structure on the topology of the group, in particular 
  its separation properties. In @{text "Topological_Group_ZF_1.thy"} theory it is shown that if 
  a topology is $T_0$, then it must be $T_3$ , and that the topology in a topological group 
  is always regular.

  For a given normal subgroup of a topological group we can define a topology on the quotient 
  group in a natural way. At the end of the @{text "Topological_Group_ZF_2.thy"} theory it is shown 
  that such topology on the quotient group makes it a topological group.

  The @{text "Topological_Group_ZF_3.thy"} theory studies the topologies on subgroups of a 
  topological group. A couple of nice basic properties are shown, like that the closure of a 
  subgroup is a subgroup, closure of a normal subgroup is normal and, a bit more surprising 
  (to me) property that every locally-compact subgroup of a $T_0$ group is closed.

  In @{text "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.

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

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

  The theories @{text "MMI_logic_and_sets"}, @{text "MMI_Complex"}, 
  @{text "MMI_Complex_1"} and @{text "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 
  @{text "Metamath_theorems.txt"} file included in the 
  IsarMathLib distribution.
  The @{text "MMI_examples"} provides some theorems imported from Metamath
  that are printed in this proof document as examples of how translated
  proofs look like.
*}

end