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 x⇩1 x⇩2
assume A5:
"x⇩1 ∈ A ∧ (∀y∈B. ⟨x⇩1,y⟩ ∉ R) ∧ (∀y∈A. ⟨y,x⇩1⟩ ∈ R ⟶ ( ∃z∈B. ⟨y,z⟩ ∈ R))"
"x⇩2 ∈ A ∧ (∀y∈B. ⟨x⇩2,y⟩ ∉ R) ∧ (∀y∈A. ⟨y,x⇩2⟩ ∈ 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 "⟨x⇩1,x⇩2⟩ ∈ R ∨ x⇩1=x⇩2 ∨ ⟨x⇩2,x⇩1⟩ ∈ R" by blast
moreover
{ assume "⟨x⇩1,x⇩2⟩ ∈ R"
with A5 obtain z where "z∈B" and "⟨x⇩1,z⟩ ∈ R" by auto
with A5 have False by auto }
moreover
{ assume "⟨x⇩2,x⇩1⟩ ∈ R"
with A5 obtain z where "z∈B" and "⟨x⇩2,z⟩ ∈ R" by auto
with A5 have False by auto }
ultimately show "x⇩1 = x⇩2" 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