IsarMathLib

Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

theory Order_ZF_1 imports ZF.Order ZF1
begin

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.

Definitions and basic properties

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

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

\( R \text{ orders } A \equiv \forall x y z.\ (x\in A \wedge y\in A \wedge z\in A) \longrightarrow \) \( (\langle x,y\rangle \in R \longleftrightarrow \neg (x=y \vee \langle y,x\rangle \in R)) \wedge \) \( (\langle x,y\rangle \in R \wedge \langle y,z\rangle \in R \longrightarrow \langle x,z\rangle \in R) \)

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

definition

\( \text{Sup}(B,A,R) \equiv \) \( \bigcup \{x \in A.\ (\forall y\in B.\ \langle x,y\rangle \notin R) \wedge \) \( (\forall y\in A.\ \langle y,x\rangle \in R \longrightarrow (\exists z\in B.\ \langle y,z\rangle \in R))\} \)

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

definition

\( \text{Infim}(B,A,R) \equiv \text{Sup}(B,A,converse(R)) \)

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 \text{ orders } A \)

shows \( ir\text{refl}(A,R) \), \( trans[A](R) \), \( part\_ord(A,R) \), \( linear(A,R) \), \( tot\_ord(A,R) \)proof
from A1 have I: \( \forall x y z.\ (x\in A \wedge y\in A \wedge z\in A) \longrightarrow \) \( (\langle x,y\rangle \in R \longleftrightarrow \neg (x=y \vee \langle y,x\rangle \in R)) \wedge \) \( (\langle x,y\rangle \in R \wedge \langle y,z\rangle \in R \longrightarrow \langle x,z\rangle \in R) \) unfolding StrictOrder_def
then have \( \forall x\in A.\ \langle x,x\rangle \notin R \)
then show \( ir\text{refl}(A,R) \) using irrefl_def
moreover
from I have \( \forall x\in A.\ \forall y\in A.\ \forall z\in A.\ \langle x,y\rangle \in R \longrightarrow \langle y,z\rangle \in R \longrightarrow \langle x,z\rangle \in R \)
then show \( trans[A](R) \) unfolding trans_on_def
ultimately show \( part\_ord(A,R) \) using part_ord_def
moreover
from I have \( \forall x\in A.\ \forall y\in A.\ \langle x,y\rangle \in R \vee x=y \vee \langle y,x\rangle \in R \)
then show \( linear(A,R) \) unfolding linear_def
ultimately show \( tot\_ord(A,R) \) using tot_ord_def
qed

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 \text{ orders } A \)proof
from A1 have I: \( linear(A,R) \) and II: \( ir\text{refl}(A,R) \) and III: \( trans[A](R) \) and IV: \( part\_ord(A,R) \) using tot_ord_def, part_ord_def
from IV have \( asym(R \cap A\times A) \) using part_ord_Imp_asym
then have V: \( \forall x y.\ \langle x,y\rangle \in (R \cap A\times A) \longrightarrow \neg (\langle y,x\rangle \in (R \cap A\times A)) \) unfolding asym_def
from I have VI: \( \forall x\in A.\ \forall y\in A.\ \langle x,y\rangle \in R \vee x=y \vee \langle y,x\rangle \in R \) unfolding linear_def
from III have VII: \( \forall x\in A.\ \forall y\in A.\ \forall z\in A.\ \langle x,y\rangle \in R \longrightarrow \langle y,z\rangle \in R \longrightarrow \langle x,z\rangle \in R \) unfolding trans_on_def
{
fix \( x \) \( y \) \( z \)
assume T: \( x\in A \), \( y\in A \), \( z\in A \)
have \( \langle x,y\rangle \in R \longleftrightarrow \neg (x=y \vee \langle y,x\rangle \in R) \)proof
assume A2: \( \langle x,y\rangle \in R \)
with V, T have \( \neg (\langle y,x\rangle \in R) \)
moreover
from II, T, A2 have \( x\neq y \) using irrefl_def
ultimately show \( \neg (x=y \vee \langle y,x\rangle \in R) \)
next
assume \( \neg (x=y \vee \langle y,x\rangle \in R) \)
with VI, T show \( \langle x,y\rangle \in R \)
qed
moreover
from VII, T have \( \langle x,y\rangle \in R \wedge \langle y,z\rangle \in R \longrightarrow \langle x,z\rangle \in R \)
ultimately have \( (\langle x,y\rangle \in R \longleftrightarrow \neg (x=y \vee \langle y,x\rangle \in R)) \wedge \) \( (\langle x,y\rangle \in R \wedge \langle y,z\rangle \in R \longrightarrow \langle x,z\rangle \in R) \)
}
then have \( \forall x y z.\ (x\in A \wedge y\in A \wedge z\in A) \longrightarrow \) \( (\langle x,y\rangle \in R \longleftrightarrow \neg (x=y \vee \langle y,x\rangle \in R)) \wedge \) \( (\langle x,y\rangle \in R \wedge \langle y,z\rangle \in R \longrightarrow \langle x,z\rangle \in R) \)
then show \( R \text{ orders } A \) using StrictOrder_def
qed

Properties of (strict) total orders

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.

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 \text{ orders } A \longleftrightarrow converse(R) \text{ orders } A \)proof
let \( r = converse(R) \)
assume \( R \text{ orders } A \)
then have \( tot\_ord(A,r) \) using orders_imp_tot_ord, tot_ord_converse
then show \( r \text{ orders } A \) using tot_ord_imp_orders
next
let \( r = converse(R) \)
assume \( r \text{ orders } A \)
then have A2: \( \forall x y z.\ (x\in A \wedge y\in A \wedge z\in A) \longrightarrow \) \( (\langle x,y\rangle \in r \longleftrightarrow \neg (x=y \vee \langle y,x\rangle \in r)) \wedge \) \( (\langle x,y\rangle \in r \wedge \langle y,z\rangle \in r \longrightarrow \langle x,z\rangle \in r) \) using StrictOrder_def
{
fix \( x \) \( y \) \( z \)
assume \( x\in A \wedge y\in A \wedge z\in A \)
with A2 have I: \( \langle y,x\rangle \in r \longleftrightarrow \neg (x=y \vee \langle x,y\rangle \in r) \) and II: \( \langle y,x\rangle \in r \wedge \langle z,y\rangle \in r \longrightarrow \langle z,x\rangle \in r \)
from I have \( \langle x,y\rangle \in R \longleftrightarrow \neg (x=y \vee \langle y,x\rangle \in R) \)
moreover
from II have \( \langle x,y\rangle \in R \wedge \langle y,z\rangle \in R \longrightarrow \langle x,z\rangle \in R \)
ultimately have \( (\langle x,y\rangle \in R \longleftrightarrow \neg (x=y \vee \langle y,x\rangle \in R)) \wedge \) \( (\langle x,y\rangle \in R \wedge \langle y,z\rangle \in R \longrightarrow \langle x,z\rangle \in R) \)
}
then have \( \forall x y z.\ (x\in A \wedge y\in A \wedge z\in A) \longrightarrow \) \( (\langle x,y\rangle \in R \longleftrightarrow \neg (x=y \vee \langle y,x\rangle \in R)) \wedge \) \( (\langle x,y\rangle \in R \wedge \langle y,z\rangle \in R \longrightarrow \langle x,z\rangle \in R) \)
then show \( R \text{ orders } A \) using StrictOrder_def
qed

Supremum is unique, if it exists.

lemma supeu:

assumes A1: \( R \text{ orders } A \) and A2: \( x\in A \) and A3: \( \forall y\in B.\ \langle x,y\rangle \notin R \) and A4: \( \forall y\in A.\ \langle y,x\rangle \in R \longrightarrow ( \exists z\in B.\ \langle y,z\rangle \in R) \)

shows \( \exists !x.\ x\in A\wedge (\forall y\in B.\ \langle x,y\rangle \notin R) \wedge (\forall y\in A.\ \langle y,x\rangle \in R \longrightarrow ( \exists z\in B.\ \langle y,z\rangle \in R)) \)proof
from A2, A3, A4 show \( \exists x.\ x\in A\wedge (\forall y\in B.\ \langle x,y\rangle \notin R) \wedge (\forall y\in A.\ \langle y,x\rangle \in R \longrightarrow ( \exists z\in B.\ \langle y,z\rangle \in R)) \)
next
fix \( x_1 \) \( x_2 \)
assume A5: \( x_1 \in A \wedge (\forall y\in B.\ \langle x_1,y\rangle \notin R) \wedge (\forall y\in A.\ \langle y,x_1\rangle \in R \longrightarrow ( \exists z\in B.\ \langle y,z\rangle \in R)) \), \( x_2 \in A \wedge (\forall y\in B.\ \langle x_2,y\rangle \notin R) \wedge (\forall y\in A.\ \langle y,x_2\rangle \in R \longrightarrow ( \exists z\in B.\ \langle y,z\rangle \in R)) \)
from A1 have \( linear(A,R) \) using orders_imp_tot_ord, tot_ord_def
then have \( \forall x\in A.\ \forall y\in A.\ \langle x,y\rangle \in R \vee x=y \vee \langle y,x\rangle \in R \) unfolding linear_def
with A5 have \( \langle x_1,x_2\rangle \in R \vee x_1=x_2 \vee \langle x_2,x_1\rangle \in R \)
moreover {
assume \( \langle x_1,x_2\rangle \in R \)
with A5 obtain \( z \) where \( z\in B \) and \( \langle x_1,z\rangle \in R \)
with A5 have \( False \)
} moreover {
assume \( \langle x_2,x_1\rangle \in R \)
with A5 obtain \( z \) where \( z\in B \) and \( \langle x_2,z\rangle \in R \)
with A5 have \( False \)
} ultimately show \( x_1 = x_2 \)
qed

Supremum has expected properties if it exists.

lemma sup_props:

assumes A1: \( R \text{ orders } A \) and A2: \( \exists x\in A.\ (\forall y\in B.\ \langle x,y\rangle \notin R) \wedge (\forall y\in A.\ \langle y,x\rangle \in R \longrightarrow ( \exists z\in B.\ \langle y,z\rangle \in R)) \)

shows \( \text{Sup}(B,A,R) \in A \), \( \forall y\in B.\ \langle \text{Sup}(B,A,R),y\rangle \notin R \), \( \forall y\in A.\ \langle y, \text{Sup}(B,A,R)\rangle \in R \longrightarrow ( \exists z\in B.\ \langle y,z\rangle \in R ) \)proof
let \( S = \{x\in A.\ (\forall y\in B.\ \langle x,y\rangle \notin R) \wedge (\forall y\in A.\ \langle y,x\rangle \in R \longrightarrow ( \exists z\in B.\ \langle y,z\rangle \in R ) ) \} \)
from A2 obtain \( x \) where \( x\in A \) and \( (\forall y\in B.\ \langle x,y\rangle \notin R) \) and \( \forall y\in A.\ \langle y,x\rangle \in R \longrightarrow ( \exists z\in B.\ \langle y,z\rangle \in R) \)
with A1 have I: \( \exists !x.\ x\in A\wedge (\forall y\in B.\ \langle x,y\rangle \notin R) \wedge (\forall y\in A.\ \langle y,x\rangle \in R \longrightarrow ( \exists z\in B.\ \langle y,z\rangle \in R)) \) using supeu
then have \( ( \bigcup S ) \in A \) by (rule ZF1_1_L9 )
then show \( \text{Sup}(B,A,R) \in A \) using Sup_def
from I have II: \( (\forall y\in B.\ \langle \bigcup S ,y\rangle \notin R) \wedge (\forall y\in A.\ \langle y,\bigcup S\rangle \in R \longrightarrow ( \exists z\in B.\ \langle y,z\rangle \in R)) \) by (rule ZF1_1_L9 )
hence \( \forall y\in B.\ \langle \bigcup S,y\rangle \notin R \)
moreover
have III: \( (\bigcup S) = \text{Sup}(B,A,R) \) using Sup_def
ultimately show \( \forall y\in B.\ \langle \text{Sup}(B,A,R),y\rangle \notin R \)
from II have IV: \( \forall y\in A.\ \langle y,\bigcup S\rangle \in R \longrightarrow ( \exists z\in B.\ \langle y,z\rangle \in R) \)
{
fix \( y \)
assume A3: \( y\in A \) and \( \langle y, \text{Sup}(B,A,R)\rangle \in R \)
with III have \( \langle y,\bigcup S\rangle \in R \)
with IV, A3 have \( \exists z\in B.\ \langle y,z\rangle \in R \)
}
thus \( \forall y\in A.\ \langle y, \text{Sup}(B,A,R)\rangle \in R \longrightarrow ( \exists z\in B.\ \langle y,z\rangle \in R ) \)
qed

Elements greater or equal than any element of \(B\) are greater or equal than supremum of \(B\).

lemma supnub:

assumes A1: \( R \text{ orders } A \) and A2: \( \exists x\in A.\ (\forall y\in B.\ \langle x,y\rangle \notin R) \wedge (\forall y\in A.\ \langle y,x\rangle \in R \longrightarrow ( \exists z\in B.\ \langle y,z\rangle \in R)) \) and A3: \( c \in A \) and A4: \( \forall z\in B.\ \langle c,z\rangle \notin R \)

shows \( \langle c, \text{Sup}(B,A,R)\rangle \notin R \)proof
from A1, A2 have \( \forall y\in A.\ \langle y, \text{Sup}(B,A,R)\rangle \in R \longrightarrow ( \exists z\in B.\ \langle y,z\rangle \in R ) \) by (rule sup_props )
with A3, A4 show \( \langle c, \text{Sup}(B,A,R)\rangle \notin R \)
qed
end
Definition of StrictOrder: \( R \text{ orders } A \equiv \forall x y z.\ (x\in A \wedge y\in A \wedge z\in A) \longrightarrow \) \( (\langle x,y\rangle \in R \longleftrightarrow \neg (x=y \vee \langle y,x\rangle \in R)) \wedge \) \( (\langle x,y\rangle \in R \wedge \langle y,z\rangle \in R \longrightarrow \langle x,z\rangle \in R) \)
lemma orders_imp_tot_ord:

assumes \( R \text{ orders } A \)

shows \( ir\text{refl}(A,R) \), \( trans[A](R) \), \( part\_ord(A,R) \), \( linear(A,R) \), \( tot\_ord(A,R) \)
lemma tot_ord_imp_orders:

assumes \( tot\_ord(A,R) \)

shows \( R \text{ orders } A \)
lemma supeu:

assumes \( R \text{ orders } A \) and \( x\in A \) and \( \forall y\in B.\ \langle x,y\rangle \notin R \) and \( \forall y\in A.\ \langle y,x\rangle \in R \longrightarrow ( \exists z\in B.\ \langle y,z\rangle \in R) \)

shows \( \exists !x.\ x\in A\wedge (\forall y\in B.\ \langle x,y\rangle \notin R) \wedge (\forall y\in A.\ \langle y,x\rangle \in R \longrightarrow ( \exists z\in B.\ \langle y,z\rangle \in R)) \)
lemma ZF1_1_L9:

assumes \( \exists ! x.\ x\in A \wedge \phi (x) \)

shows \( \exists a.\ \{x\in A.\ \phi (x)\} = \{a\} \), \( \bigcup \{x\in A.\ \phi (x)\} \in A \), \( \phi (\bigcup \{x\in A.\ \phi (x)\}) \)
Definition of Sup: \( \text{Sup}(B,A,R) \equiv \) \( \bigcup \{x \in A.\ (\forall y\in B.\ \langle x,y\rangle \notin R) \wedge \) \( (\forall y\in A.\ \langle y,x\rangle \in R \longrightarrow (\exists z\in B.\ \langle y,z\rangle \in R))\} \)
lemma sup_props:

assumes \( R \text{ orders } A \) and \( \exists x\in A.\ (\forall y\in B.\ \langle x,y\rangle \notin R) \wedge (\forall y\in A.\ \langle y,x\rangle \in R \longrightarrow ( \exists z\in B.\ \langle y,z\rangle \in R)) \)

shows \( \text{Sup}(B,A,R) \in A \), \( \forall y\in B.\ \langle \text{Sup}(B,A,R),y\rangle \notin R \), \( \forall y\in A.\ \langle y, \text{Sup}(B,A,R)\rangle \in R \longrightarrow ( \exists z\in B.\ \langle y,z\rangle \in R ) \)