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.

If \(a,b\) are natural numbers then \(a\) is less or equal \(b\) or \(b\) is (strictly) less than \(a\). We use a result on ordinals in the proof.

lemma nat_order_2cases:

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

shows \( a \leq b \vee b \lt 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 \lt a \) using le_iff
qed

A special case of nat_order_2cases: If \(a,b\) are natural numbers then \(a\) is less or equal \(b\) or \(b\) is less or equal than \(a\).

lemma NatOrder_ZF_1_L1:

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

shows \( a \leq b \vee b \leq a \) using assms, nat_order_2cases, leI

\(\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
lemma nat_order_2cases:

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

shows \( a \leq b \vee b \lt a \)
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) \)