IsarMathLib

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

theory NatOrder_ZF imports Nat_ZF_IML Order_ZF
begin

This theory proves that \(\leq\) is a linear order on \(\mathbb{N}\). \(\leq\) is defined in Isabelle's Nat theory, and linear order is defined in Order_ZF theory. Contributed by Seo Sanghyeon.

Order on natural numbers

This is the only section in this theory.

To prove that \(\leq\) is a total order, we use a result on ordinals.

lemma NatOrder_ZF_1_L1:

assumes \( a\in nat \) and \( b\in nat \)

shows \( a \leq b \vee b \leq a \)proof
from assms have I: \( Ord(a) \wedge Ord(b) \) using nat_into_Ord
then have \( a \in b \vee a = b \vee b \in a \) using Ord_linear
with I have \( a \lt b \vee a = b \vee b \lt a \) using ltI
with I show \( a \leq b \vee b \leq a \) using le_iff
qed

\(\leq\) is antisymmetric, transitive, total, and linear. Proofs by rewrite using definitions.

lemma NatOrder_ZF_1_L2:

shows \( \text{antisym}(Le) \), \( \text{trans}(Le) \), \( Le \text{ is total on } nat \), \( \text{IsLinOrder}(nat,Le) \)proof
show \( \text{antisym}(Le) \) using antisym_def, Le_def, le_anti_sym
moreover
show \( \text{trans}(Le) \) using trans_def, Le_def, le_trans
moreover
show \( Le \text{ is total on } nat \) using IsTotal_def, Le_def, NatOrder_ZF_1_L1
ultimately show \( \text{IsLinOrder}(nat,Le) \) using IsLinOrder_def
qed

The order on natural numbers is linear on every natural number. Recall that each natural number is a subset of the set of all natural numbers (as well as a member).

lemma natord_lin_on_each_nat:

assumes A1: \( n \in nat \)

shows \( \text{IsLinOrder}(n,Le) \)proof
from A1 have \( n \subseteq nat \) using nat_subset_nat
then show \( thesis \) using NatOrder_ZF_1_L2, ord_linear_subset
qed
end
Definition of IsTotal: \( r \text{ is total on } X \equiv (\forall a\in X.\ \forall b\in X.\ \langle a,b\rangle \in r \vee \langle b,a\rangle \in r) \)
lemma NatOrder_ZF_1_L1:

assumes \( a\in nat \) and \( b\in nat \)

shows \( a \leq b \vee b \leq a \)
Definition of IsLinOrder: \( \text{IsLinOrder}(X,r) \equiv \text{antisym}(r) \wedge \text{trans}(r) \wedge (r \text{ is total on } X) \)
lemma nat_subset_nat:

assumes \( n \in nat \)

shows \( n \subseteq nat \)
lemma NatOrder_ZF_1_L2: shows \( \text{antisym}(Le) \), \( \text{trans}(Le) \), \( Le \text{ is total on } nat \), \( \text{IsLinOrder}(nat,Le) \)
lemma ord_linear_subset:

assumes \( \text{IsLinOrder}(X,r) \) and \( A\subseteq X \)

shows \( \text{IsLinOrder}(A,r) \) and \( \text{IsLinOrder}(A,r \cap A\times A) \)