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
