section ‹Finite sets 1›
theory Finite_ZF_1 imports Finite1 Order_ZF_1a
begin
text‹This theory is based on ‹Finite1› theory and is obsolete. It
contains properties of finite sets related to order
relations. See the ‹FinOrd› theory for a better approach.›
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‹Finite set has a maximum - induction step.›
lemma Finite_ZF_1_1_L1:
assumes A1: "r {is total on} X" and A2: "trans(r)"
and A3: "A∈Fin(X)" and A4: "x∈X" and A5: "A=0 ∨ HasAmaximum(r,A)"
shows "A∪{x} = 0 ∨ HasAmaximum(r,A∪{x})"
proof -
{ assume "A=0" then have T1: "A∪{x} = {x}" by simp
from A1 have "refl(X,r)" using total_is_refl by simp
with T1 A4 have "A∪{x} = 0 ∨ HasAmaximum(r,A∪{x})"
using Order_ZF_4_L8 by simp }
moreover
{ assume "A≠0"
with A1 A2 A3 A4 A5 have "A∪{x} = 0 ∨ HasAmaximum(r,A∪{x})"
using FinD Order_ZF_4_L9 by simp }
ultimately show ?thesis by blast
qed
text‹For total and transitive relations finite set has a maximum.›
theorem Finite_ZF_1_1_T1A:
assumes A1: "r {is total on} X" and A2: "trans(r)"
and A3: "B∈Fin(X)"
shows "B=0 ∨ HasAmaximum(r,B)"
proof -
have "0=0 ∨ HasAmaximum(r,0)" by simp
moreover note A3
moreover from A1 A2 have "∀A∈Fin(X). ∀x∈X.
x∉A ∧ (A=0 ∨ HasAmaximum(r,A)) ⟶ (A∪{x}=0 ∨ HasAmaximum(r,A∪{x}))"
using Finite_ZF_1_1_L1 by simp
ultimately show "B=0 ∨ HasAmaximum(r,B)" by (rule Finite1_L16B)
qed
text‹Finite set has a minimum - induction step.›
lemma Finite_ZF_1_1_L2:
assumes A1: "r {is total on} X" and A2: "trans(r)"
and A3: "A∈Fin(X)" and A4: "x∈X" and A5: "A=0 ∨ HasAminimum(r,A)"
shows "A∪{x} = 0 ∨ HasAminimum(r,A∪{x})"
proof -
{ assume "A=0" then have T1: "A∪{x} = {x}" by simp
from A1 have "refl(X,r)" using total_is_refl by simp
with T1 A4 have "A∪{x} = 0 ∨ HasAminimum(r,A∪{x})"
using Order_ZF_4_L8 by simp }
moreover
{ assume "A≠0"
with A1 A2 A3 A4 A5 have "A∪{x} = 0 ∨ HasAminimum(r,A∪{x})"
using FinD Order_ZF_4_L10 by simp }
ultimately show ?thesis by blast
qed
text‹For total and transitive relations finite set has a minimum.›
theorem Finite_ZF_1_1_T1B:
assumes A1: "r {is total on} X" and A2: "trans(r)"
and A3: "B ∈ Fin(X)"
shows "B=0 ∨ HasAminimum(r,B)"
proof -
have "0=0 ∨ HasAminimum(r,0)" by simp
moreover note A3
moreover from A1 A2 have "∀A∈Fin(X). ∀x∈X.
x∉A ∧ (A=0 ∨ HasAminimum(r,A)) ⟶ (A∪{x}=0 ∨ HasAminimum(r,A∪{x}))"
using Finite_ZF_1_1_L2 by simp
ultimately show "B=0 ∨ HasAminimum(r,B)" by (rule Finite1_L16B)
qed
text‹For transitive and total relations finite sets are bounded.›
theorem Finite_ZF_1_T1:
assumes A1: "r {is total on} X" and A2: "trans(r)"
and A3: "B∈Fin(X)"
shows "IsBounded(B,r)"
proof -
from A1 A2 A3 have "B=0 ∨ HasAminimum(r,B)" "B=0 ∨ HasAmaximum(r,B)"
using Finite_ZF_1_1_T1A Finite_ZF_1_1_T1B by auto
then have
"B = 0 ∨ IsBoundedBelow(B,r)" "B = 0 ∨ IsBoundedAbove(B,r)"
using Order_ZF_4_L7 Order_ZF_4_L8A by auto
then show "IsBounded(B,r)" using
IsBounded_def IsBoundedBelow_def IsBoundedAbove_def
by simp
qed
text‹For linearly ordered finite sets maximum and minimum have desired
properties. The reason we need linear order is that we need the order
to be total and transitive for the finite sets to have a maximum and minimum
and then we also need antisymmetry for the maximum and minimum to be unique.
›
theorem Finite_ZF_1_T2:
assumes A1: "IsLinOrder(X,r)" and A2: "A ∈ Fin(X)" and A3: "A≠0"
shows
"Maximum(r,A) ∈ A"
"Minimum(r,A) ∈ A"
"∀x∈A. ⟨x,Maximum(r,A)⟩ ∈ r"
"∀x∈A. ⟨Minimum(r,A),x⟩ ∈ r"
proof -
from A1 have T1: "r {is total on} X" "trans(r)" "antisym(r)"
using IsLinOrder_def by auto
moreover from T1 A2 A3 have "HasAmaximum(r,A)"
using Finite_ZF_1_1_T1A by auto
moreover from T1 A2 A3 have "HasAminimum(r,A)"
using Finite_ZF_1_1_T1B by auto
ultimately show
"Maximum(r,A) ∈ A"
"Minimum(r,A) ∈ A"
"∀x∈A. ⟨x,Maximum(r,A)⟩ ∈ r" "∀x∈A. ⟨Minimum(r,A),x⟩ ∈ r"
using Order_ZF_4_L3 Order_ZF_4_L4 by auto
qed
text‹A special case of ‹Finite_ZF_1_T2› when the set has three
elements.›
corollary Finite_ZF_1_L2A:
assumes A1: "IsLinOrder(X,r)" and A2: "a∈X" "b∈X" "c∈X"
shows
"Maximum(r,{a,b,c}) ∈ {a,b,c}"
"Minimum(r,{a,b,c}) ∈ {a,b,c}"
"Maximum(r,{a,b,c}) ∈ X"
"Minimum(r,{a,b,c}) ∈ X"
"⟨a,Maximum(r,{a,b,c})⟩ ∈ r"
"⟨b,Maximum(r,{a,b,c})⟩ ∈ r"
"⟨c,Maximum(r,{a,b,c})⟩ ∈ r"
proof -
from A2 have I: "{a,b,c} ∈ Fin(X)" "{a,b,c} ≠ 0"
by auto
with A1 show II: "Maximum(r,{a,b,c}) ∈ {a,b,c}"
by (rule Finite_ZF_1_T2)
moreover from A1 I show III: "Minimum(r,{a,b,c}) ∈ {a,b,c}"
by (rule Finite_ZF_1_T2)
moreover from A2 have "{a,b,c} ⊆ X"
by auto
ultimately show
"Maximum(r,{a,b,c}) ∈ X"
"Minimum(r,{a,b,c}) ∈ X"
by auto
from A1 I have "∀x∈{a,b,c}. ⟨x,Maximum(r,{a,b,c})⟩ ∈ r"
by (rule Finite_ZF_1_T2)
then show
"⟨a,Maximum(r,{a,b,c})⟩ ∈ r"
"⟨b,Maximum(r,{a,b,c})⟩ ∈ r"
"⟨c,Maximum(r,{a,b,c})⟩ ∈ r"
by auto
qed
text‹If for every element of $X$ we can find one in $A$
that is greater, then the $A$ can not be finite. Works for relations
that are total, transitive and antisymmetric.›
lemma Finite_ZF_1_1_L3:
assumes A1: "r {is total on} X"
and A2: "trans(r)" and A3: "antisym(r)"
and A4: "r ⊆ X×X" and A5: "X≠0"
and A6: "∀x∈X. ∃a∈A. x≠a ∧ ⟨x,a⟩ ∈ r"
shows "A ∉ Fin(X)"
proof -
from assms have "¬IsBounded(A,r)"
using Order_ZF_3_L14 IsBounded_def
by simp
with A1 A2 show "A ∉ Fin(X)"
using Finite_ZF_1_T1 by auto
qed
end