Theory Order_ZF

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

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

theory Order_ZF imports Fol1 

begin

text{*This theory file considers various notion related to order. We redefine
  the notions of a 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 that finite sets are bounded in Finite\_ZF.thy.*}

section{*Definitions*}

text{*In this section we formulate the definitions related to order 
  relations.*}

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. The sets that are bounded below and 
  above are also defined, as are bounded sets. Empty sets are defined as 
  bounded.
  The notation for the definition of an interval may be mysterious for some
  readers, see @{text "Order_ZF_2_L1"} for more intuitive notation. 
  We aslo define the maximum (the greater of) two elemnts and the minmum 
  (the smaller of) two elements. 
  We say that a set has a maximum (minimum) if it has an element that is 
  not smaller (not greater, resp.) that any other one. We show that
  under some conditions this element of the set is unique (if exists).
  The element with this
  property is called the maximum (minimum) of the set.
  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\}$. 
  Infimum is defined analogously. Recall that
  @{text "r-``(A)"}=$\{ x: \langle x,y\rangle\in r$ for some $y\in A$ 
  is the inverse image of the set $A$ by relation $r$. 
  We define a (order) relation to be complete if every nonempty bounded
  above set has a supremum. This terminolgy may conflict with the one
  for complete metric space. We will worry about that when we actually
  define a complete metric space.*}

constdefs 

  IsTotal (infixl "{is total on}" 65)
  "r {is total on} X ≡ (∀a∈X.∀b∈X. <a,b> ∈ r ∨ <b,a> ∈ r)"

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

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

  "IsBoundedAbove(A,r) ≡ ( A=0 ∨ (∃u. ∀x∈A. <x,u> ∈ r))"

  "IsBoundedBelow(A,r) ≡ (A=0 ∨ (∃l. ∀x∈A. <l,x> ∈ r))"

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

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

  "GreaterOf(r,a,b) ≡ (if <a,b> ∈ r then b else a)"

  "SmallerOf(r,a,b) ≡ (if <a,b> ∈ r then a else b)"

  "HasAmaximum(r,A) ≡ ∃M∈A.∀x∈A. <x,M> ∈ r"

  "HasAminimum(r,A) ≡ ∃m∈A.∀x∈A. <m,x> ∈ r"

  "Maximum(r,A) ≡ THE M. M∈A ∧ (∀x∈A. <x,M> ∈ r)"

  "Minimum(r,A) ≡ THE m. m∈A ∧ (∀x∈A. <m,x> ∈ r)"

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

  "Infimum(r,A) ≡ Maximum(r,\<Inter>a∈A. r-``{a})"

  (*IsComplete ("_ {is complete}")
  "r {is complete} ≡ 
  ∀A. IsBoundedAbove(A,r) ∧ A≠0 --> (∃s. s = Supremum(r,A))" wrong definition*)

  IsComplete ("_ {is complete}")
  "r {is complete} ≡ 
  ∀A. IsBoundedAbove(A,r) ∧ A≠0 --> HasAminimum(r,\<Inter>a∈A. r``{a})";

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 prems 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 prems 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 prems 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 prems 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 prems IsTotal_def by auto;

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 prems IsTotal_def by auto;

section{*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 @{text "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 prems  Order_ZF_2_L1 by auto;

text{*@{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 prems 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 prems refl_def Order_ZF_2_L1 by auto;

text{*Under the assumptions of @{text "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 prems 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)"
  from A1 have "trans(r)" .
  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);
  from A1 have "trans(r)" .
  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 (rule ccontr);
  assume "Interval(r,a,b)≠0" then obtain x where "x ∈ Interval(r,a,b)"
    by auto;
  with A1 A2 show False using Order_ZF_2_L1A Fol1_L3 by fast;
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 prems Interval_def by auto;

section{*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 prems 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 prems 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 prems 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 prems 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 (cases "x∈A");
    assume "x∈A"
    with A4 T1 have "<x,u> ∈ r ∧ <u,?v> ∈ r" by simp
    with A2 show "⟨x,?v⟩ ∈ r" by (rule Fol1_L3);
  next assume "x∉A" 
    with A5 A4 T2 have "<x,w> ∈ r ∧ <w,?v> ∈ r" by simp;
    with A2 show "⟨x,?v⟩ ∈ r" by (rule Fol1_L3);
  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 (cases "A=0 ∨ B=0");
  assume "A=0 ∨ B=0" 
  with A3 show ?thesis by auto;
next 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 show "IsBoundedAbove(A∪B,r)"
    using IsBoundedAbove_def 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 prems 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 (cases "x∈A");
    assume "x∈A"
    with A4 T1 have "<?k,l> ∈ r ∧ <l,x> ∈ r" by simp
    with A2 show "⟨?k,x⟩ ∈ r" by (rule Fol1_L3);
  next assume "x∉A" 
    with A5 A4 T2 have "<?k,m> ∈ r ∧ <m,x> ∈ r" by simp;
    with A2 show "⟨?k,x⟩ ∈ r" by (rule Fol1_L3);
  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 (cases "A=0 ∨ B=0");
  assume "A=0 ∨ B=0" 
  with A3 show ?thesis by auto;
next 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 show "IsBoundedBelow(A∪B,r)"
    using IsBoundedBelow_def 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 prems 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 prems 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 prems 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 "IsBoundedBelow(A,r)" and "B⊆A"
  shows "IsBoundedBelow(B,r)"
  using prems IsBoundedBelow_def by auto;

text{*A subset of a set that is bounded above is bounded above.*}

lemma Order_ZF_3_L13: assumes "IsBoundedAbove(A,r)" and "B⊆A"
  shows "IsBoundedAbove(B,r)"
  using prems IsBoundedAbove_def by auto;


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

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 (cases "A=0")
  assume "A=0" 
  then show "IsBounded({x∈A. ⟨x,a⟩ ∈ r},r)"
    using IsBoundedBelow_def IsBoundedAbove_def IsBounded_def
    by auto;
next 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 show "IsBounded({x∈A. ⟨x,a⟩ ∈ r},r)" 
    using Order_ZF_3_L15 IsBounded_def by simp;
qed;

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 Finite\_ZF.thy) 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 prems 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 prems 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 prems 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 prems 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 prems 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 prems 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 prems 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.*}

constdefs
  "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 prems 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 prems 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 prems StrictVersion_def by auto;


end