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

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$$