Re: [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
Description: Embed.thy



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