> 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
