Theory Teichmuller_Tukey_Lemma
section ‹The Teichmüller--Tukey Lemma›
theory Teichmuller_Tukey_Lemma
imports Main
begin
text ‹
The Teichmüller--Tukey lemma states that every nonempty family of sets of
finite character has a member that is maximal under inclusion. Although the
result follows from Zorn's lemma, the development below formalizes the direct
choice-function construction presented by Sun and Yu
\<^cite>‹"SunYu2019"›. Their proof is formulated in Morse--Kelley set
theory and checked in Coq; here it is adapted to polymorphic HOL sets.
This result was developed as infrastructure for a separate formalization of
first-order logic following Shoenfield \<^cite>‹"Shoenfield1967"›.
›
subsection ‹Families of finite character›
definition Maximal :: "'a set ⇒ 'a set set ⇒ bool" where
"Maximal A J ≡ A ∈ J ∧ (∀B∈J. ¬ A ⊂ B)"
definition Nest :: "'a set set ⇒ bool" where
"Nest A ≡ ∀x∈A. ∀y∈A. x ⊆ y ∨ y ⊆ x"
definition Finite_character :: "'a set set ⇒ bool" where
"Finite_character J ≡ ∀Δ. Δ ∈ J ⟷ (∀δ⊆Δ. finite δ ⟶ δ ∈ J)"
text ‹
A family of finite character is downward closed. It is also closed under the
union of a nest. Nonemptiness is needed for the empty nest: it ensures that
the empty set belongs to the family.
›
proposition property_fin_char:
assumes "Finite_character J" and "J ≠ {}"
shows "∀A∈J. ∀B⊆A. B ∈ J"
and "∀G. Nest G ∧ G ⊆ J ⟶ ⋃G ∈ J"
proof -
show "∀A∈J. ∀B⊆A. B ∈ J"
using Finite_character_def assms(1) by (meson subset_trans)
next
show "∀G. Nest G ∧ G ⊆ J ⟶ ⋃G ∈ J"
proof (rule allI, rule impI)
fix G
assume B: "Nest G ∧ G ⊆ J"
have C: "⋀g. set g ⊆ ⋃G ⟹ g ≠ [] ⟹ ∃X∈G. set g ⊆ X"
proof -
fix g
show "set g ⊆ ⋃G ⟹ g ≠ [] ⟹ ∃X∈G. set g ⊆ X"
proof (induction g rule: measure_induct[of length])
case (1 g)
then show ?case
proof cases
assume "g = [] ∨ (∃a. g = [a])"
then show ?case using "1.prems"(1,2) by fastforce
next
assume "¬ (g = [] ∨ (∃a. g = [a]))"
then obtain a and xs where axs: "g = a # xs ∧ xs ≠ []"
by (metis list.exhaust)
from this 1(1-2) have
"(∃X∈G. {a} ⊆ X) ∧ (∃X∈G. set xs ⊆ X)"
by auto
thus ?case
using B Nest_def axs
by (metis dual_order.trans insert_subset list.simps(15))
qed
qed
qed
thus "⋃G ∈ J"
using assms(1-2) B C Finite_character_def
by (smt (z3) ex_in_conv finite_list set_empty subset_eq list.set(1,1,1,1)
subsetI subset_antisym)
qed
qed
subsection ‹The choice extension›
fun enlarge :: "'a set ⇒ 'a set set ⇒ 'a set" where
"enlarge F J = {x. x ∈ ⋃J ∧ F∪{x} ∈ J}"
proposition enlarge_subset: "F ∈ J ⟹ F ⊆ enlarge F J"
using UnionI insert_absorb by force
fun 𝒳_choice :: "'a set ⇒ 'a set set ⇒ ('a set ⇒ 'a) ⇒ 'a set" where
"𝒳_choice F J c =
(if enlarge F J - F = {} then F else F∪{c (enlarge F J - F)})"
text ‹
For a member @{term F} of @{term J}, @{term "enlarge F J"} contains the
elements that can be adjoined to @{term F} while staying in @{term J}. The
operation @{term "𝒳_choice F J c"} adjoins an element chosen outside
@{term F}, unless no such element exists.
›
text ‹
The fixed-point argument below makes explicit a detail that is only implicit
in Proof 4.7 of the source article. From
@{term "𝒳_choice F J c = F"} one may conclude
@{term "enlarge F J = F"} only by using the choice property of @{term c}:
if @{term "enlarge F J - F"} were nonempty, its chosen element would lie
both outside and inside @{term F}. This is the step that turns a fixed point
of the choice extension into a maximal member.
›
lemma 𝒳_implies_TTL:
assumes "Finite_character J"
and "∃F∈J. ∃c. ((∀Y. Y ≠ {} ⟶ c Y ∈ Y) ∧ 𝒳_choice F J c = F)"
shows "∃Δ∈J. Maximal Δ J"
proof -
from assms(2) obtain Δ and c where
Δc: "Δ ∈ J ∧ (∀Y. Y ≠ {} ⟶ c Y ∈ Y) ∧ 𝒳_choice Δ J c = Δ"
by blast
hence ig: "enlarge Δ J = Δ"
by (metis DiffD2 Un_upper2 𝒳_choice.elims diff_shunt enlarge_subset
insert_subset order_antisym_conv)
have "Maximal Δ J"
proof (rule ccontr)
assume "¬ Maximal Δ J"
from this Δc obtain B where B: "B ∈ J ∧ Δ ⊂ B"
using Maximal_def by meson
then obtain d where d: "d ∈ B ∧ d ∉ Δ" by blast
hence "d ∈ enlarge Δ J"
using assms(1) Finite_character_def B property_fin_char(1) by fastforce
thus False using ig d by blast
qed
thus "∃Δ∈J. Maximal Δ J" using Δc by blast
qed
subsection ‹The least closed subclass›
text ‹
Following the notation of the source proof, a @{emph ‹t-subclass›}
contains the empty set and is closed under both choice extensions and unions
of nests. Intersecting all t-subclasses gives the least such subclass.
›
definition tSubclass :: "'a set set ⇒ 'a set set ⇒ ('a set ⇒ 'a) ⇒ bool" where
"tSubclass G J c ≡
G ⊆ J ∧ {} ∈ G ∧ (∀F∈G. 𝒳_choice F J c ∈ G) ∧
(∀L⊆G. Nest L ⟶ ⋃L ∈ G)"
definition inter_subclass :: "'a set set ⇒ ('a set ⇒ 'a) ⇒ 'a set set" where
"inter_subclass J c ≡ ⋂{G. tSubclass G J c}"
definition μ_function :: "'a set ⇒ 'a set set ⇒ ('a set ⇒ 'a) ⇒ 'a set set" where
"μ_function C J c ≡
{A∈inter_subclass J c. A ⊆ C ∨ C ⊆ A}"
definition total_subclass :: "'a set set ⇒ ('a set ⇒ 'a) ⇒ 'a set set" where
"total_subclass J c ≡
{C∈inter_subclass J c. μ_function C J c = inter_subclass J c}"
definition ν_function :: "'a set ⇒ 'a set set ⇒ ('a set ⇒ 'a) ⇒ 'a set set" where
"ν_function D J c ≡
{A∈inter_subclass J c. A ⊆ D ∨ 𝒳_choice D J c ⊆ A}"
proposition property_𝒳: "F ∈ J ⟹ F ⊆ 𝒳_choice F J c"
by auto
proposition property_inter_subclass:
assumes "Finite_character J" and "J ≠ {}"
and "∀Y. Y ≠ {} ⟶ c Y ∈ Y"
shows "tSubclass (inter_subclass J c) J c"
and "∀G. tSubclass G J c ⟶ inter_subclass J c ⊆ G"
proof -
have JSubJ: "tSubclass J J c"
using tSubclass_def Nest_def assms(1-3) property_fin_char(2)
by (smt (verit, ccfv_threshold) Diff_iff Sup_empty 𝒳_choice.simps
dual_order.refl empty_iff empty_subsetI enlarge.simps mem_Collect_eq)
show "tSubclass (inter_subclass J c) J c"
proof (auto simp only: tSubclass_def[of "inter_subclass J c" J c])
show "{} ∈ inter_subclass J c"
using inter_subclass_def tSubclass_def
by (metis (no_types, lifting) Inter_iff mem_Collect_eq)
next
have "∀G F. tSubclass G J c ⟶ F ∈ G ⟶ 𝒳_choice F J c ∈ G"
using tSubclass_def by blast
thus "⋀F. F ∈ inter_subclass J c ⟹ 𝒳_choice F J c ∈ inter_subclass J c"
using inter_subclass_def by blast
next
have "∀G L. tSubclass G J c ⟶ L ⊆ G ⟶ Nest L ⟶ ⋃L ∈ G"
using tSubclass_def by metis
thus "⋀L. L ⊆ inter_subclass J c ⟹ Nest L ⟹ ⋃L ∈ inter_subclass J c"
using inter_subclass_def[of J c] by blast
qed (auto simp add: JSubJ inter_subclass_def)
qed (auto simp add: inter_subclass_def)
subsection ‹The least t-subclass is a Nest›
text ‹
The next three lemmas correspond to Steps I--III of Section 4.1 in the
source. The auxiliary subclasses @{term "μ_function C J c"} and
@{term "ν_function D J c"} isolate the members comparable with a given
set and allow comparability to be propagated through the choice extension.
›
lemma step1:
assumes "Finite_character J" and "J ≠ {}"
and "∀Y. Y ≠ {} ⟶ c Y ∈ Y"
and "D ∈ total_subclass J c"
shows "tSubclass (ν_function D J c) J c"
proof -
show ?thesis
proof (auto simp only: tSubclass_def[of "ν_function D J c" J c])
have "ν_function D J c ⊆ inter_subclass J c"
using ν_function_def by blast
thus "⋀x. x ∈ ν_function D J c ⟹ x ∈ J"
using tSubclass_def property_inter_subclass(1) assms by (metis in_mono)
next
fix F
assume "F ∈ ν_function D J c"
then have F: "F ∈ inter_subclass J c ∧
(F ⊆ D ∨ 𝒳_choice D J c ⊆ F)"
using ν_function_def by blast
show "𝒳_choice F J c ∈ ν_function D J c"
proof cases
assume c1: "𝒳_choice D J c ⊆ F"
then show ?thesis
using F ν_function_def assms(1-3) property_𝒳
property_inter_subclass(1) tSubclass_def
by (smt (verit) in_mono mem_Collect_eq subset_trans)
next
assume "¬ 𝒳_choice D J c ⊆ F"
hence b: "𝒳_choice F J c ⊆ D ∨ D ⊆ 𝒳_choice F J c"
using assms F μ_function_def tSubclass_def property_inter_subclass(1)
total_subclass_def
by (smt (verit, del_insts) mem_Collect_eq)
show ?thesis
proof (rule ccontr)
assume hyp: "𝒳_choice F J c ∉ ν_function D J c"
then have "¬ 𝒳_choice F J c ⊆ D"
using assms(1-3) ν_function_def F tSubclass_def
property_inter_subclass(1)
by (metis (no_types, lifting) mem_Collect_eq)
from this b have "D ⊂ 𝒳_choice F J c" by blast
hence "D ⊂ F ∨ D ⊂ F∪{c (enlarge F J - F)}"
by (metis 𝒳_choice.simps)
hence "𝒳_choice D J c ⊆ 𝒳_choice F J c"
using F ‹¬ 𝒳_choice D J c ⊆ F›
by (metis Un_insert_right insert_subsetI leD order_class.order_eq_iff
psubset_insert_iff sup_bot_right)
thus False
using hyp ν_function_def F assms(1-3) property_inter_subclass(1)
tSubclass_def
by (metis (no_types, lifting) mem_Collect_eq)
qed
qed
next
fix L
assume hyp1: "L ⊆ ν_function D J c" and hyp2: "Nest L"
then have UL: "⋃L ∈ inter_subclass J c"
using ν_function_def[of D J c] property_inter_subclass(1) assms(1-3)
tSubclass_def
by (smt (verit) mem_Collect_eq subset_eq)
have "⋃L ⊆ D ∨ 𝒳_choice D J c ⊆ ⋃L"
proof cases
assume "∀l∈L. l ⊆ D"
then show ?thesis using UL ν_function_def by blast
next
assume "¬ (∀l∈L. l ⊆ D)"
from this hyp1 show ?thesis using ν_function_def[of D J c] by blast
qed
thus "⋃L ∈ ν_function D J c"
using ν_function_def[of D J c] UL by blast
qed (simp add: ν_function_def inter_subclass_def tSubclass_def)
qed
lemma step2:
assumes "Finite_character J" and "J ≠ {}"
and "∀Y. Y ≠ {} ⟶ c Y ∈ Y"
and "D ∈ total_subclass J c"
shows "𝒳_choice D J c ∈ total_subclass J c"
proof -
from assms have "inter_subclass J c ⊆ ν_function D J c"
using step1 property_inter_subclass(2) by metis
moreover have "ν_function D J c ⊆ μ_function (𝒳_choice D J c) J c"
using μ_function_def ν_function_def
by (smt (verit, best) Un_upper1 𝒳_choice.simps mem_Collect_eq subsetD subsetI)
moreover have "... ⊆ inter_subclass J c" using μ_function_def by blast
ultimately have
"μ_function (𝒳_choice D J c) J c = inter_subclass J c"
by order
thus ?thesis
using assms total_subclass_def[of J c] property_inter_subclass[of J c]
tSubclass_def[of "inter_subclass J c" J c] by simp
qed
lemma step3:
assumes "Finite_character J" and "J ≠ {}"
and "∀Y. Y ≠ {} ⟶ c Y ∈ Y"
shows "Nest (inter_subclass J c)"
proof -
have "Nest (total_subclass J c)"
using Nest_def[of "total_subclass J c"] total_subclass_def[of J c]
μ_function_def[of _ J c] by blast
moreover have a: "total_subclass J c ⊆ inter_subclass J c"
using total_subclass_def by auto
moreover have "tSubclass (total_subclass J c) J c"
proof (auto simp only: tSubclass_def[of "total_subclass J c" J c])
show "⋀x. x ∈ total_subclass J c ⟹ x ∈ J"
using a assms property_inter_subclass[of J c] tSubclass_def by (meson subsetD)
show "{} ∈ total_subclass J c"
using assms property_inter_subclass[of J c] μ_function_def
tSubclass_def[of "inter_subclass J c"] total_subclass_def[of J c]
by fastforce
show "⋀F. F ∈ total_subclass J c ⟹
𝒳_choice F J c ∈ total_subclass J c"
using assms step2 by blast
show "⋀L. L ⊆ total_subclass J c ⟹ Nest L ⟹
⋃L ∈ total_subclass J c"
proof -
fix L
assume hyp1: "L ⊆ total_subclass J c" and "Nest L"
then have "⋃L ∈ inter_subclass J c"
using property_inter_subclass(1) assms tSubclass_def a
by (metis subset_trans)
moreover from hyp1 have
"∀A∈inter_subclass J c. A ⊆ ⋃L ∨ ⋃L ⊆ A"
using total_subclass_def[of J c] μ_function_def[of _ J c] by blast
ultimately show "⋃L ∈ total_subclass J c"
using total_subclass_def[of J c] μ_function_def[of "⋃L" J c]
by auto
qed
qed
hence "inter_subclass J c ⊆ total_subclass J c"
using inter_subclass_def by blast
ultimately show ?thesis by simp
qed
subsection ‹The fixed point and the main theorem›
text ‹
Since the least t-subclass is a nest, its union belongs to it. Closure under
the choice extension then places the extension in the same nest, while the
definition of union bounds it from above. Hence the union is a fixed point.
›
lemma step4:
assumes "Finite_character J" and "J ≠ {}"
and "∀Y. Y ≠ {} ⟶ c Y ∈ Y"
shows "𝒳_choice (⋃(inter_subclass J c)) J c = ⋃(inter_subclass J c)"
using assms property_𝒳 property_fin_char(2) property_inter_subclass step3
tSubclass_def
by (metis Union_upper subset_antisym)
theorem teichmueller_tuckey_lemma:
fixes J :: "'a set set"
assumes "Finite_character J" and "J ≠ {}"
shows "∃Δ∈J. Maximal Δ J"
proof -
let ?c = "λY :: 'a set. SOME y. y ∈ Y"
have choice: "∀Y :: 'a set. Y ≠ {} ⟶ ?c Y ∈ Y"
by (simp add: some_in_eq)
have fixed:
"𝒳_choice (⋃(inter_subclass J ?c)) J ?c =
⋃(inter_subclass J ?c)"
using assms choice step4 by metis
have member: "⋃(inter_subclass J ?c) ∈ J"
using assms choice property_fin_char(2) property_inter_subclass(1)
step3 tSubclass_def by metis
show ?thesis
using assms(1) choice fixed member 𝒳_implies_TTL[of J]
by metis
qed
end