# Re: [isabelle] A question about sets and embeddings in HOL

```Hi Gene,

Thank you for your question -- this theorem was an important fact missing in our cardinal library,
and it triggered some further useful infrastructure lemmas.

A polished version of it will be part of the next distribution. In the meantime, attached is a theory file
that has the theorem at the end (also included in this message).

All the best,
Andrei

theory Embed imports Main
begin

(* Some order-filter infrastructure *)

lemma ofilter_embed2:
assumes r: "Well_order r" and e: "embed r r' f" and o: "ofilter r A"
shows "embed (Restr r A) r' f"
using assms Field_Restr_ofilter[OF r o] ofilter_Restr_under[OF r o]
unfolding embed_def ofilter_embed[OF r] by auto

lemma ofilter_incl_embed:
assumes r: "Well_order r" and oA: "ofilter r A" and oB: "ofilter r B"
and e: "embed (Restr r A) r' f" and i: "B â A"
shows "embed (Restr r B) r' f"
using Well_order_Restr[OF r] ofilter_Restr_subset[OF r oB i] ofilter_embed2[OF _ e] Restr_subset[OF i]
by fastforce

lemma ofilter_int:
assumes r: "Well_order r" and oA: "ofilter r A" and oB: "ofilter r B"
shows "ofilter r (A â B)"
by (metis Int_absorb1 Int_absorb2 oA oB r wo_rel.intro wo_rel.ofilter_linord)

lemma ofilter_UNION:
assumes "â i â I. ofilter r (A i)"
shows "ofilter r (â i â I. A i)"
using assms unfolding ofilter_def under_def by blast

lemma Restr_UNION_ofilter:
assumes "â i â I. ofilter r (A i)"
shows "Restr r (â i â I. A i) = (â i â I. Restr r (A i))"
using assms unfolding ofilter_def under_def by blast

lemma ofilter_ordLeq_UNION:
assumes r: "Well_order r" and r': "Well_order r'"
and ofl: "â i â I. ofilter r (A i) â ordLeq3 (Restr r (A i)) r'"
shows "ordLeq3 (Restr r (â i â I. A i)) r'"
proof-
let ?U = "â i â I. A i"
{fix i assume i: "i â I"
have "Well_order (Restr r (A i))" using Well_order_Restr r by fastforce
have "â gi. embed (Restr r (A i)) r' gi" using ofl i unfolding ordLeq_def by auto
}
then obtain g where g: "â i â I. embed (Restr r (A i)) r' (g i)" by metis
def ii â "Î a. SOME i. i â I â a â A i"
def gg â "Î a. g (ii a) a"
have "ofilter r ?U" using ofilter_UNION ofl by metis
hence F: "Field (Restr r ?U) = ?U" using Field_Restr_ofilter[OF r] by auto
have "embed (Restr r ?U) r' gg" unfolding embed_def proof
fix a let ?i = "ii a"
assume "a â Field (Restr r ?U)"
hence "â i. i â I â a â A i" unfolding F by auto
hence i: "?i â I" and aa: "a â A ?i" unfolding ii_def by (metis (no_types, lifting) someI_ex)+
hence a: "aâField (Restr r (A ?i))" using Field_Restr_ofilter[OF r] ofl by auto
hence 1: "bij_betw (g ?i) (under (Restr r (A ?i)) a) (under r' (g ?i a))" using g i unfolding embed_def by auto
have 2: "under (Restr r ?U) a = under (Restr r (A ?i)) a"
using aa ofl i aa unfolding under_def ofilter_def by auto
{fix b assume 0: "b â under (Restr r (A ?i)) a"
let ?j = "ii b"
have "b â Field (Restr r ?U)" using 2 subsetCE under_Field 0 by fastforce
hence "â i. i â I â b â A i" unfolding F by auto
hence j: "?j â I" and bb: "b â A ?j" unfolding ii_def by (metis (no_types, lifting) someI_ex)+
hence b: "b â Field (Restr r (A ?j))" using Field_Restr_ofilter[OF r] ofl by auto
hence 1: "embed (Restr r (A ?j)) r' (g ?j)" using g j by auto
let ?B = "A ?i â A ?j"
have b: "b â ?B" by (metis 0 Int_iff bb mem_Collect_eq mem_Sigma_iff under_def)
have 11: "embed (Restr r (A ?i)) r' (g ?i)" using g i by auto
have oB: "ofilter r ?B" using ofl i j ofilter_int r by fastforce
hence B1: "embed (Restr r ?B) r' (g ?i)" using 11 i inf_le1 ofilter_incl_embed ofl r by fastforce
have B2: "embed (Restr r ?B) r' (g ?j)" using 1 j by (metis oB inf_commute inf_le1 ofilter_incl_embed ofl r)
have B: "Well_order (Restr r ?B)" using Well_order_Restr r by blast
have "g ?i b = g ?j b" using b B1 B2 embed_unique[OF B r' B1 B2] Field_Restr_ofilter i j ofilter_int ofl r by blast
}
thus "bij_betw gg (under (Restr r ?U) a) (under r' (gg a))" using 1 2 unfolding gg_def
unfolding bij_betw_def inj_on_def image_def by auto
qed
thus ?thesis unfolding ordLeq_def using Restr_UNION_ofilter ofl r'
by (auto simp: Well_order_Restr r)
qed

(* Cardinal suprema (for a family of cardinals on the same host type) *)

context fixes I :: "'i set" and k :: "'i â 'a rel"
begin

definition K::"'a rel" where "K = card_of UNIV"

lemma card_order_K: "card_order K"

lemma ordLeq_K:
assumes "Card_order (k i)" shows "ordLeq3 (k i) K"
by (metis Card_order_iff_ordLeq_card_of Embed.K_def UNIV_I assms card_of_mono1
ordLeq_transitive subsetI)

definition f :: "'i â 'a â 'a" where
"f i â SOME f. embed (k i) K f"

lemma embed_f:
assumes "Card_order (k i)"
shows "embed (k i) K (f i)"
unfolding f_def
apply(rule someI_ex[of "%f. embed (k i) K f"])
unfolding K_def
by (metis Cnotzero_UNIV K_def assms card_order_on_def not_ordLess_ordLeq ordLeq_K ordLess_iff)

definition A :: "'i â 'a set" where
"A i â f i ` (Field (k i))"

lemma iso_A:
assumes "Card_order (k i)"
shows "iso (k i) (Restr K (A i)) (f i)"
by (metis A_def Embed.K_def Embed.card_order_K Embed.embed_f Field_card_of
assms card_order_on_def embed_implies_iso_Restr)

lemma ordIso2_A:
assumes "Card_order (k i)"
shows "ordIso2 (k i) (Restr K (A i))"
using iso_A[OF assms] assms card_order_on_def unfolding ordIso_def
by (auto simp: K_def Well_order_Restr card_of_Well_order)

lemma Card_order_A:
assumes "Card_order (k i)"
shows "Card_order (Restr K (A i))"
using Card_order_ordIso2 ordIso2_A[OF assms] assms by blast

definition csupr :: "'a rel" where
"csupr â card_of (â i â I. A i)"

lemma Card_order_csupr:
"Card_order csupr"

lemma ordLeq_csupr:
assumes c:  "â i â I. Card_order (k i)"  and i: "i â I"
shows "ordLeq3 (k i) csupr"
proof-
let ?k = "card_of (Field (k i))"
have "ordIso2 (k i) (Restr K (A i))" using ordIso2_A c i by auto
also have "ordIso2 (Restr K (A i)) (card_of (A i))"
by (metis Card_order_A Embed.A_def c card_of_unique i iso_A iso_Field)
also have "ordLeq3 (card_of (A i)) csupr" unfolding csupr_def
by (meson UN_I assms(2) card_of_mono1 subsetI)
finally show ?thesis .
qed

lemma ofilter_A:
assumes ci: "Card_order (k i)"
shows "ofilter K (A i)"
using ci iso_A[OF ci] unfolding A_def
by (metis Cnotzero_UNIV embed_f K_def card_order_on_well_order_on embed_Field_ofilter)

lemma csupr_ordLeq:
assumes ci: "â i â I. Card_order (k i)"
and c: "Card_order r"
and ord: "â i. i â I â ordLeq3 (k i) r"
shows "ordLeq3 csupr r"
proof-
let ?U = "â i â I. A i"
let ?restr = "Restr K ?U"
have 0: "âi â I. ofilter K (A i)" using ofilter_A ci by auto
have restr: "Well_order ?restr" and K: "Well_order K" and r: "Well_order r"
using c card_order_on_def by (auto simp: Field_card_of K_def Well_order_Restr card_of_well_order_on)
have "Field ?restr = ?U"
using ofilter_A ofilter_UNION 0 by (intro Field_Restr_ofilter) (auto simp: K_def Field_card_of card_of_well_order_on)
hence 1: "well_order_on ?U ?restr" using restr by auto
have restr: "?restr = (â i â I. Restr K (A i))" using Restr_UNION_ofilter[OF 0] by auto
have 2: "â i. i â I â ordLeq3 (Restr K (A i)) r"
using ord by (metis ordIso2_A ci ordIso_iff_ordLeq ordLeq_transitive)
have "ordLeq3 (card_of ?U) ?restr" using 1 card_of_least by blast
also have "ordLeq3 ?restr r" using ofilter_ordLeq_UNION[OF K r] 0 2 by metis
finally show ?thesis unfolding csupr_def .
qed

end (* context *)

hide_const A K f

term csupr
thm Card_order_csupr
thm ordLeq_csupr
thm csupr_ordLeq

definition "embeds A B â â f. f ` B â A â inj_on f B"

lemma embeds_ordLeq: "embeds A B â ordLeq3 (card_of B) (card_of A)"
unfolding card_of_ordLeq[symmetric] embeds_def by auto

lemma embeds_universal:
fixes I :: "'i set" and F :: "'i â 'a set"
defines "S â Field (csupr I (card_of o F))"
shows "(â i. i â I â embeds S (F i)) â
(â S'. (â i. i â I â embeds S' (F i)) â embeds S' S)"
proof-
have 1: "â i â I. Card_order ((card_of o F) i)"
have "ordIso2 (card_of S) (csupr I (card_of o F))"
unfolding S_def using card_of_Field_ordIso[OF Card_order_csupr] .
with ordLeq_csupr[OF 1] csupr_ordLeq[OF 1]
show ?thesis unfolding S_def embeds_ordLeq o_def
by safe (simp add: Field_card_of csupr_def,
qed

end

________________________________________
From: Eugene W. Stark [isabelle-users at starkeffect.com]
Sent: Sunday, April 10, 2016 12:37 PM
To: cl-isabelle-users at lists.cam.ac.uk
Cc: Andrei Popescu; traytel at inf.ethz.ch
Subject: [SPAM: 3.000] Re: [isabelle] A question about sets and embeddings in HOL

That sounds like the answer I was looking for.  Thank you both for your replies.

- Gene Stark

On 04/09/2016 06:54 PM, Andrei Popescu wrote:
> Hi Dmitriy and Gene,
>
> Sorry, I lost sight of the word "embedding" in Gene's email...
>
> Indeed, disjoint union does not fully work, as shown by Dmitriy's need for extra hypotheses. In particular, the size of the index causes trouble.
> For a full solution, we really need cardinal suprema. In HOL, this is a bit more bureaucratic than in ZFC, but it works.
> We can fix a well-order on 'b (where the family F has type 'a => 'b set).
> For each i::'a, there exists a restriction of this fixed well-order, say, "k i", representing the cardinal of "F i".
> The desired weakly universal set is the union of the fields of all these cardinals "k i".
>
> All the best,
>    Andrei
>
> -----Original Message-----
> From: Dmitriy Traytel [mailto:traytel at inf.ethz.ch]
> Sent: 09 April 2016 21:29
> To: stark at cs.stonybrook.edu
> Cc: cl-isabelle-users at lists.cam.ac.uk; Andrei Popescu
> Subject: Re: [isabelle] A question about sets and embeddings in HOL
>
> Hi Gene,
>
> while Andrei is right on the high level, I should point out that your lemma does not hold in HOL as stated.
>
> For instance the type of the existentially quantified "S :: âc set" might simply be not large enough to embed "(F :: âa => âb set) iâ (counterexample: âc = unit, âa = âb = nat, F = %_. UNIV).
>
> Here is a theorem, which I can prove easily using our cardinals library [1]. It fixes âc to be a large enough type to use Sigma as the witness (as Andrei suggested). It also requires the index type âa to be infinite and Sâ to be larger than the index type as well.
>
> theory Scratch
> imports
>   "~~/src/HOL/Library/Cardinal_Notations"
>   "~~/src/HOL/Library/FuncSet"
> begin
>
> definition embeds
>  where "embeds A B â âf. f â B â A â inj_on f B"
>
> lemma embeds_ordLeq: "embeds A B â |B| âo |A|"
>   unfolding card_of_ordLeq[symmetric] embeds_def by auto
>
> lemma
>   fixes F :: "'a â 'b set"
>   assumes "infinite (UNIV :: 'a set)"
>   shows "âS :: ('a Ã 'b) set.
>     (âx. embeds S (F x)) â
>     (âS'. (âx. embeds S' (F x)) â embeds S' (UNIV :: 'a set) â embeds S' S)"
>   unfolding embeds_ordLeq using assms
>   by (auto simp: image_iff card_of_ordLeq_finite
>    intro!: exI[of _ "Sigma UNIV F"] surj_imp_ordLeq[of _ snd] card_of_Sigma_ordLeq_infinite)
>
> end
>
> I did not think thoroughly if all my modifications are necessary. I.e., what happens if the index type âa is finite?
>
> Best wishes,
> Dmitriy
>
> [1] Cardinals in Isabelle/HOL
> Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel ITP 2014, http://people.inf.ethz.ch/trayteld/papers/itp14-card/card.pdf
>
>
>> On 09 Apr 2016, at 21:48, Andrei Popescu <a.popescu at mdx.ac.uk> wrote:
>>
>> Hi Gene,
>>
>> You can use the disjoint union (which is of course not only weakly, but also strongly universal).
>> Search for the text "Disjoint union of a family of sets" in
>> https://isabelle.in.tum.de/dist/library/HOL/HOL/Product_Type.html
>>
>> All the best,
>>  Andrei
>>
>> -----Original Message-----
>> From: cl-isabelle-users-bounces at lists.cam.ac.uk
>> [mailto:cl-isabelle-users-bounces at lists.cam.ac.uk] On Behalf Of Eugene
>> W. Stark
>> Sent: 09 April 2016 14:08
>> To: cl-isabelle-users at lists.cam.ac.uk
>> Subject: [isabelle] A question about sets and embeddings in HOL
>>
>> Is it possible, in HOL, to prove that for any I-indexed collection of sets {F i: i â I} there exists a set S that embeds (via injective maps) all of the sets F i and furthermore is weakly universal for this property, so that if S' is any other set that embeds all the F i then S' embeds S?
>> In more detail, I am thinking of something like the following:
>>
>>  definition embeds
>>  where "embeds A B â âf. f â B â A â inj_on f B"
>>
>>  lemma "âF. âS. (âx. embeds S (F x)) â (âS'. (âx. embeds S' (F x)) â embeds S' S)"
>>
>> In ZFC I suppose it would just be possible to take as S the least cardinal greater than the cardinals of all the F i, but I don't have a very clear idea of how/whether something similar could be done in HOL.
>>
>> Before I spend a lot of time rummaging through the well ordering stuff in the Isabelle library I thought I would risk asking to see if somebody on this list knows the answer instantly.  Thanks for any help you can give.
>>
>>                                                      - Gene Stark
>>
>

```

Attachment: Embed.thy
Description: Embed.thy

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.