*To*: "stark at cs.stonybrook.edu" <stark at cs.stonybrook.edu>*Subject*: Re: [isabelle] A question about sets and embeddings in HOL*From*: Dmitriy Traytel <traytel at inf.ethz.ch>*Date*: Sat, 9 Apr 2016 22:28:34 +0200*Cc*: Andrei Popescu <a.popescu at mdx.ac.uk>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <5F22105EAD3CAD4689EC4570AA1802B0BF06E7189F@WGFP-EXMAV1.uni.mdx.ac.uk>*References*: <5708FEC9.3080907@starkeffect.com> <5F22105EAD3CAD4689EC4570AA1802B0BF06E7189F@WGFP-EXMAV1.uni.mdx.ac.uk>

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 >

**References**:**[isabelle] A question about sets and embeddings in HOL***From:*Eugene W. Stark

**Re: [isabelle] A question about sets and embeddings in HOL***From:*Andrei Popescu

- Previous by Date: Re: [isabelle] A question about sets and embeddings in HOL
- Next by Date: [isabelle] Solving big quantifier-free linear real arithmetic goals
- Previous by Thread: Re: [isabelle] A question about sets and embeddings in HOL
- Next by Thread: Re: [isabelle] A question about sets and embeddings in HOL
- Cl-isabelle-users April 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list