Theory Complex_ZF

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

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{Complex\_ZF.thy}*}

theory Complex_ZF imports func_ZF_1 OrderedField_ZF

begin

text{*The goal of this theory is to define complex numbers
and prove that the Metamath complex numbers axioms hold.*}


section{*From complete ordered fields to complex numbers*}

text{*This section consists mostly of definitions and a proof
context for talking about complex numbers.
Suppose we have a set $R$ with binary operations $A$ and
$M$ and a relation $r$ such that the quadruple $(R,A,M,r)$
forms a complete ordered field.
The next definitions take $(R,A,M,r)$ and
construct the sets that represent the structure of complex numbers:
the carrier ($\mathbb{C}=R\times R$), binary operations of
addition and multiplication of complex numbers and the order
relation on $\mathbb{R}=R\times 0$.
The @{text "ImCxAdd, ReCxAdd, ImCxMul, ReCxMul"} are helper
meta-functions representing the imaginary part of a sum of
complex numbers, the real part of a sum of real numbers, the
imaginary part of a product of
complex numbers and the real part of a product of real numbers,
respectively. The actual operations (subsets of $(R\times R)\times R$
are named @{text "CplxAdd"} and @{text "CplxMul"}.

When $R$ is an ordered field, it comes with an order relation.
This induces a natural strict order relation on
$\{\langle x,0\rangle : x\in R\}\subseteq R\times R$. We call the
set $\{\langle x,0\rangle : x\in R\}$ @{text "ComplexReals(R,A)"}
and the strict order relation @{text "CplxROrder(R,A,r)"}.
The order on the real axis of complex numbers is defined
as the relation induced on it by the
canonical projection on the first coordinate and the order
we have on the real numbers.
OK, lets repeat this slower.
We start with the order relation $r$ on a (model of) real numbers $R$.
We want to define an order relation on a subset of complex
numbers, namely on $R\times \{0\}$. To do that we use the notion of
a relation induced by a mapping. The mapping here is
$f:R\times \{0\}\rightarrow R, f\langle x,0 \rangle = x$
which is defined under a name of
@{text "SliceProjection"} in @{text "func_ZF.thy"}.
This defines a relation $r_1$ (called @{text "InducedRelation(f,r)"},
see @{text "func_ZF"}) on $R\times \{0\}$ such that
$ \langle \langle x, 0\rangle, \langle y,0\rangle
\in r_1$ iff $\langle x,y\rangle \in r$. This way we get what we call
@{text "CplxROrder(R,A,r)"}. However, this is not the
end of the story, because Metamath uses strict inequalities in its axioms,
rather than weak ones like IsarMathLib (mostly). So we need to take
the strict version of this order relation. This is done in
the syntax definition of @{text "\<lsr>"} in the definition of
@{text "complex0"} context. Since Metamath proves a lot of theorems
about the real numbers extended with $+\infty$ and $-\infty$, we define
the notation for inequalites on the extended real line as well.
*}


text{*A helper expression representing the real part
of the sum of two complex numbers.*}


definition
"ReCxAdd(R,A,a,b) ≡ A`⟨fst(a),fst(b)⟩"

text{*An expression representing the imaginary part of the sum
of two complex numbers.*}


definition
"ImCxAdd(R,A,a,b) ≡ A`⟨snd(a),snd(b)⟩"

text{*The set (function) that is the binary operation that adds complex numbers.*}

definition
"CplxAdd(R,A) ≡
{⟨p, ⟨ ReCxAdd(R,A,fst(p),snd(p)),ImCxAdd(R,A,fst(p),snd(p)) ⟩ ⟩.
p∈(R×R)×(R×R)}"


text{*The expression representing the imaginary part of the
product of complex numbers.*}


definition
"ImCxMul(R,A,M,a,b) ≡ A`⟨M`⟨fst(a),snd(b)⟩, M`⟨snd(a),fst(b)⟩ ⟩"

text{*The expression representing the real part of the
product of complex numbers.*}


definition
"ReCxMul(R,A,M,a,b) ≡
A`⟨M`⟨fst(a),fst(b)⟩,GroupInv(R,A)`(M`⟨snd(a),snd(b)⟩)⟩"


text{*The function (set) that represents the binary operation of
multiplication of complex numbers.*}


definition
"CplxMul(R,A,M) ≡
{ ⟨p, ⟨ReCxMul(R,A,M,fst(p),snd(p)),ImCxMul(R,A,M,fst(p),snd(p))⟩ ⟩.
p ∈ (R×R)×(R×R)}"


text{*The definition real numbers embedded in the complex plane.*}

definition
"ComplexReals(R,A) ≡ R×{TheNeutralElement(R,A)}"

text{*Definition of order relation on the real line.*}

definition
"CplxROrder(R,A,r) ≡
InducedRelation(SliceProjection(ComplexReals(R,A)),r)"


text{*The next locale defines proof context and notation that will be
used for complex numbers.*}


locale complex0 =
fixes R and A and M and r
assumes R_are_reals: "IsAmodelOfReals(R,A,M,r)"

fixes complex ("\<complex>")
defines complex_def[simp]: "\<complex> ≡ R×R"

fixes rone ("\<one>R")
defines rone_def[simp]: "\<one>R ≡ TheNeutralElement(R,M)"

fixes rzero ("\<zero>R")
defines rzero_def[simp]: "\<zero>R ≡ TheNeutralElement(R,A)"

fixes one ("\<one>")
defines one_def[simp]: "\<one> ≡ ⟨\<one>R, \<zero>R⟩"

fixes zero ("\<zero>")
defines zero_def[simp]: "\<zero> ≡ ⟨\<zero>R, \<zero>R⟩"

fixes iunit ("\<i>")
defines iunit_def[simp]: "\<i> ≡ ⟨\<zero>R,\<one>R⟩"

fixes creal ("\<real>")
defines creal_def[simp]: "\<real> ≡ {⟨r,\<zero>R⟩. r∈R}"

fixes rmul (infixl "\<rmu>" 71)
defines rmul_def[simp]: "a \<rmu> b ≡ M`⟨a,b⟩"

fixes radd (infixl "\<ra>" 69)
defines radd_def[simp]: "a \<ra> b ≡ A`⟨a,b⟩"

fixes rneg ("\<rm> _" 70)
defines rneg_def[simp]: "\<rm> a ≡ GroupInv(R,A)`(a)"

fixes ca (infixl "\<ca>" 69)
defines ca_def[simp]: "a \<ca> b ≡ CplxAdd(R,A)`⟨a,b⟩"

fixes cm (infixl "·" 71)
defines cm_def[simp]: "a · b ≡ CplxMul(R,A,M)`⟨a,b⟩"

fixes cdiv (infixl "\<cdiv>" 70)
defines cdiv_def[simp]: "a \<cdiv> b ≡ \<Union> { x ∈ \<complex>. b · x = a }"

fixes sub (infixl "\<cs>" 69)
defines sub_def[simp]: "a \<cs> b ≡ \<Union> { x ∈ \<complex>. b \<ca> x = a }"

fixes cneg ("\<cn>_" 95)
defines cneg_def[simp]: "\<cn> a ≡ \<zero> \<cs> a"

fixes lessr (infix "\<lsr>" 68)
defines lessr_def[simp]:
"a \<lsr> b ≡ ⟨a,b⟩ ∈ StrictVersion(CplxROrder(R,A,r))"

fixes cpnf ("\<cpnf>")
defines cpnf_def[simp]: "\<cpnf> ≡ \<complex>"

fixes cmnf ("\<cmnf>")
defines cmnf_def[simp]: "\<cmnf> ≡ {\<complex>}"

fixes cxr ("\<real>*")
defines cxr_def[simp]: "\<real>* ≡ \<real> ∪ {\<cpnf>,\<cmnf>}"

fixes cxn ("\<nat>")
defines cxn_def[simp]:
"\<nat> ≡ \<Inter> {N ∈ Pow(\<real>). \<one> ∈ N ∧ (∀n. n∈N --> n\<ca>\<one> ∈ N)}"

fixes cltrrset ("\<cltrrset>")
defines cltrrset_def[simp]:
"\<cltrrset> ≡ StrictVersion(CplxROrder(R,A,r)) ∩ \<real>×\<real> ∪
{⟨\<cmnf>,\<cpnf>⟩} ∪ (\<real>×{\<cpnf>}) ∪ ({\<cmnf>}×\<real> )"


fixes cltrr (infix "\<ls>" 68)
defines cltrr_def[simp]: "a \<ls> b ≡ ⟨a,b⟩ ∈ \<cltrrset>"

fixes lsq (infix "\<lsq>" 68)
defines lsq_def[simp]: "a \<lsq> b ≡ ¬ (b \<ls> a)"

fixes two ("\<two>")
defines two_def[simp]: "\<two> ≡ \<one> \<ca> \<one>"

fixes three ("\<three>")
defines three_def[simp]: "\<three> ≡ \<two>\<ca>\<one>"

fixes four ("\<four>")
defines four_def[simp]: "\<four> ≡ \<three>\<ca>\<one>"

fixes five ("\<five>")
defines five_def[simp]: "\<five> ≡ \<four>\<ca>\<one>"

fixes six ("\<six>")
defines six_def[simp]: "\<six> ≡ \<five>\<ca>\<one>"

fixes seven ("\<seven>")
defines seven_def[simp]: "\<seven> ≡ \<six>\<ca>\<one>"

fixes eight ("\<eight>")
defines eight_def[simp]: "\<eight> ≡ \<seven>\<ca>\<one>"

fixes nine ("\<nine>")
defines nine_def[simp]: "\<nine> ≡ \<eight>\<ca>\<one>";

section{*Axioms of complex numbers*}

text{*In this section we will prove that all Metamath's axioms of complex
numbers hold in the @{text "complex0"} context.*}


text{*The next lemma lists some contexts that are valid in the @{text "complex0"}
context.*}


lemma (in complex0) valid_cntxts: shows
"field1(R,A,M,r)"
"field0(R,A,M)"
"ring1(R,A,M,r)"
"group3(R,A,r)"
"ring0(R,A,M)"
"M {is commutative on} R"
"group0(R,A)"
proof -
from R_are_reals have I: "IsAnOrdField(R,A,M,r)"
using IsAmodelOfReals_def by simp;
then show "field1(R,A,M,r)" using OrdField_ZF_1_L2 by simp;
then show "ring1(R,A,M,r)" and I: "field0(R,A,M)"
using field1.axioms ring1_def field1.OrdField_ZF_1_L1B
by auto;
then show "group3(R,A,r)" using ring1.OrdRing_ZF_1_L4
by simp;
from I have "IsAfield(R,A,M)" using field0.Field_ZF_1_L1
by simp;
then have "IsAring(R,A,M)" and "M {is commutative on} R"
using IsAfield_def by auto;
then show "ring0(R,A,M)" and "M {is commutative on} R"
using ring0_def by auto
then show "group0(R,A)" using ring0.Ring_ZF_1_L1
by simp;
qed;

text{*The next lemma shows the definition of real and imaginary part of
complex sum and product in a more readable form using notation defined
in @{text "complex0"} locale.*}


lemma (in complex0) cplx_mul_add_defs: shows
"ReCxAdd(R,A,⟨a,b⟩,⟨c,d⟩) = a \<ra> c"
"ImCxAdd(R,A,⟨a,b⟩,⟨c,d⟩) = b \<ra> d"
"ImCxMul(R,A,M,⟨a,b⟩,⟨c,d⟩) = a\<rmu>d \<ra> b\<rmu>c"
"ReCxMul(R,A,M,⟨a,b⟩,⟨c,d⟩) = a\<rmu>c \<ra> (\<rm>b\<rmu>d)"
proof -
let ?z1 = "⟨a,b⟩"
let ?z2 = "⟨c,d⟩"
have "ReCxAdd(R,A,?z1,?z2) ≡ A`⟨fst(?z1),fst(?z2)⟩"
by (rule ReCxAdd_def);
moreover have "ImCxAdd(R,A,?z1,?z2) ≡ A`⟨snd(?z1),snd(?z2)⟩"
by (rule ImCxAdd_def);
moreover have
"ImCxMul(R,A,M,?z1,?z2) ≡ A`⟨M`<fst(?z1),snd(?z2)>,M`<snd(?z1),fst(?z2)>⟩"
by (rule ImCxMul_def);
moreover have
"ReCxMul(R,A,M,?z1,?z2) ≡
A`⟨M`<fst(?z1),fst(?z2)>,GroupInv(R,A)`(M`⟨snd(?z1),snd(?z2)⟩)⟩"

by (rule ReCxMul_def);
ultimately show
"ReCxAdd(R,A,?z1,?z2) = a \<ra> c"
"ImCxAdd(R,A,⟨a,b⟩,⟨c,d⟩) = b \<ra> d"
"ImCxMul(R,A,M,⟨a,b⟩,⟨c,d⟩) = a\<rmu>d \<ra> b\<rmu>c"
"ReCxMul(R,A,M,⟨a,b⟩,⟨c,d⟩) = a\<rmu>c \<ra> (\<rm>b\<rmu>d)"
by auto;
qed;

text{*Real and imaginary parts of sums and products of complex numbers
are real.*}


lemma (in complex0) cplx_mul_add_types:
assumes A1: "z1 ∈ \<complex>" "z2 ∈ \<complex>"
shows
"ReCxAdd(R,A,z1,z2) ∈ R"
"ImCxAdd(R,A,z1,z2) ∈ R"
"ImCxMul(R,A,M,z1,z2) ∈ R"
"ReCxMul(R,A,M,z1,z2) ∈ R"
proof -
let ?a = "fst(z1)"
let ?b = "snd(z1)"
let ?c = "fst(z2)"
let ?d = "snd(z2)"
from A1 have "?a ∈ R" "?b ∈ R" "?c ∈ R" "?d ∈ R"
by auto;
then have
"?a \<ra> ?c ∈ R"
"?b \<ra> ?d ∈ R"
"?a\<rmu>?d \<ra> ?b\<rmu>?c ∈ R"
"?a\<rmu>?c \<ra> (\<rm> ?b\<rmu>?d) ∈ R"
using valid_cntxts ring0.Ring_ZF_1_L4 by auto;
with A1 show
"ReCxAdd(R,A,z1,z2) ∈ R"
"ImCxAdd(R,A,z1,z2) ∈ R"
"ImCxMul(R,A,M,z1,z2) ∈ R"
"ReCxMul(R,A,M,z1,z2) ∈ R"
using cplx_mul_add_defs by auto;
qed;

text{*Complex reals are complex. Recall the definition of @{text "\<real>"}
in the @{text "complex0"} locale.*}


lemma (in complex0) axresscn: shows "\<real> ⊆ \<complex>"
using valid_cntxts group0.group0_2_L2 by auto

text{*Complex $1$ is not complex $0$.*}

lemma (in complex0) ax1ne0: shows "\<one> ≠ \<zero>"
proof -
have "IsAfield(R,A,M)" using valid_cntxts field0.Field_ZF_1_L1
by simp;
then show "\<one> ≠ \<zero>" using IsAfield_def by auto;
qed;

text{*Complex addition is a complex valued binary
operation on complex numbers.*}


lemma (in complex0) axaddopr: shows "CplxAdd(R,A): \<complex> × \<complex> -> \<complex>"
proof -;
have "∀p ∈ \<complex>×\<complex>.
⟨ReCxAdd(R,A,fst(p),snd(p)),ImCxAdd(R,A,fst(p),snd(p))⟩ ∈ \<complex>"

using cplx_mul_add_types by simp;
then have
"{⟨p,⟨ReCxAdd(R,A,fst(p),snd(p)),ImCxAdd(R,A,fst(p),snd(p))⟩ ⟩.
p ∈ \<complex>×\<complex>}: \<complex>×\<complex> -> \<complex>"

by (rule ZF_fun_from_total);
then show "CplxAdd(R,A): \<complex> × \<complex> -> \<complex>" using CplxAdd_def by simp;
qed;

text{*Complex multiplication is a complex valued binary
operation on complex numbers.*}


lemma (in complex0) axmulopr: shows "CplxMul(R,A,M): \<complex> × \<complex> -> \<complex>"
proof -
have "∀p ∈ \<complex>×\<complex>.
⟨ReCxMul(R,A,M,fst(p),snd(p)),ImCxMul(R,A,M,fst(p),snd(p))⟩ ∈ \<complex>"

using cplx_mul_add_types by simp;
then have
"{⟨p,⟨ReCxMul(R,A,M,fst(p),snd(p)),ImCxMul(R,A,M,fst(p),snd(p))⟩⟩.
p ∈ \<complex>×\<complex>}: \<complex>×\<complex> -> \<complex>"
by (rule ZF_fun_from_total);
then show "CplxMul(R,A,M): \<complex> × \<complex> -> \<complex>" using CplxMul_def by simp;
qed;

text{*What are the values of omplex addition and multiplication
in terms of their real and imaginary parts?*}


lemma (in complex0) cplx_mul_add_vals:
assumes A1: "a∈R" "b∈R" "c∈R" "d∈R"
shows
"⟨a,b⟩ \<ca> ⟨c,d⟩ = ⟨a \<ra> c, b \<ra> d⟩"
"⟨a,b⟩ · ⟨c,d⟩ = ⟨a\<rmu>c \<ra> (\<rm>b\<rmu>d), a\<rmu>d \<ra> b\<rmu>c⟩"
proof -
let ?S = "CplxAdd(R,A)"
let ?P = "CplxMul(R,A,M)"
let ?p = "⟨ ⟨a,b⟩, ⟨c,d⟩ ⟩"
from A1 have "?S : \<complex> × \<complex> -> \<complex>" and "?p ∈ \<complex> × \<complex>"
using axaddopr by auto;
moreover have
"?S = {⟨p, <ReCxAdd(R,A,fst(p),snd(p)),ImCxAdd(R,A,fst(p),snd(p))>⟩.
p ∈ \<complex> × \<complex>}"

using CplxAdd_def by simp;
ultimately have "?S`(?p) = ⟨ReCxAdd(R,A,fst(?p),snd(?p)),ImCxAdd(R,A,fst(?p),snd(?p))⟩"
by (rule ZF_fun_from_tot_val);
then show "⟨a,b⟩ \<ca> ⟨c,d⟩ = ⟨a \<ra> c, b \<ra> d⟩"
using cplx_mul_add_defs by simp;
from A1 have "?P : \<complex> × \<complex> -> \<complex>" and "?p ∈ \<complex> × \<complex>"
using axmulopr by auto;
moreover have
"?P = {⟨p, ⟨ReCxMul(R,A,M,fst(p),snd(p)),ImCxMul(R,A,M,fst(p),snd(p))⟩ ⟩.
p ∈ \<complex> × \<complex>}"

using CplxMul_def by simp;
ultimately have
"?P`(?p) = ⟨ReCxMul(R,A,M,fst(?p),snd(?p)),ImCxMul(R,A,M,fst(?p),snd(?p))⟩"
by (rule ZF_fun_from_tot_val);
then show "⟨a,b⟩ · ⟨c,d⟩ = ⟨a\<rmu>c \<ra> (\<rm>b\<rmu>d), a\<rmu>d \<ra> b\<rmu>c⟩"
using cplx_mul_add_defs by simp;
qed;

text{*Complex multiplication is commutative.*}

lemma (in complex0) axmulcom: assumes A1: "a ∈ \<complex>" "b ∈ \<complex>"
shows "a·b = b·a"
using assms cplx_mul_add_vals valid_cntxts ring0.Ring_ZF_1_L4
field0.field_mult_comm by auto;

text{*A sum of complex numbers is complex.*}

lemma (in complex0) axaddcl: assumes "a ∈ \<complex>" "b ∈ \<complex>"
shows "a\<ca>b ∈ \<complex>"
using assms axaddopr apply_funtype by simp;

text{*A product of complex numbers is complex.*}

lemma (in complex0) axmulcl: assumes "a ∈ \<complex>" "b ∈ \<complex>"
shows "a·b ∈ \<complex>"
using assms axmulopr apply_funtype by simp;

text{*Multiplication is distributive with respect to
addition.*}


lemma (in complex0) axdistr:
assumes A1: "a ∈ \<complex>" "b ∈ \<complex>" "c ∈ \<complex>"
shows "a·(b \<ca> c) = a·b \<ca> a·c"
proof -
let ?ar = "fst(a)"
let ?ai = "snd(a)"
let ?br = "fst(b)"
let ?bi = "snd(b)"
let ?cr = "fst(c)"
let ?ci = "snd(c)"
from A1 have T:
"?ar ∈ R" "?ai ∈ R" "?br ∈ R" "?bi ∈ R" "?cr ∈ R" "?ci ∈ R"
"?br\<ra>?cr ∈ R" "?bi\<ra>?ci ∈ R"
"?ar\<rmu>?br \<ra> (\<rm>?ai\<rmu>?bi) ∈ R"
"?ar\<rmu>?cr \<ra> (\<rm>?ai\<rmu>?ci) ∈ R"
"?ar\<rmu>?bi \<ra> ?ai\<rmu>?br ∈ R"
"?ar\<rmu>?ci \<ra> ?ai\<rmu>?cr ∈ R"
using valid_cntxts ring0.Ring_ZF_1_L4 by auto;
with A1 have "a·(b \<ca> c) =
⟨?ar\<rmu>(?br\<ra>?cr) \<ra> (\<rm>?ai\<rmu>(?bi\<ra>?ci)),?ar\<rmu>(?bi\<ra>?ci) \<ra> ?ai\<rmu>(?br\<ra>?cr)⟩"

using cplx_mul_add_vals by auto;
moreover from T have
"?ar\<rmu>(?br\<ra>?cr) \<ra> (\<rm>?ai\<rmu>(?bi\<ra>?ci)) =
?ar\<rmu>?br \<ra> (\<rm>?ai\<rmu>?bi) \<ra> (?ar\<rmu>?cr \<ra> (\<rm>?ai\<rmu>?ci))"

and
"?ar\<rmu>(?bi\<ra>?ci) \<ra> ?ai\<rmu>(?br\<ra>?cr) =
?ar\<rmu>?bi \<ra> ?ai\<rmu>?br \<ra> (?ar\<rmu>?ci \<ra> ?ai\<rmu>?cr)"

using valid_cntxts ring0.Ring_ZF_2_L6 by auto;
moreover from A1 T have
"⟨?ar\<rmu>?br \<ra> (\<rm>?ai\<rmu>?bi) \<ra> (?ar\<rmu>?cr \<ra> (\<rm>?ai\<rmu>?ci)),
?ar\<rmu>?bi \<ra> ?ai\<rmu>?br \<ra> (?ar\<rmu>?ci \<ra> ?ai\<rmu>?cr)⟩ =
a·b \<ca> a·c"

using cplx_mul_add_vals by auto;
ultimately show "a·(b \<ca> c) = a·b \<ca> a·c"
by simp;
qed;

text{*Complex addition is commutative.*}

lemma (in complex0) axaddcom: assumes "a ∈ \<complex>" "b ∈ \<complex>"
shows "a\<ca>b = b\<ca>a"
using assms cplx_mul_add_vals valid_cntxts ring0.Ring_ZF_1_L4
by auto;

text{*Complex addition is associative.*}

lemma (in complex0) axaddass: assumes A1: "a ∈ \<complex>" "b ∈ \<complex>" "c ∈ \<complex>"
shows "a \<ca> b \<ca> c = a \<ca> (b \<ca> c)"
proof -
let ?ar = "fst(a)"
let ?ai = "snd(a)"
let ?br = "fst(b)"
let ?bi = "snd(b)"
let ?cr = "fst(c)"
let ?ci = "snd(c)"
from A1 have T:
"?ar ∈ R" "?ai ∈ R" "?br ∈ R" "?bi ∈ R" "?cr ∈ R" "?ci ∈ R"
"?ar\<ra>?br ∈ R" "?ai\<ra>?bi ∈ R"
"?br\<ra>?cr ∈ R" "?bi\<ra>?ci ∈ R"
using valid_cntxts ring0.Ring_ZF_1_L4 by auto;
with A1 have "a \<ca> b \<ca> c = ⟨?ar\<ra>?br\<ra>?cr,?ai\<ra>?bi\<ra>?ci⟩"
using cplx_mul_add_vals by auto;
also from A1 T have "… = a \<ca> (b \<ca> c)"
using valid_cntxts ring0.Ring_ZF_1_L11 cplx_mul_add_vals
by auto;
finally show "a \<ca> b \<ca> c = a \<ca> (b \<ca> c)"
by simp;
qed;

text{*Complex multiplication is associative.*}

lemma (in complex0) axmulass: assumes A1: "a ∈ \<complex>" "b ∈ \<complex>" "c ∈ \<complex>"
shows "a · b · c = a · (b · c)"
proof -
let ?ar = "fst(a)"
let ?ai = "snd(a)"
let ?br = "fst(b)"
let ?bi = "snd(b)"
let ?cr = "fst(c)"
let ?ci = "snd(c)"
from A1 have T:
"?ar ∈ R" "?ai ∈ R" "?br ∈ R" "?bi ∈ R" "?cr ∈ R" "?ci ∈ R"
"?ar\<rmu>?br \<ra> (\<rm>?ai\<rmu>?bi) ∈ R"
"?ar\<rmu>?bi \<ra> ?ai\<rmu>?br ∈ R"
"?br\<rmu>?cr \<ra> (\<rm>?bi\<rmu>?ci) ∈ R"
"?br\<rmu>?ci \<ra> ?bi\<rmu>?cr ∈ R"
using valid_cntxts ring0.Ring_ZF_1_L4 by auto;
with A1 have "a · b · c =
⟨(?ar\<rmu>?br \<ra> (\<rm>?ai\<rmu>?bi))\<rmu>?cr \<ra> (\<rm>(?ar\<rmu>?bi \<ra> ?ai\<rmu>?br)\<rmu>?ci),
(?ar\<rmu>?br \<ra> (\<rm>?ai\<rmu>?bi))\<rmu>?ci \<ra> (?ar\<rmu>?bi \<ra> ?ai\<rmu>?br)\<rmu>?cr⟩"

using cplx_mul_add_vals by auto;
moreover from A1 T have
"⟨?ar\<rmu>(?br\<rmu>?cr \<ra> (\<rm>?bi\<rmu>?ci)) \<ra> (\<rm>?ai\<rmu>(?br\<rmu>?ci \<ra> ?bi\<rmu>?cr)),
?ar\<rmu>(?br\<rmu>?ci \<ra> ?bi\<rmu>?cr) \<ra> ?ai\<rmu>(?br\<rmu>?cr \<ra> (\<rm>?bi\<rmu>?ci))⟩ =
a · (b · c)"

using cplx_mul_add_vals by auto;
moreover from T have
"?ar\<rmu>(?br\<rmu>?cr \<ra> (\<rm>?bi\<rmu>?ci)) \<ra> (\<rm>?ai\<rmu>(?br\<rmu>?ci \<ra> ?bi\<rmu>?cr)) =
(?ar\<rmu>?br \<ra> (\<rm>?ai\<rmu>?bi))\<rmu>?cr \<ra> (\<rm>(?ar\<rmu>?bi \<ra> ?ai\<rmu>?br)\<rmu>?ci)"

and
"?ar\<rmu>(?br\<rmu>?ci \<ra> ?bi\<rmu>?cr) \<ra> ?ai\<rmu>(?br\<rmu>?cr \<ra> (\<rm>?bi\<rmu>?ci)) =
(?ar\<rmu>?br \<ra> (\<rm>?ai\<rmu>?bi))\<rmu>?ci \<ra> (?ar\<rmu>?bi \<ra> ?ai\<rmu>?br)\<rmu>?cr"

using valid_cntxts ring0.Ring_ZF_2_L6 by auto;
ultimately show "a · b · c = a · (b · c)"
by auto;
qed;

text{*Complex $1$ is real. This really means that the pair
$\langle 1,0 \rangle$ is on the real axis.*}


lemma (in complex0) ax1re: shows "\<one> ∈ \<real>"
using valid_cntxts ring0.Ring_ZF_1_L2 by simp;

text{*The imaginary unit is a "square root" of $-1$ (that is, $i^2 +1 =0$).
*}


lemma (in complex0) axi2m1: shows "\<i>·\<i> \<ca> \<one> = \<zero>"
using valid_cntxts ring0.Ring_ZF_1_L2 ring0.Ring_ZF_1_L3
cplx_mul_add_vals ring0.Ring_ZF_1_L6 group0.group0_2_L6
by simp;

text{*$0$ is the neutral element of complex addition. *}

lemma (in complex0) ax0id: assumes "a ∈ \<complex>"
shows "a \<ca> \<zero> = a"
using assms cplx_mul_add_vals valid_cntxts
ring0.Ring_ZF_1_L2 ring0.Ring_ZF_1_L3
by auto;

text{*The imaginary unit is a complex number.*}

lemma (in complex0) axicn: shows "\<i> ∈ \<complex>"
using valid_cntxts ring0.Ring_ZF_1_L2 by auto;

text{*All complex numbers have additive inverses.*}

lemma (in complex0) axnegex: assumes A1: "a ∈ \<complex>"
shows "∃x∈\<complex>. a \<ca> x = \<zero>"
proof -
let ?ar = "fst(a)"
let ?ai = "snd(a)"
let ?x = "⟨\<rm>?ar, \<rm>?ai⟩"
from A1 have T:
"?ar ∈ R" "?ai ∈ R" "(\<rm>?ar) ∈ R" "(\<rm>?ar) ∈ R"
using valid_cntxts ring0.Ring_ZF_1_L3 by auto;
then have "?x ∈ \<complex>" using valid_cntxts ring0.Ring_ZF_1_L3
by auto;
moreover from A1 T have "a \<ca> ?x = \<zero>"
using cplx_mul_add_vals valid_cntxts ring0.Ring_ZF_1_L3
by auto;
ultimately show "∃x∈\<complex>. a \<ca> x = \<zero>"
by auto;
qed;

text{*A non-zero complex number has a multiplicative inverse.*}

lemma (in complex0) axrecex: assumes A1: "a ∈ \<complex>" and A2: "a≠\<zero>"
shows "∃x∈\<complex>. a·x = \<one>"
proof -
let ?ar = "fst(a)"
let ?ai = "snd(a)"
let ?m = "?ar\<rmu>?ar \<ra> ?ai\<rmu>?ai"
from A1 have T1: "?ar ∈ R" "?ai ∈ R" by auto
moreover from A1 A2 have "?ar ≠ \<zero>R ∨ ?ai ≠ \<zero>R"
by auto;
ultimately have "∃c∈R. ?m\<rmu>c = \<one>R"
using valid_cntxts field1.OrdField_ZF_1_L10
by auto;
then obtain c where I: "c∈R" and II: "?m\<rmu>c = \<one>R"
by auto;
let ?x = "⟨?ar\<rmu>c, \<rm>?ai\<rmu>c⟩";
from T1 I have T2: "?ar\<rmu>c ∈ R" "(\<rm>?ai\<rmu>c) ∈ R"
using valid_cntxts ring0.Ring_ZF_1_L4 ring0.Ring_ZF_1_L3
by auto;
then have "?x ∈ \<complex>" by auto;
moreover from A1 T1 T2 I II have "a·?x = \<one>"
using cplx_mul_add_vals valid_cntxts ring0.ring_rearr_3_elemA
by auto;
ultimately show "∃x∈\<complex>. a·x = \<one>" by auto;
qed;

text{*Complex $1$ is a right neutral element for multiplication.*}

lemma (in complex0) ax1id: assumes A1: "a ∈ \<complex>"
shows "a·\<one> = a"
using assms valid_cntxts ring0.Ring_ZF_1_L2 cplx_mul_add_vals
ring0.Ring_ZF_1_L3 ring0.Ring_ZF_1_L6 by auto;

text{*A formula for sum of (complex) real numbers.*}

lemma (in complex0) sum_of_reals: assumes "a∈\<real>" "b∈\<real>"
shows
"a \<ca> b = ⟨fst(a) \<ra> fst(b),\<zero>R⟩"
using assms valid_cntxts ring0.Ring_ZF_1_L2 cplx_mul_add_vals
ring0.Ring_ZF_1_L3 by auto;

text{*The sum of real numbers is real.*}

lemma (in complex0) axaddrcl: assumes A1: "a∈\<real>" "b∈\<real>"
shows "a \<ca> b ∈ \<real>"
using assms sum_of_reals valid_cntxts ring0.Ring_ZF_1_L4
by auto;

text{*The formula for the product of (complex) real numbers.*}

lemma (in complex0) prod_of_reals: assumes A1: "a∈\<real>" "b∈\<real>"
shows "a · b = ⟨fst(a)\<rmu>fst(b),\<zero>R⟩"
proof -
let ?ar = "fst(a)"
let ?br = "fst(b)"
from A1 have T:
"?ar ∈ R" "?br ∈ R" "\<zero>R ∈ R" "?ar\<rmu>?br ∈ R"
using valid_cntxts ring0.Ring_ZF_1_L2 ring0.Ring_ZF_1_L4
by auto;
with A1 show "a · b = ⟨?ar\<rmu>?br,\<zero>R⟩"
using cplx_mul_add_vals valid_cntxts ring0.Ring_ZF_1_L2
ring0.Ring_ZF_1_L6 ring0.Ring_ZF_1_L3 by auto;
qed;

text{*The product of (complex) real numbers is real.*}

lemma (in complex0) axmulrcl: assumes "a∈\<real>" "b∈\<real>"
shows "a · b ∈ \<real>"
using assms prod_of_reals valid_cntxts ring0.Ring_ZF_1_L4
by auto;

text{*The existence of a real negative of a real number.*}

lemma (in complex0) axrnegex: assumes A1: "a∈\<real>"
shows "∃ x ∈ \<real>. a \<ca> x = \<zero>"
proof -
let ?ar = "fst(a)"
let ?x = "⟨\<rm>?ar,\<zero>R⟩"
from A1 have T:
"?ar ∈ R" "(\<rm>?ar) ∈ R" "\<zero>R ∈ R"
using valid_cntxts ring0.Ring_ZF_1_L3 ring0.Ring_ZF_1_L2
by auto;
then have "?x∈ \<real>" by auto;
moreover from A1 T have "a \<ca> ?x = \<zero>"
using cplx_mul_add_vals valid_cntxts ring0.Ring_ZF_1_L3
by auto;
ultimately show "∃x∈\<real>. a \<ca> x = \<zero>" by auto;
qed;

text{*Each nonzero real number has a real inverse*}

lemma (in complex0) axrrecex:
assumes A1: "a ∈ \<real>" "a ≠ \<zero>"
shows "∃x∈\<real>. a · x = \<one>"
proof -
let ?R0 = "R-{\<zero>R}"
let ?ar = "fst(a)"
let ?y = "GroupInv(?R0,restrict(M,?R0×?R0))`(?ar)"
from A1 have T: "⟨?y,\<zero>R⟩ ∈ \<real>" using valid_cntxts field0.Field_ZF_1_L5
by auto;
moreover from A1 T have "a · ⟨?y,\<zero>R⟩ = \<one>"
using prod_of_reals valid_cntxts
field0.Field_ZF_1_L5 field0.Field_ZF_1_L6 by auto;
ultimately show "∃ x ∈ \<real>. a · x = \<one>" by auto;
qed;

text{*Our @{text "\<real>"} symbol is the real axis on the complex plane.*}

lemma (in complex0) real_means_real_axis: shows "\<real> = ComplexReals(R,A)"
using ComplexReals_def by auto;

text{*The @{text "CplxROrder"} thing is a relation on the complex reals.
*}


lemma (in complex0) cplx_ord_on_cplx_reals:
shows "CplxROrder(R,A,r) ⊆ \<real>×\<real>"
using ComplexReals_def slice_proj_bij real_means_real_axis
CplxROrder_def InducedRelation_def by auto;

text{*The strict version of the complex relation is a
relation on complex reals.*}


lemma (in complex0) cplx_strict_ord_on_cplx_reals:
shows "StrictVersion(CplxROrder(R,A,r)) ⊆ \<real>×\<real>"
using cplx_ord_on_cplx_reals strict_ver_rel by simp;

text{*The @{text "CplxROrder"} thing is a relation on the complex reals.
Here this is formulated as a statement that in @{text "complex0"} context
$a<b$ implies that $a,b$ are complex reals*}


lemma (in complex0) strict_cplx_ord_type: assumes "a \<lsr> b"
shows "a∈\<real>" "b∈\<real>"
using assms CplxROrder_def def_of_strict_ver InducedRelation_def
slice_proj_bij ComplexReals_def real_means_real_axis
by auto;

text{*A more readable version of the definition of the strict order
relation on the real axis. Recall that in the @{text "complex0"}
context $r$ denotes the (non-strict) order relation on the underlying
model of real numbers.*}


lemma (in complex0) def_of_real_axis_order: shows
"⟨x,\<zero>R⟩ \<lsr> ⟨y,\<zero>R⟩ <-> ⟨x,y⟩ ∈ r ∧ x≠y"
proof;
let ?f = "SliceProjection(ComplexReals(R,A))"
assume A1: "⟨x,\<zero>R⟩ \<lsr> ⟨y,\<zero>R⟩"
then have "⟨ ?f`⟨x,\<zero>R⟩, ?f`⟨y,\<zero>R⟩ ⟩ ∈ r ∧ x ≠ y"
using CplxROrder_def def_of_strict_ver def_of_ind_relA
by simp;
moreover from A1 have "⟨x,\<zero>R⟩ ∈ \<real>" "⟨y,\<zero>R⟩ ∈ \<real>"
using strict_cplx_ord_type by auto;
ultimately show "⟨x,y⟩ ∈ r ∧ x≠y"
using slice_proj_bij ComplexReals_def by simp;
next assume A1: "⟨x,y⟩ ∈ r ∧ x≠y"
let ?f = "SliceProjection(ComplexReals(R,A))"
have "?f : \<real> -> R"
using ComplexReals_def slice_proj_bij real_means_real_axis
by simp;
moreover from A1 have T: "⟨x,\<zero>R⟩ ∈ \<real>" "⟨y,\<zero>R⟩ ∈ \<real>"
using valid_cntxts ring1.OrdRing_ZF_1_L3 by auto;
moreover from A1 T have "⟨ ?f`⟨x,\<zero>R⟩, ?f`⟨y,\<zero>R⟩ ⟩ ∈ r"
using slice_proj_bij ComplexReals_def by simp;
ultimately have "⟨ ⟨x,\<zero>R⟩, ⟨y,\<zero>R⟩ ⟩ ∈ InducedRelation(?f,r)"
using def_of_ind_relB by simp;
with A1 show "⟨x,\<zero>R⟩ \<lsr> ⟨y,\<zero>R⟩"
using CplxROrder_def def_of_strict_ver
by simp;
qed;

text{*The (non strict) order on complex reals is antisymmetric,
transitive and total.*}


lemma (in complex0) cplx_ord_antsym_trans_tot: shows
"antisym(CplxROrder(R,A,r))"
"trans(CplxROrder(R,A,r))"
"CplxROrder(R,A,r) {is total on} \<real>"
proof -
let ?f = "SliceProjection(ComplexReals(R,A))"
have "?f ∈ ord_iso(\<real>,CplxROrder(R,A,r),R,r)"
using ComplexReals_def slice_proj_bij real_means_real_axis
bij_is_ord_iso CplxROrder_def by simp;
moreover have "CplxROrder(R,A,r) ⊆ \<real>×\<real>"
using cplx_ord_on_cplx_reals by simp;
moreover have I:
"antisym(r)" "r {is total on} R" "trans(r)"
using valid_cntxts ring1.OrdRing_ZF_1_L1 IsAnOrdRing_def
IsLinOrder_def by auto;
ultimately show
"antisym(CplxROrder(R,A,r))"
"trans(CplxROrder(R,A,r))"
"CplxROrder(R,A,r) {is total on} \<real>"
using ord_iso_pres_antsym ord_iso_pres_tot ord_iso_pres_trans
by auto;
qed;

text{*The trichotomy law for the strict order on the complex
reals.*}


lemma (in complex0) cplx_strict_ord_trich:
assumes "a ∈ \<real>" "b ∈ \<real>"
shows "Exactly_1_of_3_holds(a\<lsr>b, a=b, b\<lsr>a)"
using assms cplx_ord_antsym_trans_tot strict_ans_tot_trich
by simp;

text{*The strict order on the complex reals is kind of
antisymetric.*}


lemma (in complex0) pre_axlttri: assumes A1: "a ∈ \<real>" "b ∈ \<real>"
shows "a \<lsr> b <-> ¬(a=b ∨ b \<lsr> a)"
proof -
from A1 have "Exactly_1_of_3_holds(a\<lsr>b, a=b, b\<lsr>a)"
by (rule cplx_strict_ord_trich);
then show "a \<lsr> b <-> ¬(a=b ∨ b \<lsr> a)"
by (rule Fol1_L8A);
qed;

text{*The strict order on complex reals is transitive.*}

lemma (in complex0) cplx_strict_ord_trans:
shows "trans(StrictVersion(CplxROrder(R,A,r)))"
using cplx_ord_antsym_trans_tot strict_of_transB by simp;


text{*The strict order on complex reals is transitive - the explicit version
of @{text "cplx_strict_ord_trans"}.*}


lemma (in complex0) pre_axlttrn:
assumes A1: "a \<lsr> b" "b \<lsr> c"
shows "a \<lsr> c"
proof -
let ?s = "StrictVersion(CplxROrder(R,A,r))"
from A1 have
"trans(?s)" "⟨a,b⟩ ∈ ?s ∧ ⟨b,c⟩ ∈ ?s"
using cplx_strict_ord_trans by auto;
then have "⟨a,c⟩ ∈ ?s" by (rule Fol1_L3);
then show "a \<lsr> c" by simp;
qed;

text{*The strict order on complex reals is preserved by translations.*}

lemma (in complex0) pre_axltadd:
assumes A1: "a \<lsr> b" and A2: "c ∈ \<real>"
shows "c\<ca>a \<lsr> c\<ca>b"
proof -
from A1 have T: "a∈\<real>" "b∈\<real>" using strict_cplx_ord_type
by auto;
with A1 A2 show "c\<ca>a \<lsr> c\<ca>b"
using def_of_real_axis_order valid_cntxts
group3.group_strict_ord_transl_inv sum_of_reals
by auto;
qed

text{*The set of positive complex reals is closed with respect to
multiplication.*}


lemma (in complex0) pre_axmulgt0: assumes A1: "\<zero> \<lsr> a" "\<zero> \<lsr> b"
shows "\<zero> \<lsr> a·b"
proof -
from A1 have T: "a∈\<real>" "b∈\<real>" using strict_cplx_ord_type
by auto;
with A1 show "\<zero> \<lsr> a·b"
using def_of_real_axis_order valid_cntxts field1.pos_mul_closed
def_of_real_axis_order prod_of_reals
by auto;
qed;

text{*The order on complex reals is linear and complete.*}

lemma (in complex0) cmplx_reals_ord_lin_compl: shows
"CplxROrder(R,A,r) {is complete}"
"IsLinOrder(\<real>,CplxROrder(R,A,r))"
proof -
have "SliceProjection(\<real>) ∈ bij(\<real>,R)"
using slice_proj_bij ComplexReals_def real_means_real_axis
by simp;
moreover have "r ⊆ R×R" using valid_cntxts ring1.OrdRing_ZF_1_L1
IsAnOrdRing_def by simp;
moreover from R_are_reals have
"r {is complete}" and "IsLinOrder(R,r)"
using IsAmodelOfReals_def valid_cntxts ring1.OrdRing_ZF_1_L1
IsAnOrdRing_def by auto;
ultimately show
"CplxROrder(R,A,r) {is complete}"
"IsLinOrder(\<real>,CplxROrder(R,A,r))"
using CplxROrder_def real_means_real_axis ind_rel_pres_compl
ind_rel_pres_lin by auto
qed;

text{*The property of the strict order on complex reals
that corresponds to completeness.*}


lemma (in complex0) pre_axsup: assumes A1: "X ⊆ \<real>" "X ≠ 0" and
A2: "∃x∈\<real>. ∀y∈X. y \<lsr> x"
shows
"∃x∈\<real>. (∀y∈X. ¬(x \<lsr> y)) ∧ (∀y∈\<real>. (y \<lsr> x --> (∃z∈X. y \<lsr> z)))"
proof -
let ?s = "StrictVersion(CplxROrder(R,A,r))"
have
"CplxROrder(R,A,r) ⊆ \<real>×\<real>"
"IsLinOrder(\<real>,CplxROrder(R,A,r))"
"CplxROrder(R,A,r) {is complete}"
using cplx_ord_on_cplx_reals cmplx_reals_ord_lin_compl
by auto;
moreover note A1
moreover have "?s = StrictVersion(CplxROrder(R,A,r))"
by simp;
moreover from A2 have "∃u∈\<real>. ∀y∈X. ⟨y,u⟩ ∈ ?s"
by simp;
ultimately have
"∃x∈\<real>. ( ∀y∈X. ⟨x,y⟩ ∉ ?s ) ∧
(∀y∈\<real>. ⟨y,x⟩ ∈ ?s --> (∃z∈X. ⟨y,z⟩ ∈ ?s))"

by (rule strict_of_compl);
then show "(∃x∈\<real>. (∀y∈X. ¬(x \<lsr> y)) ∧
(∀y∈\<real>. (y \<lsr> x --> (∃z∈X. y \<lsr> z))))"

by simp;
qed;

end;