I agree with Florian wrt syntax. Tobias
On 27/12/2018 13:39, Florian Haftmann wrote:
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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
