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
>>
> 





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