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

Lawrence Paulson lp15 at cam.ac.uk
Wed Jan 23 12:53:14 CET 2019

The question of dependency is tricky. I tried deleting the reference to HOL-Cardinals.Cardinals and found that most of the elementary results were easily provable using other library facts. But then there was this:

lemma lepoll_trans1 [trans]: "⟦A ≈ B; B ≲ C⟧ ⟹ A ≲ C"
  by (meson card_of_ordLeq eqpoll_iff_card_of_ordIso lepoll_def lepoll_trans ordIso_iff_ordLeq)

The theorem ordIso_iff_ordLeq is proved in BNF_Wellorder_Constructions, so clearly a lot of facts about cardinals are available already in Main.

But I do prove a couple of things involving the operator Fpow:

lemma lepoll_restricted_funspace:
   "{f. f ` A ⊆ B ∧ {x. f x ≠ k x} ⊆ A ∧ finite {x. f x ≠ k x}} ≲ Fpow (A × B)"
proof -
  have *: "∃U ∈ Fpow (A × B). f = (λx. if ∃y. (x, y) ∈ U then SOME y. (x,y) ∈ U else k x)"
    if "f ` A ⊆ B" "{x. f x ≠ k x} ⊆ A" "finite {x. f x ≠ k x}" for f
    apply (rule_tac x="(λx. (x, f x)) ` {x. f x ≠ k x}" in bexI)
    using that by (auto simp: image_def Fpow_def)
  show ?thesis
    apply (rule subset_image_lepoll [where f = "λU x. if ∃y. (x,y) ∈ U then @y. (x,y) ∈ U else k x"])
    using * by (auto simp: image_def)

lemma eqpoll_Fpow:
  assumes "infinite A" shows "Fpow A ≈ A”

The thing is though, Fpow (which is nothing but the finite powerset operator) probably belongs in Main as well.

An alternative proposal is to create a new theory, Library/Equipollence. I agree about hiding the syntax.


> On 23 Jan 2019, at 10:11, Traytel Dmitriy <traytel at inf.ethz.ch> wrote:
> Hi Larry,
> if you want to put the definitions and the basic properties in Main, then Fun.thy would probably be the place. But then I would argue that the syntax should be hidden, as users might want to use these symbols for something else.
> For the advanced material, do you need some theorems from HOL-Cardinals or just the syntax from HOL-Library.Cardinal_Notations in addition to what is already there in Main about cardinals? If it is only the syntax, then a separate theory in HOL-Library is probably a good fit. Otherwise, a separate theory in HOL-Cardinals would make sense.
> Dmitriy

More information about the isabelle-dev mailing list