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) qed 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. Larry > On 23 Jan 2019, at 10:11, Traytel Dmitriy <tray...@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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev