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

Lawrence Paulson lp15 at cam.ac.uk
Fri Dec 28 19:36:01 CET 2018

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.


> 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

More information about the isabelle-dev mailing list