Theory FinOrd_ZF
section ‹Finite sets and order relations›
theory FinOrd_ZF imports Finite_ZF func_ZF_1 NatOrder_ZF
begin
text‹This theory file contains properties of finite sets related to order
relations. Part of this is similar to what is done in ‹Finite_ZF_1›
except that the development is based on the notion of finite powerset
defined in ‹Finite_ZF› rather the one defined in standard
Isabelle ‹Finite› theory.›
subsection‹Finite vs. bounded sets›
text‹The goal of this section is to show that finite sets are bounded and
have maxima and minima.›
text‹For total and transitive relations
nonempty finite set has a maximum.›
theorem fin_has_max:
assumes A1: "r {is total on} X" and A2: "trans(r)"
and A3: "B ∈ FinPow(X)" and A4: "B ≠ 0"
shows "HasAmaximum(r,B)"
proof -
have "0=0 ∨ HasAmaximum(r,0)" by simp
moreover have
"∀A ∈ FinPow(X). A=0 ∨ HasAmaximum(r,A) ⟶
(∀x∈X. (A ∪ {x}) = 0 ∨ HasAmaximum(r,A ∪ {x}))"
proof -
{ fix A
assume "A ∈ FinPow(X)" "A = 0 ∨ HasAmaximum(r,A)"
have "∀x∈X. (A ∪ {x}) = 0 ∨ HasAmaximum(r,A ∪ {x})"
proof -
{ fix x assume "x∈X"
note ‹A = 0 ∨ HasAmaximum(r,A)›
moreover
{ assume "A = 0"
then have "A∪{x} = {x}" by simp
from A1 have "refl(X,r)" using total_is_refl
by simp
with ‹x∈X› ‹A∪{x} = {x}› have "HasAmaximum(r,A∪{x})"
using Order_ZF_4_L8 by simp }
moreover
{ assume "HasAmaximum(r,A)"
with A1 A2 ‹A ∈ FinPow(X)› ‹x∈X›
have "HasAmaximum(r,A∪{x})"
using FinPow_def Order_ZF_4_L9 by simp }
ultimately have "A ∪ {x} = 0 ∨ HasAmaximum(r,A ∪ {x})"
by auto
} thus "∀x∈X. (A ∪ {x}) = 0 ∨ HasAmaximum(r,A ∪ {x})"
by simp
qed
} thus ?thesis by simp
qed
moreover note A3
ultimately have "B = 0 ∨ HasAmaximum(r,B)"
by (rule FinPow_induct)
with A4 show "HasAmaximum(r,B)" by simp
qed
text‹For linearly ordered nonempty finite sets the
maximum is in the set and indeed it is the greatest
element of the set.›
lemma linord_max_props: assumes A1: "IsLinOrder(X,r)" and
A2: "A ∈ FinPow(X)" "A ≠ 0"
shows
"Maximum(r,A) ∈ A"
"Maximum(r,A) ∈ X"
"∀a∈A. ⟨a,Maximum(r,A)⟩ ∈ r"
proof -
from A1 A2 show
"Maximum(r,A) ∈ A" and "∀a∈A. ⟨a,Maximum(r,A)⟩ ∈ r"
using IsLinOrder_def fin_has_max Order_ZF_4_L3
by auto
with A2 show "Maximum(r,A) ∈ X" using FinPow_def
by auto
qed
text‹Every nonempty subset of a natural number has a maximum with expected properties.›
lemma nat_max_props: assumes "n∈nat" "A⊆n" "A≠0"
shows
"Maximum(Le,A) ∈ A"
"Maximum(Le,A) ∈ nat"
"∀k∈A. k ≤ Maximum(Le,A)"
proof -
from assms(1,2) have "A ∈ FinPow(nat)"
using nat_finpow_nat subset_finpow by blast
with assms(3) show
"Maximum(Le,A) ∈ A"
"Maximum(Le,A) ∈ nat"
using NatOrder_ZF_1_L2(4) linord_max_props(1,2) by simp_all
from assms(3) ‹A ∈ FinPow(nat)› have "∀k∈A. ⟨k,Maximum(Le,A)⟩ ∈ Le"
using linord_max_props NatOrder_ZF_1_L2(4) by blast
then show "∀k∈A. k ≤ Maximum(Le,A)" by simp
qed
text‹Yet another version of induction where the induction step is valid only up to $n\in \mathbb{N}$
rather than for all natural numbers.
This lemma is redundant as it is easier to prove this assertion using lemma ‹fin_nat_ind›
from ‹Nat_ZF_IML› which was done in lemma ‹fin_nat_ind1› there.
It is left here for now as an alternative proof based on properties of the
maximum of a finite set. ›
lemma ind_on_nat2:
assumes "n∈nat" and "P(0)" and "∀j∈n. P(j)⟶P(j #+ 1)"
shows "∀j∈n #+ 1. P(j)" and "P(n)"
proof -
let ?A = "{k∈succ(n). ∀j∈succ(k). P(j)}"
let ?M = "Maximum(Le,?A)"
from assms(1,2) have I: "succ(n) ∈ nat" "?A⊆succ(n)" "?A≠0"
using empty_in_every_succ by auto
then have "?M ∈ ?A" by (rule nat_max_props)
have "n=?M"
proof -
from ‹?M ∈ ?A› have "?M ∈ succ(n)" by blast
with assms(1) have "?M∈n ∨ ?M=n" by auto
moreover
{ assume "?M ∈ n"
from I have "?M ∈ nat" by (rule nat_max_props)
from assms(3) ‹?M∈?A› ‹?M∈n› have "P(?M #+ 1)" by blast
with ‹?M ∈ nat› have "P(succ(?M))" using succ_add_one(1) by simp
with ‹?M∈?A› have "∀j∈succ(succ(?M)). P(j)" by blast
moreover from assms(1) ‹?M ∈ n› have "succ(?M) ∈ succ(n)"
using succ_ineq1 by simp
moreover from I have "∀k∈?A. k ≤ ?M"
by (rule nat_max_props)
ultimately have False by blast
}
ultimately show "n=?M" by auto
qed
with ‹?M ∈ ?A› have "n∈?A" by (rule eq_mem)
with assms(1) show "∀j∈n #+ 1. P(j)" and "P(n)"
using succ_add_one(1) by simp_all
qed
subsection‹Order isomorphisms of finite sets›
text‹In this section we establish that if two linearly
ordered finite sets have the same number of elements,
then they are order-isomorphic and the isomorphism
is unique. This allows us to talk about ''enumeration''
of a linearly ordered finite set. We define the enumeration as
the order isomorphism between the number of elements
of the set (which is a natural number $n = \{0,1,..,n-1\}$)
and the set.›
text‹A really weird corner case - empty set is order isomorphic with itself. ›
lemma empty_ord_iso: shows "ord_iso(0,r,0,R) ≠ 0"
proof -
have "0 ≈ 0" using eqpoll_refl by simp
then obtain f where "f ∈ bij(0,0)"
using eqpoll_def by blast
then show ?thesis using ord_iso_def by auto
qed
text‹Even weirder than ‹empty_ord_iso›
The order automorphism of the empty set is unique.›
lemma empty_ord_iso_uniq:
assumes "f ∈ ord_iso(0,r,0,R)" "g ∈ ord_iso(0,r,0,R)"
shows "f = g"
proof -
from assms have "f : 0 → 0" and "g: 0 → 0"
using ord_iso_def bij_def surj_def by auto
moreover have "∀x∈0. f`(x) = g`(x)" by simp
ultimately show "f = g" by (rule func_eq)
qed
text‹The empty set is the only order automorphism of itself.›
lemma empty_ord_iso_empty: shows "ord_iso(0,r,0,R) = {0}"
proof -
have "0 ∈ ord_iso(0,r,0,R)"
proof -
have "ord_iso(0,r,0,R) ≠ 0" by (rule empty_ord_iso)
then obtain f where "f ∈ ord_iso(0,r,0,R)" by auto
then show "0 ∈ ord_iso(0,r,0,R)"
using ord_iso_def bij_def surj_def fun_subset_prod
by auto
qed
then show "ord_iso(0,r,0,R) = {0}" using empty_ord_iso_uniq
by blast
qed
text‹An induction (or maybe recursion?) scheme for linearly ordered sets.
The induction step is that we show that if the property holds
when the set is a singleton or for a set with the maximum removed,
then it holds for the set. The idea is that since we can build
any finite set by adding elements on the right, then if the property
holds for the empty set and is invariant with respect to this operation, then
it must hold for all finite sets.›
lemma fin_ord_induction:
assumes A1: "IsLinOrder(X,r)" and A2: "P(0)" and
A3: "∀A ∈ FinPow(X). A ≠ 0 ⟶ (P(A - {Maximum(r,A)}) ⟶ P(A))"
and A4: "B ∈ FinPow(X)" shows "P(B)"
proof -
note A2
moreover have "∀ A ∈ FinPow(X). A ≠ 0 ⟶ (∃a∈A. P(A-{a}) ⟶ P(A))"
proof -
{ fix A assume "A ∈ FinPow(X)" and "A ≠ 0"
with A1 A3 have "∃a∈A. P(A-{a}) ⟶ P(A)"
using IsLinOrder_def fin_has_max
IsLinOrder_def Order_ZF_4_L3
by blast
} thus ?thesis by simp
qed
moreover note A4
ultimately show "P(B)" by (rule FinPow_ind_rem_one)
qed
text‹A sligltly more complicated version of ‹fin_ord_induction›
that allows to prove properties that are not true for the empty set.›
lemma fin_ord_ind:
assumes A1: "IsLinOrder(X,r)" and A2: "∀A ∈ FinPow(X).
A = 0 ∨ (A = {Maximum(r,A)} ∨ P(A - {Maximum(r,A)}) ⟶ P(A))"
and A3: "B ∈ FinPow(X)" and A4: "B≠0"
shows "P(B)"
proof -
{ fix A assume "A ∈ FinPow(X)" and "A ≠ 0"
with A1 A2 have
"∃a∈A. A = {a} ∨ P(A-{a}) ⟶ P(A)"
using IsLinOrder_def fin_has_max
IsLinOrder_def Order_ZF_4_L3
by blast
} then have "∀A ∈ FinPow(X).
A = 0 ∨ (∃a∈A. A = {a} ∨ P(A-{a}) ⟶ P(A))"
by auto
with A3 A4 show "P(B)" using FinPow_rem_ind
by simp
qed
text‹Yet another induction scheme. We build a linearly ordered
set by adding elements that are greater than all elements in the
set.›
lemma fin_ind_add_max:
assumes A1: "IsLinOrder(X,r)" and A2: "P(0)" and A3: "∀ A ∈ FinPow(X).
( ∀ x ∈ X-A. P(A) ∧ (∀a∈A. ⟨a,x⟩ ∈ r ) ⟶ P(A ∪ {x}))"
and A4: "B ∈ FinPow(X)"
shows "P(B)"
proof -
note A1 A2
moreover have
"∀C ∈ FinPow(X). C ≠ 0 ⟶ (P(C - {Maximum(r,C)}) ⟶ P(C))"
proof -
{ fix C assume "C ∈ FinPow(X)" and "C ≠ 0"
let ?x = "Maximum(r,C)"
let ?A = "C - {?x}"
assume "P(?A)"
moreover from ‹C ∈ FinPow(X)› have "?A ∈ FinPow(X)"
using fin_rem_point_fin by simp
moreover from A1 ‹C ∈ FinPow(X)› ‹C ≠ 0› have
"?x ∈ C" and "?x ∈ X - ?A" and "∀a∈?A. ⟨a,?x⟩ ∈ r"
using linord_max_props by auto
moreover note A3
ultimately have "P(?A ∪ {?x})" by auto
moreover from ‹?x ∈ C› have "?A ∪ {?x} = C"
by auto
ultimately have "P(C)" by simp
} thus ?thesis by simp
qed
moreover note A4
ultimately show "P(B)" by (rule fin_ord_induction)
qed
text‹The only order automorphism of a linearly ordered
finite set is the identity.›
theorem fin_ord_auto_id: assumes A1: "IsLinOrder(X,r)"
and A2: "B ∈ FinPow(X)" and A3: "B≠0"
shows "ord_iso(B,r,B,r) = {id(B)}"
proof -
note A1
moreover
{ fix A assume "A ∈ FinPow(X)" "A≠0"
let ?M = "Maximum(r,A)"
let ?A⇩0 = "A - {?M}"
assume "A = {?M} ∨ ord_iso(?A⇩0,r,?A⇩0,r) = {id(?A⇩0)}"
moreover
{ assume "A = {?M}"
have "ord_iso({?M},r,{?M},r) = {id({?M})}"
using id_ord_auto_singleton by simp
with ‹A = {?M}› have "ord_iso(A,r,A,r) = {id(A)}"
by simp }
moreover
{ assume "ord_iso(?A⇩0,r,?A⇩0,r) = {id(?A⇩0)}"
have "ord_iso(A,r,A,r) = {id(A)}"
proof
show "{id(A)} ⊆ ord_iso(A,r,A,r)"
using id_ord_iso by simp
{ fix f assume "f ∈ ord_iso(A,r,A,r)"
with A1 ‹A ∈ FinPow(X)› ‹A≠0› have
"restrict(f,?A⇩0) ∈ ord_iso(?A⇩0, r, A-{f`(?M)},r)"
using IsLinOrder_def fin_has_max ord_iso_rem_max
by auto
with A1 ‹A ∈ FinPow(X)› ‹A≠0› ‹f ∈ ord_iso(A,r,A,r)›
‹ord_iso(?A⇩0,r,?A⇩0,r) = {id(?A⇩0)}›
have "restrict(f,?A⇩0) = id(?A⇩0)"
using IsLinOrder_def fin_has_max max_auto_fixpoint
by auto
moreover from A1 ‹f ∈ ord_iso(A,r,A,r)›
‹A ∈ FinPow(X)› ‹A≠0› have
"f : A → A" and "?M ∈ A" and "f`(?M) = ?M"
using ord_iso_def bij_is_fun IsLinOrder_def
fin_has_max Order_ZF_4_L3 max_auto_fixpoint
by auto
ultimately have "f = id(A)" using id_fixpoint_rem
by simp
} then show "ord_iso(A,r,A,r) ⊆ {id(A)}"
by auto
qed
}
ultimately have "ord_iso(A,r,A,r) = {id(A)}"
by auto
} then have "∀A ∈ FinPow(X). A = 0 ∨
(A = {Maximum(r,A)} ∨
ord_iso(A-{Maximum(r,A)},r,A-{Maximum(r,A)},r) =
{id(A-{Maximum(r,A)})} ⟶ ord_iso(A,r,A,r) = {id(A)})"
by auto
moreover note A2 A3
ultimately show "ord_iso(B,r,B,r) = {id(B)}"
by (rule fin_ord_ind)
qed
text‹Every two finite linearly ordered sets are order
isomorphic. The statement is formulated to make the
proof by induction on the size of the set easier,
see ‹fin_ord_iso_ex› for an alternative formulation.
›
lemma fin_order_iso:
assumes A1: "IsLinOrder(X,r)" "IsLinOrder(Y,R)" and
A2: "n ∈ nat"
shows "∀A ∈ FinPow(X). ∀B ∈ FinPow(Y).
A ≈ n ∧ B ≈ n ⟶ ord_iso(A,r,B,R) ≠ 0"
proof -
note A2
moreover have "∀A ∈ FinPow(X). ∀B ∈ FinPow(Y).
A ≈ 0 ∧ B ≈ 0 ⟶ ord_iso(A,r,B,R) ≠ 0"
using eqpoll_0_is_0 empty_ord_iso by blast
moreover have "∀k ∈ nat.
(∀A ∈ FinPow(X). ∀B ∈ FinPow(Y).
A ≈ k ∧ B ≈ k ⟶ ord_iso(A,r,B,R) ≠ 0) ⟶
(∀C ∈ FinPow(X). ∀D ∈ FinPow(Y).
C ≈ succ(k) ∧ D ≈ succ(k) ⟶ ord_iso(C,r,D,R) ≠ 0)"
proof -
{ fix k assume "k ∈ nat"
assume A3: "∀A ∈ FinPow(X). ∀B ∈ FinPow(Y).
A ≈ k ∧ B ≈ k ⟶ ord_iso(A,r,B,R) ≠ 0"
have "∀C ∈ FinPow(X). ∀D ∈ FinPow(Y).
C ≈ succ(k) ∧ D ≈ succ(k) ⟶ ord_iso(C,r,D,R) ≠ 0"
proof -
{ fix C assume "C ∈ FinPow(X)"
fix D assume "D ∈ FinPow(Y)"
assume "C ≈ succ(k)" "D ≈ succ(k)"
then have "C ≠ 0" and "D≠ 0"
using eqpoll_succ_imp_not_empty by auto
let ?M⇩C = "Maximum(r,C)"
let ?M⇩D = "Maximum(R,D)"
let ?C⇩0 = "C - {?M⇩C}"
let ?D⇩0 = "D - {?M⇩D}"
from ‹C ∈ FinPow(X)› have "C ⊆ X"
using FinPow_def by simp
with A1 have "IsLinOrder(C,r)"
using ord_linear_subset by blast
from ‹D ∈ FinPow(Y)› have "D ⊆ Y"
using FinPow_def by simp
with A1 have "IsLinOrder(D,R)"
using ord_linear_subset by blast
from A1 ‹C ∈ FinPow(X)› ‹D ∈ FinPow(Y)›
‹C ≠ 0› ‹D≠ 0› have
"HasAmaximum(r,C)" and "HasAmaximum(R,D)"
using IsLinOrder_def fin_has_max
by auto
with A1 have "?M⇩C ∈ C" and "?M⇩D ∈ D"
using IsLinOrder_def Order_ZF_4_L3 by auto
with ‹C ≈ succ(k)› ‹D ≈ succ(k)› have
"?C⇩0 ≈ k" and "?D⇩0 ≈ k" using Diff_sing_eqpoll by auto
from ‹C ∈ FinPow(X)› ‹D ∈ FinPow(Y)›
have "?C⇩0 ∈ FinPow(X)" and "?D⇩0 ∈ FinPow(Y)"
using fin_rem_point_fin by auto
with A3 ‹?C⇩0 ≈ k› ‹?D⇩0 ≈ k› have
"ord_iso(?C⇩0,r,?D⇩0,R) ≠ 0" by simp
with ‹IsLinOrder(C,r)› ‹IsLinOrder(D,R)›
‹HasAmaximum(r,C)› ‹HasAmaximum(R,D)›
have "ord_iso(C,r,D,R) ≠ 0"
by (rule rem_max_ord_iso)
} thus ?thesis by simp
qed
} thus ?thesis by blast
qed
ultimately show ?thesis by (rule ind_on_nat)
qed
text‹Every two finite linearly ordered sets are order
isomorphic.›
lemma fin_ord_iso_ex:
assumes A1: "IsLinOrder(X,r)" "IsLinOrder(Y,R)" and
A2: "A ∈ FinPow(X)" "B ∈ FinPow(Y)" and A3: "B ≈ A"
shows "ord_iso(A,r,B,R) ≠ 0"
proof -
from A2 obtain n where "n ∈ nat" and "A ≈ n"
using finpow_decomp by auto
from A3 ‹A ≈ n› have "B ≈ n" by (rule eqpoll_trans)
with A1 A2 ‹A ≈ n› ‹n ∈ nat› show "ord_iso(A,r,B,R) ≠ 0"
using fin_order_iso by simp
qed
text‹Existence and uniqueness of order isomorphism for two
linearly ordered sets with the same number of elements.›
theorem fin_ord_iso_ex_uniq:
assumes A1: "IsLinOrder(X,r)" "IsLinOrder(Y,R)" and
A2: "A ∈ FinPow(X)" "B ∈ FinPow(Y)" and A3: "B ≈ A"
shows "∃!f. f ∈ ord_iso(A,r,B,R)"
proof
from assms show "∃f. f ∈ ord_iso(A,r,B,R)"
using fin_ord_iso_ex by blast
fix f g
assume A4: "f ∈ ord_iso(A,r,B,R)" "g ∈ ord_iso(A,r,B,R)"
then have "converse(g) ∈ ord_iso(B,R,A,r)"
using ord_iso_sym by simp
with ‹f ∈ ord_iso(A,r,B,R)› have
I: "converse(g) O f ∈ ord_iso(A,r,A,r)"
by (rule ord_iso_trans)
{ assume "A ≠ 0"
with A1 A2 I have "converse(g) O f = id(A)"
using fin_ord_auto_id by auto
with A4 have "f = g"
using ord_iso_def comp_inv_id_eq_bij by auto }
moreover
{ assume "A = 0"
then have "A ≈ 0" using eqpoll_0_iff
by simp
with A3 have "B ≈ 0" by (rule eqpoll_trans)
with A4 ‹A = 0› have
"f ∈ ord_iso(0,r,0,R)" and "g ∈ ord_iso(0,r,0,R)"
using eqpoll_0_iff by auto
then have "f = g" by (rule empty_ord_iso_uniq) }
ultimately show "f = g"
using ord_iso_def comp_inv_id_eq_bij
by auto
qed
end