Theory Order_ZF_1

theory Order_ZF_1
imports Order ZF1
(*   This file is a part of IsarMathLib - 
    a library of formalized mathematics for Isabelle/Isar.

    Copyright (C) 2005, 2006, 2007  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 ‹More on order relations›

theory Order_ZF_1 imports ZF.Order ZF1

begin

text‹In ‹Order_ZF› we define some notions related to order relations
  based on the nonstrict orders ($\leq $ type). Some people however prefer to talk
  about these notions in terms of the strict order relation ($<$ type). 
  This is the case for the standard Isabelle ‹Order.thy› and also for 
  Metamath. In this theory file we repeat some developments from ‹Order_ZF›
  using the strict order relation as a basis.This is mostly useful for Metamath 
  translation, but is also of some general interest. The names of theorems are 
  copied from Metamath.›


subsection‹Definitions and basic properties›

text‹In this section we introduce some definitions taken from Metamath and relate 
  them to the ones used by the standard Isabelle ‹Order.thy›.
›

text‹The next definition is the strict version of the linear order.
  What we write as ‹R Orders A› is written $R Ord A$ in Metamath.
›

definition
StrictOrder (infix "Orders" 65) where
  "R Orders A ≡ ∀x y z. (x∈A ∧ y∈A ∧ z∈A) ⟶ 
  (⟨x,y⟩ ∈ R ⟷ ¬(x=y ∨ ⟨y,x⟩ ∈ R)) ∧ 
  (⟨x,y⟩ ∈ R ∧ ⟨y,z⟩ ∈ R ⟶ ⟨x,z⟩ ∈ R)"

text‹The definition of supremum for a (strict) linear order.›

definition
  "Sup(B,A,R) ≡ 
  ⋃ {x ∈ A. (∀y∈B. ⟨x,y⟩ ∉ R) ∧ 
  (∀y∈A. ⟨y,x⟩ ∈ R ⟶ (∃z∈B. ⟨y,z⟩ ∈ R))}"

text‹Definition of infimum for a linear order. 
  It is defined in terms of supremum.›

definition
  "Infim(B,A,R) ≡ Sup(B,A,converse(R))"

text‹If relation $R$ orders a set $A$, (in Metamath sense) then $R$ 
  is irreflexive, transitive and linear therefore is a total order on $A$ 
  (in Isabelle sense).›

lemma orders_imp_tot_ord: assumes A1: "R Orders A"
  shows 
  "irrefl(A,R)"
  "trans[A](R)"
  "part_ord(A,R)"
  "linear(A,R)"
  "tot_ord(A,R)"
proof -
  from A1 have I:
    "∀x y z. (x∈A ∧ y∈A ∧ z∈A) ⟶ 
    (⟨x,y⟩ ∈ R ⟷ ¬(x=y ∨ ⟨y,x⟩ ∈ R)) ∧ 
    (⟨x,y⟩ ∈ R ∧ ⟨y,z⟩ ∈ R ⟶ ⟨x,z⟩ ∈ R)"
    unfolding StrictOrder_def by simp
  then have "∀x∈A. ⟨x,x⟩ ∉ R" by blast
  then show "irrefl(A,R)" using irrefl_def by simp
  moreover
  from I have 
    "∀x∈A. ∀y∈A. ∀z∈A. ⟨x,y⟩ ∈ R ⟶ ⟨y,z⟩ ∈ R ⟶ ⟨x,z⟩ ∈ R"
    by blast
  then show "trans[A](R)" unfolding trans_on_def by blast
  ultimately show "part_ord(A,R)" using part_ord_def
    by simp
  moreover
  from I have
    "∀x∈A. ∀y∈A. ⟨x,y⟩ ∈ R ∨ x=y ∨ ⟨y,x⟩ ∈ R"
    by blast
  then show "linear(A,R)" unfolding linear_def by blast
  ultimately show "tot_ord(A,R)" using tot_ord_def
    by simp
qed

text‹A converse of ‹orders_imp_tot_ord›. Together with that
  theorem this shows that Metamath's notion of an order relation is equivalent to
  Isabelles ‹tot_ord› predicate.›

lemma tot_ord_imp_orders: assumes A1: "tot_ord(A,R)"
  shows "R Orders A"
proof -
  from A1 have 
    I: "linear(A,R)" and  
    II: "irrefl(A,R)" and 
    III: "trans[A](R)" and
    IV: "part_ord(A,R)"
    using tot_ord_def part_ord_def by auto
  from IV have "asym(R ∩ A×A)"
    using part_ord_Imp_asym by simp
  then have V: "∀x y. ⟨x,y⟩ ∈ (R ∩ A×A) ⟶ ¬(⟨y,x⟩ ∈ (R ∩ A×A))"
    unfolding asym_def by blast
  from I have VI: "∀x∈A. ∀y∈A. ⟨x,y⟩ ∈ R ∨ x=y ∨ ⟨y,x⟩ ∈ R"
    unfolding linear_def by blast
  from III have VII:
    "∀x∈A. ∀y∈A. ∀z∈A. ⟨x,y⟩ ∈ R ⟶ ⟨y,z⟩ ∈ R ⟶ ⟨x,z⟩ ∈ R"
    unfolding trans_on_def by blast
  { fix x y z
    assume T: "x∈A" "y∈A" "z∈A"
    have "⟨x,y⟩ ∈ R ⟷ ¬(x=y ∨ ⟨y,x⟩ ∈ R)"
    proof
      assume A2: "⟨x,y⟩ ∈ R"
      with V T have  "¬(⟨y,x⟩ ∈ R)" by blast
      moreover from II T A2 have "x≠y" using irrefl_def
	by auto
      ultimately show "¬(x=y ∨ ⟨y,x⟩ ∈ R)" by simp
    next assume  "¬(x=y ∨ ⟨y,x⟩ ∈ R)"
      with VI T show "⟨x,y⟩ ∈ R" by auto
    qed
    moreover from VII T have
      "⟨x,y⟩ ∈ R ∧ ⟨y,z⟩ ∈ R ⟶ ⟨x,z⟩ ∈ R"
      by blast
    ultimately have "(⟨x,y⟩ ∈ R ⟷ ¬(x=y ∨ ⟨y,x⟩ ∈ R)) ∧ 
      (⟨x,y⟩ ∈ R ∧ ⟨y,z⟩ ∈ R ⟶ ⟨x,z⟩ ∈ R)"
      by simp
  } then have "∀x y z. (x∈A ∧ y∈A ∧ z∈A) ⟶ 
      (⟨x,y⟩ ∈ R ⟷ ¬(x=y ∨ ⟨y,x⟩ ∈ R)) ∧ 
      (⟨x,y⟩ ∈ R ∧ ⟨y,z⟩ ∈ R ⟶ ⟨x,z⟩ ∈ R)"
    by auto
  then show "R Orders A" using StrictOrder_def by simp
qed
    
subsection‹Properties of (strict) total orders›

text‹In this section we discuss the properties of strict order relations. 
  This continues the development contained in the standard Isabelle's 
  ‹Order.thy› with a view towards using the theorems 
  translated from Metamath.›

text‹A relation orders a set iff the converse relation orders a set. Going
  one way we can use the the lemma ‹tot_od_converse› from the standard 
  Isabelle's ‹Order.thy›.The other way is a bit more complicated (note that
  in Isabelle for ‹converse(converse(r)) = r› one needs $r$ to consist
  of ordered pairs, which does not follow from the ‹StrictOrder› 
  definition above).›

lemma cnvso: shows "R Orders A ⟷ converse(R) Orders A"
proof
  let ?r = "converse(R)"
  assume "R Orders A"
  then have "tot_ord(A,?r)" using orders_imp_tot_ord tot_ord_converse
    by simp
  then show "?r Orders A" using tot_ord_imp_orders
    by simp
next
  let ?r = "converse(R)"
  assume "?r Orders A"
  then have A2: "∀x y z. (x∈A ∧ y∈A ∧ z∈A) ⟶ 
    (⟨x,y⟩ ∈ ?r ⟷ ¬(x=y ∨ ⟨y,x⟩ ∈ ?r)) ∧ 
    (⟨x,y⟩ ∈ ?r ∧ ⟨y,z⟩ ∈ ?r ⟶ ⟨x,z⟩ ∈ ?r)"
    using StrictOrder_def by simp
  { fix x y z
    assume "x∈A ∧ y∈A ∧ z∈A"
    with A2 have
      I: "⟨y,x⟩ ∈ ?r ⟷ ¬(x=y ∨ ⟨x,y⟩ ∈ ?r)" and
      II: "⟨y,x⟩ ∈ ?r ∧ ⟨z,y⟩ ∈ ?r ⟶ ⟨z,x⟩ ∈ ?r"
      by auto
    from I have "⟨x,y⟩ ∈ R ⟷ ¬(x=y ∨ ⟨y,x⟩ ∈ R)"
      by auto
    moreover from II have "⟨x,y⟩ ∈ R ∧ ⟨y,z⟩ ∈ R ⟶ ⟨x,z⟩ ∈ R"
      by auto
    ultimately have "(⟨x,y⟩ ∈ R ⟷ ¬(x=y ∨ ⟨y,x⟩ ∈ R)) ∧ 
      (⟨x,y⟩ ∈ R ∧ ⟨y,z⟩ ∈ R ⟶ ⟨x,z⟩ ∈ R)" by simp
  } then have  "∀x y z. (x∈A ∧ y∈A ∧ z∈A) ⟶ 
      (⟨x,y⟩ ∈ R ⟷ ¬(x=y ∨ ⟨y,x⟩ ∈ R)) ∧ 
      (⟨x,y⟩ ∈ R ∧ ⟨y,z⟩ ∈ R ⟶ ⟨x,z⟩ ∈ R)"
    by auto
  then show "R Orders A" using StrictOrder_def by simp
qed

text‹Supremum is unique, if it exists.›

lemma supeu: assumes A1: "R Orders A" and A2: "x∈A" and
  A3: "∀y∈B. ⟨x,y⟩ ∉ R" and A4: "∀y∈A. ⟨y,x⟩ ∈ R  ⟶ ( ∃z∈B. ⟨y,z⟩ ∈ R)"
   shows 
  "∃!x. x∈A∧(∀y∈B. ⟨x,y⟩ ∉ R) ∧ (∀y∈A. ⟨y,x⟩ ∈ R ⟶ ( ∃z∈B. ⟨y,z⟩ ∈ R))"
proof
  from A2 A3 A4 show
    "∃ x. x∈A∧(∀y∈B. ⟨x,y⟩ ∉ R) ∧ (∀y∈A. ⟨y,x⟩ ∈ R ⟶ ( ∃z∈B. ⟨y,z⟩ ∈ R))"
    by auto
next fix x1 x2
  assume A5:
    "x1 ∈ A ∧ (∀y∈B. ⟨x1,y⟩ ∉ R) ∧ (∀y∈A. ⟨y,x1⟩ ∈ R ⟶ ( ∃z∈B. ⟨y,z⟩ ∈ R))"
    "x2 ∈ A ∧ (∀y∈B. ⟨x2,y⟩ ∉ R) ∧ (∀y∈A. ⟨y,x2⟩ ∈ R ⟶ ( ∃z∈B. ⟨y,z⟩ ∈ R))"
  from A1 have "linear(A,R)" using orders_imp_tot_ord tot_ord_def
    by simp
  then have "∀x∈A. ∀y∈A. ⟨x,y⟩ ∈ R ∨ x=y ∨ ⟨y,x⟩ ∈ R"
    unfolding linear_def by blast
  with A5 have "⟨x1,x2⟩ ∈ R ∨ x1=x2 ∨ ⟨x2,x1⟩ ∈ R" by blast
  moreover 
  { assume "⟨x1,x2⟩ ∈ R"
    with A5 obtain z where "z∈B" and "⟨x1,z⟩ ∈ R" by auto
    with A5 have False by auto }
  moreover
  { assume "⟨x2,x1⟩ ∈ R"
    with A5 obtain z where "z∈B" and "⟨x2,z⟩ ∈ R" by auto
    with A5 have False by auto }
  ultimately  show "x1 = x2" by auto
qed

text‹Supremum has expected properties if it exists.›

lemma sup_props: assumes A1: "R Orders A" and 
  A2: "∃x∈A. (∀y∈B. ⟨x,y⟩ ∉ R) ∧ (∀y∈A. ⟨y,x⟩ ∈ R ⟶ ( ∃z∈B. ⟨y,z⟩ ∈ R))"
  shows 
  "Sup(B,A,R) ∈ A"
  "∀y∈B. ⟨Sup(B,A,R),y⟩ ∉ R"
  "∀y∈A. ⟨y,Sup(B,A,R)⟩ ∈ R ⟶ ( ∃z∈B. ⟨y,z⟩ ∈ R )"
proof -
  let ?S = "{x∈A. (∀y∈B. ⟨x,y⟩ ∉ R) ∧ (∀y∈A. ⟨y,x⟩ ∈ R ⟶ ( ∃z∈B. ⟨y,z⟩ ∈ R ) ) }"
  from A2 obtain x where 
    "x∈A" and "(∀y∈B. ⟨x,y⟩ ∉ R)" and "∀y∈A. ⟨y,x⟩ ∈ R ⟶ ( ∃z∈B. ⟨y,z⟩ ∈ R)"
    by auto
  with A1 have I:
    "∃!x. x∈A∧(∀y∈B. ⟨x,y⟩ ∉ R) ∧ (∀y∈A. ⟨y,x⟩ ∈ R ⟶ ( ∃z∈B. ⟨y,z⟩ ∈ R))"
    using supeu by simp
  then have "( ⋃?S ) ∈ A" by (rule ZF1_1_L9)
  then show "Sup(B,A,R) ∈ A" using Sup_def by simp
  from I have II:
    "(∀y∈B. ⟨⋃?S ,y⟩ ∉ R) ∧ (∀y∈A. ⟨y,⋃?S⟩ ∈ R ⟶ ( ∃z∈B. ⟨y,z⟩ ∈ R))"
    by (rule ZF1_1_L9)
  hence "∀y∈B. ⟨⋃?S,y⟩ ∉ R" by blast
  moreover have III: "(⋃?S) = Sup(B,A,R)" using Sup_def by simp
  ultimately show "∀y∈B. ⟨Sup(B,A,R),y⟩ ∉ R" by simp
  from II have IV: "∀y∈A. ⟨y,⋃?S⟩ ∈ R ⟶ ( ∃z∈B. ⟨y,z⟩ ∈ R)"
    by blast
  { fix y assume A3: "y∈A" and "⟨y,Sup(B,A,R)⟩ ∈ R"
    with III have "⟨y,⋃?S⟩ ∈ R" by simp
    with IV A3 have "∃z∈B. ⟨y,z⟩ ∈ R" by blast
  } thus  "∀y∈A. ⟨y,Sup(B,A,R)⟩ ∈ R ⟶ ( ∃z∈B. ⟨y,z⟩ ∈ R )"
    by simp
qed

text‹Elements greater or equal than any element of $B$ are 
  greater or equal than supremum of $B$.›

lemma supnub: assumes A1: "R Orders A" and A2: 
  "∃x∈A. (∀y∈B. ⟨x,y⟩ ∉ R) ∧ (∀y∈A. ⟨y,x⟩ ∈ R ⟶ ( ∃z∈B. ⟨y,z⟩ ∈ R))"
  and A3: "c ∈ A" and A4: "∀z∈B. ⟨c,z⟩ ∉ R"
  shows "⟨c, Sup(B,A,R)⟩ ∉ R"
proof -
  from A1 A2 have
    "∀y∈A. ⟨y,Sup(B,A,R)⟩ ∈ R ⟶ ( ∃z∈B. ⟨y,z⟩ ∈ R )"
    by (rule sup_props)
  with A3 A4 show "⟨c, Sup(B,A,R)⟩ ∉ R" by auto
qed

end