(* This file is a part of IsarMathLib -

a library of formalized mathematics for Isabelle/Isar.

Copyright (C) 2005-2008 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{Order\_ZF\_1a.thy}*}

theory Order_ZF_1a imports Order_ZF

begin

text{*This theory is a continuation of @{text "Order_ZF"} and talks

about maximuma and minimum of a set, supremum and infimum

and strict (not reflexive) versions of order relations.*}

section{*Maximum and minimum of a set*}

text{*In this section we show that maximum and minimum are unique if they

exist. We also show that union of sets that have maxima (minima) has a

maximum (minimum). We also show that singletons have maximum and minimum.

All this allows to show (in @{text "Finite_ZF"}) that every finite set has

well-defined maximum and minimum. *}

text{*For antisymmetric relations maximum of a set is unique if it exists.*}

lemma Order_ZF_4_L1: assumes A1: "antisym(r)" and A2: "HasAmaximum(r,A)"

shows "∃!M. M∈A ∧ (∀x∈A. ⟨ x,M⟩ ∈ r)"

proof

from A2 show "∃M. M ∈ A ∧ (∀x∈A. ⟨x, M⟩ ∈ r)"

using HasAmaximum_def by auto

fix M1 M2 assume

A2: "M1 ∈ A ∧ (∀x∈A. ⟨x, M1⟩ ∈ r)" "M2 ∈ A ∧ (∀x∈A. ⟨x, M2⟩ ∈ r)"

then have "⟨M1,M2⟩ ∈ r" "⟨M2,M1⟩ ∈ r" by auto

with A1 show "M1=M2" by (rule Fol1_L4)

qed

text{*For antisymmetric relations minimum of a set is unique if it exists.*}

lemma Order_ZF_4_L2: assumes A1: "antisym(r)" and A2: "HasAminimum(r,A)"

shows "∃!m. m∈A ∧ (∀x∈A. ⟨ m,x⟩ ∈ r)"

proof

from A2 show "∃m. m ∈ A ∧ (∀x∈A. ⟨m, x⟩ ∈ r)"

using HasAminimum_def by auto

fix m1 m2 assume

A2: "m1 ∈ A ∧ (∀x∈A. ⟨m1, x⟩ ∈ r)" "m2 ∈ A ∧ (∀x∈A. ⟨m2, x⟩ ∈ r)"

then have "⟨m1,m2⟩ ∈ r" "⟨m2,m1⟩ ∈ r" by auto

with A1 show "m1=m2" by (rule Fol1_L4)

qed

text{*Maximum of a set has desired properties. *}

lemma Order_ZF_4_L3: assumes A1: "antisym(r)" and A2: "HasAmaximum(r,A)"

shows "Maximum(r,A) ∈ A" "∀x∈A. ⟨x,Maximum(r,A)⟩ ∈ r"

proof -

let ?Max = "THE M. M∈A ∧ (∀x∈A. ⟨ x,M⟩ ∈ r)"

from A1 A2 have "∃!M. M∈A ∧ (∀x∈A. ⟨ x,M⟩ ∈ r)"

by (rule Order_ZF_4_L1)

then have "?Max ∈ A ∧ (∀x∈A. ⟨ x,?Max⟩ ∈ r)"

by (rule theI)

then show "Maximum(r,A) ∈ A" "∀x∈A. ⟨x,Maximum(r,A)⟩ ∈ r"

using Maximum_def by auto

qed

text{*Minimum of a set has desired properties.*}

lemma Order_ZF_4_L4: assumes A1: "antisym(r)" and A2: "HasAminimum(r,A)"

shows "Minimum(r,A) ∈ A" "∀x∈A. ⟨Minimum(r,A),x⟩ ∈ r"

proof -

let ?Min = "THE m. m∈A ∧ (∀x∈A. ⟨ m,x⟩ ∈ r)"

from A1 A2 have "∃!m. m∈A ∧ (∀x∈A. ⟨ m,x⟩ ∈ r)"

by (rule Order_ZF_4_L2)

then have "?Min ∈ A ∧ (∀x∈A. ⟨ ?Min,x⟩ ∈ r)"

by (rule theI)

then show "Minimum(r,A) ∈ A" "∀x∈A. ⟨Minimum(r,A),x⟩ ∈ r"

using Minimum_def by auto

qed

text{*For total and transitive relations a union a of two sets that have

maxima has a maximum.*}

lemma Order_ZF_4_L5:

assumes A1: "r {is total on} (A∪B)" and A2: "trans(r)"

and A3: "HasAmaximum(r,A)" "HasAmaximum(r,B)"

shows "HasAmaximum(r,A∪B)"

proof -

from A3 obtain M K where

D1: "M∈A ∧ (∀x∈A. ⟨ x,M⟩ ∈ r)" "K∈B ∧ (∀x∈B. ⟨ x,K⟩ ∈ r)"

using HasAmaximum_def by auto

let ?L = "GreaterOf(r,M,K)"

from D1 have T1: "M ∈ A∪B" "K ∈ A∪B"

"∀x∈A. ⟨ x,M⟩ ∈ r" "∀x∈B. ⟨ x,K⟩ ∈ r"

by auto

with A1 A2 have "∀x∈A∪B.⟨ x,?L⟩ ∈ r" by (rule Order_ZF_3_L2B)

moreover from T1 have "?L ∈ A∪B" using GreaterOf_def IsTotal_def

by simp

ultimately show "HasAmaximum(r,A∪B)" using HasAmaximum_def by auto

qed

text{*For total and transitive relations A union a of two sets that have

minima has a minimum.*}

lemma Order_ZF_4_L6:

assumes A1: "r {is total on} (A∪B)" and A2: "trans(r)"

and A3: "HasAminimum(r,A)" "HasAminimum(r,B)"

shows "HasAminimum(r,A∪B)"

proof -

from A3 obtain m k where

D1: "m∈A ∧ (∀x∈A. ⟨ m,x⟩ ∈ r)" "k∈B ∧ (∀x∈B. ⟨ k,x⟩ ∈ r)"

using HasAminimum_def by auto

let ?l = "SmallerOf(r,m,k)"

from D1 have T1: "m ∈ A∪B" "k ∈ A∪B"

"∀x∈A. ⟨ m,x⟩ ∈ r" "∀x∈B. ⟨ k,x⟩ ∈ r"

by auto

with A1 A2 have "∀x∈A∪B.⟨ ?l,x⟩ ∈ r" by (rule Order_ZF_3_L5B)

moreover from T1 have "?l ∈ A∪B" using SmallerOf_def IsTotal_def

by simp

ultimately show "HasAminimum(r,A∪B)" using HasAminimum_def by auto

qed

text{*Set that has a maximum is bounded above.*}

lemma Order_ZF_4_L7:

assumes "HasAmaximum(r,A)"

shows "IsBoundedAbove(A,r)"

using assms HasAmaximum_def IsBoundedAbove_def by auto

text{*Set that has a minimum is bounded below.*}

lemma Order_ZF_4_L8A:

assumes "HasAminimum(r,A)"

shows "IsBoundedBelow(A,r)"

using assms HasAminimum_def IsBoundedBelow_def by auto

text{*For reflexive relations singletons have a minimum and maximum.*}

lemma Order_ZF_4_L8: assumes "refl(X,r)" and "a∈X"

shows "HasAmaximum(r,{a})" "HasAminimum(r,{a})"

using assms refl_def HasAmaximum_def HasAminimum_def by auto

text{*For total and transitive relations if we add an element to a set

that has a maximum, the set still has a maximum.*}

lemma Order_ZF_4_L9:

assumes A1: "r {is total on} X" and A2: "trans(r)"

and A3: "A⊆X" and A4: "a∈X" and A5: "HasAmaximum(r,A)"

shows "HasAmaximum(r,A∪{a})"

proof -

from A3 A4 have "A∪{a} ⊆ X" by auto

with A1 have "r {is total on} (A∪{a})"

using Order_ZF_1_L4 by blast

moreover from A1 A2 A4 A5 have

"trans(r)" "HasAmaximum(r,A)" by auto

moreover from A1 A4 have "HasAmaximum(r,{a})"

using total_is_refl Order_ZF_4_L8 by blast

ultimately show "HasAmaximum(r,A∪{a})" by (rule Order_ZF_4_L5)

qed

text{*For total and transitive relations if we add an element to a set

that has a minimum, the set still has a minimum.*}

lemma Order_ZF_4_L10:

assumes A1: "r {is total on} X" and A2: "trans(r)"

and A3: "A⊆X" and A4: "a∈X" and A5: "HasAminimum(r,A)"

shows "HasAminimum(r,A∪{a})"

proof -

from A3 A4 have "A∪{a} ⊆ X" by auto

with A1 have "r {is total on} (A∪{a})"

using Order_ZF_1_L4 by blast

moreover from A1 A2 A4 A5 have

"trans(r)" "HasAminimum(r,A)" by auto

moreover from A1 A4 have "HasAminimum(r,{a})"

using total_is_refl Order_ZF_4_L8 by blast

ultimately show "HasAminimum(r,A∪{a})" by (rule Order_ZF_4_L6)

qed

text{*If the order relation has a property that every nonempty bounded set

attains a minimum (for example integers are like that),

then every nonempty set bounded below attains a minimum.*}

lemma Order_ZF_4_L11:

assumes A1: "r {is total on} X" and

A2: "trans(r)" and

A3: "r ⊆ X×X" and

A4: "∀A. IsBounded(A,r) ∧ A≠0 --> HasAminimum(r,A)" and

A5: "B≠0" and A6: "IsBoundedBelow(B,r)"

shows "HasAminimum(r,B)"

proof -

from A5 obtain b where T: "b∈B" by auto

let ?L = "{x∈B. ⟨x,b⟩ ∈ r}"

from A3 A6 T have T1: "b∈X" using Order_ZF_3_L1B by blast

with A1 T have T2: "b ∈ ?L"

using total_is_refl refl_def by simp

then have "?L ≠ 0" by auto

moreover have "IsBounded(?L,r)"

proof -

have "?L ⊆ B" by auto

with A6 have "IsBoundedBelow(?L,r)"

using Order_ZF_3_L12 by simp

moreover have "IsBoundedAbove(?L,r)"

by (rule Order_ZF_3_L15)

ultimately have "IsBoundedAbove(?L,r) ∧ IsBoundedBelow(?L,r)"

by blast

then show "IsBounded(?L,r)" using IsBounded_def

by simp

qed

ultimately have "IsBounded(?L,r) ∧ ?L ≠ 0" by blast

with A4 have "HasAminimum(r,?L)" by simp

then obtain m where I: "m∈?L" and II: "∀x∈?L. ⟨ m,x⟩ ∈ r"

using HasAminimum_def by auto

then have III: "⟨m,b⟩ ∈ r" by simp

from I have "m∈B" by simp

moreover have "∀x∈B. ⟨m,x⟩ ∈ r"

proof

fix x assume A7: "x∈B"

from A3 A6 have "B⊆X" using Order_ZF_3_L1B by blast

with A1 A7 T1 have "x ∈ ?L ∪ {x∈B. ⟨b,x⟩ ∈ r}"

using Order_ZF_1_L5 by simp

then have "x∈?L ∨ ⟨b,x⟩ ∈ r" by auto

moreover

{ assume "x∈?L"

with II have "⟨m,x⟩ ∈ r" by simp }

moreover

{ assume "⟨b,x⟩ ∈ r"

with A2 III have "trans(r)" and "⟨m,b⟩ ∈ r ∧ ⟨b,x⟩ ∈ r"

by auto

then have "⟨m,x⟩ ∈ r" by (rule Fol1_L3) }

ultimately show "⟨m,x⟩ ∈ r" by auto

qed

ultimately show "HasAminimum(r,B)" using HasAminimum_def

by auto

qed

text{*A dual to @{text "Order_ZF_4_L11"}:

If the order relation has a property that every nonempty bounded set

attains a maximum (for example integers are like that),

then every nonempty set bounded above attains a maximum.*}

lemma Order_ZF_4_L11A:

assumes A1: "r {is total on} X" and

A2: "trans(r)" and

A3: "r ⊆ X×X" and

A4: "∀A. IsBounded(A,r) ∧ A≠0 --> HasAmaximum(r,A)" and

A5: "B≠0" and A6: "IsBoundedAbove(B,r)"

shows "HasAmaximum(r,B)"

proof -

from A5 obtain b where T: "b∈B" by auto

let ?U = "{x∈B. ⟨b,x⟩ ∈ r}"

from A3 A6 T have T1: "b∈X" using Order_ZF_3_L1A by blast

with A1 T have T2: "b ∈ ?U"

using total_is_refl refl_def by simp

then have "?U ≠ 0" by auto

moreover have "IsBounded(?U,r)"

proof -

have "?U ⊆ B" by auto

with A6 have "IsBoundedAbove(?U,r)"

using Order_ZF_3_L13 by blast

moreover have "IsBoundedBelow(?U,r)"

using IsBoundedBelow_def by auto

ultimately have "IsBoundedAbove(?U,r) ∧ IsBoundedBelow(?U,r)"

by blast

then show "IsBounded(?U,r)" using IsBounded_def

by simp

qed

ultimately have "IsBounded(?U,r) ∧ ?U ≠ 0" by blast

with A4 have "HasAmaximum(r,?U)" by simp

then obtain m where I: "m∈?U" and II: "∀x∈?U. ⟨x,m⟩ ∈ r"

using HasAmaximum_def by auto

then have III: "⟨b,m⟩ ∈ r" by simp

from I have "m∈B" by simp

moreover have "∀x∈B. ⟨x,m⟩ ∈ r"

proof

fix x assume A7: "x∈B"

from A3 A6 have "B⊆X" using Order_ZF_3_L1A by blast

with A1 A7 T1 have "x ∈ {x∈B. ⟨x,b⟩ ∈ r} ∪ ?U"

using Order_ZF_1_L5 by simp

then have "x∈?U ∨ ⟨x,b⟩ ∈ r" by auto

moreover

{ assume "x∈?U"

with II have "⟨x,m⟩ ∈ r" by simp }

moreover

{ assume "⟨x,b⟩ ∈ r"

with A2 III have "trans(r)" and "⟨x,b⟩ ∈ r ∧ ⟨b,m⟩ ∈ r"

by auto

then have "⟨x,m⟩ ∈ r" by (rule Fol1_L3) }

ultimately show "⟨x,m⟩ ∈ r" by auto

qed

ultimately show "HasAmaximum(r,B)" using HasAmaximum_def

by auto

qed

text{*If a set has a minimum and $L$ is less or equal than

all elements of the set, then $L$ is less or equal than the minimum.*}

lemma Order_ZF_4_L12:

assumes "antisym(r)" and "HasAminimum(r,A)" and "∀a∈A. ⟨L,a⟩ ∈ r"

shows "⟨L,Minimum(r,A)⟩ ∈ r"

using assms Order_ZF_4_L4 by simp

text{*If a set has a maximum and all its elements are less or equal than

$M$, then the maximum of the set is less or equal than $M$.*}

lemma Order_ZF_4_L13:

assumes "antisym(r)" and "HasAmaximum(r,A)" and "∀a∈A. ⟨a,M⟩ ∈ r"

shows "⟨Maximum(r,A),M⟩ ∈ r"

using assms Order_ZF_4_L3 by simp

text{*If an element belongs to a set and is greater or equal

than all elements of that set, then it is the maximum of that set.*}

lemma Order_ZF_4_L14:

assumes A1: "antisym(r)" and A2: "M ∈ A" and

A3: "∀a∈A. ⟨a,M⟩ ∈ r"

shows "Maximum(r,A) = M"

proof -

from A2 A3 have I: "HasAmaximum(r,A)" using HasAmaximum_def

by auto

with A1 have "∃!M. M∈A ∧ (∀x∈A. ⟨x,M⟩ ∈ r)"

using Order_ZF_4_L1 by simp

moreover from A2 A3 have "M∈A ∧ (∀x∈A. ⟨x,M⟩ ∈ r)" by simp

moreover from A1 I have

"Maximum(r,A) ∈ A ∧ (∀x∈A. ⟨x,Maximum(r,A)⟩ ∈ r)"

using Order_ZF_4_L3 by simp

ultimately show "Maximum(r,A) = M" by auto

qed

text{*If an element belongs to a set and is less or equal

than all elements of that set, then it is the minimum of that set.*}

lemma Order_ZF_4_L15:

assumes A1: "antisym(r)" and A2: "m ∈ A" and

A3: "∀a∈A. ⟨m,a⟩ ∈ r"

shows "Minimum(r,A) = m"

proof -

from A2 A3 have I: "HasAminimum(r,A)" using HasAminimum_def

by auto

with A1 have "∃!m. m∈A ∧ (∀x∈A. ⟨m,x⟩ ∈ r)"

using Order_ZF_4_L2 by simp

moreover from A2 A3 have "m∈A ∧ (∀x∈A. ⟨m,x⟩ ∈ r)" by simp

moreover from A1 I have

"Minimum(r,A) ∈ A ∧ (∀x∈A. ⟨Minimum(r,A),x⟩ ∈ r)"

using Order_ZF_4_L4 by simp

ultimately show "Minimum(r,A) = m" by auto

qed

text{*If a set does not have a maximum, then for any its element we can

find one that is (strictly) greater.*}

lemma Order_ZF_4_L16:

assumes A1: "antisym(r)" and A2: "r {is total on} X" and

A3: "A⊆X" and

A4: "¬HasAmaximum(r,A)" and

A5: "x∈A"

shows "∃y∈A. ⟨x,y⟩ ∈ r ∧ y≠x"

proof -

{ assume A6: "∀y∈A. ⟨x,y⟩ ∉ r ∨ y=x"

have "∀y∈A. ⟨y,x⟩ ∈ r"

proof

fix y assume A7: "y∈A"

with A6 have "⟨x,y⟩ ∉ r ∨ y=x" by simp

with A2 A3 A5 A7 show "⟨y,x⟩ ∈ r"

using IsTotal_def Order_ZF_1_L1 by auto

qed

with A5 have "∃x∈A.∀y∈A. ⟨y,x⟩ ∈ r"

by auto

with A4 have False using HasAmaximum_def by simp

} then show "∃y∈A. ⟨x,y⟩ ∈ r ∧ y≠x" by auto

qed

section{*Supremum and Infimum*}

text{*In this section we consider the notions of supremum and infimum a set. *}

text{*Elements of the set of upper bounds are indeed upper bounds.

Isabelle also thinks it is obvious.*}

lemma Order_ZF_5_L1: assumes "u ∈ (\<Inter>a∈A. r``{a})" and "a∈A"

shows "⟨a,u⟩ ∈ r"

using assms by auto

text{*Elements of the set of lower bounds are indeed lower bounds.

Isabelle also thinks it is obvious.*}

lemma Order_ZF_5_L2: assumes "l ∈ (\<Inter>a∈A. r-``{a})" and "a∈A"

shows "⟨l,a⟩ ∈ r"

using assms by auto

text{*If the set of upper bounds has a minimum, then the supremum

is less or equal than any upper bound. We can probably do away with

the assumption that $A$ is not empty, (ab)using the fact that

intersection over an empty family is defined in Isabelle to be empty.*}

lemma Order_ZF_5_L3: assumes A1: "antisym(r)" and A2: "A≠0" and

A3: "HasAminimum(r,\<Inter>a∈A. r``{a})" and

A4: "∀a∈A. ⟨a,u⟩ ∈ r"

shows "⟨Supremum(r,A),u⟩ ∈ r"

proof -

let ?U = "\<Inter>a∈A. r``{a}"

from A4 have "∀a∈A. u ∈ r``{a}" using image_singleton_iff

by simp

with A2 have "u∈?U" by auto

with A1 A3 show "⟨Supremum(r,A),u⟩ ∈ r"

using Order_ZF_4_L4 Supremum_def by simp

qed

text{*Infimum is greater or equal than any lower bound.*}

lemma Order_ZF_5_L4: assumes A1: "antisym(r)" and A2: "A≠0" and

A3: "HasAmaximum(r,\<Inter>a∈A. r-``{a})" and

A4: "∀a∈A. ⟨l,a⟩ ∈ r"

shows "⟨l,Infimum(r,A)⟩ ∈ r"

proof -

let ?L = "\<Inter>a∈A. r-``{a}"

from A4 have "∀a∈A. l ∈ r-``{a}" using vimage_singleton_iff

by simp

with A2 have "l∈?L" by auto

with A1 A3 show "⟨l,Infimum(r,A)⟩ ∈ r"

using Order_ZF_4_L3 Infimum_def by simp

qed

text{*If $z$ is an upper bound for $A$ and is greater or equal than

any other upper bound, then $z$ is the supremum of $A$.*}

lemma Order_ZF_5_L5: assumes A1: "antisym(r)" and A2: "A≠0" and

A3: "∀x∈A. ⟨x,z⟩ ∈ r" and

A4: "∀y. (∀x∈A. ⟨x,y⟩ ∈ r) --> ⟨z,y⟩ ∈ r"

shows

"HasAminimum(r,\<Inter>a∈A. r``{a})"

"z = Supremum(r,A)"

proof -

let ?B = "\<Inter>a∈A. r``{a}"

from A2 A3 A4 have I: "z ∈ ?B" "∀y∈?B. ⟨z,y⟩ ∈ r"

by auto

then show "HasAminimum(r,\<Inter>a∈A. r``{a})"

using HasAminimum_def by auto

from A1 I show "z = Supremum(r,A)"

using Order_ZF_4_L15 Supremum_def by simp

qed

text{*If a set has a maximum, then the maximum is the supremum.*}

lemma Order_ZF_5_L6:

assumes A1: "antisym(r)" and A2: "A≠0" and

A3: "HasAmaximum(r,A)"

shows

"HasAminimum(r,\<Inter>a∈A. r``{a})"

"Maximum(r,A) = Supremum(r,A)"

proof -

let ?M = "Maximum(r,A)"

from A1 A3 have I: "?M ∈ A" and II: "∀x∈A. ⟨x,?M⟩ ∈ r"

using Order_ZF_4_L3 by auto

from I have III: "∀y. (∀x∈A. ⟨x,y⟩ ∈ r) --> ⟨?M,y⟩ ∈ r"

by simp

with A1 A2 II show "HasAminimum(r,\<Inter>a∈A. r``{a})"

by (rule Order_ZF_5_L5)

from A1 A2 II III show "?M = Supremum(r,A)"

by (rule Order_ZF_5_L5)

qed

text{*Properties of supremum of a set for complete relations.*}

lemma Order_ZF_5_L7:

assumes A1: "r ⊆ X×X" and A2: "antisym(r)" and

A3: "r {is complete}" and

A4: "A⊆X" "A≠0" and A5: "∃x∈X. ∀y∈A. ⟨y,x⟩ ∈ r"

shows

"Supremum(r,A) ∈ X"

"∀x∈A. ⟨x,Supremum(r,A)⟩ ∈ r"

proof -

from A5 have "IsBoundedAbove(A,r)" using IsBoundedAbove_def

by auto

with A3 A4 have "HasAminimum(r,\<Inter>a∈A. r``{a})"

using IsComplete_def by simp

with A2 have "Minimum(r,\<Inter>a∈A. r``{a}) ∈ ( \<Inter>a∈A. r``{a} )"

using Order_ZF_4_L4 by simp

moreover have "Minimum(r,\<Inter>a∈A. r``{a}) = Supremum(r,A)"

using Supremum_def by simp

ultimately have I: "Supremum(r,A) ∈ ( \<Inter>a∈A. r``{a} )"

by simp

moreover from A4 obtain a where "a∈A" by auto

ultimately have "⟨a,Supremum(r,A)⟩ ∈ r" using Order_ZF_5_L1

by simp

with A1 show "Supremum(r,A) ∈ X" by auto

from I show "∀x∈A. ⟨x,Supremum(r,A)⟩ ∈ r" using Order_ZF_5_L1

by simp

qed

text{*If the relation is a linear order then for any

element $y$ smaller than the supremum of a set we can

find one element of the set that is greater than $y$.*}

lemma Order_ZF_5_L8:

assumes A1: "r ⊆ X×X" and A2: "IsLinOrder(X,r)" and

A3: "r {is complete}" and

A4: "A⊆X" "A≠0" and A5: "∃x∈X. ∀y∈A. ⟨y,x⟩ ∈ r" and

A6: "⟨y,Supremum(r,A)⟩ ∈ r" "y ≠ Supremum(r,A)"

shows "∃z∈A. ⟨y,z⟩ ∈ r ∧ y ≠ z"

proof -

from A2 have

I: "antisym(r)" and

II: "trans(r)" and

III: "r {is total on} X"

using IsLinOrder_def by auto

from A1 A6 have T1: "y∈X" by auto

{ assume A7: "∀z ∈ A. ⟨y,z⟩ ∉ r ∨ y=z"

from A4 I have "antisym(r)" and "A≠0" by auto

moreover have "∀x∈A. ⟨x,y⟩ ∈ r"

proof

fix x assume A8: "x∈A"

with A4 have T2: "x∈X" by auto

from A7 A8 have "⟨y,x⟩ ∉ r ∨ y=x" by simp

with III T1 T2 show "⟨x,y⟩ ∈ r"

using IsTotal_def total_is_refl refl_def by auto

qed

moreover have "∀u. (∀x∈A. ⟨x,u⟩ ∈ r) --> ⟨y,u⟩ ∈ r"

proof-

{ fix u assume A9: "∀x∈A. ⟨x,u⟩ ∈ r"

from A4 A5 have "IsBoundedAbove(A,r)" and "A≠0"

using IsBoundedAbove_def by auto

with A3 A4 A6 I A9 have

"⟨y,Supremum(r,A)⟩ ∈ r ∧ ⟨Supremum(r,A),u⟩ ∈ r"

using IsComplete_def Order_ZF_5_L3 by simp

with II have "⟨y,u⟩ ∈ r" by (rule Fol1_L3)

} then show "∀u. (∀x∈A. ⟨x,u⟩ ∈ r) --> ⟨y,u⟩ ∈ r"

by simp

qed

ultimately have "y = Supremum(r,A)"

by (rule Order_ZF_5_L5)

with A6 have False by simp

} then show "∃z∈A. ⟨y,z⟩ ∈ r ∧ y ≠ z" by auto

qed

section{*Strict versions of order relations*}

text{*One of the problems with translating formalized mathematics from

Metamath to IsarMathLib is that Metamath uses strict orders (of the $<$

type) while in IsarMathLib we mostly use nonstrict orders (of the

$\leq$ type).

This doesn't really make any difference, but is annoying as we

have to prove many theorems twice. In this section we prove some theorems

to make it easier to translate the statements about strict orders to

statements about the corresponding non-strict order and vice versa. *}

text{*We define a strict version of a relation by removing the $y=x$ line

from the relation.*}

definition

"StrictVersion(r) ≡ r - {⟨x,x⟩. x ∈ domain(r)}"

text{*A reformulation of the definition of a strict version of an order.

*}

lemma def_of_strict_ver: shows

"⟨x,y⟩ ∈ StrictVersion(r) <-> ⟨x,y⟩ ∈ r ∧ x≠y"

using StrictVersion_def domain_def by auto

text{*The next lemma is about the strict version of an antisymmetric

relation.*}

lemma strict_of_antisym:

assumes A1: "antisym(r)" and A2: "⟨a,b⟩ ∈ StrictVersion(r)"

shows "⟨b,a⟩ ∉ StrictVersion(r)"

proof -

{ assume A3: "⟨b,a⟩ ∈ StrictVersion(r)"

with A2 have "⟨a,b⟩ ∈ r" and "⟨b,a⟩ ∈ r"

using def_of_strict_ver by auto

with A1 have "a=b" by (rule Fol1_L4)

with A2 have False using def_of_strict_ver

by simp

} then show "⟨b,a⟩ ∉ StrictVersion(r)" by auto

qed

text{*The strict version of totality.*}

lemma strict_of_tot:

assumes "r {is total on} X" and "a∈X" "b∈X" "a≠b"

shows "⟨a,b⟩ ∈ StrictVersion(r) ∨ ⟨b,a⟩ ∈ StrictVersion(r)"

using assms IsTotal_def def_of_strict_ver by auto

text{*A trichotomy law for the strict version of a total

and antisymmetric

relation. It is kind of interesting that one does not need

the full linear order for this.*}

lemma strict_ans_tot_trich:

assumes A1: "antisym(r)" and A2: "r {is total on} X"

and A3: "a∈X" "b∈X"

and A4: "s = StrictVersion(r)"

shows "Exactly_1_of_3_holds(⟨a,b⟩ ∈ s, a=b,⟨b,a⟩ ∈ s)"

proof -

let ?p = "⟨a,b⟩ ∈ s"

let ?q = "a=b"

let ?r = "⟨b,a⟩ ∈ s"

from A2 A3 A4 have "?p ∨ ?q ∨ ?r"

using strict_of_tot by auto

moreover from A1 A4 have "?p --> ¬?q ∧ ¬?r"

using def_of_strict_ver strict_of_antisym by simp

moreover from A4 have "?q --> ¬?p ∧ ¬?r"

using def_of_strict_ver by simp

moreover from A1 A4 have "?r --> ¬?p ∧ ¬?q"

using def_of_strict_ver strict_of_antisym by auto

ultimately show "Exactly_1_of_3_holds(?p, ?q, ?r)"

by (rule Fol1_L5)

qed

text{*A trichotomy law for linear order. This is a special

case of @{text "strict_ans_tot_trich"}. *}

corollary strict_lin_trich: assumes A1: "IsLinOrder(X,r)" and

A2: "a∈X" "b∈X" and

A3: "s = StrictVersion(r)"

shows "Exactly_1_of_3_holds(⟨a,b⟩ ∈ s, a=b,⟨b,a⟩ ∈ s)"

using assms IsLinOrder_def strict_ans_tot_trich by auto

text{*For an antisymmetric relation if a pair is in relation then

the reversed pair is not in the strict version of the relation.

*}

lemma geq_impl_not_less:

assumes A1: "antisym(r)" and A2: "⟨a,b⟩ ∈ r"

shows "⟨b,a⟩ ∉ StrictVersion(r)"

proof -

{ assume A3: "⟨b,a⟩ ∈ StrictVersion(r)"

with A2 have "⟨a,b⟩ ∈ StrictVersion(r)"

using def_of_strict_ver by auto

with A1 A3 have False using strict_of_antisym

by blast

} then show "⟨b,a⟩ ∉ StrictVersion(r)" by auto

qed

text{*If an antisymmetric relation is transitive,

then the strict version is also transitive, an explicit

version @{text "strict_of_transB"} below.*}

lemma strict_of_transA:

assumes A1: "trans(r)" and A2: "antisym(r)" and

A3: "s= StrictVersion(r)" and A4: "⟨a,b⟩ ∈ s" "⟨b,c⟩ ∈ s"

shows "⟨a,c⟩ ∈ s"

proof -

from A3 A4 have I: "⟨a,b⟩ ∈ r ∧ ⟨b,c⟩ ∈ r"

using def_of_strict_ver by simp

with A1 have "⟨a,c⟩ ∈ r" by (rule Fol1_L3)

moreover

{ assume "a=c"

with I have "⟨a,b⟩ ∈ r" and "⟨b,a⟩ ∈ r" by auto

with A2 have "a=b" by (rule Fol1_L4)

with A3 A4 have False using def_of_strict_ver by simp

} then have "a≠c" by auto

ultimately have "⟨a,c⟩ ∈ StrictVersion(r)"

using def_of_strict_ver by simp

with A3 show ?thesis by simp

qed

text{*If an antisymmetric relation is transitive,

then the strict version is also transitive.*}

lemma strict_of_transB:

assumes A1: "trans(r)" and A2: "antisym(r)"

shows "trans(StrictVersion(r))"

proof -

let ?s = "StrictVersion(r)"

from A1 A2 have

"∀ x y z. ⟨x, y⟩ ∈ ?s ∧ ⟨y, z⟩ ∈ ?s --> ⟨x, z⟩ ∈ ?s"

using strict_of_transA by blast

then show "trans(StrictVersion(r))" by (rule Fol1_L2)

qed

text{*The next lemma provides a condition that is satisfied by

the strict version of a relation if the original relation

is a complete linear order. *}

lemma strict_of_compl:

assumes A1: "r ⊆ X×X" and A2: "IsLinOrder(X,r)" and

A3: "r {is complete}" and

A4: "A⊆X" "A≠0" and A5: "s = StrictVersion(r)" and

A6: "∃u∈X. ∀y∈A. ⟨y,u⟩ ∈ s"

shows

"∃x∈X. ( ∀y∈A. ⟨x,y⟩ ∉ s ) ∧ (∀y∈X. ⟨y,x⟩ ∈ s --> (∃z∈A. ⟨y,z⟩ ∈ s))"

proof -

let ?x = "Supremum(r,A)"

from A2 have I: "antisym(r)" using IsLinOrder_def

by simp

moreover from A5 A6 have "∃u∈X. ∀y∈A. ⟨y,u⟩ ∈ r"

using def_of_strict_ver by auto

moreover note A1 A3 A4

ultimately have II: "?x ∈ X" "∀y∈A. ⟨y,?x⟩ ∈ r"

using Order_ZF_5_L7 by auto

then have III: "∃x∈X. ∀y∈A. ⟨y,x⟩ ∈ r" by auto

from A5 I II have "?x ∈ X" "∀y∈A. ⟨?x,y⟩ ∉ s"

using geq_impl_not_less by auto

moreover from A1 A2 A3 A4 A5 III have

"∀y∈X. ⟨y,?x⟩ ∈ s --> (∃z∈A. ⟨y,z⟩ ∈ s)"

using def_of_strict_ver Order_ZF_5_L8 by simp

ultimately show

"∃x∈X. ( ∀y∈A. ⟨x,y⟩ ∉ s ) ∧ (∀y∈X. ⟨y,x⟩ ∈ s --> (∃z∈A. ⟨y,z⟩ ∈ s))"

by auto

qed

text{*Strict version of a relation on a set is a relation on that

set.*}

lemma strict_ver_rel: assumes A1: "r ⊆ A×A"

shows "StrictVersion(r) ⊆ A×A"

using assms StrictVersion_def by auto;

end