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

[Lawrence Paulson]

Tons of useful stuff here.

Some syntactic ambiguities, particularly around the =o relation, which is also defined as Set_Algebras.elt_set_eq.

I don’t suppose there’s any chance of using quotients to define actual cardinals and use ordinary equality? And it still makes sense to introduce the actual notion of equipollence and similar relations.

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