On 27/12/2018 17:45, Traytel Dmitriy wrote:
> Hi Larry,
>
> the HOL-Cardinals library might be just right for the purpose:
>
> theory Scratch
> imports "HOL-Cardinals.Cardinals"
> begin
>
> lemma "|A| ≤o |B| ⟷ (∃f. inj_on f A ∧ f ` A ⊆ B)"
> by (rule card_of_ordLeq[symmetric])
>
> lemma "|A| =o |B| ⟷ (∃f. bij_betw f A B)"
> by (rule card_of_ordIso[symmetric])
>
> lemma
> assumes "|A| ≤o |B|" "|B| ≤o |A|"
> shows "|A| =o |B|"
> by (simp only: assms ordIso_iff_ordLeq)
>
> end
>
> The canonical entry point for the library is the above
> HOL-Cardinals.Cardinals. Many of the theorems and definitions are already in
> Main, because the (co)datatype package is based on them. The syntax is hidden
> in main—one gets it by importing HOL-Library.Cardinal_Notations (which
> HOL-Cardinals.Cardinals does transitively).
It would be great to see this all consolidated and somehow unified, i.e.
some standard notation in Main as proposed by Larry (potentially as
bundles as proposed by Florian), and avoidance of too much no_syntax
remove non-standard notation from Main.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
