[isabelle-dev] cardinality primitives in Isabelle/HOL?

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Thu Dec 27 13:39:35 CET 2018

> 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

notation …


bundle no_set_relation_syntax

no_notation …



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«.


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20181227/7adb27ad/attachment.sig>

More information about the isabelle-dev mailing list