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

[Lawrence Paulson]

I’m trying to install some of my new material and I’m wondering what to do with equipollence and related concepts:

definition eqpoll :: "'a set ⇒ 'b set ⇒ bool" (infixl "≈" 50)
  where "eqpoll A B ≡ ∃f. bij_betw f A B"

definition lepoll :: "'a set ⇒ 'b set ⇒ bool" (infixl "≲" 50)
  where "lepoll A B ≡ ∃f. inj_on f A ∧ f ` A ⊆ B"

definition lesspoll :: "'a set ⇒ 'b set ⇒ bool" (infixl ‹≺› 50) 
  where "A ≺ B == A ≲ B ∧ ~(A ≈ B)"

The raw definitions are extremely simple and could even be installed in the main Isabelle/HOL distribution. The basic properties of these concepts require few requisites. However, more advanced material requires the Cardinals development. 

Where do people think these definitions and proofs should be installed?

Larry

> On 27 Dec 2018, at 20:29, Makarius <makarius at sketis.net> wrote:
> 
> 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