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

[Makarius]

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