Re: [isabelle-dev] cardinality primitives in Isabelle/HOL?
Last January 24, I moved Fpow into Main and introduced Library/Equipollence.thy. Hope you like it. Larry > On 26 Jan 2019, at 15:14, Andrei Popescu wrote: > > Sorry for my late reply. I agree it makes sense to move such basic operators > (and facts) into Main. The Ordinals and Cardinals development was "destined" > to this sort of exports from the very beginning. > > Best wishes, ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] cardinality primitives in Isabelle/HOL?
Dear Larry, dear all,
>> I suggest moving at least the definition of Fpow into Main (it's small, and
>> fundamental) while creating a new Library entry for my own new material.
Sorry for my late reply. I agree it makes sense to move such basic operators
(and facts) into Main. The Ordinals and Cardinals development was "destined" to
this sort of exports from the very beginning.
Best wishes,
Andrei
--
Message: 1
Date: Wed, 23 Jan 2019 14:33:30 +
From: Lawrence Paulson
To: Jasmin Blanchette
Cc: Traytel Dmitriy , isabelle-dev
Subject: Re: [isabelle-dev] [Spam] cardinality primitives in
Isabelle/HOL?
Message-ID:
Content-Type: text/plain; charset=utf-8
This makes perfect sense to me.
I suggest moving at least the definition of Fpow into Main (it?s small, and
fundamental) while creating a new Library entry for my own new material.
Larry
> On 23 Jan 2019, at 12:48, Blanchette, J.C. wrote:
>
> Hi Larry,
>
> You wrote:
>
>> The theorem ordIso_iff_ordLeq is proved in BNF_Wellorder_Constructions, so
>> clearly a lot of facts about cardinals are available already in Main.
>
> FYI: As you might already know or deduced from the name convention, the
> (co)datatype (a.k.a. "BNF") package is based on some cardinality material.
> When we moved the BNF package into Main, I surgically split the HOL-Cardinals
> theories into two, moving the exact dependencies into Main and leaving the
> rest outside. As a result, it's pretty random what's in Main and what's
> outside. The alternative -- moving all of HOL-Cardinals into Main -- seemed
> undesirable because it would slow down building Main quite a bit.
>
> Jasmin
>
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] cardinality primitives in Isabelle/HOL?
The question of dependency is tricky. I tried deleting the reference to
HOL-Cardinals.Cardinals and found that most of the elementary results were
easily provable using other library facts. But then there was this:
lemma lepoll_trans1 [trans]: "⟦A ≈ B; B ≲ C⟧ ⟹ A ≲ C"
by (meson card_of_ordLeq eqpoll_iff_card_of_ordIso lepoll_def lepoll_trans
ordIso_iff_ordLeq)
The theorem ordIso_iff_ordLeq is proved in BNF_Wellorder_Constructions, so
clearly a lot of facts about cardinals are available already in Main.
But I do prove a couple of things involving the operator Fpow:
lemma lepoll_restricted_funspace:
"{f. f ` A ⊆ B ∧ {x. f x ≠ k x} ⊆ A ∧ finite {x. f x ≠ k x}} ≲ Fpow (A × B)"
proof -
have *: "∃U ∈ Fpow (A × B). f = (λx. if ∃y. (x, y) ∈ U then SOME y. (x,y) ∈ U
else k x)"
if "f ` A ⊆ B" "{x. f x ≠ k x} ⊆ A" "finite {x. f x ≠ k x}" for f
apply (rule_tac x="(λx. (x, f x)) ` {x. f x ≠ k x}" in bexI)
using that by (auto simp: image_def Fpow_def)
show ?thesis
apply (rule subset_image_lepoll [where f = "λU x. if ∃y. (x,y) ∈ U then @y.
(x,y) ∈ U else k x"])
using * by (auto simp: image_def)
qed
lemma eqpoll_Fpow:
assumes "infinite A" shows "Fpow A ≈ A”
The thing is though, Fpow (which is nothing but the finite powerset operator)
probably belongs in Main as well.
An alternative proposal is to create a new theory, Library/Equipollence. I
agree about hiding the syntax.
Larry
> On 23 Jan 2019, at 10:11, Traytel Dmitriy wrote:
>
> Hi Larry,
>
> if you want to put the definitions and the basic properties in Main, then
> Fun.thy would probably be the place. But then I would argue that the syntax
> should be hidden, as users might want to use these symbols for something else.
>
> For the advanced material, do you need some theorems from HOL-Cardinals or
> just the syntax from HOL-Library.Cardinal_Notations in addition to what is
> already there in Main about cardinals? If it is only the syntax, then a
> separate theory in HOL-Library is probably a good fit. Otherwise, a separate
> theory in HOL-Cardinals would make sense.
>
> Dmitriy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] cardinality primitives in Isabelle/HOL?
Hi Larry, if you want to put the definitions and the basic properties in Main, then Fun.thy would probably be the place. But then I would argue that the syntax should be hidden, as users might want to use these symbols for something else. For the advanced material, do you need some theorems from HOL-Cardinals or just the syntax from HOL-Library.Cardinal_Notations in addition to what is already there in Main about cardinals? If it is only the syntax, then a separate theory in HOL-Library is probably a good fit. Otherwise, a separate theory in HOL-Cardinals would make sense. Dmitriy > On 22 Jan 2019, at 15:58, Lawrence Paulson wrote: > > I’m trying to install some of my new material and I’m wondering what to do > with equipollence and related concepts: > > definition eqpoll :: "'a set ⇒ 'b set ⇒ bool" (infixl "≈" 50) > where "eqpoll A B ≡ ∃f. bij_betw f A B" > > definition lepoll :: "'a set ⇒ 'b set ⇒ bool" (infixl "≲" 50) > where "lepoll A B ≡ ∃f. inj_on f A ∧ f ` A ⊆ B" > > definition lesspoll :: "'a set ⇒ 'b set ⇒ bool" (infixl ‹≺› 50) > where "A ≺ B == A ≲ B ∧ ~(A ≈ B)" > > The raw definitions are extremely simple and could even be installed in the > main Isabelle/HOL distribution. The basic properties of these concepts > require few requisites. However, more advanced material requires the > Cardinals development. > > Where do people think these definitions and proofs should be installed? > > Larry > >> On 27 Dec 2018, at 20:29, Makarius wrote: >> >> On 27/12/2018 17:45, Traytel Dmitriy wrote: >>> Hi Larry, >>> >>> the HOL-Cardinals library might be just right for the purpose: >>> >>> theory Scratch >>> imports "HOL-Cardinals.Cardinals" >>> begin >>> >>> lemma "|A| ≤o |B| ⟷ (∃f. inj_on f A ∧ f ` A ⊆ B)" >>> by (rule card_of_ordLeq[symmetric]) >>> >>> lemma "|A| =o |B| ⟷ (∃f. bij_betw f A B)" >>> by (rule card_of_ordIso[symmetric]) >>> >>> lemma >>> assumes "|A| ≤o |B|" "|B| ≤o |A|" >>> shows "|A| =o |B|" >>> by (simp only: assms ordIso_iff_ordLeq) >>> >>> end >>> >>> The canonical entry point for the library is the above >>> HOL-Cardinals.Cardinals. Many of the theorems and definitions are already >>> in Main, because the (co)datatype package is based on them. The syntax is >>> hidden in main—one gets it by importing HOL-Library.Cardinal_Notations >>> (which HOL-Cardinals.Cardinals does transitively). >> >> It would be great to see this all consolidated and somehow unified, i.e. >> some standard notation in Main as proposed by Larry (potentially as >> bundles as proposed by Florian), and avoidance of too much no_syntax >> remove non-standard notation from Main. >> >> >> Makarius > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] cardinality primitives in Isabelle/HOL?
I’m trying to install some of my new material and I’m wondering what to do with equipollence and related concepts: definition eqpoll :: "'a set ⇒ 'b set ⇒ bool" (infixl "≈" 50) where "eqpoll A B ≡ ∃f. bij_betw f A B" definition lepoll :: "'a set ⇒ 'b set ⇒ bool" (infixl "≲" 50) where "lepoll A B ≡ ∃f. inj_on f A ∧ f ` A ⊆ B" definition lesspoll :: "'a set ⇒ 'b set ⇒ bool" (infixl ‹≺› 50) where "A ≺ B == A ≲ B ∧ ~(A ≈ B)" The raw definitions are extremely simple and could even be installed in the main Isabelle/HOL distribution. The basic properties of these concepts require few requisites. However, more advanced material requires the Cardinals development. Where do people think these definitions and proofs should be installed? Larry > On 27 Dec 2018, at 20:29, Makarius wrote: > > On 27/12/2018 17:45, Traytel Dmitriy wrote: >> Hi Larry, >> >> the HOL-Cardinals library might be just right for the purpose: >> >> theory Scratch >> imports "HOL-Cardinals.Cardinals" >> begin >> >> lemma "|A| ≤o |B| ⟷ (∃f. inj_on f A ∧ f ` A ⊆ B)" >> by (rule card_of_ordLeq[symmetric]) >> >> lemma "|A| =o |B| ⟷ (∃f. bij_betw f A B)" >> by (rule card_of_ordIso[symmetric]) >> >> lemma >> assumes "|A| ≤o |B|" "|B| ≤o |A|" >> shows "|A| =o |B|" >> by (simp only: assms ordIso_iff_ordLeq) >> >> end >> >> The canonical entry point for the library is the above >> HOL-Cardinals.Cardinals. Many of the theorems and definitions are already in >> Main, because the (co)datatype package is based on them. The syntax is >> hidden in main—one gets it by importing HOL-Library.Cardinal_Notations >> (which HOL-Cardinals.Cardinals does transitively). > > It would be great to see this all consolidated and somehow unified, i.e. > some standard notation in Main as proposed by Larry (potentially as > bundles as proposed by Florian), and avoidance of too much no_syntax > remove non-standard notation from Main. > > > Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] cardinality primitives in Isabelle/HOL?
> On 28 Dec 2018, at 19:36, Lawrence Paulson wrote: > > Tons of useful stuff here. > > Some syntactic ambiguities, particularly around the =o relation, which is > also defined as Set_Algebras.elt_set_eq. True. The same holds for +o and *o (which are less widely used in the ordinals library). I'm not sure what a good naming is in these cases. "=o" makes sense for me as "equality on ordinals". It would be ok for me to play with capitalization or other abbreviations of ordinals, e.g., "=O" or "=ord". Maybe Andrei can comment, as he picked the current notation. I don't know what "=o" stands for in the case of Set_Algebras.elt_set_eq (is this a reference to the Oh-notation?) and why there is need for an alternative notation for ∈. I believe the better textbooks are those that write "f ∈ O(g)" instead of "f = O(g)". Along similar lines, I find the notation "f > I don’t suppose there’s any chance of using quotients to define actual > cardinals and use ordinary equality? Not really. "(=o) :: 'a rel ⇒ 'b rel ⇒ bool" is too polymorphic for this to work properly. (The relation arguments are ordinals represented by well-orders.) One can quotient modulo a restricted relation "(=o) :: 'a rel ⇒ 'a rel ⇒ bool", but then the equality on the quotient type won't allow us to compare "|UNIV :: nat set| :: nat rel" to "|UNIV :: real set| :: real rel". > And it still makes sense to introduce the actual notion of equipollence and > similar relations. This is the usual trade-off between many similar definitions with dedicated reasoning support (transitivity, congruence, and monotonicity rules and such) or a few core ones. Possibly an abbreviation is sufficient in this case. Dmitriy ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] cardinality primitives in Isabelle/HOL?
Tons of useful stuff here. Some syntactic ambiguities, particularly around the =o relation, which is also defined as Set_Algebras.elt_set_eq. I don’t suppose there’s any chance of using quotients to define actual cardinals and use ordinary equality? And it still makes sense to introduce the actual notion of equipollence and similar relations. Larry > On 27 Dec 2018, at 20:29, Makarius wrote: > > On 27/12/2018 17:45, Traytel Dmitriy wrote: >> Hi Larry, >> >> the HOL-Cardinals library might be just right for the purpose: >> >> theory Scratch >> imports "HOL-Cardinals.Cardinals" >> begin >> >> lemma "|A| ≤o |B| ⟷ (∃f. inj_on f A ∧ f ` A ⊆ B)" >> by (rule card_of_ordLeq[symmetric]) >> >> lemma "|A| =o |B| ⟷ (∃f. bij_betw f A B)" >> by (rule card_of_ordIso[symmetric]) >> >> lemma >> assumes "|A| ≤o |B|" "|B| ≤o |A|" >> shows "|A| =o |B|" >> by (simp only: assms ordIso_iff_ordLeq) >> >> end >> >> The canonical entry point for the library is the above >> HOL-Cardinals.Cardinals. Many of the theorems and definitions are already in >> Main, because the (co)datatype package is based on them. The syntax is >> hidden in main—one gets it by importing HOL-Library.Cardinal_Notations >> (which HOL-Cardinals.Cardinals does transitively). > > It would be great to see this all consolidated and somehow unified, i.e. > some standard notation in Main as proposed by Larry (potentially as > bundles as proposed by Florian), and avoidance of too much no_syntax > remove non-standard notation from Main. > > > Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] cardinality primitives in Isabelle/HOL?
On 27/12/2018 17:45, Traytel Dmitriy wrote: > Hi Larry, > > the HOL-Cardinals library might be just right for the purpose: > > theory Scratch > imports "HOL-Cardinals.Cardinals" > begin > > lemma "|A| ≤o |B| ⟷ (∃f. inj_on f A ∧ f ` A ⊆ B)" > by (rule card_of_ordLeq[symmetric]) > > lemma "|A| =o |B| ⟷ (∃f. bij_betw f A B)" > by (rule card_of_ordIso[symmetric]) > > lemma > assumes "|A| ≤o |B|" "|B| ≤o |A|" > shows "|A| =o |B|" > by (simp only: assms ordIso_iff_ordLeq) > > end > > The canonical entry point for the library is the above > HOL-Cardinals.Cardinals. Many of the theorems and definitions are already in > Main, because the (co)datatype package is based on them. The syntax is hidden > in main—one gets it by importing HOL-Library.Cardinal_Notations (which > HOL-Cardinals.Cardinals does transitively). It would be great to see this all consolidated and somehow unified, i.e. some standard notation in Main as proposed by Larry (potentially as bundles as proposed by Florian), and avoidance of too much no_syntax remove non-standard notation from Main. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] cardinality primitives in Isabelle/HOL?
Hi Larry, the HOL-Cardinals library might be just right for the purpose: theory Scratch imports "HOL-Cardinals.Cardinals" begin lemma "|A| ≤o |B| ⟷ (∃f. inj_on f A ∧ f ` A ⊆ B)" by (rule card_of_ordLeq[symmetric]) lemma "|A| =o |B| ⟷ (∃f. bij_betw f A B)" by (rule card_of_ordIso[symmetric]) lemma assumes "|A| ≤o |B|" "|B| ≤o |A|" shows "|A| =o |B|" by (simp only: assms ordIso_iff_ordLeq) end The canonical entry point for the library is the above HOL-Cardinals.Cardinals. Many of the theorems and definitions are already in Main, because the (co)datatype package is based on them. The syntax is hidden in main—one gets it by importing HOL-Library.Cardinal_Notations (which HOL-Cardinals.Cardinals does transitively). Our ITP'14 paper explains the design of the library: http://people.inf.ethz.ch/trayteld/papers/itp14-card/card.pdf Dmitriy > On 27 Dec 2018, at 13:31, Lawrence Paulson wrote: > > I am inclined to introduce these definitions: > > definition lepoll :: "'a set ⇒ 'b set ⇒ bool" (infixl "≲" 50) >where "lepoll A B ≡ ∃f. inj_on f A ∧ f ` A ⊆ B" > > definition eqpoll :: "'a set ⇒ 'b set ⇒ bool" (infixl "≈" 50) >where "eqpoll A B ≡ ∃f. bij_betw f A B” > > They allow, for example, this: > > theorem Schroeder_Bernstein_eqpoll: > assumes "A ≲ B" "B ≲ A" shows "A ≈ B" > using assms unfolding eqpoll_def lepoll_def by (metis Schroeder_Bernstein) > > The names and syntax are borrowed from Isabelle/ZF, and they are needed for > some HOL Light proofs. > > But do they exist in some form already? And are there any comments on those > relation symbols? > > Larry > > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] cardinality primitives in Isabelle/HOL?
I agree with Florian wrt syntax. Tobias On 27/12/2018 13:39, Florian Haftmann wrote: I am inclined to introduce these definitions: definition lepoll :: "'a set ⇒ 'b set ⇒ bool" (infixl "≲" 50) where "lepoll A B ≡ ∃f. inj_on f A ∧ f ` A ⊆ B" definition eqpoll :: "'a set ⇒ 'b set ⇒ bool" (infixl "≈" 50) where "eqpoll A B ≡ ∃f. bij_betw f A B” They allow, for example, this: theorem Schroeder_Bernstein_eqpoll: assumes "A ≲ B" "B ≲ A" shows "A ≈ B" using assms unfolding eqpoll_def lepoll_def by (metis Schroeder_Bernstein) The names and syntax are borrowed from Isabelle/ZF, and they are needed for some HOL Light proofs. But do they exist in some form already? And are there any comments on those relation symbols? The notation itself is quite generic, so it is worth spending more thoughts on how can we keep reusable. Maybe it would be worth a try to put the syntax into a bundle (there are already some applications of that pattern): bundle set_relation_syntax begin notation … end bundle no_set_relation_syntax begin no_notation … end … unbundle set_relation_syntax … unbundle no_set_relation_syntax The input abbreviation gepoll should be added as well. Anyway, I am uncertain about the name »poll«. Cheers, Florian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] cardinality primitives in Isabelle/HOL?
> On 27 Dec 2018, at 12:45, Florian Haftmann > wrote: > > (I don't know how useful the strict versions less_poll, greater_poll > would be). Strict versions do turn up in some places (both in HOL Light and Isabelle/ZF) ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] cardinality primitives in Isabelle/HOL?
>> Anyway, I am uncertain about the name »poll«. > > From https://en.wikipedia.org/wiki/Cardinality > > "Two sets A and B have the same cardinality if there exists a bijection from > A to B, that is, a function from A to B that is both injective and > surjective. Such sets are said to be equipotent, equipollent, or > equinumerous. This relationship can also be denoted A ≈ B or A ~ B.” I see. Using »poll« is a stem, the canonical names would be less_eq_poll equiv_poll greater_eq_poll (I don't know how useful the strict versions less_poll, greater_poll would be). Florian signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] cardinality primitives in Isabelle/HOL?
> On 27 Dec 2018, at 12:39, Florian Haftmann > wrote: Thanks for the suggestions. > The input abbreviation gepoll should be added as well. > > Anyway, I am uncertain about the name »poll«. From https://en.wikipedia.org/wiki/Cardinality "Two sets A and B have the same cardinality if there exists a bijection from A to B, that is, a function from A to B that is both injective and surjective. Such sets are said to be equipotent, equipollent, or equinumerous. This relationship can also be denoted A ≈ B or A ~ B.” Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] cardinality primitives in Isabelle/HOL?
> I am inclined to introduce these definitions: > > definition lepoll :: "'a set ⇒ 'b set ⇒ bool" (infixl "≲" 50) > where "lepoll A B ≡ ∃f. inj_on f A ∧ f ` A ⊆ B" > > definition eqpoll :: "'a set ⇒ 'b set ⇒ bool" (infixl "≈" 50) > where "eqpoll A B ≡ ∃f. bij_betw f A B” > > They allow, for example, this: > > theorem Schroeder_Bernstein_eqpoll: > assumes "A ≲ B" "B ≲ A" shows "A ≈ B" > using assms unfolding eqpoll_def lepoll_def by (metis Schroeder_Bernstein) > > The names and syntax are borrowed from Isabelle/ZF, and they are needed for > some HOL Light proofs. > > But do they exist in some form already? And are there any comments on those > relation symbols? The notation itself is quite generic, so it is worth spending more thoughts on how can we keep reusable. Maybe it would be worth a try to put the syntax into a bundle (there are already some applications of that pattern): bundle set_relation_syntax begin notation … end bundle no_set_relation_syntax begin no_notation … end … unbundle set_relation_syntax … unbundle no_set_relation_syntax The input abbreviation gepoll should be added as well. Anyway, I am uncertain about the name »poll«. Cheers, Florian signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
