Re: [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
> 



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