Theory Universe
chapter "Universe"
theory Universe
imports Smallness
begin
text‹
This section defines a ``universe'' to be a set ‹univ› that admits embeddings of
various other sets, typically the result of constructions on ‹univ› itself.
These embeddings allow us to perform constructions on ‹univ› that result in sets
at higher types, and then to encode the results of these constructions back down
into ‹univ›. An example application is showing that a category admits products:
given objects ‹a› and ‹b› in a category whose arrows form a universe ‹univ›,
for each object ‹x› we may form the cartesian product ‹hom x a × hom x b ⊆ univ × univ›
and then use an embedding of ‹univ × univ› in ‹univ› (\textit{i.e.}~a pairing function)
to map the result back into ‹univ›. Assuming we can show that the resulting set
has the proper structure to be the set of arrows of an object of the category,
we obtain an object ‹a × b› with ‹hom x (a × b) ≅ hom x a × hom x b›,
as required for a product object in a category.
›
section "Embeddings"
text‹
Here we define some basic notions pertaining to injections into a set ‹univ›.
›
locale embedding =
fixes univ :: "'U set"
begin
abbreviation is_embedding_of
where "is_embedding_of ι X ≡ inj_on ι X ∧ ι ` X ⊆ univ"
definition some_embedding_of
where "some_embedding_of X ≡ SOME ι. is_embedding_of ι X"
abbreviation embeds
where "embeds X ≡ ∃ι. is_embedding_of ι X"
lemma is_embedding_of_some_embedding_of:
assumes "embeds X"
shows "is_embedding_of (some_embedding_of X) X"
unfolding some_embedding_of_def
using assms someI_ex [of "λι. is_embedding_of ι X"] by force
lemma embeds_subset:
assumes "embeds X" and "Y ⊆ X"
shows "embeds Y"
using assms
by (meson dual_order.trans image_mono inj_on_subset)
end
section "Lifting"
text‹
The locale ‹lifting› axiomatizes a set ‹univ› that embeds itself, together with
an additional element. This is equivalent to ‹univ› being infinite.
›
locale lifting =
embedding univ
for univ :: "'U set" +
assumes embeds_lift: "embeds ({None} ∪ Some ` univ)"
begin
definition some_lifting :: "'U option ⇒ 'U"
where "some_lifting ≡ some_embedding_of ({None} ∪ Some ` univ)"
lemma some_lifting_is_embedding:
shows "is_embedding_of some_lifting ({None} ∪ Some ` univ)"
unfolding some_lifting_def
using is_embedding_of_some_embedding_of embeds_lift by blast
lemma some_lifting_in_univ [intro, simp]:
shows "some_lifting None ∈ univ"
and "x ∈ univ ⟹ some_lifting (Some x) ∈ univ"
using some_lifting_is_embedding by auto
lemma some_lifting_cancel:
shows "⟦x ∈ univ; some_lifting (Some x) = some_lifting None⟧ ⟹ False"
and "⟦x ∈ univ; x' ∈ univ; some_lifting (Some x) = some_lifting (Some x')⟧ ⟹ x = x'"
using some_lifting_is_embedding
apply (meson Un_iff imageI inj_on_contraD insertI1 option.simps(3))
using some_lifting_is_embedding
by (meson UnI2 imageI inj_on_contraD option.inject)
lemma infinite_univ:
shows "infinite univ"
by (metis None_notin_image_Some card_image card_inj_on_le card_insert_disjoint
embeds_lift finite_imageI inj_Some insert_is_Un le_imp_less_Suc linorder_neq_iff)
lemma embeds_bool:
shows "embeds (UNIV :: bool set)"
by (metis comp_inj_on ex_inj image_comp image_mono infinite_univ
infinite_iff_countable_subset inj_on_subset subset_trans top_greatest)
lemma embeds_nat:
shows "embeds (UNIV :: nat set)"
by (metis infinite_univ infinite_iff_countable_subset)
end
section "Pairing"
text‹
The locale ‹pairing› axiomatizes a set ‹univ› that embeds ‹univ × univ›.
›
locale pairing =
embedding univ
for univ :: "'U set" +
assumes embeds_pairs: "embeds (univ × univ)"
begin
definition some_pairing :: "'U * 'U ⇒ 'U"
where "some_pairing ≡ some_embedding_of (univ × univ)"
lemma some_pairing_is_embedding:
shows "is_embedding_of some_pairing (univ × univ)"
unfolding some_pairing_def
using embeds_pairs is_embedding_of_some_embedding_of by blast
abbreviation pair
where "pair x y ≡ some_pairing (x, y)"
abbreviation is_pair :: "'U ⇒ bool"
where "is_pair x ≡ x ∈ some_pairing ` (univ × univ)"
definition first :: "'U ⇒ 'U"
where "first x ≡ fst (inv_into (univ × univ) some_pairing x)"
definition second :: "'U ⇒ 'U"
where "second x = snd (inv_into (univ × univ) some_pairing x)"
lemma first_conv:
assumes "x ∈ univ" and "y ∈ univ"
shows "first (pair x y) = x"
using assms first_def some_pairing_is_embedding
by (metis (mono_tags, lifting) fst_eqD inv_into_f_f mem_Times_iff snd_eqD)
lemma second_conv:
assumes "x ∈ univ" and "y ∈ univ"
shows "second (pair x y) = y"
using assms second_def some_pairing_is_embedding
by (metis (mono_tags, lifting) fst_eqD inv_into_f_f mem_Times_iff snd_eqD)
lemma pair_conv:
assumes "is_pair x"
shows "pair (first x) (second x) = x"
using assms first_def second_def embeds_pairs is_embedding_of_some_embedding_of
by (simp add: f_inv_into_f)
lemma some_pairing_in_univ [intro, simp]:
shows "⟦x ∈ univ; y ∈ univ⟧ ⟹ pair x y ∈ univ"
using some_pairing_is_embedding by blast
lemma some_pairing_cancel:
shows "⟦x ∈ univ; x' ∈ univ; y ∈ univ; y' ∈ univ; pair x y = pair x' y'⟧
⟹ x = x' ∧ y = y'"
using embeds_pairs
by (metis first_conv second_conv)
end
section "Powering"
text‹
The ‹powering› locale axiomatizes a universe that embeds the set of all its ``small'' subsets.
Obviously, some condition on the subsets is required because (by Cantor's Theorem) it is
not possible for a set to embed the set of \emph{all} its subsets.
The concept of ``smallness'' used here is not fixed, but rather is taken as a parameter.
›
locale powering =
embedding univ +
smallness sml
for sml :: "'V set ⇒ bool"
and univ :: "'U set" +
assumes embeds_small_sets: "embeds {X. X ⊆ univ ∧ small X}"
begin
abbreviation some_embedding_of_small_sets :: "('U set) ⇒ 'U"
where "some_embedding_of_small_sets ≡ some_embedding_of {X. X ⊆ univ ∧ small X}"
definition emb_set :: "('U set) ⇒ 'U"
where "emb_set ≡ some_embedding_of_small_sets"
lemma emb_set_is_embedding:
shows "is_embedding_of emb_set {X. X ⊆ univ ∧ small X}"
unfolding emb_set_def
using embeds_small_sets is_embedding_of_some_embedding_of by blast
lemma emb_set_in_univ [intro, simp]:
shows "⟦X ⊆ univ; small X⟧ ⟹ emb_set X ∈ univ"
using emb_set_is_embedding by blast
lemma emb_set_cancel:
shows "⟦X ⊆ univ; small X; X' ⊆ univ; small X'; emb_set X = emb_set X'⟧ ⟹ X = X'"
using emb_set_is_embedding
by (metis (mono_tags, lifting) inj_onD mem_Collect_eq)
text‹
If ‹univ› embeds the collection of all its small subsets, then ‹univ› itself
must be large.
›
lemma large_univ:
shows "¬ small univ"
proof -
have "small univ ⟹ False"
proof -
assume small: "small univ"
have "embeds (Pow univ)"
using small smaller_than_small embeds_small_sets
by (metis (no_types, lifting) CollectI PowD embeds_subset subsetI)
thus False
using Cantors_theorem
by (metis Pow_not_empty inj_on_iff_surj)
qed
thus ?thesis by blast
qed
end
section "Tupling"
text‹
The ‹tupling› locale axiomatizes a set ‹univ› that embeds the set of all
``small extensional functions'' on its elements. Here, the notion of
``extensional function'' is parametrized by the default value ‹null› produced
by such a function when it is applied to an argument outside of ‹univ›.
The default value ‹null› is neither assumed to be in ‹univ› nor outside of it.
›
locale tupling =
lifting univ +
pairing univ +
powering sml univ +
small_funcset sml
for sml :: "'V set ⇒ bool"
and univ :: "'U set"
and null :: "'U"
begin
text‹
‹EF› is the set of extensional functions on ‹univ›. These map ‹univ› to
‹univ ∪ {null}› and map values outside of ‹univ› to ‹null›. The default
value ‹null› might or might not be an element of ‹univ›.
The set ‹SEF› is the subset of ‹EF› consisting of those functions that
are ``small functions''.
›
definition EF
where "EF ≡ {f. f ` univ ⊆ univ ∪ {null} ∧ (∀x. x ∉ univ ⟶ f x = null)}"
abbreviation SEF
where "SEF ≡ Collect small_function ∩ EF"
lemma EF_apply:
assumes "F ∈ EF"
shows "x ∈ univ ⟹ F x ∈ univ ∪ {null}"
and "x ∉ univ ⟹ F x = null"
using assms
unfolding EF_def by auto
text‹
Since ‹univ› is large, the set of all values at type ‹'U› must also be large.
This implies that every small extensional function having type ‹'U› as its domain
type must have a popular value.
›
lemma SEFs_have_popular_value:
assumes "F ∈ SEF"
shows "∃v. popular_value F v"
using assms ex_popular_value_iff large_UNIV
by (metis Int_iff large_univ mem_Collect_eq smaller_than_small top_greatest)
text‹
The following technical lemma uses powering to obtain an encoding of small
extensional functions as elements of ‹univ›. The idea is that a small extensional
function ‹F› mapping ‹univ› to ‹univ ∪ {null}› can be canonically described
by a small subset of ‹univ × (univ ∪ {null})› consisting of all pairs
‹(x, F x) ⊆ univ × (univ ∪ {null})› for which ‹F x› is not a popular value,
together with the single popular value of ‹F› taken at other arguments ‹x›
not represented by such pairs.
›
lemma embeds_SEF:
shows "embeds SEF"
proof (intro exI conjI)
have range_F: "⋀F. F ∈ SEF ⟹ range F ⊆ univ ∪ {null}"
unfolding EF_def by blast
let ?lift = "some_embedding_of (univ ∪ {null})"
have lift: "is_embedding_of ?lift (univ ∪ {null})"
using embeds_lift is_embedding_of_some_embedding_of
by (metis bij_betw_imp_surj_on infinite_univ infinite_imp_bij_betw2
inj_on_iff_surj insert_not_empty sup_bot.neutr_eq_iff)
have lift_cancel [simp]: "⋀x y. ⟦x ∈ univ ∪ {null}; y ∈ univ ∪ {null}; ?lift x = ?lift y⟧
⟹ x = y"
using lift by (meson UnI1 inj_on_eq_iff)
have 0: "⋀F. F ∈ SEF ⟹ ?lift (some_popular_value F) ∈ univ"
using range_F popular_value_in_range popular_value_some_popular_value
SEFs_have_popular_value
by (metis image_subset_iff lift subset_eq)
have 1: "⋀F. F ∈ SEF ⟹ small {x ∈ univ. ¬ popular_value F (F x)}"
by (metis (no_types) CollectD Collect_conj_eq IntE inf_le2 small_SF_Dom
smaller_than_small)
have 2: "⋀F. F ∈ SEF ⟹
(λa. pair a (?lift (F a))) ` {x ∈ univ. ¬ popular_value F (F x)} ⊆ univ"
apply auto[1]
by (metis (no_types, lifting) CollectD EF_def Un_commute image_subset_iff insert_is_Un
lift some_pairing_in_univ)
have 3: "⋀F. F ∈ SEF ⟹
emb_set ((λa. pair a (?lift (F a))) ` {x ∈ univ. ¬ popular_value F (F x)})
∈ univ"
using 1 2 by blast
let ?e = "λF. pair (?lift (some_popular_value F))
(emb_set ((λa. pair a (?lift (F a))) `
{x ∈ univ. ¬ popular_value F (F x)}))"
show "?e ` SEF ⊆ univ"
using 0 3 some_pairing_in_univ by blast
show "inj_on ?e SEF"
proof (intro inj_onI)
fix F F' :: "'U ⇒ 'U"
assume F: "F ∈ SEF"
assume F': "F' ∈ SEF"
assume eq: "?e F = ?e F'"
have *: "⋀x. x ∈ univ ⟹
first (pair x (?lift (F x))) = x ∧
second (pair x (?lift (F x))) = ?lift (F x) ∧
first (pair x (?lift (F' x))) = x ∧
second (pair x (?lift (F' x))) = ?lift (F' x)"
by (meson F F' first_conv image_subset_iff lift range_F range_subsetD second_conv)
have 4: "?lift (some_popular_value F) = ?lift (some_popular_value F') ∧
emb_set ((λa. pair a (?lift (F a))) ` {x ∈ univ. ¬ popular_value F (F x)}) =
emb_set ((λa. pair a (?lift (F' a))) ` {x ∈ univ. ¬ popular_value F' (F' x)})"
using F F' 0 3 eq some_pairing_cancel by meson
have 5: "(λa. pair a (?lift (F a))) ` {x ∈ univ. ¬ popular_value F (F x)} =
(λa. pair a (?lift (F' a))) ` {x ∈ univ. ¬ popular_value F' (F' x)}"
using F F' 1 2 4 small_preimage_unpopular smaller_than_small
emb_set_cancel
[of "(λa. pair a (?lift (F a))) ` {x ∈ univ. ¬ popular_value F (F x)}"
"(λa. pair a (?lift (F' a))) ` {x ∈ univ. ¬ popular_value F' (F' x)}"]
by blast
have 6: "{x ∈ univ. ¬ popular_value F (F x)} = {x ∈ univ. ¬ popular_value F' (F' x)}"
proof -
have "(λa. first (pair a (?lift (F a)))) ` {x ∈ univ. ¬ popular_value F (F x)} =
(λa. first (pair a (?lift (F' a)))) ` {x ∈ univ. ¬ popular_value F' (F' x)} ∧
(λa. second (pair a (?lift (F a)))) ` {x ∈ univ. ¬ popular_value F (F x)} =
(λa. second (pair a (?lift (F' a)))) ` {x ∈ univ. ¬ popular_value F' (F' x)}"
using 5 by (metis image_image)
thus ?thesis
using * embeds_pairs is_embedding_of_some_embedding_of by auto
qed
have 7: "⋀x. x ∈ univ ∧ ¬ popular_value F (F x) ⟹ F x = F' x"
proof -
fix x
assume x: "x ∈ univ ∧ ¬ popular_value F (F x)"
have "?lift (F x) = ?lift (F' x)"
proof -
have "⋀y. ((x, y) ∈ (λx. (x, ?lift (F x))) ` {x ∈ univ. ¬ popular_value F (F x)}
⟷ y = ?lift (F x)) ∧
((x, y) ∈ (λx. (x, ?lift (F' x))) ` {x ∈ univ. ¬ popular_value F (F x)}
⟷ y = ?lift (F' x))"
using x by blast
moreover have "(λx. (x, ?lift (F x))) ` {x ∈ univ. ¬ popular_value F (F x)} =
(λx. (x, ?lift (F' x))) ` {x ∈ univ. ¬ popular_value F (F x)}"
proof -
have "(λx. (x, ?lift (F x))) ` {x ∈ univ. ¬ popular_value F (F x)} =
(λx. (x, ?lift (F' x))) ` {x ∈ univ. ¬ popular_value F' (F' x)}"
proof -
have "(λx. (first (pair x (?lift (F x))), second (pair x (?lift (F x)))))
` {x ∈ univ. ¬ popular_value F (F x)} =
(λx. (first (pair x (?lift (F' x))), second (pair x (?lift (F' x)))))
` {x ∈ univ. ¬ popular_value F' (F' x)}"
proof -
have "(λx. (first x, second x)) ` (λa. pair a (?lift (F a)))
` {x ∈ univ. ¬ popular_value F (F x)} =
(λx. (first x, second x)) ` (λa. pair a (?lift (F' a)))
` {x ∈ univ. ¬ popular_value F' (F' x)}"
using 5 by argo
thus ?thesis by blast
qed
thus ?thesis
using * some_pairing_cancel by auto
qed
thus ?thesis
using 6 by blast
qed
ultimately show ?thesis by fastforce
qed
thus "F x = F' x"
by (metis EF_apply(1) F F' Int_iff lift_cancel x)
qed
show "F = F'"
proof
fix x
show "F x = F' x"
proof (cases "x ∈ univ")
case False
show ?thesis
using F F' False EF_def
by (metis EF_apply(2) IntE)
next
assume x: "x ∈ univ"
show ?thesis
proof (cases "popular_value F (F x)")
case False
show ?thesis
using 7 False x by blast
next
case True
show ?thesis
proof -
have "F x = some_popular_value F"
by (metis (mono_tags, lifting) CollectD Collect_mono F IntE True
small_preimage_unpopular smallness.smaller_than_small smallness_axioms)
moreover have "F' x = some_popular_value F'"
proof -
have "popular_value F' (F' x)"
using True x 6 by blast
thus ?thesis
by (metis (mono_tags, lifting) CollectD Collect_mono F' IntE
small_preimage_unpopular smallness.smaller_than_small smallness_axioms)
qed
moreover have "some_popular_value F = some_popular_value F'"
using F F' 4 calculation lift_cancel range_F range_subsetD
by (metis (no_types, opaque_lifting))
ultimately show ?thesis by auto
qed
qed
qed
qed
qed
qed
definition some_embedding_of_small_functions :: "('U ⇒ 'U) ⇒ 'U"
where "some_embedding_of_small_functions ≡ some_embedding_of SEF"
lemma some_embedding_of_small_functions_is_embedding:
shows "is_embedding_of some_embedding_of_small_functions SEF"
unfolding some_embedding_of_small_functions_def
using embeds_SEF is_embedding_of_some_embedding_of by blast
lemma some_embedding_of_small_functions_in_univ [intro, simp]:
assumes "F ∈ SEF"
shows "some_embedding_of_small_functions F ∈ univ"
using assms some_embedding_of_small_functions_is_embedding by blast
lemma some_embedding_of_small_functions_cancel:
assumes "F ∈ SEF" and "F' ∈ SEF"
and "some_embedding_of_small_functions F = some_embedding_of_small_functions F'"
shows "F = F'"
using assms some_embedding_of_small_functions_is_embedding
by (meson inj_onD)
end
section "Universe"
text‹
The ‹universe› locale axiomatizes a set that is equipped with an embedding of its
own small extensional function space, and in addition the set of natural numbers
is required to be small (\textit{i.e.}~there is a small infinite set).
›
locale universe =
tupling sml univ null +
small_nat sml
for sml :: "'V set ⇒ bool"
and univ :: "'U set"
and null :: "'U"
begin
text‹
For a fixed notion of smallness, the property of being a universe is respected
by equipollence; thus it is a property of the set itself, rather than something
that depends on the ambient type.
›
lemma is_respected_by_equipollence:
assumes "eqpoll univ univ'"
shows "universe sml univ'"
proof
obtain γ where γ: "bij_betw γ univ univ'"
using assms eqpoll_def by blast
show "∃ι. inj_on ι ({None} ∪ Some ` univ') ∧ ι ` ({None} ∪ Some ` univ') ⊆ univ'"
proof -
let ?ι = "λ None ⇒ γ (some_lifting None)
| Some x ⇒ γ (some_lifting (Some (inv_into univ γ x)))"
have "?ι ` ({None} ∪ Some ` univ') ⊆ univ'"
using γ is_embedding_of_some_embedding_of bij_betw_apply
apply auto[1]
apply fastforce
by (simp add: bij_betw_imp_surj_on inv_into_into)
moreover have "inj_on ?ι ({None} ∪ Some ` univ')"
proof
fix x y
assume x: "x ∈ {None} ∪ Some ` univ'"
assume y: "y ∈ {None} ∪ Some ` univ'"
assume eq: "?ι x = ?ι y"
show "x = y"
using x y eq γ some_lifting_cancel
apply auto[1]
by (metis bij_betw_def inv_into_f_eq inv_into_into inv_into_injective
inv_into_into some_lifting_in_univ(1,2))+
qed
ultimately show ?thesis by blast
qed
show "∃ι. inj_on ι (univ' × univ') ∧ ι ` (univ' × univ') ⊆ univ'"
proof -
let ?ι = "λx. γ (some_pairing (inv_into univ γ (fst x), inv_into univ γ (snd x)))"
have "?ι ` (univ' × univ') ⊆ univ'"
proof -
have "⋀x. x ∈ univ' × univ' ⟹ ?ι x ∈ univ'"
by (metis γ bij_betw_def imageI inv_into_into mem_Times_iff some_pairing_in_univ)
thus ?thesis by blast
qed
moreover have "inj_on ?ι (univ' × univ')"
proof
fix x y
assume x: "x ∈ univ' × univ'" and y: "y ∈ univ' × univ'"
assume eq: "?ι x = ?ι y"
show "x = y"
proof -
have "pair (inv_into univ γ (fst x)) (inv_into univ γ (snd x)) =
pair (inv_into univ γ (fst y)) (inv_into univ γ (snd y))"
proof -
have "inv_into univ γ (fst x) ∈ univ ∧ inv_into univ γ (snd x) ∈ univ ∧
inv_into univ γ (fst y) ∈ univ ∧ inv_into univ γ (snd y) ∈ univ"
by (metis γ bij_betw_imp_surj_on inv_into_into mem_Times_iff x y)
thus ?thesis
by (metis γ bij_betw_inv_into_left eq some_pairing_in_univ)
qed
hence "inv_into univ γ (fst x) = inv_into univ γ (fst y) ∧
inv_into univ γ (snd x) = inv_into univ γ (snd y)"
using x y eq γ
by (metis bij_betw_imp_surj_on first_conv inv_into_into mem_Times_iff second_conv)
hence "fst x = fst y ∧ snd x = snd y"
by (metis (full_types) γ bij_betw_inv_into_right mem_Times_iff x y)
thus "x = y"
by (simp add: prod_eq_iff)
qed
qed
ultimately show ?thesis by blast
qed
show "∃ι. inj_on ι {X. X ⊆ univ' ∧ small X} ∧ ι ` {X. X ⊆ univ' ∧ small X} ⊆ univ'"
proof -
let ?ι = "λX. γ (emb_set (inv_into univ γ ` X))"
have "?ι ` {X. X ⊆ univ' ∧ small X} ⊆ univ'"
proof
fix X'
assume X': "X' ∈ ?ι ` {X. X ⊆ univ' ∧ small X}"
obtain X where X: "X ⊆ univ' ∧ small X ∧ ?ι X = X'"
using X' by blast
have "?ι X ∈ univ'"
by (metis X γ bij_betw_def bij_betw_inv_into imageI image_mono emb_set_in_univ
small_image)
thus "X' ∈ univ'"
using X by blast
qed
moreover have "inj_on ?ι {X. X ⊆ univ' ∧ small X}"
proof
fix X X'
assume X: "X ∈ {X. X ⊆ univ' ∧ small X}"
assume X': "X' ∈ {X. X ⊆ univ' ∧ small X}"
assume eq: "?ι X = ?ι X'"
show "X = X'"
proof -
have "emb_set (inv_into univ γ ` X) = emb_set (inv_into univ γ ` X')"
proof -
have "emb_set (inv_into univ γ ` X) ∈ univ ∧ emb_set (inv_into univ γ ` X') ∈ univ"
by (metis (no_types, lifting) Int_Collect Int_iff X X' γ bij_betw_def
bij_betw_inv_into powering.emb_set_in_univ powering_axioms small_image
subset_image_iff)
thus ?thesis
by (metis γ bij_betw_inv_into_left eq)
qed
hence "inv_into univ γ ` X = inv_into univ γ ` X'"
by (metis (no_types, lifting) Int_Collect Int_iff X X' γ bij_betw_def
bij_betw_inv_into powering.emb_set_cancel powering_axioms small_image
subset_image_iff)
thus ?thesis
by (metis X X' γ bij_betw_imp_surj_on image_inv_into_cancel mem_Collect_eq)
qed
qed
ultimately show ?thesis by blast
qed
qed
text‹
A universe admits an embedding of all lists formed from its elements.
›
sublocale small_funcset_and_nat ..
fun some_embedding_of_lists :: "'U list ⇒ 'U"
where "some_embedding_of_lists [] = some_lifting None"
| "some_embedding_of_lists (x # l) =
some_lifting (Some (some_pairing (x, some_embedding_of_lists l)))"
lemma embeds_lists:
shows "embeds {l. List.set l ⊆ univ}"
and "is_embedding_of some_embedding_of_lists {l. List.set l ⊆ univ}"
proof -
show "is_embedding_of some_embedding_of_lists {l. List.set l ⊆ univ}"
proof
show *: "some_embedding_of_lists ` {l. list.set l ⊆ univ} ⊆ univ"
proof -
have "⋀l. List.set l ⊆ univ ⟹ some_embedding_of_lists l ∈ univ"
proof -
fix l
show "List.set l ⊆ univ ⟹ some_embedding_of_lists l ∈ univ"
by (induct l) auto
qed
thus ?thesis by blast
qed
show "inj_on some_embedding_of_lists {l. list.set l ⊆ univ}"
proof -
have "⋀n l m. ⟦l ∈ {l. list.set l ⊆ univ ∧ length l ≤ n};
m ∈ {l. list.set l ⊆ univ ∧ length l ≤ n};
some_embedding_of_lists l = some_embedding_of_lists m⟧
⟹ l = m"
proof -
fix n l m
show "⟦l ∈ {l. list.set l ⊆ univ ∧ length l ≤ n};
m ∈ {l. list.set l ⊆ univ ∧ length l ≤ n};
some_embedding_of_lists l = some_embedding_of_lists m⟧
⟹ l = m"
proof (induct n arbitrary: l m)
show "⋀l m. ⟦l ∈ {l. list.set l ⊆ univ ∧ length l ≤ 0};
m ∈ {l. list.set l ⊆ univ ∧ length l ≤ 0};
some_embedding_of_lists l = some_embedding_of_lists m⟧
⟹ l = m"
by auto
fix n l m
assume ind: "⋀l m. ⟦l ∈ {l. list.set l ⊆ univ ∧ length l ≤ n};
m ∈ {l. list.set l ⊆ univ ∧ length l ≤ n};
some_embedding_of_lists l = some_embedding_of_lists m⟧
⟹ l = m"
assume l: "l ∈ {l. list.set l ⊆ univ ∧ length l ≤ Suc n}"
assume m: "m ∈ {l. list.set l ⊆ univ ∧ length l ≤ Suc n}"
assume eq: "some_embedding_of_lists l = some_embedding_of_lists m"
show "l = m"
proof (cases l; cases m)
show "⟦l = []; m = []⟧ ⟹ l = m" by simp
show "⋀a m'. ⟦l = []; m = a # m'⟧ ⟹ l = m"
by (metis (no_types, lifting) "*" eq image_subset_iff insert_subset
list.simps(15) m mem_Collect_eq some_pairing_in_univ
some_embedding_of_lists.simps(1,2) some_lifting_cancel(1))
show "⋀a l'. ⟦l = a # l'; m = []⟧ ⟹ l = m"
by (metis (lifting) "*" eq image_subset_iff l some_lifting_cancel(1)
list.set_intros(1) mem_Collect_eq some_pairing_in_univ set_subset_Cons
some_embedding_of_lists.simps(1,2) subset_code(1))
show "⋀a b l' m'. ⟦l = a # l'; m = b # m'⟧ ⟹ l = m"
proof -
fix a b l' m'
assume al': "l = a # l'" and bm': "m = b # m'"
have "some_pairing (a, some_embedding_of_lists l') =
some_pairing (b, some_embedding_of_lists m')"
using l m al' bm' eq some_lifting_is_embedding embeds_pairs
apply simp
by (metis (no_types, lifting) "*" image_subset_iff mem_Collect_eq
some_lifting_cancel(2) some_pairing_in_univ)
hence "a = b ∧ some_embedding_of_lists l' = some_embedding_of_lists m'"
using l m al' bm' embeds_pairs
by (metis (lifting) "*" image_subset_iff insert_subset list.simps(15)
mem_Collect_eq first_conv second_conv)
hence "a = b ∧ l' = m'"
using l m al' bm' ind by auto
thus "l = m"
using al' bm' by auto
qed
qed
qed
qed
thus ?thesis
using inj_on_def [of some_embedding_of_lists "{l. list.set l ⊆ univ}"]
by (metis (lifting) linorder_le_cases mem_Collect_eq)
qed
qed
thus "embeds {l. List.set l ⊆ univ}" by blast
qed
text‹
A universe also admits an embedding of all small sets of lists formed from its elements.
›
lemma embeds_small_sets_of_lists:
shows "is_embedding_of (λX. some_embedding_of_small_sets (some_embedding_of_lists ` X))
{X. X ⊆ {l. list.set l ⊆ univ} ∧ small X}"
and "embeds {X. X ⊆ {l. list.set l ⊆ univ} ∧ small X}"
proof -
show "is_embedding_of (λX. some_embedding_of_small_sets (some_embedding_of_lists ` X))
{X. X ⊆ {l. list.set l ⊆ univ} ∧ small X}"
proof
show "inj_on (λX. some_embedding_of_small_sets (some_embedding_of_lists ` X))
{X. X ⊆ {l. list.set l ⊆ univ} ∧ small X}"
proof
fix X Y :: "'U list set"
assume X: "X ∈ {X. X ⊆ {l. list.set l ⊆ univ} ∧ small X}"
and Y: "Y ∈ {X. X ⊆ {l. list.set l ⊆ univ} ∧ small X}"
assume eq: "some_embedding_of_small_sets (some_embedding_of_lists ` X) =
some_embedding_of_small_sets (some_embedding_of_lists ` Y)"
have "some_embedding_of_lists ` X = some_embedding_of_lists ` Y"
by (metis (mono_tags, lifting) CollectD X Y emb_set_cancel emb_set_def
embeds_lists(2) eq image_mono small_image subset_trans)
thus "X = Y"
using X Y embeds_lists inj_on_image_eq_iff by fastforce
qed
show "(λX. some_embedding_of_small_sets (some_embedding_of_lists ` X)) `
{X. X ⊆ {l. list.set l ⊆ univ} ∧ small X} ⊆ univ"
proof
fix X'
assume X': "X' ∈ (λX. some_embedding_of {X. X ⊆ univ ∧ small X}
(some_embedding_of_lists ` X))
` {X. X ⊆ {l. set l ⊆ univ} ∧ small X}"
obtain X where X: "X ⊆ {l. set l ⊆ univ} ∧ small X ∧
(λX. some_embedding_of {X. X ⊆ univ ∧ small X}
(some_embedding_of_lists ` X)) X = X'"
using X' by blast
have "some_embedding_of_lists ` X ⊆ univ ∧ small (some_embedding_of_lists ` X)"
using X embeds_lists small_image by blast
hence "(λX. some_embedding_of {X. X ⊆ univ ∧ small X}
(some_embedding_of_lists ` X)) X ∈ univ"
by (metis emb_set_def emb_set_in_univ)
thus "X' ∈ univ"
using X by blast
qed
qed
thus "embeds {X. X ⊆ {l. list.set l ⊆ univ} ∧ small X}" by blast
qed
end
end