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 \)