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

[Florian Haftmann]

> 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

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