Theory MMI_prelude

(* 
    This file is a part of MMIsar - a translation of Metamath's set.mm to Isabelle 2005 (ZF logic).

    Copyright (C) 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{MMI\_prelude.thy}*} 

theory MMI_prelude imports equalities

begin

text{*In this theory file we define the context in which theorems
  imported from Metamath are proven and prove the logic and set theory
  Metamath lemmas that the proofs of Metamath theorems about 
  real and complex numbers depend on.*}

section{*Importing from Metamath - how is it done*}

(* Metamath's set.mm features a large (over 8000) collection of theorems 
  proven in the ZFC set theory. We aim at making this collection available
  for Isabelle's ZF logic users.*)

text{* 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 distribution.
  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 stataments
  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 @{text "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 @{text "MMI_logis_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.*}

section{*The context for Metamath theorems*}

text{*We list the Metamth's axioms of complex numbers
  and define notation here.*}

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

consts
   IsASet :: "i=>o" ("_ isASet" [90] 90)

defs
  set_def [simp]: "X isASet ≡  X = X"

text{*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 @{text "f`⟨a,b⟩"} with a possibility of 
  defining a syntax say @{text "a \<ca> b"} to mean the same as @{text "f`⟨a,b⟩"} 
  (please correct me if I am wrong here). This is why we have
  two objects for addition: one called @{text "caddset"} that represents
  the binary function, and the second one called @{text "ca"} which 
  defines the @{text "a \<ca> b"} notation for @{text "caddset`⟨a,b⟩"}.
  The same applies to multiplication of real numbers.*}

locale MMIsar0 =
  fixes real ("\<real>")
  fixes complex ("\<complex>")
  fixes one :: i ("\<one>")
  fixes zero :: i ("\<zero>")
  fixes iunit :: i ("\<i>")
  fixes caddset ("\<caddset>")
  fixes cmulset ("\<cmulset>")
  fixes lessrrel ("\<lsrset>")

  fixes ca (infixl "\<ca>" 69)
  defines ca_def: "a \<ca> b ≡ \<caddset>`⟨a,b⟩"
  fixes cm (infixl "·" 71)
  defines cm_def: "a · b ≡ \<cmulset>`⟨a,b⟩"
  fixes sub (infixl "\<cs>" 69)
  defines sub_def: "a \<cs> b ≡ \<Union> { x ∈ \<complex>. b \<ca> x = a }"
  fixes cneg :: "i=>i" ("\<cn>_" 95)
  defines cneg_def: "\<cn> a ≡ \<zero> \<cs> a"
  fixes cdiv (infixl "\<cdiv>" 70)
  defines cdiv_def: "a \<cdiv> b ≡ \<Union> { x ∈ \<complex>. b · x = a }"
  fixes cpnf ("\<cpnf>")
  defines cpnf_def: "\<cpnf> ≡ \<complex>"
  fixes cmnf ("\<cmnf>")
  defines cmnf_def: "\<cmnf> ≡ {\<complex>}"
  fixes cxr ("\<real>*")
  defines cxr_def: "\<real>* ≡ \<real> ∪ {\<cpnf>,\<cmnf>}"
  fixes lessr (infix "\<lsr>" 68)
  defines lessr_def: "a \<lsr> b ≡ ⟨a,b⟩ ∈ \<lsrset>"
  fixes cltrrset ("\<cltrrset>")
  defines cltrrset_def: 
  "\<cltrrset> ≡ (\<lsrset> ∩ \<real>×\<real>) ∪ {⟨\<cmnf>,\<cpnf>⟩} ∪ 
  (\<real>×{\<cpnf>}) ∪ ({\<cmnf>}×\<real> )"
  fixes cltrr (infix "\<ls>" 68)
  defines cltrr_def: "a \<ls> b ≡ ⟨a,b⟩ ∈ \<cltrrset>"
  fixes lsq (infix "\<lsq>" 68)
  defines lsq_def: "a \<lsq> b ≡ ¬ (b \<ls> a)"

  assumes MMI_pre_axlttri: 
  "A ∈ \<real> ∧ B ∈ \<real> --> (A \<lsr> B <-> ¬(A=B ∨ B \<lsr> A))"
  assumes MMI_pre_axlttrn: 
  "A ∈ \<real> ∧ B ∈ \<real> ∧ C ∈ \<real> --> ((A \<lsr> B ∧ B \<lsr> C) --> A \<lsr> C)"
  assumes MMI_pre_axltadd:
  "A ∈ \<real> ∧ B ∈ \<real> ∧ C ∈ \<real> --> (A \<lsr> B --> C\<ca>A \<lsr> C\<ca>B)"
  assumes MMI_pre_axmulgt0:
  "A ∈ \<real> ∧ B ∈ \<real> --> ( \<zero> \<lsr> A ∧ \<zero> \<lsr> B --> \<zero> \<lsr> A·B)"
  assumes MMI_pre_axsup:
  "A ⊆ \<real> ∧ A ≠ 0 ∧ (∃x∈\<real>. ∀y∈A. y \<lsr> x) -->
  (∃x∈\<real>. (∀y∈A. ¬(x \<lsr> y)) ∧ (∀y∈\<real>. (y \<lsr> x --> (∃z∈A. y \<lsr> z))))"
  assumes MMI_axresscn: "\<real> ⊆ \<complex>"
  assumes MMI_ax1ne0: "\<one> ≠ \<zero>"
  assumes MMI_axcnex: "\<complex> isASet"
  assumes MMI_axaddopr: "\<caddset> : ( \<complex> × \<complex> ) -> \<complex>"
  assumes MMI_axmulopr: "\<cmulset> : ( \<complex> × \<complex> ) -> \<complex>"
  assumes MMI_axmulcom: "A ∈ \<complex> ∧ B ∈ \<complex> --> A · B = B · A"
  assumes MMI_axaddcl: "A ∈ \<complex> ∧ B ∈ \<complex> --> A \<ca> B ∈ \<complex>"
  assumes MMI_axmulcl: "A ∈ \<complex> ∧ B ∈ \<complex> --> A · B ∈ \<complex>"
  assumes MMI_axdistr: 
  "A ∈ \<complex> ∧ B ∈ \<complex> ∧ C ∈ \<complex> --> A·(B \<ca> C) = A·B \<ca> A·C" 
  assumes MMI_axaddcom: "A ∈ \<complex> ∧ B ∈ \<complex> --> A \<ca> B = B \<ca> A"
  assumes MMI_axaddass: 
  "A ∈ \<complex> ∧ B ∈ \<complex> ∧ C ∈ \<complex> --> A \<ca> B \<ca> C = A \<ca> (B \<ca> C)"
  assumes MMI_axmulass: 
  "A ∈ \<complex> ∧ B ∈ \<complex> ∧ C ∈ \<complex> --> A · B · C = A · (B · C)"
  assumes MMI_ax1re: "\<one> ∈ \<real>"
  assumes MMI_axi2m1: "\<i> · \<i> \<ca> \<one> = \<zero>"
  assumes MMI_ax0id: "A ∈ \<complex> --> A \<ca> \<zero> = A"
  assumes MMI_axicn: "\<i> ∈ \<complex>"
  assumes MMI_axnegex: "A ∈ \<complex> --> ( ∃ x ∈ \<complex>. ( A \<ca> x ) = \<zero> )"
  assumes MMI_axrecex: "A ∈ \<complex> ∧ A ≠ \<zero> --> ( ∃ x ∈ \<complex>. A · x = \<one>)"
  assumes MMI_ax1id: "A ∈ \<complex> --> A · \<one> = A"
  assumes MMI_axaddrcl: "A ∈ \<real> ∧ B ∈ \<real> --> A \<ca> B ∈ \<real>"
  assumes MMI_axmulrcl: "A ∈ \<real> ∧ B ∈ \<real> --> A · B ∈ \<real>"
  assumes MMI_axrnegex: "A ∈ \<real> --> ( ∃ x ∈ \<real>. A \<ca> x = \<zero> )"
  assumes MMI_axrrecex: "A ∈ \<real> ∧ A ≠ \<zero> --> ( ∃ x ∈ \<real>. A · x = \<one> )"
  

constdefs
  StrictOrder (infix "Orders" 65)
  "R Orders A ≡ ∀x y z. (x∈A ∧ y∈A ∧ z∈A) --> 
  (⟨x,y⟩ ∈ R <-> ¬(x=y ∨ ⟨y,x⟩ ∈ R)) ∧ (⟨x,y⟩ ∈ R ∧ ⟨y,z⟩ ∈ R --> ⟨x,z⟩ ∈ R)";


end