Theory Order_ZF

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

    Copyright (C) 2005 - 2022  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.

*)

section ‹Order relations - introduction›

theory Order_ZF imports Fol1

begin

text‹This theory file considers various notion related to order. We redefine
  the notions of a preorder, directed set, total order, linear order and partial order to have the 
  same terminology as Wikipedia (I found it very consistent across different 
  areas of math). We also define and study the notions of intervals and bounded
  sets. We show the inclusion relations between the intervals with endpoints
  being in certain order. We also show that union of bounded sets are bounded. 
  This allows to show in ‹Finite_ZF.thy› that finite sets are bounded.›

subsection‹Definitions›

text‹In this section we formulate the definitions related to order 
  relations.›

text‹A relation $r$ is ''total'' on a set $X$ if for all elements 
  $a,b$ of $X$ we have $a$ is in relation with $b$ or $b$ is in relation
  with $a$. An example is the $\leq $ relation on numbers.
›

definition
  IsTotal (infixl "{is total on}" 65) where
  "r {is total on} X ≡ (∀a∈X.∀b∈X. ⟨ a,b⟩ ∈ r ∨ ⟨ b,a⟩ ∈ r)"

text‹A relation $r$ is a partial order on $X$ if it is reflexive on $X$
  (i.e. $\langle x,x \rangle$ for every $x\in X$), antisymmetric 
  (if $\langle x, y\rangle \in r $ and $\langle y, x\rangle \in r $, then
  $x=y$) and transitive $\langle x, y\rangle \in r $ and 
  $\langle y, z\rangle \in r $ implies $\langle x, z\rangle \in r $). 
›

definition
  "IsPartOrder(X,r) ≡ refl(X,r) ∧ antisym(r) ∧ trans(r)"

text‹A relation that is reflexive and transitive is called a ‹preorder›.›

definition
  "IsPreorder(X,r) ≡ refl(X,r) ∧ trans(r)"

text‹We say that a relation $r$ up-directs a set
  if every two-element subset of $X$ has an upper bound. ›

definition
  UpDirects ("_ {up-directs} _" 90)
  where "r {up-directs} X ≡ X≠0 ∧ (∀x∈X.∀y∈X.∃z∈X. ⟨x,z⟩ ∈ r ∧ ⟨y,z⟩ ∈ r)"

text‹Analogously we say that a relation $r$ down-directs a set
  if every two-element subset of $X$ has a lower bound. ›

definition
  DownDirects ("_ {down-directs} _" 90)
  where "r {down-directs} X ≡ X≠0 ∧ (∀x∈X.∀y∈X.∃z∈X. ⟨z,x⟩ ∈ r ∧ ⟨z,y⟩ ∈ r)"

text‹Typically the notion that is actually defined is the notion of a ‹directed set›. 
  or an ‹upward directed set›, rather than $r$ down-directs $X$ (or $r$ up-directs $X$). 
  This is a nonempty set $X$ together which a preorder $r$ 
  such that $r$ up-directs $X$. We set that up in separate definitions as we sometimes want to
  use an upward or downward directed set with a partial order rather than a preorder. ›

definition
  "IsUpDirectedSet(X,r) ≡  IsPreorder(X,r) ∧ (r {up-directs} X)"

text‹We define the notion of a ‹downward directed set› analogously.›

definition
  "IsDownDirectedSet(X,r) ≡ IsPreorder(X,r) ∧ (r {down-directs} X)"

text‹We define a linear order as a binary relation that is antisymmetric, 
  transitive and total. Note that this terminology is different than the
  one used the standard Order.thy file.›

definition
  "IsLinOrder(X,r) ≡ antisym(r) ∧ trans(r) ∧ (r {is total on} X)"

text‹A set is bounded above if there is that is an upper
  bound for it,  i.e. there are some $u$ such that 
  $\langle x, u\rangle \in r$ for all $x\in A$. 
  In addition, the empty set is defined as bounded.›

definition
  "IsBoundedAbove(A,r) ≡ ( A=0 ∨ (∃u. ∀x∈A. ⟨ x,u⟩ ∈ r))"

text‹We define sets bounded below analogously.›

definition
  "IsBoundedBelow(A,r) ≡ (A=0 ∨ (∃l. ∀x∈A. ⟨ l,x⟩ ∈ r))"

text‹A set is bounded if it is bounded below and above.›

definition
  "IsBounded(A,r) ≡ (IsBoundedAbove(A,r) ∧ IsBoundedBelow(A,r))"

text‹The notation for the definition of an interval may be mysterious for some
  readers, see lemma ‹Order_ZF_2_L1› for more intuitive notation.›

definition
  "Interval(r,a,b) ≡ r``{a} ∩ r-``{b}"

text‹We also define the maximum (the greater of) two elemnts 
  in the obvious way.›

definition
  "GreaterOf(r,a,b) ≡ (if ⟨ a,b⟩ ∈ r then b else a)"

text‹The definition a a minimum (the smaller of) two elements.›

definition
  "SmallerOf(r,a,b) ≡ (if ⟨ a,b⟩ ∈ r then a else b)"

text‹We say that a set has a maximum if it has an element that is 
  not smaller that any other one. We show that
  under some conditions this element of the set is unique (if exists).›

definition
  "HasAmaximum(r,A) ≡ ∃M∈A.∀x∈A. ⟨x,M⟩ ∈ r"

text‹A similar definition what it means that a set has a minimum.›

definition
  "HasAminimum(r,A) ≡ ∃m∈A.∀x∈A. ⟨m,x⟩ ∈ r"

text‹Definition of the maximum of a set.›

definition
  "Maximum(r,A) ≡ THE M. M∈A ∧ (∀x∈A. ⟨x,M⟩ ∈ r)"

text‹Definition of a minimum of a set.›

definition
  "Minimum(r,A) ≡ THE m. m∈A ∧ (∀x∈A. ⟨m,x⟩ ∈ r)"

text‹The supremum of a set $A$ is defined as the minimum of the set of
  upper bounds, i.e. the set 
  $\{u.\forall_{a\in A} \langle a,u\rangle \in r\}=\bigcap_{a\in A} r\{a\}$. 
   Recall that in Isabelle/ZF
  ‹r-``(A)› denotes the inverse image of the set $A$ by relation $r$
  (i.e. ‹r-``(A)›=$\{ x: \langle x,y\rangle\in r$ for some $y\in A\}$).›

definition
  "Supremum(r,A) ≡ Minimum(r,⋂a∈A. r``{a})"

text‹ The notion of "having a supremum" is the same as the set of upper bounds having a
  minimum, but having it a a separate notion does simplify notation in some cases.
  The definition is written in terms of 
  images of singletons $\{ x\}$ under relation. To understand this formulation note
  that the set of upper bounds of a set $A\subseteq X$ is 
  $\bigcap_{x\in A}\{ y\in X | \langle x,y\rangle \in r \}$, which is the same
  as $\bigcap_{x\in A} r(\{ x \})$, where $r(\{ x \})$ is the image of the singleton $\{ x\}$ under
  relation $r$. ›

definition
  "HasAsupremum(r,A) ≡ HasAminimum(r,⋂a∈A. r``{a})"

text‹ The notion of "having an infimum" is the same as the set of lower bounds having a
  maximum. ›

definition
  "HasAnInfimum(r,A) ≡ HasAmaximum(r,⋂a∈A. r-``{a})"


text‹Infimum is defined analogously.›

definition
  "Infimum(r,A) ≡ Maximum(r,⋂a∈A. r-``{a})"

text‹We define a relation to be complete if every nonempty bounded
  above set has a supremum.›

definition
  IsComplete ("_ {is complete}") where
  "r {is complete} ≡ 
  ∀A. IsBoundedAbove(A,r) ∧ A≠0 ⟶ HasAminimum(r,⋂a∈A. r``{a})"

text‹If a relation down-directs a set, then a larger one does as well.›

lemma down_dir_mono: assumes "r {down-directs} X" "r⊆R"
  shows "R {down-directs} X" using assms unfolding DownDirects_def
  by blast

text‹If a relation up-directs a set, then a larger one does as well.›

lemma up_dir_mono: assumes "r {up-directs} X" "r⊆R"
  shows "R {up-directs} X" using assms unfolding UpDirects_def
  by blast

text‹The essential condition to show that a total relation is reflexive.›

lemma Order_ZF_1_L1: assumes "r {is total on} X" and "a∈X"
  shows "⟨a,a⟩ ∈ r" using assms IsTotal_def by auto

text‹A total relation is reflexive.›

lemma total_is_refl:
  assumes "r {is total on} X"
  shows "refl(X,r)" using assms Order_ZF_1_L1 refl_def by simp

text‹A linear order is partial order.›

lemma Order_ZF_1_L2: assumes "IsLinOrder(X,r)" 
  shows "IsPartOrder(X,r)" 
  using assms IsLinOrder_def IsPartOrder_def refl_def Order_ZF_1_L1
  by auto

text‹Partial order that is total is linear.›

lemma Order_ZF_1_L3: 
  assumes "IsPartOrder(X,r)" and "r {is total on} X"
  shows "IsLinOrder(X,r)"
  using assms IsPartOrder_def IsLinOrder_def
  by simp

text‹Relation that is total on a set is total on any subset.›

lemma Order_ZF_1_L4: assumes "r {is total on} X" and "A⊆X"
  shows "r {is total on} A"
  using assms IsTotal_def by auto

text‹We can restrict a partial order relation to the domain. ›

lemma part_ord_restr: assumes "IsPartOrder(X,r)"
  shows "IsPartOrder(X,r ∩ X×X)"
  using assms unfolding IsPartOrder_def refl_def antisym_def trans_def by auto

text‹ We can restrict a total order relation to the domain. ›

lemma total_ord_restr: assumes "r {is total on} X"
  shows "(r ∩ X×X) {is total on} X"
  using assms unfolding IsTotal_def by auto

text‹A linear relation is linear on any subset and we can restrict it to any subset.›

lemma ord_linear_subset: assumes  "IsLinOrder(X,r)" and "A⊆X"
  shows  "IsLinOrder(A,r)" and  "IsLinOrder(A,r ∩ A×A)"
proof -
  from assms show "IsLinOrder(A,r)" using IsLinOrder_def Order_ZF_1_L4 by blast
  then have "IsPartOrder(A,r ∩ A×A)" and "(r ∩ A×A) {is total on} A"
    using Order_ZF_1_L2 part_ord_restr total_ord_restr unfolding IsLinOrder_def 
    by auto
  then show "IsLinOrder(A,r ∩ A×A)" using Order_ZF_1_L3 by simp
qed

text‹If the relation is total, then every set is a union of those elements
  that are nongreater than a given one and nonsmaller than a given one.›

lemma Order_ZF_1_L5: 
  assumes "r {is total on} X" and "A⊆X" and "a∈X"
  shows "A = {x∈A. ⟨x,a⟩ ∈ r} ∪ {x∈A. ⟨a,x⟩ ∈ r}"
  using assms IsTotal_def by auto

text‹A technical fact about reflexive relations.›

lemma refl_add_point: 
  assumes "refl(X,r)" and "A ⊆ B ∪ {x}" and "B ⊆ X" and
  "x ∈ X" and "∀y∈B. ⟨y,x⟩ ∈ r"
  shows "∀a∈A. ⟨a,x⟩ ∈ r"
  using assms refl_def by auto
  
subsection‹Intervals›

text‹In this section we discuss intervals.›

text‹The next lemma explains the notation of the definition of an interval.›

lemma Order_ZF_2_L1: 
  shows "x ∈ Interval(r,a,b) ⟷ ⟨ a,x⟩ ∈ r ∧ ⟨ x,b⟩ ∈ r"
  using Interval_def by auto

text‹Since there are some problems with applying the above lemma 
  (seems that simp and auto don't handle equivalence very well), we
  split ‹Order_ZF_2_L1› into two lemmas.›

lemma Order_ZF_2_L1A: assumes "x ∈ Interval(r,a,b)"
  shows "⟨ a,x⟩ ∈ r"  "⟨ x,b⟩ ∈ r"
  using assms  Order_ZF_2_L1 by auto

text‹ ‹Order_ZF_2_L1›, implication from right to left.›

lemma Order_ZF_2_L1B: assumes "⟨ a,x⟩ ∈ r"  "⟨ x,b⟩ ∈ r"
  shows "x ∈ Interval(r,a,b)"
  using assms Order_ZF_2_L1 by simp

text‹If the relation is reflexive, the endpoints belong to the interval.›

lemma Order_ZF_2_L2: assumes "refl(X,r)" 
  and "a∈X"  "b∈X" and "⟨ a,b⟩ ∈ r"
  shows 
  "a ∈ Interval(r,a,b)"  
  "b ∈ Interval(r,a,b)"  
  using assms refl_def Order_ZF_2_L1 by auto

text‹Under the assumptions of ‹Order_ZF_2_L2›, the interval is 
  nonempty.›

lemma Order_ZF_2_L2A: assumes "refl(X,r)" 
  and "a∈X"  "b∈X" and "⟨ a,b⟩ ∈ r"
  shows "Interval(r,a,b) ≠ 0"
proof -
  from assms have "a ∈ Interval(r,a,b)"
    using Order_ZF_2_L2 by simp
  then show "Interval(r,a,b) ≠ 0" by auto
qed

text‹If $a,b,c,d$ are in this order, then $[b,c]\subseteq [a,d]$. We
  only need trasitivity for this to be true.›

lemma Order_ZF_2_L3: 
  assumes A1: "trans(r)" and A2:"⟨ a,b⟩∈r"  "⟨ b,c⟩∈r"  "⟨ c,d⟩∈r"
shows "Interval(r,b,c) ⊆ Interval(r,a,d)"
proof
  fix x assume A3: "x ∈ Interval(r, b, c)"
  note A1
  moreover from A2 A3 have "⟨ a,b⟩ ∈ r ∧ ⟨ b,x⟩ ∈ r" using Order_ZF_2_L1A
    by simp
  ultimately have T1: "⟨ a,x⟩ ∈ r" by (rule Fol1_L3)
  note A1
  moreover from A2 A3 have "⟨ x,c⟩ ∈ r ∧ ⟨ c,d⟩ ∈ r" using Order_ZF_2_L1A
    by simp
  ultimately have "⟨ x,d⟩ ∈ r" by (rule Fol1_L3)
  with T1 show "x ∈ Interval(r,a,d)" using Order_ZF_2_L1B
    by simp
qed

text‹For reflexive and antisymmetric relations the interval with equal 
  endpoints consists only of that endpoint.›

lemma Order_ZF_2_L4: 
  assumes A1: "refl(X,r)" and A2: "antisym(r)" and A3: "a∈X"
  shows "Interval(r,a,a) = {a}"
proof
  from A1 A3 have "⟨ a,a⟩ ∈ r" using refl_def by simp
  with A1 A3 show "{a} ⊆ Interval(r,a,a)" using Order_ZF_2_L2 by simp
  from A2 show "Interval(r,a,a) ⊆ {a}" using Order_ZF_2_L1A Fol1_L4
    by fast
qed

text‹For transitive relations the endpoints have to be in the relation for
  the interval to be nonempty.›

lemma Order_ZF_2_L5: assumes A1: "trans(r)" and A2: "⟨ a,b⟩ ∉ r"
  shows "Interval(r,a,b) = 0"
proof -
  { assume "Interval(r,a,b)≠0" then obtain x where "x ∈ Interval(r,a,b)"
    by auto
  with A1 A2 have False using Order_ZF_2_L1A Fol1_L3 by fast
  } thus ?thesis by auto
qed

text‹If a relation is defined on a set, then intervals are subsets of that
  set.›

lemma Order_ZF_2_L6: assumes A1: "r ⊆ X×X"
  shows "Interval(r,a,b) ⊆ X"
  using assms Interval_def by auto

subsection‹Bounded sets›

text‹In this section we consider properties of bounded sets.›

text‹For reflexive relations singletons are bounded.›

lemma Order_ZF_3_L1: assumes "refl(X,r)" and "a∈X"
  shows "IsBounded({a},r)"
  using assms refl_def IsBoundedAbove_def IsBoundedBelow_def
    IsBounded_def by auto

text‹Sets that are bounded above are contained in the domain of 
  the relation.›

lemma Order_ZF_3_L1A: assumes "r ⊆ X×X" 
  and "IsBoundedAbove(A,r)"
  shows "A⊆X" using assms IsBoundedAbove_def by auto

text‹Sets that are bounded below are contained in the domain of 
  the relation.›

lemma Order_ZF_3_L1B: assumes "r ⊆ X×X" 
  and "IsBoundedBelow(A,r)"
  shows "A⊆X" using assms IsBoundedBelow_def by auto

text‹For a total relation, the greater of two elements, 
  as defined above, is indeed greater of any of the two.›

lemma Order_ZF_3_L2: assumes "r {is total on} X"
  and "x∈X" "y∈X"
  shows 
  "⟨x,GreaterOf(r,x,y)⟩ ∈ r" 
  "⟨y,GreaterOf(r,x,y)⟩ ∈ r"
  "⟨SmallerOf(r,x,y),x⟩ ∈ r" 
  "⟨SmallerOf(r,x,y),y⟩ ∈ r"
  using assms IsTotal_def Order_ZF_1_L1 GreaterOf_def SmallerOf_def
  by auto

text‹If $A$ is bounded above by $u$, $B$ is bounded above by $w$,
  then $A\cup B$ is bounded above by the greater of $u,w$.›

lemma Order_ZF_3_L2B:  
  assumes A1: "r {is total on} X" and A2: "trans(r)"
  and A3: "u∈X" "w∈X" 
  and A4: "∀x∈A. ⟨ x,u⟩ ∈ r" "∀x∈B. ⟨ x,w⟩ ∈ r"
  shows "∀x∈A∪B. ⟨x,GreaterOf(r,u,w)⟩ ∈ r"
proof
  let ?v = "GreaterOf(r,u,w)"
  from A1 A3 have T1: "⟨ u,?v⟩ ∈ r" and T2: "⟨ w,?v⟩ ∈ r"
    using Order_ZF_3_L2 by auto
  fix x assume A5: "x∈A∪B" show "⟨x,?v⟩ ∈ r"
  proof -
    { assume "x∈A"
    with A4 T1 have "⟨ x,u⟩ ∈ r ∧ ⟨ u,?v⟩ ∈ r" by simp
    with A2 have "⟨x,?v⟩ ∈ r" by (rule Fol1_L3) }
  moreover
  { assume "x∉A" 
    with A5 A4 T2 have "⟨ x,w⟩ ∈ r ∧ ⟨ w,?v⟩ ∈ r" by simp
    with A2 have "⟨x,?v⟩ ∈ r" by (rule Fol1_L3) }
  ultimately show ?thesis by auto
  qed
qed

text‹For total and transitive relation the union of two sets bounded 
  above is bounded above.›

lemma Order_ZF_3_L3: 
  assumes A1: "r {is total on} X" and A2: "trans(r)"
  and A3: "IsBoundedAbove(A,r)" "IsBoundedAbove(B,r)"
  and A4: "r ⊆ X×X"
  shows "IsBoundedAbove(A∪B,r)"
proof -
  { assume "A=0 ∨ B=0" 
    with A3 have "IsBoundedAbove(A∪B,r)" by auto }
  moreover
  { assume "¬ (A = 0 ∨ B = 0)"
    then have T1: "A≠0" "B≠0" by auto
    with A3 obtain u w where D1: "∀x∈A. ⟨ x,u⟩ ∈ r" "∀x∈B. ⟨ x,w⟩ ∈ r"
      using IsBoundedAbove_def by auto
    let ?U = "GreaterOf(r,u,w)"
    from T1 A4 D1 have "u∈X" "w∈X" by auto
    with A1 A2 D1 have "∀x∈A∪B.⟨ x,?U⟩ ∈ r"
      using Order_ZF_3_L2B by blast
    then have "IsBoundedAbove(A∪B,r)"
      using IsBoundedAbove_def by auto }
  ultimately show ?thesis by auto
qed
  
text‹For total and transitive relations if a set $A$ is bounded above then 
  $A\cup \{a\}$ is bounded above.›

lemma Order_ZF_3_L4: 
  assumes A1: "r {is total on} X" and A2: "trans(r)"
  and A3: "IsBoundedAbove(A,r)" and A4: "a∈X" and A5: "r ⊆ X×X"
  shows "IsBoundedAbove(A∪{a},r)"
proof -
  from A1 have "refl(X,r)"
    using total_is_refl by simp
  with assms show ?thesis using
    Order_ZF_3_L1 IsBounded_def Order_ZF_3_L3 by simp
qed

text‹If $A$ is bounded below by $l$, $B$ is bounded below by $m$,
  then $A\cup B$ is bounded below by the smaller of $u,w$.›

lemma Order_ZF_3_L5B:  
  assumes A1: "r {is total on} X" and A2: "trans(r)"
  and A3: "l∈X" "m∈X" 
  and A4: "∀x∈A. ⟨ l,x⟩ ∈ r" "∀x∈B. ⟨ m,x⟩ ∈ r"
  shows "∀x∈A∪B. ⟨SmallerOf(r,l,m),x⟩ ∈ r"
proof
  let ?k = "SmallerOf(r,l,m)"
  from A1 A3 have T1: "⟨ ?k,l⟩ ∈ r" and T2: "⟨ ?k,m⟩ ∈ r"
    using Order_ZF_3_L2 by auto
  fix x assume A5: "x∈A∪B" show "⟨?k,x⟩ ∈ r"
  proof -
    { assume "x∈A"
      with A4 T1 have "⟨ ?k,l⟩ ∈ r ∧ ⟨ l,x⟩ ∈ r" by simp
      with A2 have "⟨?k,x⟩ ∈ r" by (rule Fol1_L3) }
    moreover
    { assume "x∉A" 
      with A5 A4 T2 have "⟨ ?k,m⟩ ∈ r ∧ ⟨ m,x⟩ ∈ r" by simp
      with A2 have "⟨?k,x⟩ ∈ r" by (rule Fol1_L3) }
    ultimately show ?thesis by auto
  qed
qed

text‹For total and transitive relation the union of two sets bounded 
  below is bounded below.›

lemma Order_ZF_3_L6: 
  assumes A1: "r {is total on} X" and A2: "trans(r)"
  and A3: "IsBoundedBelow(A,r)" "IsBoundedBelow(B,r)"
  and A4: "r ⊆ X×X"
  shows "IsBoundedBelow(A∪B,r)"
proof -
  { assume "A=0 ∨ B=0" 
    with A3 have ?thesis by auto }
  moreover
  { assume "¬ (A = 0 ∨ B = 0)"
    then have T1: "A≠0" "B≠0" by auto
    with A3 obtain l m where D1: "∀x∈A. ⟨ l,x⟩ ∈ r" "∀x∈B. ⟨ m,x⟩ ∈ r"
      using IsBoundedBelow_def by auto
    let ?L = "SmallerOf(r,l,m)"
    from T1 A4 D1 have T1: "l∈X" "m∈X" by auto
    with A1 A2 D1 have "∀x∈A∪B.⟨ ?L,x⟩ ∈ r"
      using Order_ZF_3_L5B by blast
    then have "IsBoundedBelow(A∪B,r)"
      using IsBoundedBelow_def by auto }
  ultimately show ?thesis by auto
qed

text‹For total and transitive relations if a set $A$ is bounded below then 
  $A\cup \{a\}$ is bounded below.›

lemma Order_ZF_3_L7:
  assumes A1: "r {is total on} X" and A2: "trans(r)"
  and A3: "IsBoundedBelow(A,r)" and A4: "a∈X" and A5: "r ⊆ X×X"
  shows "IsBoundedBelow(A∪{a},r)"
proof -
  from A1 have "refl(X,r)"
    using total_is_refl by simp
  with assms show ?thesis using
    Order_ZF_3_L1 IsBounded_def Order_ZF_3_L6 by simp
qed

text‹For total and transitive relations unions of two bounded sets are 
  bounded.›

theorem Order_ZF_3_T1: 
  assumes "r {is total on} X" and "trans(r)" 
  and "IsBounded(A,r)" "IsBounded(B,r)"
  and "r ⊆ X×X"
  shows "IsBounded(A∪B,r)"
  using assms Order_ZF_3_L3 Order_ZF_3_L6 Order_ZF_3_L7 IsBounded_def
  by simp

text‹For total and transitive relations if a set $A$ is bounded then 
  $A\cup \{a\}$ is bounded.›

lemma Order_ZF_3_L8: 
  assumes "r {is total on} X" and "trans(r)"
  and "IsBounded(A,r)" and "a∈X" and "r ⊆ X×X"
  shows "IsBounded(A∪{a},r)"
  using assms total_is_refl Order_ZF_3_L1 Order_ZF_3_T1 by blast

text‹A sufficient condition for a set to be bounded below.›

lemma Order_ZF_3_L9: assumes A1: "∀a∈A. ⟨l,a⟩ ∈ r"
  shows "IsBoundedBelow(A,r)"
proof -
  from A1 have "∃l. ∀x∈A. ⟨l,x⟩ ∈ r"
    by auto
  then show "IsBoundedBelow(A,r)"
    using IsBoundedBelow_def by simp
qed

text‹A sufficient condition for a set to be bounded above.›

lemma Order_ZF_3_L10: assumes A1: "∀a∈A. ⟨a,u⟩ ∈ r"
  shows "IsBoundedAbove(A,r)"
proof -
  from A1 have "∃u. ∀x∈A. ⟨x,u⟩ ∈ r"
    by auto
  then show "IsBoundedAbove(A,r)"
    using IsBoundedAbove_def by simp
qed

text‹Intervals are bounded.›
(*proof that uses Order_ZF_3_L9 and Order_ZF_3_L10 and is not shorter *)
lemma Order_ZF_3_L11: shows 
  "IsBoundedAbove(Interval(r,a,b),r)"
  "IsBoundedBelow(Interval(r,a,b),r)"
  "IsBounded(Interval(r,a,b),r)"
proof -
  { fix x assume "x ∈ Interval(r,a,b)" 
    then have "⟨ x,b⟩ ∈ r"  "⟨ a,x⟩ ∈ r" 
      using Order_ZF_2_L1A by auto
  } then have 
      "∃u. ∀x∈Interval(r,a,b). ⟨ x,u⟩ ∈ r" 
      "∃l. ∀x∈Interval(r,a,b). ⟨ l,x⟩ ∈ r"
    by auto
  then show 
    "IsBoundedAbove(Interval(r,a,b),r)"
    "IsBoundedBelow(Interval(r,a,b),r)"
    "IsBounded(Interval(r,a,b),r)"
    using IsBoundedAbove_def IsBoundedBelow_def IsBounded_def
    by auto
qed

text‹A subset of a set that is bounded below is bounded below.›

lemma Order_ZF_3_L12: assumes A1: "IsBoundedBelow(A,r)" and A2: "B⊆A"
  shows "IsBoundedBelow(B,r)"
proof -
  { assume "A = 0"
    with assms have "IsBoundedBelow(B,r)" 
      using IsBoundedBelow_def by auto }
  moreover
  { assume "A ≠ 0"
    with A1 have "∃l. ∀x∈A. ⟨l,x⟩ ∈ r"
      using IsBoundedBelow_def by simp
    with A2 have "∃l.∀x∈B. ⟨l,x⟩ ∈ r" by auto
    then have "IsBoundedBelow(B,r)" using IsBoundedBelow_def
      by auto }
  ultimately show "IsBoundedBelow(B,r)" by auto
qed

text‹A subset of a set that is bounded above is bounded above.›

lemma Order_ZF_3_L13: assumes A1: "IsBoundedAbove(A,r)" and A2: "B⊆A"
  shows "IsBoundedAbove(B,r)"
proof -
  { assume "A = 0"
    with assms have "IsBoundedAbove(B,r)" 
      using IsBoundedAbove_def by auto }
  moreover
  { assume "A ≠ 0"
    with A1 have "∃u. ∀x∈A. ⟨x,u⟩ ∈ r"
      using IsBoundedAbove_def by simp
    with A2 have "∃u.∀x∈B. ⟨x,u⟩ ∈ r" by auto
    then have "IsBoundedAbove(B,r)" using IsBoundedAbove_def
      by auto }
  ultimately show "IsBoundedAbove(B,r)" by auto
qed

text‹If for every element of $X$ we can find one in $A$ 
  that is greater, then the $A$ can not be bounded above.
  Works for relations that are total, transitive and antisymmetric,
  (i.e. for linear order relations).›

lemma Order_ZF_3_L14:  
  assumes A1: "r {is total on} X" 
  and A2: "trans(r)" and A3: "antisym(r)"
  and A4: "r ⊆ X×X" and A5: "X≠0" 
  and A6: "∀x∈X. ∃a∈A. x≠a ∧ ⟨x,a⟩ ∈ r"
  shows "¬IsBoundedAbove(A,r)"
proof -
  { from A5 A6 have I: "A≠0" by auto
    moreover assume "IsBoundedAbove(A,r)"
    ultimately obtain u where II: "∀x∈A. ⟨ x,u⟩ ∈ r"
      using IsBounded_def IsBoundedAbove_def by auto
    with A4 I have "u∈X" by auto
    with A6 obtain b where "b∈A" and III: "u≠b" and "⟨u,b⟩ ∈ r"
      by auto
    with II have "⟨b,u⟩ ∈ r"  "⟨u,b⟩ ∈ r" by auto
    with A3 have "b=u" by (rule Fol1_L4)
    with III have False by simp
  } thus "¬IsBoundedAbove(A,r)" by auto
qed

text‹The set of elements in a set $A$ that are nongreater than 
  a given element is bounded above.›

lemma Order_ZF_3_L15: shows "IsBoundedAbove({x∈A. ⟨x,a⟩ ∈ r},r)"
  using IsBoundedAbove_def by auto

text‹If $A$ is bounded below, then the set of elements in a set $A$ 
  that are nongreater than a given element is bounded.›

lemma Order_ZF_3_L16: assumes A1: "IsBoundedBelow(A,r)"
  shows "IsBounded({x∈A. ⟨x,a⟩ ∈ r},r)"
proof -
  { assume "A=0" 
    then have "IsBounded({x∈A. ⟨x,a⟩ ∈ r},r)"
      using IsBoundedBelow_def IsBoundedAbove_def IsBounded_def
      by auto }
  moreover
  { assume "A≠0"
    with A1 obtain l where I: "∀x∈A. ⟨l,x⟩ ∈ r"
      using IsBoundedBelow_def by auto
    then have "∀y∈{x∈A. ⟨x,a⟩ ∈ r}. ⟨l,y⟩ ∈ r" by simp
    then have "IsBoundedBelow({x∈A. ⟨x,a⟩ ∈ r},r)"
      by (rule Order_ZF_3_L9)
    then have "IsBounded({x∈A. ⟨x,a⟩ ∈ r},r)" 
      using Order_ZF_3_L15 IsBounded_def by simp }
  ultimately show ?thesis by blast
qed

end