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

Reply via email to