Theory Smallness
chapter "Smallness"
theory Smallness
imports "HOL-Library.Equipollence"
begin
text ‹
The purpose of this theory is to axiomatize, using locales, a notion of ``small set'' that
is polymorphic over types and that is preserved by certain set-theoretic constructions
in the way we would usually expect. We first observe that we cannot simply define
such a notion within normal HOL, because HOL does not permit us to quantify over types,
nor does it permit us to show the existence of a single type ``large enough'' to admit
sets of all cardinalities that would result, say, by iterating the application of the
powerset operator starting with some infinite set. So any way of defining ``smallness''
is going to require extending HOL in some way. Note that this is exactly what is already
done in the article \<^cite>‹"ZFC_in_HOL-AFP"›, which axiomatizes a particular type ‹V›
and then defines a polymorphic function ‹small› using the properties of that type.
However, we would prefer to have a notion of smallness that is not tied to one particular
type or construction.
Ideally, what we would like to do is to define a locale ‹smallness›, whose assumptions
express closure properties that we would like to hold for a function
‹small :: 'a set ⇒ bool›. This does not quite work, though, because the types involved
in locale assumptions are essentially fixed, so that the function ‹small› could not
be applied polymorphically. A workaround is to have the locale assumption express
closure properties of a function ‹sml :: 'b ⇒ bool›, where type ‹'b› is essentially
fixed, and then to define within the locale context the actually polymorphic function
‹small :: 'a ⇒ bool›, which extends ‹sml› by equipollence to an arbitrary type ‹'a›.
This is essentially what is done in \<^cite>‹"ZFC_in_HOL-AFP"›, except rather than basing the definition
on a notion of smallness derived from a particular type ‹V› we are defining a locale
that takes the type and associated basic notion of smallness as a parameter.
In the development here we have defined a basic ‹smallness› locale, along with several
extensions that express various collections of closure properties. It is not yet clear
how useful this level of generality might turn out to be in practice, however at the
very least, this allows us to segregate the property ``the set of natural number is
small'' from the others. This allows us to consider two interpretations for
``category of small sets and functions''; one of which only has objects corresponding
to finite sets and the other of which also has objects corresponding to infinite sets.
›
section "Basic Notions"
text ‹
Here we define the base locale ‹smallness›, which takes as a parameter a function
‹sml :: 'a set ⇒ bool› that defines a basic notion of smallness at some fixed type,
and extends this basic notion by equipollence to arbitrary types. We assume that
the basic notion of smallness ‹sml› given as a parameter already respects
equipollence, so that ‹small› and ‹sml› coincide at type ‹'a›.
›
locale smallness =
fixes sml :: "'V set ⇒ bool"
assumes lepoll_small_ax: "⟦sml X; lepoll Y X⟧ ⟹ sml Y"
begin
definition small :: "'a set ⇒ bool"
where "small X ≡ ∃X⇩0. sml X⇩0 ∧ X ≈ X⇩0"
lemma smallI:
assumes "sml X⇩0" and "X ≈ X⇩0"
shows "small X"
using assms small_def by auto
lemma smallE:
assumes "small X"
and "⋀X⇩0. ⟦sml X⇩0; X ≈ X⇩0⟧ ⟹ T"
shows T
using assms small_def by blast
lemma small_iff_sml:
shows "small X ⟷ sml X"
using eqpoll_imp_lepoll small_def lepoll_small_ax by blast
lemma lepoll_small:
assumes "small X" and "lepoll Y X"
shows "small Y"
by (metis assms(1,2) eqpoll_sym image_lepoll inj_on_image_eqpoll_self
lepoll_def' lepoll_small_ax lepoll_trans lepoll_trans2 small_def)
lemma smaller_than_small:
assumes "small X" and "Y ⊆ X"
shows "small Y"
using assms lepoll_small subset_imp_lepoll by blast
lemma small_image [intro, simp]:
assumes "small X"
shows "small (f ` X)"
using assms small_def image_lepoll lepoll_small by blast
lemma small_image_iff [simp]: "inj_on f A ⟹ small (f ` A) ⟷ small A"
by (metis small_image the_inv_into_onto)
lemma small_Collect [simp]: "small X ⟹ small {x ∈ X. P x}"
by (simp add: smaller_than_small subset_imp_lepoll)
end
section "Smallness of Finite Sets"
text ‹
The locale ‹small_finite› is satisfied by notions of smallness that admit small
sets of arbitrary finite cardinality.
›
locale small_finite =
smallness +
assumes small_finite_ax: "∃Y. sml Y ∧ eqpoll {1..n :: nat} Y"
begin
lemma small_finite:
shows "finite X ⟹ small X"
using small_finite_ax
by (meson eqpoll_def eqpoll_sym eqpoll_trans ex_bij_betw_nat_finite_1 small_def)
lemma small_insert:
assumes "small X"
shows "small (insert a X)"
by (meson assms eqpoll_imp_lepoll finite.insertI infinite_insert_eqpoll
small_finite lepoll_small)
lemma small_insert_iff [iff]: "small (insert a X) ⟷ small X"
by (meson small_insert smaller_than_small subset_imp_lepoll subset_insertI)
end
section "Smallness of Binary Products"
text ‹
The locale ‹small_product› is satisfied by notions of smallness that are preserved
under cartesian product.
›
locale small_product =
smallness +
assumes small_product_ax: "⟦sml X; sml Y⟧ ⟹ ∃Z. sml Z ∧ eqpoll (X × Y) Z"
begin
lemma small_product [simp]:
assumes "small X" "small Y" shows "small (X × Y)"
by (metis assms(1,2) eqpoll_trans small_def small_product_ax times_eqpoll_cong)
end
section "Smallness of Sums"
text ‹
The locale ‹small_sum› is satisfied by notions of smallness that are preserved
under the formation of small-indexed unions.
›
locale small_sum =
small_finite +
assumes small_sum_ax: "⟦sml X; ⋀x. x ∈ X ⟹ sml (F x)⟧
⟹ ∃U. sml U ∧ eqpoll (Sigma X F) U"
begin
lemma small_binary_sum:
assumes "small X" and "small Y"
shows "small (({False} × X) ∪ ({True} × Y))"
proof -
obtain X⇩0 ρ where X⇩0: "sml X⇩0 ∧ bij_betw ρ X X⇩0"
using assms(1) small_def eqpoll_def by blast
obtain Y⇩0 σ where Y⇩0: "sml Y⇩0 ∧ bij_betw σ Y Y⇩0"
using assms(2) small_def eqpoll_def by blast
obtain B⇩0 β where B⇩0: "sml B⇩0 ∧
bij_betw β {None, Some ({} :: 'b set)} B⇩0"
by (metis eqpoll_def finite.emptyI smallE small_finite.small_finite
small_finite.small_insert_iff small_finite_axioms)
let ?False = "β None" and ?True = "β (Some {})"
have ne: "?False ≠ ?True"
by (metis B⇩0 bij_betw_inv_into_left insertCI option.discI)
let ?ι = "λz. if fst z = False then (?False, ρ (snd z)) else (?True, σ (snd z))"
have "small (({?False} × X⇩0) ∪ ({?True} × Y⇩0))"
proof -
have "Sigma B⇩0 (λx. if x = ?False then X⇩0 else Y⇩0) =
({?False} × X⇩0) ∪ ({?True} × Y⇩0)"
proof
show "Sigma B⇩0 (λx. if x = ?False then X⇩0 else Y⇩0) ⊆
({?False} × X⇩0) ∪ ({?True} × Y⇩0)"
proof
fix bx
assume bx: "bx ∈ Sigma B⇩0 (λx. if x = ?False then X⇩0 else Y⇩0)"
have "fst bx = ?False ∨ fst bx = ?True"
using B⇩0 bij_betw_imp_surj_on bx by fastforce
moreover have "fst bx = ?False ⟹ snd bx ∈ X⇩0"
using bx by force
moreover have "fst bx ≠ ?False ⟹ snd bx ∈ Y⇩0"
using bx by force
ultimately show "bx ∈ ({?False} × X⇩0) ∪ ({?True} × Y⇩0)"
by (metis Un_iff insertCI mem_Times_iff)
qed
show "({?False} × X⇩0) ∪ ({?True} × Y⇩0) ⊆
Sigma B⇩0 (λx. if x = ?False then X⇩0 else Y⇩0)"
using B⇩0 bij_betw_apply ne by fastforce
qed
moreover have "small (Sigma B⇩0 (λx. if x = ?False then X⇩0 else Y⇩0))"
using X⇩0 Y⇩0 B⇩0 small_sum_ax small_def by force
ultimately show ?thesis by auto
qed
moreover have "bij_betw ?ι
(({False} × X) ∪ ({True} × Y))
(({?False} × X⇩0) ∪ ({?True} × Y⇩0))"
proof (intro bij_betwI)
let ?ι' = "λz. if fst z = ?False then (False, inv_into X ρ (snd z))
else (True, inv_into Y σ (snd z))"
show "?ι ∈ ({False} × X) ∪ ({True} × Y) → ({?False} × X⇩0) ∪ ({?True} × Y⇩0)"
using X⇩0 Y⇩0 bij_betw_def
by (auto simp add: bij_betw_apply)
show "?ι' ∈ ({?False} × X⇩0) ∪ ({?True} × Y⇩0) → ({False} × X) ∪ ({True} × Y)"
proof
fix z
assume z: "z ∈ ({?False} × X⇩0) ∪ ({?True} × Y⇩0)"
show "?ι' z ∈ ({False} × X) ∪ ({True} × Y)"
using z
by (metis Un_iff X⇩0 Y⇩0 bij_betw_def inv_into_into mem_Sigma_iff ne prod.collapse
singleton_iff)
qed
show "⋀x. x ∈ {False} × X ∪ {True} × Y ⟹ ?ι' (?ι x) = x"
proof -
fix x
assume x: "x ∈ {False} × X ∪ {True} × Y"
have "?ι x ∈ ({?False} × X⇩0) ∪ ({?True} × Y⇩0)"
using X⇩0 Y⇩0 bij_betwE fst_conv mem_Times_iff x by fastforce
thus "?ι' (?ι x) = x"
using x X⇩0 Y⇩0 bij_betw_inv_into_left ne
by auto[1] fastforce+
qed
show "⋀y. y ∈ ({?False} × X⇩0) ∪ ({?True} × Y⇩0) ⟹ ?ι (?ι' y) = y"
using X⇩0 Y⇩0 bij_betw_inv_into_right ne by fastforce
qed
ultimately show ?thesis
by (meson eqpoll_def eqpoll_trans small_def)
qed
lemma small_union:
assumes X: "small X" and Y: "small Y"
shows "small (X ∪ Y)"
proof -
have "lepoll (X ∪ Y) (({False} × X) ∪ ({True} × Y))"
proof -
let ?ι = "λz. if z ∈ X then (False, z) else (True, z)"
have "?ι ∈ X ∪ Y → ({False} × X) ∪ ({True} × Y) ∧ inj_on ?ι (X ∪ Y)"
by (simp add: inj_on_def)
thus ?thesis
using lepoll_def' by blast
qed
moreover have "small (({False} × X) ∪ ({True} × Y))"
using assms small_binary_sum by blast
ultimately show ?thesis
using lepoll_small by blast
qed
lemma small_Union_spc:
assumes A⇩0: "sml A⇩0" and B: "⋀x. x ∈ A⇩0 ⟹ small (B x)"
shows "small (⋃x∈A⇩0. B x)"
proof -
have 1: "∃B⇩0. ∀x. x ∈ A⇩0 ⟶ sml (B⇩0 x) ∧ eqpoll (B x) (B⇩0 x)"
using A⇩0 B small_def by meson
obtain B⇩0 where B⇩0: "⋀x. x ∈ A⇩0 ⟹ sml (B⇩0 x) ∧ eqpoll (B⇩0 x) (B x)"
using assms 1 eqpoll_sym by blast
have 2: "∃σ. ∀x. x ∈ A⇩0 ⟶ bij_betw (σ x) (B⇩0 x) (B x)"
using B⇩0 eqpoll_def
by (meson ‹⋀x. x ∈ A⇩0 ⟹ sml (B⇩0 x) ∧ B⇩0 x ≈ B x› eqpoll_def)
obtain σ where σ: "⋀x. x ∈ A⇩0 ⟹ bij_betw (σ x) (B⇩0 x) (B x)"
using 2 by blast
have "small (Sigma A⇩0 B⇩0)"
using assms small_sum_ax [of A⇩0 B⇩0] B⇩0 small_def by blast
moreover have "lepoll (⋃x∈A⇩0. B x) (Sigma A⇩0 B⇩0)"
proof -
have "(λz. σ (fst z) (snd z)) ` Sigma A⇩0 B⇩0 = (⋃x∈A⇩0. B x)"
proof
show "(λz. σ (fst z) (snd z)) ` Sigma A⇩0 B⇩0 ⊆ ⋃ (B ` A⇩0)"
unfolding Sigma_def
using σ bij_betwE by fastforce
show "⋃ (B ` A⇩0) ⊆ (λz. σ (fst z) (snd z)) ` Sigma A⇩0 B⇩0"
proof
fix z
assume z: "z ∈ (⋃ (B ` A⇩0))"
obtain x where x: "x ∈ A⇩0 ∧ z ∈ B x"
using z by blast
have "(x, inv_into (B⇩0 x) (σ x) z) ∈ Sigma A⇩0 B⇩0"
by (metis SigmaI σ bij_betw_def inv_into_into x)
moreover have "(λz. σ (fst z) (snd z)) (x, inv_into (B⇩0 x) (σ x) z) = z"
using σ bij_betw_inv_into_right x by fastforce
ultimately show "z ∈ (λz. σ (fst z) (snd z)) ` Sigma A⇩0 B⇩0"
by force
qed
qed
thus ?thesis
by (metis image_lepoll)
qed
ultimately show ?thesis
using lepoll_small by blast
qed
lemma small_Union [simp, intro]:
assumes A: "small A" and B: "⋀x. x ∈ A ⟹ small (B x)"
shows "small (⋃x∈A. B x)"
proof -
obtain A⇩0 ρ where A⇩0: "sml A⇩0 ∧ bij_betw ρ A⇩0 A"
using assms(1) small_def eqpoll_def eqpoll_sym by blast
have "eqpoll (⋃x∈A. B x) (⋃x∈A⇩0. (B ∘ ρ) x)"
by (metis A⇩0 bij_betw_def eqpoll_refl image_comp)
moreover have "small (⋃x∈A⇩0. (B ∘ ρ) x)"
by (metis A⇩0 B bij_betwE comp_apply small_Union_spc)
ultimately show ?thesis
using eqpoll_imp_lepoll lepoll_small by blast
qed
text‹
The @{locale small_sum} locale subsumes the @{locale small_product} locale,
in the sense that any notion of smallness that satisfies @{locale small_sum}
also satisfies @{locale small_product}.
›
sublocale small_product
proof
show "⋀X Y. ⟦sml X; sml Y⟧ ⟹ ∃Z. sml Z ∧ X × Y ≈ Z"
by (simp add: small_sum_ax)
qed
end
section "Smallness of Powersets"
text ‹
The locale ‹small_powerset› is satisfied by notions of smallness for which the set of
all subsets of a small set is again small.
›
locale small_powerset =
smallness +
assumes small_powerset_ax: "sml X ⟹ ∃PX. sml PX ∧ eqpoll (Pow X) PX"
begin
lemma small_powerset:
assumes "small X"
shows "small (Pow X)"
using assms small_powerset_ax
by (meson bij_betw_Pow eqpoll_def eqpoll_trans small_def)
lemma large_UNIV:
shows "¬ small (UNIV :: 'a set)"
using small_powerset_ax Cantors_theorem
by (metis Pow_UNIV UNIV_I eqpoll_iff_bijections small_iff_sml surjI)
end
section "Smallness of the Set of Natural Numbers"
text ‹
The locale ‹small_nat› is satisfied by notions of smallness for which the set of
natural numbers is small.
›
locale small_nat =
smallness +
assumes small_nat_ax: "∃X. sml X ∧ eqpoll X (UNIV :: nat set)"
begin
lemma small_nat:
shows "small (UNIV :: nat set)"
using small_nat_ax small_def eqpoll_sym by auto
end
section "Smallness of Function Spaces"
text ‹
The objective of this section is to define a locale that is satisfied by notions of
smallness for which ``the set of functions between two small sets is small.''
This is complicated in HOL by the requirement that all functions be total,
which forces us to define the value of a function at points outside of what we
would consider to be its domain. If we don't impose some restriction on the values
taken on by a function outside of its domain, then the set of functions between
a domain and codomain set could be large, even if the domain and codomain sets
themselves are small. We could limit the possible variation by restricting our
consideration to ``extensional'' functions; \textit{i.e.}~those that take on a
particular default value outside of their domain, but it becomes awkward if we
have to make an \textit{a priori} choice of what this value should be.
The approach we take here is to define the notion of a ``popular value'' of a function.
This will be a value, in the function's range, whose preimage is a large set.
The idea here is that the default values of extensional functions will typically
have their default values as popular values (though this is not necessarily the
case, as a function whose domain type is small will not have any popular values
according to this definition). We then define a ``small function'' to be a function
whose range is a small set and which has at most one popular value.
The ``essential domain'' of small function is the set of arguments on which the
value of the function is not a popular value. Then we can consistently require of
a smallness notion that, if ‹A› and ‹B› are small sets, that the set of functions
whose essential domains are contained in ‹A› and whose ranges are contained in ‹B›,
is again small.
›
subsection "Small Functions"
context smallness
begin
abbreviation popular_value :: "('b ⇒ 'c) ⇒ 'c ⇒ bool"
where "popular_value F y ≡ ¬ small {x. F x = y}"
definition some_popular_value :: "('b ⇒ 'c) ⇒ 'c"
where "some_popular_value F ≡ SOME y. popular_value F y"
lemma popular_value_some_popular_value:
assumes "∃y. popular_value F y"
shows "popular_value F (some_popular_value F)"
using assms someI_ex [of "λy. popular_value F y"] some_popular_value_def by metis
abbreviation at_most_one_popular_value
where "at_most_one_popular_value F ≡ ∃⇩≤⇩1 y. popular_value F y"
definition small_function
where "small_function F ≡ small (range F) ∧ at_most_one_popular_value F"
lemma small_functionI [intro]:
assumes "small (range f)" and "at_most_one_popular_value f"
shows "small_function f"
using assms small_function_def by blast
lemma small_functionD [dest]:
assumes "small_function f"
shows "small (range f)" and "at_most_one_popular_value f"
using assms small_function_def by auto
end
text‹
If there are small sets of arbitrarily large finite cardinality, then the preimage
of a popular value of a function must be an infinite set (in particular, it must be
nonempty, since the empty set must be small). We can derive various useful consequences
of this fairly lax assumption.
›
context small_finite
begin
lemma popular_value_in_range:
assumes "popular_value F v"
shows "v ∈ range F"
using assms not_finite_existsD small_finite by auto
lemma small_function_const:
shows "small_function (λx. y)"
by (auto simp add: Uniq_def small_finite)
definition inv_into⇩E
where "inv_into⇩E X f ≡ λy. if y ∈ f ` X then inv_into X f y
else SOME x. popular_value f (f x)"
lemma small_function_inv_into⇩E:
assumes "small_function f" and "inj_on f X"
shows "small_function (inv_into⇩E X f)"
proof
show "small (range (inv_into⇩E X f))"
proof -
have "small X"
by (meson assms(1,2) small_functionD(1) small_image_iff smaller_than_small
subset_UNIV subset_image_iff)
moreover have "range (inv_into⇩E X f) ⊆ X ∪ {SOME x. popular_value f (f x)}"
unfolding inv_into⇩E_def
using assms(2) inf_sup_aci(5) by auto
ultimately show ?thesis
using smaller_than_small by auto
qed
show "at_most_one_popular_value (inv_into⇩E X f)"
proof -
have "⋀x. popular_value (inv_into⇩E X f) x ⟹ x = (SOME x. popular_value f (f x))"
proof -
fix x
assume x: "popular_value (inv_into⇩E X f) x"
have "f x ∈ {y. y ∈ f ` X ∧ x = inv_into X f y} ∨ x = (SOME x. popular_value f (f x))"
using assms x
unfolding inv_into⇩E_def
using not_finite_existsD small_finite by fastforce
moreover have "x ≠ (SOME x. popular_value f (f x)) ⟹
f x ∉ {y. y ∈ f ` X ∧ x = inv_into X f y}"
proof -
assume 1: "x ≠ (SOME x. popular_value f (f x))"
have "small {y. y ∈ f ` X ∧ x = inv_into X f y}"
using assms
by (metis (no_types, lifting) image_subset_iff mem_Collect_eq rangeI
small_functionD(1) smaller_than_small subsetI)
thus ?thesis
using x 1
unfolding inv_into⇩E_def
by (simp add: Collect_mono smallness.smaller_than_small smallness_axioms)
qed
ultimately show "x = (SOME x. popular_value f (f x))" by blast
qed
thus ?thesis
using Uniq_def by blast
qed
qed
end
context small_sum
begin
lemma small_function_comp:
assumes "small_function f" and "small_function g"
shows "small_function (g ∘ f)"
proof
show "small (range (g ∘ f))"
by (metis assms(1) fun.set_map small_image small_functionD(1))
show "at_most_one_popular_value (g ∘ f)"
proof -
have *: "⋀z. popular_value (g ∘ f) z ⟹ ∃y. popular_value f y ∧ g y = z"
proof -
fix z
assume z: "popular_value (g ∘ f) z"
have "¬ small {x. g (f x) = z}"
using z by auto
moreover have "{x. g (f x) = z} = (⋃y∈range f ∩ {y. g y = z}. {x. f x = y})"
by auto
moreover have "small (range f ∩ {y. g y = z})"
using assms(1) small_functionD(1) smaller_than_small by force
ultimately have "∃y. y ∈ range f ∩ {y. g y = z} ∧ popular_value f y"
by auto
thus "∃y. popular_value f y ∧ g y = z" by blast
qed
show ?thesis
proof
fix y y'
assume y: "popular_value (g ∘ f) y" and y': "popular_value (g ∘ f) y'"
have "∃x. popular_value f x ∧ g x = y"
using y * by blast
moreover have "∃x. popular_value f x ∧ g x = y'"
using y' * by blast
ultimately show "y = y'"
using assms(2)
by (metis (mono_tags, lifting) assms(1) small_functionD(2) the1_equality')
qed
qed
qed
text‹
In the present context, a small function has a popular value if and only if its domain
type is large. This simplifies special cases that concern whether or not a function
happens to have any popular value at all.
›
lemma ex_popular_value_iff:
assumes "small_function (F :: 'b ⇒ 'c)"
shows "(∃v. popular_value F v) ⟷ ¬ small (UNIV :: 'b set)"
proof
show "∃v. popular_value F v ⟹ ¬ small (UNIV :: 'b set)"
using smaller_than_small by blast
have "¬ (∃v. popular_value F v) ⟹ small (UNIV :: 'b set)"
proof -
assume "¬ (∃y. popular_value F y)"
hence "⋀y. small {x. F x = y}"
by blast
moreover have "UNIV = (⋃y∈range F. {x. F x = y})"
by auto
ultimately show "small (UNIV :: 'b set)"
using assms(1) small_function_def by (metis small_Union)
qed
thus "¬ small (UNIV :: 'b set) ⟹ ∃v. popular_value F v"
by blast
qed
text‹
A consequence is that the preimage of the set of all unpopular values of a function
is small.
›
lemma small_preimage_unpopular:
fixes F :: "'b ⇒ 'c"
assumes "small_function F"
shows "small {x. F x ≠ some_popular_value F}"
proof (cases "∃y. popular_value F y")
assume 1: "¬ (∃y. popular_value F y)"
thus ?thesis
using assms ex_popular_value_iff smaller_than_small by blast
next
assume 1: "∃y. popular_value F y"
have "popular_value F (some_popular_value F)"
using 1 popular_value_some_popular_value by metis
hence 2: "⋀y. y ≠ some_popular_value F ⟹ small {x. F x = y}"
using assms
unfolding small_function_def
by (meson Uniq_D)
moreover have "{x. F x ≠ some_popular_value F} =
(⋃y∈{y. y ∈ range F ∧ y ≠ some_popular_value F}. {x. F x = y})"
by auto
ultimately show ?thesis
using assms
unfolding small_function_def
by auto
qed
text‹
Here we are working toward showing that a small function has a ``small encoding'',
which consists of its graph for arguments that map to non-popular values,
paired with the single popular value it has on all other arguments.
›
abbreviation SF_Dom
where "SF_Dom f ≡ {x. ¬ popular_value f (f x)}"
abbreviation SF_Rng
where "SF_Rng f ≡ f ` SF_Dom f"
abbreviation SF_Grph
where "SF_Grph f ≡ (λx. (x, f x)) ` SF_Dom f"
abbreviation the_PV
where "the_PV f ≡ THE y. popular_value f y"
lemma small_SF_Dom:
assumes "small_function f"
shows "small (SF_Dom f)"
proof -
let ?F = "λy. {x. f x = y}"
have "SF_Dom f = (⋃y ∈ SF_Rng f. ?F y)"
proof
show "SF_Dom f ⊆ (⋃y ∈ SF_Rng f. ?F y)"
by blast
show "(⋃y ∈ SF_Rng f. ?F y) ⊆ SF_Dom f"
proof
fix x
assume x: "x ∈ (⋃y ∈ SF_Rng f. ?F y)"
obtain S y where S: "x ∈ S ∧ y ∈ SF_Rng f ∧ S = {x. f x = y}"
using x by force
show "x ∈ SF_Dom f"
using S by fastforce
qed
qed
moreover have "⋀y. y ∈ SF_Rng f ⟹ small (?F y)"
using assms by blast
ultimately show ?thesis
using small_Union [of "SF_Rng f" ?F]
by (metis assms image_mono small_functionD(1) smaller_than_small subset_UNIV)
qed
lemma small_SF_Rng:
assumes "small_function f"
shows "small (SF_Rng f)"
using assms small_SF_Dom by blast
lemma small_SF_Grph:
assumes "small_function f"
shows "small (SF_Grph f)"
using assms small_SF_Dom by blast
lemma small_function_expansion:
assumes "small_function f"
shows "f = (λx. if x ∈ fst ` SF_Grph f then (THE y. (x, y) ∈ SF_Grph f) else the_PV f)"
proof
fix x
show "f x = (if x ∈ fst ` SF_Grph f then (THE y. (x, y) ∈ SF_Grph f) else the_PV f)"
proof (cases "x ∈ SF_Dom f")
show "x ∉ SF_Dom f ⟹ ?thesis"
proof -
assume "x ∉ SF_Dom f"
hence "f x = the_PV f"
using assms the1_equality' by fastforce
thus ?thesis
by (simp add: image_iff)
qed
show "x ∈ SF_Dom f ⟹ ?thesis"
by (simp add: image_iff)
qed
qed
end
subsection "Small Funcsets"
locale small_funcset =
small_sum +
small_powerset
begin
text‹
For a suitable definition of ``between'', the set of small functions between
small sets is small.
›
lemma small_funcset:
assumes "small X" and "small Y"
shows "small {f. small_function f ∧ SF_Dom f ⊆ X ∧ range f ⊆ Y}"
proof -
let ?Rep = "λf. (SF_Grph f, Collect (popular_value f))"
let ?SF = "{f. small_function f ∧ SF_Dom f ⊆ X ∧ range f ⊆ Y}"
have *: "⋀f x. ⟦f ∈ ?SF; x ∉ SF_Dom f⟧ ⟹ {f x} = Collect (popular_value f)"
proof -
fix f x
assume f: "f ∈ ?SF" and x: "x ∉ SF_Dom f"
show "{f x} = Collect (popular_value f)"
proof -
have 1: "popular_value f (f x)"
using x by blast
have "∃!y. popular_value f y"
proof -
have "∃y. popular_value f y"
using 1 by blast
moreover have "⋀y y'. ⟦popular_value f y; popular_value f y'⟧ ⟹ y = y'"
using f Uniq_def small_functionD(2)
by (metis (mono_tags, lifting) mem_Collect_eq)
ultimately show ?thesis by blast
qed
thus ?thesis
using f 1 by blast
qed
qed
have "small (?Rep ` ?SF)"
proof -
have "?Rep ∈ ?SF → Pow (X × Y) × Pow Y"
using popular_value_in_range by fastforce
moreover have "small (Pow (X × Y) × Pow Y)"
using assms by (simp add: small_powerset)
ultimately show ?thesis
by (simp add: image_subset_iff_funcset smaller_than_small)
qed
moreover have "inj_on ?Rep ?SF"
proof
fix f g :: "'b ⇒ 'c"
assume f: "f ∈ ?SF" and g: "g ∈ ?SF"
assume eq: "?Rep f = ?Rep g"
show "f = g"
proof
fix x
show "f x = g x"
proof (cases "x ∈ SF_Dom f")
show "x ∉ SF_Dom f ⟹ ?thesis"
proof -
assume x: "x ∉ SF_Dom f"
have "{f x} = Collect (popular_value f)"
using f x * by blast
also have "... = Collect (popular_value g)"
using eq by force
also have "... = {g x}"
using g x eq * [of g x] by blast
finally show "f x = g x" by blast
qed
show "x ∈ SF_Dom f ⟹ ?thesis"
using f g eq small_function_expansion by blast
qed
qed
qed
ultimately show ?thesis
using small_image_iff by blast
qed
end
section "Smallness of Sets of Lists"
text‹
A notion of smallness that is preserved under sum and powerset, and in addition declares
the set of natural numbers to be small, is sufficiently inclusive as to include any
set whose existence is provable in ZFC. So it is not a surprise that we can show,
for example, that the set of lists with elements in a given small set is again small.
We do not use this particular fact in the present development, but we will have a use for
it in a subsequent article.
›
locale small_funcset_and_nat =
small_funcset +
small_nat
begin
definition list_as_fn :: "'b list ⇒ nat ⇒ 'b option"
where "list_as_fn l n = (if n ≥ length l then None else Some (l ! n))"
lemma inj_list_as_fn:
shows "inj list_as_fn"
proof
fix x y :: "'b list"
have 1: "⋀l :: 'b list. list_as_fn l (length l) = None"
unfolding list_as_fn_def by simp
assume eq: "list_as_fn x = list_as_fn y"
have "length x = length y"
using eq 1
by (metis (no_types, lifting) list_as_fn_def nle_le not_Some_eq)
moreover have "⋀n. n < length x ⟹ x ! n = y ! n"
using eq list_as_fn_def
by (metis calculation leD option.inject)
ultimately show "x = y"
using nth_equalityI by blast
qed
lemma small_function_list_as_fn:
shows "small_function (list_as_fn l)"
using Uniq_def small_function_def small_nat smaller_than_small by fastforce
lemma small_listset:
assumes "small Y"
shows "small {l. List.set l ⊆ Y}"
proof -
let ?SF = "λf. small_function f ∧ SF_Dom f ⊆ (UNIV :: nat set) ∧
range f ⊆ Some ` Y ∪ {None}"
have "list_as_fn ` {l. List.set l ⊆ Y} ⊆ Collect ?SF"
proof
fix f
assume f: "f ∈ list_as_fn ` {l. List.set l ⊆ Y}"
show "f ∈ Collect ?SF"
using f small_function_list_as_fn
unfolding list_as_fn_def
apply auto
by fastforce
qed
moreover have "small (Collect ?SF)"
using assms small_nat small_funcset [of "UNIV :: nat set" "Some ` Y ∪ {None}"]
by auto
ultimately show ?thesis
using small_image_iff [of list_as_fn "{l. list.set l ⊆ Y}"] inj_list_as_fn
smaller_than_small
by (metis (mono_tags, lifting) injD inj_onI)
qed
end
end