(*

This file is a part of IsarMathLib -

a library of formalized mathematics for Isabelle/Isar.

Copyright (C) 2006-2009 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{Metamath\_sampler.thy}*}

theory Metamath_sampler imports Metamath_interface MMI_Complex_ZF_2

begin

text{* The theorems translated from Metamath reside in the @{text "MMI_Complex_ZF"},

@{text "MMI_Complex_ZF_1"} and @{text "MMI_Complex_ZF_2"} theories.

The proofs of these theorems are very verbose and for this

reason the theories are not shown in the proof document or the FormaMath.org

site. This theory file contains some examples of theorems

translated from Metamath and formulated in the @{text "complex0"} context.

This serves two purposes: to give an overview of the material covered in

the translated theorems and to provide examples of how to take a translated

theorem (proven in the @{text "MMIsar0"} context) and transfer it to the

@{text "complex0"} context. The typical procedure for moving a theorem from

@{text "MMIsar0"} to @{text "complex0"} is as follows:

First we define certain aliases that map names defined in the @{text "complex0"}

to their corresponding names in the @{text "MMIsar0"} context. This makes it

easy to copy and paste the statement of the theorem as

displayed with ProofGeneral. Then we run the Isabelle

from ProofGeneral up to the theorem we want to move. When the theorem is verified

ProofGeneral displays the statement in the raw set theory notation, stripped

from any notation defined in the @{text "MMIsar0"} locale. This is what we copy

to the proof in the @{text "complex0"} locale. After that we just can write

"then have ?thesis by simp" and the simplifier translates the raw set

theory notation to the one used in @{text "complex0"}.

*}

section{*Extended reals and order*}

text{*In this sectin we import a couple of theorems about the extended

real line and the linear order on it.*}

text{*Metamath uses the set of real numbers extended with $+\infty$ and $-\infty$.

The $+\infty$ and $-\infty$ symbols are defined quite arbitrarily as $\mathbb{C}$

and $\mathbb{\{ C\} }$, respectively. The next lemma that corresponds to

Metamath's @{text "renfdisj"} states that $+\infty$ and $-\infty$ are not

elements of $\mathbb{R}$.*}

lemma (in complex0) renfdisj: shows "\<real> ∩ {\<cpnf>,\<cmnf>} = 0"

proof -

let ?real = "\<real>"

let ?complex = "\<complex>"

let ?one = "\<one>"

let ?zero = "\<zero>"

let ?iunit = "\<i>"

let ?caddset = "CplxAdd(R,A)"

let ?cmulset = "CplxMul(R,A,M)"

let ?lessrrel = "StrictVersion(CplxROrder(R,A,r))"

have "MMIsar0

(?real, ?complex, ?one, ?zero, ?iunit, ?caddset, ?cmulset, ?lessrrel)"

using MMIsar_valid by simp;

then have "?real ∩ {?complex, {?complex}} = 0"

by (rule MMIsar0.MMI_renfdisj);

thus "\<real> ∩ {\<cpnf>,\<cmnf>} = 0" by simp;

qed;

text{* The order relation used most often in Metamath is defined on

the set of complex reals extended with $+\infty$ and $-\infty$.

The next lemma

allows to use Metamath's @{text "xrltso"} that states that the @{text "\<ls>"}

relations is a strict linear order on the extended set.*}

lemma (in complex0) xrltso: shows "\<cltrrset> Orders \<real>⇧^{*}"

proof -

let ?real = "\<real>"

let ?complex = "\<complex>"

let ?one = "\<one>"

let ?zero = "\<zero>"

let ?iunit = "\<i>"

let ?caddset = "CplxAdd(R,A)"

let ?cmulset = "CplxMul(R,A,M)"

let ?lessrrel = "StrictVersion(CplxROrder(R,A,r))"

have "MMIsar0

(?real, ?complex, ?one, ?zero, ?iunit, ?caddset, ?cmulset, ?lessrrel)"

using MMIsar_valid by simp;

then have

"(?lessrrel ∩ ?real × ?real ∪

{⟨{?complex}, ?complex⟩} ∪ ?real × {?complex} ∪

{{?complex}} × ?real) Orders (?real ∪ {?complex, {?complex}})"

by (rule MMIsar0.MMI_xrltso);

moreover have "?lessrrel ∩ ?real × ?real = ?lessrrel"

using cplx_strict_ord_on_cplx_reals by auto

ultimately show "\<cltrrset> Orders \<real>⇧^{*}" by simp;

qed;

text{*Metamath defines the usual $<$ and $\leq$ ordering relations for the

extended real line, including $+\infty$ and $-\infty$.*}

lemma (in complex0) xrrebndt: assumes A1: "x ∈ \<real>⇧^{*}"

shows "x ∈ \<real> <-> ( \<cmnf> \<ls> x ∧ x \<ls> \<cpnf> )"

proof -

let ?real = "\<real>"

let ?complex = "\<complex>"

let ?one = "\<one>"

let ?zero = "\<zero>"

let ?iunit = "\<i>"

let ?caddset = "CplxAdd(R,A)"

let ?cmulset = "CplxMul(R,A,M)"

let ?lessrrel = "StrictVersion(CplxROrder(R,A,r))"

have "MMIsar0

(?real, ?complex, ?one, ?zero, ?iunit, ?caddset, ?cmulset, ?lessrrel)"

using MMIsar_valid by simp;

then have "x ∈ \<real> ∪ {\<complex>, {\<complex>}} -->

x ∈ \<real> <-> ⟨{\<complex>}, x⟩ ∈ ?lessrrel ∩ \<real> × \<real> ∪ {⟨{\<complex>}, \<complex>⟩} ∪

\<real> × {\<complex>} ∪ {{\<complex>}} × \<real> ∧

⟨x, \<complex>⟩ ∈ ?lessrrel ∩ \<real> × \<real> ∪ {⟨{\<complex>}, \<complex>⟩} ∪

\<real> × {\<complex>} ∪ {{\<complex>}} × \<real>"

by (rule MMIsar0.MMI_xrrebndt);

then have "x ∈ \<real>⇧^{*}--> ( x ∈ \<real> <-> ( \<cmnf> \<ls> x ∧ x \<ls> \<cpnf> ) )"

by simp;

with A1 show ?thesis by simp;

qed;

text{*A quite involved inequality.*}

lemma (in complex0) lt2mul2divt:

assumes A1: "a ∈ \<real>" "b ∈ \<real>" "c ∈ \<real>" "d ∈ \<real>" and

A2: "\<zero> \<ls> b" "\<zero> \<ls> d"

shows "a·b \<ls> c·d <-> a\<cdiv>d \<ls> c\<cdiv>b"

proof -

let ?real = "\<real>"

let ?complex = "\<complex>"

let ?one = "\<one>"

let ?zero = "\<zero>"

let ?iunit = "\<i>"

let ?caddset = "CplxAdd(R,A)"

let ?cmulset = "CplxMul(R,A,M)"

let ?lessrrel = "StrictVersion(CplxROrder(R,A,r))"

have "MMIsar0

(?real, ?complex, ?one, ?zero, ?iunit, ?caddset, ?cmulset, ?lessrrel)"

using MMIsar_valid by simp;

then have

"(a ∈ ?real ∧ b ∈ ?real) ∧

(c ∈ ?real ∧ d ∈ ?real) ∧

⟨?zero, b⟩ ∈ ?lessrrel ∩ ?real × ?real ∪

{⟨{?complex}, ?complex⟩} ∪ ?real × {?complex} ∪ {{?complex}} × ?real ∧

⟨?zero, d⟩ ∈ ?lessrrel ∩ ?real × ?real ∪

{⟨{?complex}, ?complex⟩} ∪ ?real × {?complex} ∪ {{?complex}} × ?real -->

⟨?cmulset ` ⟨a, b⟩, ?cmulset ` ⟨c, d⟩⟩ ∈

?lessrrel ∩ ?real × ?real ∪ {⟨{?complex}, ?complex⟩} ∪

?real × {?complex} ∪ {{?complex}} × ?real <->

⟨\<Union>{x ∈ ?complex . ?cmulset ` ⟨d, x⟩ = a},

\<Union>{x ∈ ?complex . ?cmulset ` ⟨b, x⟩ = c}⟩ ∈

?lessrrel ∩ ?real × ?real ∪ {⟨{?complex}, ?complex⟩} ∪

?real × {?complex} ∪ {{?complex}} × ?real"

by (rule MMIsar0.MMI_lt2mul2divt);

with A1 A2 show ?thesis by simp;

qed;

text{*A real number is smaller than its half iff it is positive. *}

lemma (in complex0) halfpos: assumes A1: "a ∈ \<real>"

shows "\<zero> \<ls> a <-> a\<cdiv>\<two> \<ls> a"

proof -

let ?real = "\<real>"

let ?complex = "\<complex>"

let ?one = "\<one>"

let ?zero = "\<zero>"

let ?iunit = "\<i>"

let ?caddset = "CplxAdd(R,A)"

let ?cmulset = "CplxMul(R,A,M)"

let ?lessrrel = "StrictVersion(CplxROrder(R,A,r))"

from A1 have "MMIsar0

(?real, ?complex, ?one, ?zero, ?iunit, ?caddset, ?cmulset, ?lessrrel)"

and "a ∈ ?real"

using MMIsar_valid by auto;

then have

"⟨?zero, a⟩ ∈

?lessrrel ∩ ?real × ?real ∪ {⟨{?complex}, ?complex⟩} ∪

?real × {?complex} ∪ {{?complex}} × ?real <->

⟨\<Union>{x ∈ ?complex . ?cmulset ` ⟨?caddset ` ⟨?one, ?one⟩, x⟩ = a}, a⟩ ∈

?lessrrel ∩ ?real × ?real ∪

{⟨{?complex}, ?complex⟩} ∪ ?real × {?complex} ∪ {{?complex}} × ?real"

by (rule MMIsar0.MMI_halfpos);

then show ?thesis by simp;

qed;

text{*One more inequality.*}

lemma (in complex0) ledivp1t:

assumes A1: "a ∈ \<real>" "b ∈ \<real>" and

A2: "\<zero> \<lsq> a" "\<zero> \<lsq> b"

shows "(a\<cdiv>(b \<ca> \<one>))·b \<lsq> a"

proof -

let ?real = "\<real>"

let ?complex = "\<complex>"

let ?one = "\<one>"

let ?zero = "\<zero>"

let ?iunit = "\<i>"

let ?caddset = "CplxAdd(R,A)"

let ?cmulset = "CplxMul(R,A,M)"

let ?lessrrel = "StrictVersion(CplxROrder(R,A,r))"

have "MMIsar0

(?real, ?complex, ?one, ?zero, ?iunit, ?caddset, ?cmulset, ?lessrrel)"

using MMIsar_valid by simp;

then have

"(a ∈ ?real ∧ ⟨a, ?zero⟩ ∉

?lessrrel ∩ ?real × ?real ∪ {⟨{?complex}, ?complex⟩} ∪

?real × {?complex} ∪ {{?complex}} × ?real) ∧

b ∈ ?real ∧ ⟨b, ?zero⟩ ∉ ?lessrrel ∩ ?real × ?real ∪

{⟨{?complex}, ?complex⟩} ∪ ?real × {?complex} ∪

{{?complex}} × ?real -->

⟨a,?cmulset`⟨\<Union>{x ∈ ?complex . ?cmulset`⟨?caddset`⟨b, ?one⟩, x⟩ = a}, b⟩⟩ ∉

?lessrrel ∩ ?real × ?real ∪ {⟨{?complex}, ?complex⟩} ∪

?real × {?complex} ∪ {{?complex}} × ?real"

by (rule MMIsar0.MMI_ledivp1t)

with A1 A2 show ?thesis by simp;

qed

section{*Natural real numbers*}

text{*In standard mathematics natural numbers are treated as a subset of

real numbers.

From the set theory point of view however those are quite different objects.

In this section we talk about "real natural" numbers i.e. the conterpart of

natural numbers that is a subset of the reals.*}

text{*Two ways of saying that there are no natural numbers between $n$ and $n+1$.*}

lemma (in complex0) no_nats_between:

assumes A1: "n ∈ \<nat>" "k ∈ \<nat>"

shows

"n\<lsq>k <-> n \<ls> k\<ca>\<one>"

"n \<ls> k <-> n \<ca> \<one> \<lsq> k"

proof -

let ?real = "\<real>"

let ?complex = "\<complex>"

let ?one = "\<one>"

let ?zero = "\<zero>"

let ?iunit = "\<i>"

let ?caddset = "CplxAdd(R,A)"

let ?cmulset = "CplxMul(R,A,M)"

let ?lessrrel = "StrictVersion(CplxROrder(R,A,r))"

have I: "MMIsar0

(?real, ?complex, ?one, ?zero, ?iunit, ?caddset, ?cmulset, ?lessrrel)"

using MMIsar_valid by simp;

then have

"n ∈ \<Inter>{N ∈ Pow(?real) . ?one ∈ N ∧

(∀n. n ∈ N --> ?caddset ` ⟨n, ?one⟩ ∈ N)} ∧

k ∈ \<Inter>{N ∈ Pow(?real) . ?one ∈ N ∧

(∀n. n ∈ N --> ?caddset ` ⟨n, ?one⟩ ∈ N)} -->

⟨k, n⟩ ∉

?lessrrel ∩ ?real × ?real ∪ {⟨{?complex}, ?complex⟩} ∪ ?real × {?complex} ∪

{{?complex}} × ?real <->

⟨n, ?caddset ` ⟨k, ?one⟩⟩ ∈

?lessrrel ∩ ?real × ?real ∪ {⟨{?complex}, ?complex⟩} ∪ ?real × {?complex} ∪

{{?complex}} × ?real" by (rule MMIsar0.MMI_nnleltp1t);

then have "n ∈ \<nat> ∧ k ∈ \<nat> --> n \<lsq> k <-> n \<ls> k \<ca> \<one>"

by simp;

with A1 show "n\<lsq>k <-> n \<ls> k\<ca>\<one>" by simp;

from I have

"n ∈ \<Inter>{N ∈ Pow(?real) . ?one ∈ N ∧

(∀n. n ∈ N --> ?caddset ` ⟨n, ?one⟩ ∈ N)} ∧

k ∈ \<Inter>{N ∈ Pow(?real) . ?one ∈ N ∧

(∀n. n ∈ N --> ?caddset ` ⟨n, ?one⟩ ∈ N)} -->

⟨n, k⟩ ∈

?lessrrel ∩ ?real × ?real ∪

{⟨{?complex}, ?complex⟩} ∪ ?real × {?complex} ∪

{{?complex}} × ?real <-> ⟨k, ?caddset ` ⟨n, ?one⟩⟩ ∉

?lessrrel ∩ ?real × ?real ∪ {⟨{?complex}, ?complex⟩} ∪ ?real × {?complex} ∪

{{?complex}} × ?real" by (rule MMIsar0.MMI_nnltp1let);

then have "n ∈ \<nat> ∧ k ∈ \<nat> --> n \<ls> k <-> n \<ca> \<one> \<lsq> k"

by simp;

with A1 show "n \<ls> k <-> n \<ca> \<one> \<lsq> k" by simp;

qed;

text{*Metamath has some very complicated and general version of induction

on (complex) natural numbers that I can't even understand. As an exercise

I derived a more standard version that is imported to the @{text "complex0"}

context below.*}

lemma (in complex0) cplx_nat_ind: assumes A1: "ψ(\<one>)" and

A2: "∀k ∈ \<nat>. ψ(k) --> ψ(k\<ca>\<one>)" and

A3: "n ∈ \<nat>"

shows "ψ(n)"

proof -

let ?real = "\<real>"

let ?complex = "\<complex>"

let ?one = "\<one>"

let ?zero = "\<zero>"

let ?iunit = "\<i>"

let ?caddset = "CplxAdd(R,A)"

let ?cmulset = "CplxMul(R,A,M)"

let ?lessrrel = "StrictVersion(CplxROrder(R,A,r))"

have I: "MMIsar0

(?real, ?complex, ?one, ?zero, ?iunit, ?caddset, ?cmulset, ?lessrrel)"

using MMIsar_valid by simp;

moreover from A1 A2 A3 have

"ψ(?one)"

"∀k∈\<Inter>{N ∈ Pow(?real) . ?one ∈ N ∧

(∀n. n ∈ N --> ?caddset ` ⟨n, ?one⟩ ∈ N)}.

ψ(k) --> ψ(?caddset ` ⟨k, ?one⟩)"

"n ∈ \<Inter>{N ∈ Pow(?real) . ?one ∈ N ∧

(∀n. n ∈ N --> ?caddset ` ⟨n, ?one⟩ ∈ N)}"

by auto;

ultimately show "ψ(n)" by (rule MMIsar0.nnind1);

qed;

text{*Some simple arithmetics.*}

lemma (in complex0) arith: shows

"\<two> \<ca> \<two> = \<four>"

"\<two>·\<two> = \<four>"

"\<three>·\<two> = \<six>"

"\<three>·\<three> = \<nine>"

proof -

let ?real = "\<real>"

let ?complex = "\<complex>"

let ?one = "\<one>"

let ?zero = "\<zero>"

let ?iunit = "\<i>"

let ?caddset = "CplxAdd(R,A)"

let ?cmulset = "CplxMul(R,A,M)"

let ?lessrrel = "StrictVersion(CplxROrder(R,A,r))"

have I: "MMIsar0

(?real, ?complex, ?one, ?zero, ?iunit, ?caddset, ?cmulset, ?lessrrel)"

using MMIsar_valid by simp;

then have

"?caddset ` ⟨?caddset ` ⟨?one, ?one⟩, ?caddset ` ⟨?one, ?one⟩⟩ =

?caddset ` ⟨?caddset ` ⟨?caddset ` ⟨?one, ?one⟩, ?one⟩, ?one⟩"

by (rule MMIsar0.MMI_2p2e4)

thus "\<two> \<ca> \<two> = \<four>" by simp;

from I have

"?cmulset`⟨?caddset`⟨?one, ?one⟩, ?caddset`⟨?one, ?one⟩⟩ =

?caddset`⟨?caddset`⟨?caddset`⟨?one, ?one⟩, ?one⟩, ?one⟩"

by (rule MMIsar0.MMI_2t2e4)

thus "\<two>·\<two> = \<four>" by simp

from I have

"?cmulset`⟨?caddset`⟨?caddset`⟨?one, ?one⟩, ?one⟩, ?caddset`⟨?one, ?one⟩⟩ =

?caddset `⟨?caddset`⟨?caddset`⟨?caddset`⟨?caddset`

⟨?one, ?one⟩, ?one⟩, ?one⟩, ?one⟩, ?one⟩"

by (rule MMIsar0.MMI_3t2e6)

thus "\<three>·\<two> = \<six>" by simp;

from I have "?cmulset `

⟨?caddset`⟨?caddset`⟨?one, ?one⟩, ?one⟩,

?caddset`⟨?caddset`⟨?one, ?one⟩, ?one⟩⟩ =

?caddset`⟨?caddset`⟨?caddset `⟨?caddset `

⟨?caddset`⟨?caddset`⟨?caddset`⟨?caddset`⟨?one, ?one⟩, ?one⟩, ?one⟩, ?one⟩,

?one⟩, ?one⟩, ?one⟩, ?one⟩"

by (rule MMIsar0.MMI_3t3e9);

thus "\<three>·\<three> = \<nine>" by simp;

qed;

section{*Infimum and supremum in real numbers*}

text{*Real numbers form a complete ordered field. Here we import a couple

of Metamath theorems about supremu and infimum.*}

text{*If a set $S$ has a smallest element, then the infimum of $S$ belongs

to it.*}

lemma (in complex0) lbinfmcl: assumes A1: "S ⊆ \<real>" and

A2: "∃x∈S. ∀y∈S. x \<lsq> y"

shows "Infim(S,\<real>,\<cltrrset>) ∈ S"

proof -

let ?real = "\<real>"

let ?complex = "\<complex>"

let ?one = "\<one>"

let ?zero = "\<zero>"

let ?iunit = "\<i>"

let ?caddset = "CplxAdd(R,A)"

let ?cmulset = "CplxMul(R,A,M)"

let ?lessrrel = "StrictVersion(CplxROrder(R,A,r))"

have I: "MMIsar0

(?real, ?complex, ?one, ?zero, ?iunit, ?caddset, ?cmulset, ?lessrrel)"

using MMIsar_valid by simp

then have

"S ⊆ ?real ∧ (∃x∈S. ∀y∈S. ⟨y, x⟩ ∉

?lessrrel ∩ ?real × ?real ∪ {⟨{?complex}, ?complex⟩} ∪

?real × {?complex} ∪ {{?complex}} × ?real) -->

Sup(S, ?real,

converse(?lessrrel ∩ ?real × ?real ∪

{⟨{?complex}, ?complex⟩} ∪ ?real × {?complex} ∪

{{?complex}} × ?real)) ∈ S"

by (rule MMIsar0.MMI_lbinfmcl);

then have

"S ⊆\<real> ∧ ( ∃x∈S. ∀y∈S. x \<lsq> y) -->

Sup(S,\<real>,converse(\<cltrrset>)) ∈ S" by simp;

with A1 A2 show ?thesis using Infim_def by simp;

qed;

text{*Supremum of any subset of reals that is bounded above is real.*}

lemma (in complex0) sup_is_real:

assumes "A ⊆ \<real> " and "A ≠ 0" and "∃x∈\<real>. ∀y∈A. y \<lsq> x"

shows "Sup(A,\<real>,\<cltrrset>) ∈ \<real>"

proof -

let ?real = "\<real>"

let ?complex = "\<complex>"

let ?one = "\<one>"

let ?zero = "\<zero>"

let ?iunit = "\<i>"

let ?caddset = "CplxAdd(R,A)"

let ?cmulset = "CplxMul(R,A,M)"

let ?lessrrel = "StrictVersion(CplxROrder(R,A,r))"

have "MMIsar0

(?real, ?complex, ?one, ?zero, ?iunit, ?caddset, ?cmulset, ?lessrrel)"

using MMIsar_valid by simp

then have

"A ⊆ ?real ∧ A ≠ 0 ∧ (∃x∈?real. ∀y∈A. ⟨x, y⟩ ∉

?lessrrel ∩ ?real × ?real ∪ {⟨{?complex}, ?complex⟩} ∪

?real × {?complex} ∪ {{?complex}} × ?real) -->

Sup(A, ?real,

?lessrrel ∩ ?real × ?real ∪ {⟨{?complex}, ?complex⟩} ∪

?real × {?complex} ∪ {{?complex}} × ?real) ∈ ?real"

by (rule MMIsar0.MMI_suprcl);

with assms show ?thesis by simp;

qed;

text{*If a real number is smaller that the supremum of $A$, then

we can find an element of $A$ greater than it. *}

lemma (in complex0) suprlub:

assumes "A ⊆\<real>" and "A ≠ 0" and "∃x∈\<real>. ∀y∈A. y \<lsq> x"

and "B ∈ \<real>" and "B \<ls> Sup(A,\<real>,\<cltrrset>)"

shows "∃z∈A. B \<ls> z"

proof -

let ?real = "\<real>"

let ?complex = "\<complex>"

let ?one = "\<one>"

let ?zero = "\<zero>"

let ?iunit = "\<i>"

let ?caddset = "CplxAdd(R,A)"

let ?cmulset = "CplxMul(R,A,M)"

let ?lessrrel = "StrictVersion(CplxROrder(R,A,r))"

have "MMIsar0

(?real, ?complex, ?one, ?zero, ?iunit, ?caddset, ?cmulset, ?lessrrel)"

using MMIsar_valid by simp

then have "(A ⊆ ?real ∧ A ≠ 0 ∧ (∃x∈?real. ∀y∈A. ⟨x, y⟩ ∉

?lessrrel ∩ ?real × ?real ∪ {⟨{?complex}, ?complex⟩} ∪

?real × {?complex} ∪

{{?complex}} × ?real)) ∧ B ∈ ?real ∧ ⟨B, Sup(A, ?real,

?lessrrel ∩ ?real × ?real ∪ {⟨{?complex}, ?complex⟩} ∪

?real × {?complex} ∪

{{?complex}} × ?real)⟩ ∈ ?lessrrel ∩ ?real × ?real ∪

{⟨{?complex}, ?complex⟩} ∪ ?real × {?complex} ∪

{{?complex}} × ?real -->

(∃z∈A. ⟨B, z⟩ ∈ ?lessrrel ∩ ?real × ?real ∪

{⟨{?complex}, ?complex⟩} ∪ ?real × {?complex} ∪

{{?complex}} × ?real)"

by (rule MMIsar0.MMI_suprlub);

with assms show ?thesis by simp;

qed;

text{*Something a bit more interesting: infimum of a set that is bounded

below is real and equal to the

minus supremum of the set flipped around zero.*}

lemma (in complex0) infmsup:

assumes "A ⊆ \<real>" and "A ≠ 0" and "∃x∈\<real>. ∀y∈A. x \<lsq> y"

shows

"Infim(A,\<real>,\<cltrrset>) ∈ \<real>"

"Infim(A,\<real>,\<cltrrset>) = ( \<cn>Sup({z ∈ \<real>. (\<cn>z) ∈ A },\<real>,\<cltrrset>) )"

proof -

let ?real = "\<real>"

let ?complex = "\<complex>"

let ?one = "\<one>"

let ?zero = "\<zero>"

let ?iunit = "\<i>"

let ?caddset = "CplxAdd(R,A)"

let ?cmulset = "CplxMul(R,A,M)"

let ?lessrrel = "StrictVersion(CplxROrder(R,A,r))"

have I: "MMIsar0

(?real, ?complex, ?one, ?zero, ?iunit, ?caddset, ?cmulset, ?lessrrel)"

using MMIsar_valid by simp;

then have

"A ⊆ ?real ∧ A ≠ 0 ∧ (∃x∈?real. ∀y∈A. ⟨y, x⟩ ∉

?lessrrel ∩ ?real × ?real ∪ {⟨{?complex}, ?complex⟩} ∪

?real × {?complex} ∪

{{?complex}} × ?real) --> Sup(A, ?real, converse

(?lessrrel ∩ ?real × ?real ∪ {⟨{?complex}, ?complex⟩} ∪

?real × {?complex} ∪

{{?complex}} × ?real)) =

\<Union>{x ∈ ?complex . ?caddset`

⟨Sup({z ∈ ?real . \<Union>{x ∈ ?complex . ?caddset`⟨z, x⟩ = ?zero} ∈ A}, ?real,

?lessrrel ∩ ?real × ?real ∪ {⟨{?complex}, ?complex⟩} ∪

?real × {?complex} ∪ {{?complex}} × ?real), x⟩ = ?zero}"

by (rule MMIsar0.MMI_infmsup);

then have "A ⊆\<real> ∧ ¬(A = 0) ∧ ( ∃x∈\<real>. ∀y∈A. x \<lsq> y) -->

Sup(A,\<real>,converse(\<cltrrset>)) = ( \<cn>Sup({z ∈ \<real>. (\<cn>z) ∈ A },\<real>,\<cltrrset>) )"

by simp;

with assms show

"Infim(A,\<real>,\<cltrrset>) = ( \<cn>Sup({z ∈ \<real>. (\<cn>z) ∈ A },\<real>,\<cltrrset>) )"

using Infim_def by simp;

from I have

"A ⊆ ?real ∧ A ≠ 0 ∧ (∃x∈?real. ∀y∈A. ⟨y, x⟩ ∉

?lessrrel ∩ ?real × ?real ∪ {⟨{?complex}, ?complex⟩} ∪

?real × {?complex} ∪

{{?complex}} × ?real) --> Sup(A, ?real, converse

(?lessrrel ∩ ?real × ?real ∪ {⟨{?complex}, ?complex⟩} ∪

?real × {?complex} ∪ {{?complex}} × ?real)) ∈ ?real"

by (rule MMIsar0.MMI_infmrcl);

with assms show "Infim(A,\<real>,\<cltrrset>) ∈ \<real>"

using Infim_def by simp;

qed;

end