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

Lawrence Paulson lp15 at cam.ac.uk
Thu Dec 27 13:31:58 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?


More information about the isabelle-dev mailing list