header{*\isaheader{Order\_ZF\_1.thy}*}
theory Order_ZF_1 imports Order ZF1
begin
text{*In @{text "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 @{text "Order.thy"} and also for
Metamath. In this theory file we repeat some developments from @{text "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.*}
section{*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 @{text "Order.thy"}.
*}
text{* The next definition is th strict version of the linear order.
What we write as @{text "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) ≡
\<Union> {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 @{text "orders_imp_tot_ord"}. Together with that
theorem this shows that Metamath's notion of an order relation is equivalent to
Isabelles @{text "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;
section{*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
@{text "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 @{text "tot_od_converse"} from the standard
Isabelle's @{text "Order.thy"}.The other way is a bit more complicated (note that
in Isabelle for @{text "converse(converse(r)) = r"} one needs $r$ to consist
of ordered pairs, which does not follow from the @{text "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 "( \<Union>?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. ⟨\<Union>?S ,y⟩ ∉ R) ∧ (∀y∈A. ⟨y,\<Union>?S⟩ ∈ R --> ( ∃z∈B. ⟨y,z⟩ ∈ R))"
by (rule ZF1_1_L9);
hence "∀y∈B. ⟨\<Union>?S,y⟩ ∉ R" by blast;
moreover have III: "(\<Union>?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,\<Union>?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,\<Union>?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