*To*: "stark at cs.stonybrook.edu" <stark at cs.stonybrook.edu>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] A question about sets and embeddings in HOL*From*: Andrei Popescu <A.Popescu at mdx.ac.uk>*Date*: Mon, 11 Apr 2016 11:16:13 +0100*Accept-language*: en-US, en-GB*Acceptlanguage*: en-US, en-GB*Cc*: "traytel at inf.ethz.ch" <traytel at inf.ethz.ch>*In-reply-to*: <570A3B0E.70008@starkeffect.com>*References*: <5F22105EAD3CAD4689EC4570AA1802B0BF06E718B1@WGFP-EXMAV1.uni.mdx.ac.uk> <570A3B0E.70008@starkeffect.com>*Thread-index*: AQHRk9rQDWK/DNDESkmVerzw/4W27A==*Thread-topic*: [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" by (simp add: Embed.K_def card_of_card_order_on) 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" by (simp add: csupr_def card_of_Card_order) 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)" by (simp add: Field_card_of card_of_card_order_on) 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, simp add: card_of_Card_order csupr_ordLeq ordIso_ordLeq_trans) 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**

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

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

- Previous by Date: [isabelle] Empty session_graph files
- Next by Date: Re: [isabelle] Simplifying addition and subtraction of multisets
- Previous by Thread: Re: [isabelle] A question about sets and embeddings in HOL
- Next by Thread: [isabelle] Solving big quantifier-free linear real arithmetic goals
- 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