Theory Fol1

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

    Copyright (C) 2005, 2006  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{Fol1.thy}*}

theory Fol1 imports Trancl 

begin

section{*Mission statement*}

text{*Until we come up with something better let's just say
  that writing formalized proofs protects from Alzheimer's disease
  better than solving crossword puzzles.*}

section{*Release notes*}

text{* This release continues the process of importing Metamath's \cite{Metamath}
  set.mm database into IsarMathLib, adding about 440 facts and 200 translated proofs.
  We also add a construction of a model of complex numbers from a complete ordered
  field.*}

section{*Overview of the project*}

text{* 
  The theory files @{text "Fo11"}, @{text " ZF1"}, @{text "Nat_ZF"}, 
  @{text "func1"}, @{text "func_ZF"}, @{text "EquivClass1"}, 
  @{text "Finite1"}, @{text "Finite_ZF"}, @{text "Order_ZF"} contain some 
  background material that is needed for the remaining theories. 

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

  @{text "Field_ZF"} and @{text "OrderedField_ZF"} contain basic facts
  about (you guessed it) fields and ordered fields. 
  
  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"} @{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 showing that real numbers constructed this way
  form a complete ordered field.

  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.

  The @{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.thy"} 
  and @{text "MMI_Complex_1"} 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 "known_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 looks like.
*}

section{*Notions and lemmas in FOL*}

text{*This section contains mostly shortcuts and workarounds 
  that allow to use more readable coding style.*}

(*temporarily removed bc. it takes too long to check
text{*The definition and lemma below implement a common idiom used in 
romantic mathematics when the author states some assumptions, says
"then the following are equivalent" and proceeds with the proof that shows 
implications between the statements. The usefulness of theorems stated this 
way is rather limited in Isar as the simp and auto methods may take a really 
long time to infer anything from equivalences if there is more than one. 
Still, we believe that being able to formulate a theorem like this 
is good for readibility.*}

constdefs
  All4areEquivalent :: "[o,o,o,o]=>o"
  "All4areEquivalent(p,q,r,s) ≡ 
  (p<->q) & (p<->r) & (p<->s) & (q<->r) & (q<->s) & (r<->s)";

lemma Fol1_L1: assumes A1: "p-->q" and A2: "q-->r" 
  and A3: "r-->s" and A4: "s-->p" 
  shows "All4areEquivalent(p,q,r,s)"
proof-;  
  from A1 A2 A3 A4 have "p<->q"by auto;
  moreover from A1 A2 A3 A4 have "p<->r" by auto;
  moreover from A1 A2 A3 A4 have "p<->s" by auto;
  moreover from A1 A2 A3 A4 have "q<->r" by auto;
  moreover from A1 A2 A3 A4 have "q<->s" by auto;
  moreover from A1 A2 A3 A4 have "r<->s" by auto;
  ultimately show ?thesis using All4areEquivalent_def by simp;
qed; 

text{*It happens quite often that we need to prove a statement of the form
$\forall x y. P(x,y) \rightarrow Q(x,y)$. The next lemma provides a shortcut 
for proving this type of statements. To apply this shortcut we can say 
"(rule double\_forall\_implies)" after the "proof" keyword and we are free to
show the statement by doing "fix x y assume P(x,y) show Q(x,y).*}

lemma double_forall_implies: 
  assumes A1:" !!x y. P(x,y) ==> R(x,y)"
  shows "∀x y. (P(x,y) --> R(x,y))"
proof -;
  from A1 show ?thesis by simp;
qed;

*)

text{*The next lemma serves as a workaround to problems with applying 
  the definition of transitivity (of a relation) in our coding style 
  (any attempt to do
  something like @{text "using trans_def"} results up Isabelle in an 
  infinite loop). We reluctantly use @{text "(unfold trans_def)"} after the 
  @{text "proof"} keyword  to workaround this.*}

lemma Fol1_L2: assumes 
  A1: "∀ x y z. ⟨x, y⟩ ∈ r ∧ ⟨y, z⟩ ∈ r --> ⟨x, z⟩ ∈ r"
  shows "trans(r)"
proof (unfold trans_def)
  from A1 show
    "∀ x y z. ⟨x, y⟩ ∈ r --> ⟨y, z⟩ ∈ r --> ⟨x, z⟩ ∈ r"
    using imp_conj by blast;
qed;

text{*Another workaround for the problem of Isabelle simplifier looping when 
  the transitivity definition is used. *}

lemma Fol1_L3: assumes A1: "trans(r)" and A2: "<a,b> ∈ r  ∧ <b,c> ∈ r"
  shows "<a,c> ∈ r"
proof -;
  from A1 have  "∀x y z. ⟨x, y⟩ ∈ r --> ⟨y, z⟩ ∈ r --> ⟨x, z⟩ ∈ r"
    by (unfold trans_def);
  with A2 show ?thesis using imp_conj by fast;
qed;
  
text{*There is a problem with application of the definition of asymetry for
  relations. The next lemma is a workaround.*}

lemma Fol1_L4: 
  assumes A1: "antisym(r)" and A2: "<a,b> ∈ r"   "<b,a> ∈ r"  
  shows "a=b"
proof -;
  from A1 have "∀ x y. <x,y> ∈ r --> <y,x> ∈ r --> x=y"
    by (unfold antisym_def);
  with A2 show "a=b" using imp_conj by fast;
qed;

text{*The definition below implements a common idiom that states that 
  (perhaps under some assumptions) exactly one of give three statements 
  is true.*}

constdefs
  "Exactly_1_of_3_holds(p,q,r) ≡ 
  (p∨q∨r) ∧ (p --> ¬q ∧ ¬r) ∧ (q --> ¬p ∧ ¬r) ∧ (r --> ¬p ∧ ¬q)";

text{*The next lemma allows to prove statements of the form 
  @{text "Exactly_1_of_3_holds (p,q,r)"}.*}

lemma Fol1_L5:
  assumes "p∨q∨r"
  and "p --> ¬q ∧ ¬r"
  and "q --> ¬p ∧ ¬r"
  and "r --> ¬p ∧ ¬q"
  shows "Exactly_1_of_3_holds (p,q,r)"
proof -;
  from prems have
    "(p∨q∨r) ∧ (p --> ¬q ∧ ¬r) ∧ (q --> ¬p ∧ ¬r) ∧ (r --> ¬p ∧ ¬q)"
    by blast;
  then show "Exactly_1_of_3_holds (p,q,r)"
    by (unfold Exactly_1_of_3_holds_def);
qed;

text{*If exactly one of $p,q,r$ holds and $p$ is not true, then
  $q$ or $r$.*}

lemma Fol1_L6: 
  assumes A1: "¬p" and A2: "Exactly_1_of_3_holds (p,q,r)" 
  shows "q∨r"
proof -
  from A2 have  
    "(p∨q∨r) ∧ (p --> ¬q ∧ ¬r) ∧ (q --> ¬p ∧ ¬r) ∧ (r --> ¬p ∧ ¬q)"
    by (unfold Exactly_1_of_3_holds_def);
  then have "p∨q∨r" by blast;
  with A1 show "q∨r" by simp;
qed;

text{*If exactly one of $p,q,r$ holds and $q$ is true, then 
  $r$ can not be true.*}

lemma Fol1_L7:
  assumes A1: "q" and A2: "Exactly_1_of_3_holds (p,q,r)"
  shows "¬r"
proof -
   from A2 have  
    "(p∨q∨r) ∧ (p --> ¬q ∧ ¬r) ∧ (q --> ¬p ∧ ¬r) ∧ (r --> ¬p ∧ ¬q)"
    by (unfold Exactly_1_of_3_holds_def)
  with A1 show "¬r" by blast;
qed;

text{* The next lemma demonstrates an elegant form of the 
  @{text "Exactly_1_of_3_holds (p,q,r)"} predicate. More on that
  at www.solcon.nl/mklooster/calc/calc-tri.html . *}

lemma Fol1_L8: 
  shows "Exactly_1_of_3_holds (p,q,r) <-> (p<->q<->r) ∧ ¬(p∧q∧r)"
proof;
  assume "Exactly_1_of_3_holds (p,q,r)"
  then have 
    "(p∨q∨r) ∧ (p --> ¬q ∧ ¬r) ∧ (q --> ¬p ∧ ¬r) ∧ (r --> ¬p ∧ ¬q)"
    by (unfold Exactly_1_of_3_holds_def);
  thus "(p<->q<->r) ∧ ¬(p∧q∧r)" by blast;
next assume "(p<->q<->r) ∧ ¬(p∧q∧r)" 
  then have 
    "(p∨q∨r) ∧ (p --> ¬q ∧ ¬r) ∧ (q --> ¬p ∧ ¬r) ∧ (r --> ¬p ∧ ¬q)"
    by auto;
  thus "Exactly_1_of_3_holds (p,q,r)"
    using Exactly_1_of_3_holds_def by (unfold Exactly_1_of_3_holds_def);
qed;

text{*A property of the @{text "Exactly_1_of_3_holds"} predicate.*}

lemma Fol1_L8A: assumes A1: "Exactly_1_of_3_holds (p,q,r)"
  shows "p <-> ¬(q ∨ r)"
proof -
  from A1 have "(p∨q∨r) ∧ (p --> ¬q ∧ ¬r) ∧ (q --> ¬p ∧ ¬r) ∧ (r --> ¬p ∧ ¬q)"
    by (unfold Exactly_1_of_3_holds_def)
  then show "p <-> ¬(q ∨ r)" by blast;
qed;

text{*Exclusive or definition. There is one also defined in the standard 
  Isabelle, denoted @{text "xor"}, but it relates to boolean values, 
  which are sets. Here we define a logical functor.*}

constdefs
  Xor (infixl "Xor" 66)
  "p Xor q ≡ (p∨q) ∧ ¬(p ∧ q)"

text{*The "exclusive or" is the same as negation of equivalence.*}

lemma Fol1_L9: shows "p Xor q <-> ¬(p<->q)"
  using Xor_def by auto;

(*
text{*This is an example how we can show a statement of the form 
  @{text "p Xor q"}.*}

lemma Fol1_L6: assumes "p∨q" and "¬p ∨ ¬q"
  shows "p Xor q"
proof -
  from prems show "p Xor q" using Xor_def by simp;
qed;*)

text{*Equivalence relations are symmetric.*}

lemma equiv_is_sym: assumes A1:  "equiv(X,r)" and A2: "⟨x,y⟩ ∈ r"
  shows  "⟨y,x⟩ ∈ r"
proof -
  from A1 have "sym(r)" using equiv_def by simp;
  then have "∀x y. ⟨x,y⟩ ∈ r --> ⟨y,x⟩ ∈ r"
    by (unfold sym_def);
  with A2 show "⟨y,x⟩ ∈ r" by blast;
qed;

text{*This lemma is needed to be used as a rule in some very 
  complicated cases.*}

lemma five_more_conj: assumes "Axs"  "Ax1" "Ax2" "Ax3" "Ax4" "Ax5"
  shows "Ax1 ∧ Ax2 ∧ Ax3 ∧ Ax4 ∧ Ax5 ∧ Axs" using prems by simp;

(* In Isabelle/ZF conjunction associates to the right!.
lemma test: assumes A1: "P" "Q∧R"
  shows "P∧Q∧R"
proof - 
  from A1 show "P∧Q∧R" by (rule one_more_conj);
qed;

*)

  
    

end