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
[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? Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
