# IsarMathLib

## A library of formalized mathematics for Isabelle/ZF theorem proving environment

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)$$
10
6
3
3