*To*: Dmitriy Traytel <traytel at inf.ethz.ch>, "stark at cs.stonybrook.edu" <stark at cs.stonybrook.edu>*Subject*: Re: [isabelle] A question about sets and embeddings in HOL*From*: Andrei Popescu <a.popescu at mdx.ac.uk>*Date*: Sat, 09 Apr 2016 23:54:27 +0100*Accept-language*: en-US, en-GB*Acceptlanguage*: en-US, en-GB*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Thread-index*: AdGSsdgocoZ7ScieSzarKs39HzEKhA==*Thread-topic*: [isabelle] A question about sets and embeddings in HOL

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 >

**Follow-Ups**:**Re: [isabelle] A question about sets and embeddings in HOL***From:*Eugene W. Stark

- Previous by Date: Re: [isabelle] A question about sets and embeddings in HOL
- Next by Date: Re: [isabelle] A question about sets and embeddings in HOL
- 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