IsarMathLib

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

theory Enumeration_ZF imports NatOrder_ZF FiniteSeq_ZF FinOrd_ZF
begin

Suppose \(r\) is a linear order on a set \(A\) that has \(n\) elements, where \(n \in\mathbb{N}\) . In the FinOrd_ZF theory we prove a theorem stating that there is a unique order isomorphism between \(n = \{0,1,..,n-1\}\) (with natural order) and \(A\). Another way of stating that is that there is a unique way of counting the elements of \(A\) in the order increasing according to relation \(r\). Yet another way of stating the same thing is that there is a unique sorted list of elements of \(A\). We will call this list the Enumeration of \(A\).

Enumerations: definition and notation

In this section we introduce the notion of enumeration and define a proof context (a ''locale'' in Isabelle terms) that sets up the notation for writing about enumarations.

We define enumeration as the only order isomorphism beween a set \(A\) and the number of its elements. We are using the formula \(\bigcup \{x\} = x\) to extract the only element from a singleton. Le is the (natural) order on natural numbers, defined is Nat_ZF theory in the standard Isabelle library.

definition

\( \text{Enumeration}(A,r) \equiv \bigcup ord\_iso(|A|,Le,A,r) \)

To set up the notation we define a locale enums. In this locale we will assume that \(r\) is a linear order on some set \(X\). In most applications this set will be just the set of natural numbers. Standard Isabelle uses \(\leq \) to denote the "less or equal" relation on natural numbers. We will use the \( \leq \) symbol to denote the relation \(r\). Those two symbols usually look the same in the presentation, but they are different in the source.To shorten the notation the enumeration \( \text{Enumeration}(A,r) \) will be denoted as \(\sigma (A)\). Similarly as in the Semigroup theory we will write \(a\hookleftarrow x\) for the result of appending an element \(x\) to the finite sequence (list) \(a\). Finally, \(a\sqcup b\) will denote the concatenation of the lists \(a\) and \(b\).

locale enums

assumes linord: \( \text{IsLinOrder}(X,r) \)

defines \( x \leq y \equiv \langle x,y\rangle \in r \)

defines \( \sigma (A) \equiv \text{Enumeration}(A,r) \)

defines \( a \hookleftarrow x \equiv \text{Append}(a,x) \)

defines \( a \sqcup b \equiv \text{Concat}(a,b) \)

Properties of enumerations

In this section we prove basic facts about enumerations.

A special case of the existence and uniqueess of the order isomorphism for finite sets when the first set is a natural number.

lemma (in enums) ord_iso_nat_fin:

assumes \( A \in \text{FinPow}(X) \) and \( n \in nat \) and \( A \approx n \)

shows \( \exists !f.\ f \in ord\_iso(n,Le,A,r) \) using assms, NatOrder_ZF_1_L2, linord, nat_finpow_nat, fin_ord_iso_ex_uniq

An enumeration is an order isomorhism, a bijection, and a list.

lemma (in enums) enum_props:

assumes \( A \in \text{FinPow}(X) \)

shows \( \sigma (A) \in ord\_iso(|A|,Le, A,r) \), \( \sigma (A) \in \text{bij}(|A|,A) \), \( \sigma (A) : |A| \rightarrow A \)proof
from assms have \( \text{IsLinOrder}(nat,Le) \) and \( |A| \in \text{FinPow}(nat) \) and \( A \approx |A| \) using NatOrder_ZF_1_L2, card_fin_is_nat, nat_finpow_nat
with assms show \( \sigma (A) \in ord\_iso(|A|,Le, A,r) \) using linord, fin_ord_iso_ex_uniq, singleton_extract, Enumeration_def
then show \( \sigma (A) \in \text{bij}(|A|,A) \) and \( \sigma (A) : |A| \rightarrow A \) using ord_iso_def, bij_def, surj_def
qed

A corollary from enum_props. Could have been attached as another assertion, but this slows down verification of some other proofs.

lemma (in enums) enum_fun:

assumes \( A \in \text{FinPow}(X) \)

shows \( \sigma (A) : |A| \rightarrow X \)proof
from assms have \( \sigma (A) : |A| \rightarrow A \) and \( A\subseteq X \) using enum_props, FinPow_def
then show \( \sigma (A) : |A| \rightarrow X \) by (rule func1_1_L1B )
qed

If a list is an order isomorphism then it must be the enumeration.

lemma (in enums) ord_iso_enum:

assumes A1: \( A \in \text{FinPow}(X) \) and A2: \( n \in nat \) and A3: \( f \in ord\_iso(n,Le,A,r) \)

shows \( f = \sigma (A) \)proof
from A3 have \( n \approx A \) using ord_iso_def, eqpoll_def
then have \( A \approx n \) by (rule eqpoll_sym )
with A1, A2 have \( \exists !f.\ f \in ord\_iso(n,Le,A,r) \) using ord_iso_nat_fin
with assms, \( A \approx n \) show \( f = \sigma (A) \) using enum_props, card_card
qed

What is the enumeration of the empty set?

lemma (in enums) empty_enum:

shows \( \sigma (0) = 0 \)proof
have \( 0 \in \text{FinPow}(X) \) and \( 0 \in nat \) and \( 0 \in ord\_iso(0,Le,0,r) \) using empty_in_finpow, empty_ord_iso_empty
then show \( \sigma (0) = 0 \) using ord_iso_enum
qed

Adding a new maximum to a set appends it to the enumeration.

lemma (in enums) enum_append:

assumes A1: \( A \in \text{FinPow}(X) \) and A2: \( b \in X-A \) and A3: \( \forall a\in A.\ a\leq b \)

shows \( \sigma (A \cup \{b\}) = \sigma (A)\hookleftarrow b \)proof
let \( f = \sigma (A) \cup \{\langle |A|,b\rangle \} \)
from A1 have \( |A| \in nat \) using card_fin_is_nat
from A1, A2 have \( A \cup \{b\} \in \text{FinPow}(X) \) using singleton_in_finpow, union_finpow
moreover
from this have \( |A \cup \{b\}| \in nat \) using card_fin_is_nat
moreover
have \( f \in ord\_iso(|A \cup \{b\}| , Le, A \cup \{b\} ,r) \)proof
from A1, A2 have \( \sigma (A) \in ord\_iso(|A|,Le, A,r) \) and \( |A| \notin |A| \) and \( b \notin A \) using enum_props, mem_not_refl
moreover
from \( |A| \in nat \) have \( \forall k \in |A|.\ \langle k, |A|\rangle \in Le \) using elem_nat_is_nat
moreover
from A3 have \( \forall a\in A.\ \langle a,b\rangle \in r \)
moreover
have \( \text{antisym}(Le) \) and \( \text{antisym}(r) \) using linord, NatOrder_ZF_1_L2, IsLinOrder_def
moreover
from A2, \( |A| \in nat \) have \( \langle |A|,|A|\rangle \in Le \) and \( \langle b,b\rangle \in r \) using linord, NatOrder_ZF_1_L2, IsLinOrder_def, total_is_refl, refl_def
hence \( \langle |A|,|A|\rangle \in Le \longleftrightarrow \langle b,b\rangle \in r \)
ultimately have \( f \in ord\_iso(|A| \cup \{|A|\} , Le, A \cup \{b\} ,r) \) by (rule ord_iso_extend )
with A1, A2 show \( f \in ord\_iso(|A \cup \{b\}| , Le, A \cup \{b\} ,r) \) using card_fin_add_one
qed
ultimately have \( f = \sigma (A \cup \{b\}) \) using ord_iso_enum
moreover
have \( \sigma (A)\hookleftarrow b = f \)proof
have \( \sigma (A)\hookleftarrow b = \sigma (A) \cup \{\langle domain(\sigma (A)),b\rangle \} \) using Append_def
moreover
from A1 have \( domain(\sigma (A)) = |A| \) using enum_props, func1_1_L1
ultimately show \( \sigma (A)\hookleftarrow b = f \)
qed
ultimately show \( \sigma (A \cup \{b\}) = \sigma (A)\hookleftarrow b \)
qed

What is the enumeration of a singleton?

lemma (in enums) enum_singleton:

assumes A1: \( x\in X \)

shows \( \sigma (\{x\}): 1 \rightarrow X \) and \( \sigma (\{x\})(0) = x \)proof
from A1 have \( 0 \in \text{FinPow}(X) \) and \( x \in (X - 0) \) and \( \forall a\in 0.\ a\leq x \) using empty_in_finpow
then have \( \sigma (0 \cup \{x\}) = \sigma (0)\hookleftarrow x \) by (rule enum_append )
with A1 show \( \sigma (\{x\}): 1 \rightarrow X \) and \( \sigma (\{x\})(0) = x \) using empty_enum, empty_append1
qed
end
lemma NatOrder_ZF_1_L2: shows \( \text{antisym}(Le) \), \( \text{trans}(Le) \), \( Le \text{ is total on } nat \), \( \text{IsLinOrder}(nat,Le) \)
lemma nat_finpow_nat:

assumes \( n \in nat \)

shows \( n \in \text{FinPow}(nat) \)
theorem fin_ord_iso_ex_uniq:

assumes \( \text{IsLinOrder}(X,r) \), \( \text{IsLinOrder}(Y,R) \) and \( A \in \text{FinPow}(X) \), \( B \in \text{FinPow}(Y) \) and \( B \approx A \)

shows \( \exists !f.\ f \in ord\_iso(A,r,B,R) \)
lemma card_fin_is_nat:

assumes \( A \in \text{FinPow}(X) \)

shows \( |A| \in nat \) and \( A \approx |A| \)
corollary singleton_extract:

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

shows \( (\bigcup A) \in A \)
Definition of Enumeration: \( \text{Enumeration}(A,r) \equiv \bigcup ord\_iso(|A|,Le,A,r) \)
lemma (in enums) enum_props:

assumes \( A \in \text{FinPow}(X) \)

shows \( \sigma (A) \in ord\_iso(|A|,Le, A,r) \), \( \sigma (A) \in \text{bij}(|A|,A) \), \( \sigma (A) : |A| \rightarrow A \)
Definition of FinPow: \( \text{FinPow}(X) \equiv \{A \in Pow(X).\ Finite(A)\} \)
lemma func1_1_L1B:

assumes \( f:X\rightarrow Y \) and \( Y\subseteq Z \)

shows \( f:X\rightarrow Z \)
lemma (in enums) ord_iso_nat_fin:

assumes \( A \in \text{FinPow}(X) \) and \( n \in nat \) and \( A \approx n \)

shows \( \exists !f.\ f \in ord\_iso(n,Le,A,r) \)
lemma card_card:

assumes \( A \approx n \) and \( n \in nat \)

shows \( |A| = n \)
lemma empty_in_finpow: shows \( 0 \in \text{FinPow}(X) \)
lemma empty_ord_iso_empty: shows \( ord\_iso(0,r,0,R) = \{0\} \)
lemma (in enums) ord_iso_enum:

assumes \( A \in \text{FinPow}(X) \) and \( n \in nat \) and \( f \in ord\_iso(n,Le,A,r) \)

shows \( f = \sigma (A) \)
lemma singleton_in_finpow:

assumes \( x \in X \)

shows \( \{x\} \in \text{FinPow}(X) \)
lemma union_finpow:

assumes \( A \in \text{FinPow}(X) \) and \( B \in \text{FinPow}(X) \)

shows \( A \cup B \in \text{FinPow}(X) \)
lemma elem_nat_is_nat:

assumes \( n \in nat \) and \( k\in n \)

shows \( k \lt n \), \( k \in nat \), \( k \leq n \), \( \langle k,n\rangle \in Le \)
Definition of IsLinOrder: \( \text{IsLinOrder}(X,r) \equiv \text{antisym}(r) \wedge \text{trans}(r) \wedge (r \text{ is total on } X) \)
lemma total_is_refl:

assumes \( r \text{ is total on } X \)

shows \( \text{refl}(X,r) \)
lemma ord_iso_extend:

assumes \( f \in ord\_iso(A,r,B,R) \) and \( M_A \notin A \), \( M_B \notin B \) and \( \forall a\in A.\ \langle a, M_A\rangle \in r \), \( \forall b\in B.\ \langle b, M_B\rangle \in R \) and \( \text{antisym}(r) \), \( \text{antisym}(R) \) and \( \langle M_A,M_A\rangle \in r \longleftrightarrow \langle M_B,M_B\rangle \in R \)

shows \( f \cup \{\langle M_A,M_B\rangle \} \in ord\_iso(A\cup \{M_A\} ,r,B\cup \{M_B\} ,R) \)
lemma card_fin_add_one:

assumes \( A \in \text{FinPow}(X) \) and \( a \in X-A \)

shows \( |A \cup \{a\}| = succ( |A| ) \), \( |A \cup \{a\}| = |A| \cup \{|A|\} \)
Definition of Append: \( \text{Append}(a,x) \equiv a \cup \{\langle domain(a),x\rangle \} \)
lemma func1_1_L1:

assumes \( f:A\rightarrow C \)

shows \( domain(f) = A \)
lemma (in enums) enum_append:

assumes \( A \in \text{FinPow}(X) \) and \( b \in X-A \) and \( \forall a\in A.\ a\leq b \)

shows \( \sigma (A \cup \{b\}) = \sigma (A)\hookleftarrow b \)
lemma (in enums) empty_enum: shows \( \sigma (0) = 0 \)
lemma empty_append1:

assumes \( x\in X \)

shows \( \text{Append}(0,x): 1 \rightarrow X \) and \( \text{Append}(0,x)(0) = x \)