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


Attachment: signature.asc
Description: OpenPGP digital signature

isabelle-dev mailing list

Reply via email to