# 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 <makar...@sketis.net> 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
```