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

[Traytel Dmitriy]

Hi Larry,

if you want to put the definitions and the basic properties in Main, then Fun.thy would probably be the place. But then I would argue that the syntax should be hidden, as users might want to use these symbols for something else.

For the advanced material, do you need some theorems from HOL-Cardinals or just the syntax from HOL-Library.Cardinal_Notations in addition to what is already there in Main about cardinals? If it is only the syntax, then a separate theory in HOL-Library is probably a good fit. Otherwise, a separate theory in HOL-Cardinals would make sense.

Dmitriy

> On 22 Jan 2019, at 15:58, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> 
> 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
>