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

```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
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  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  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
>

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

```

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

```

> On 28 Dec 2018, at 19:36, Lawrence Paulson  wrote:
>
> Tons of useful stuff here.
>
> Some syntactic ambiguities, particularly around the =o relation, which is
> also defined as Set_Algebras.elt_set_eq.

True. The same holds for +o and *o (which are less widely used in the ordinals
library).

I'm not sure what a good naming is in these cases. "=o" makes sense for me as
"equality on ordinals". It would be ok for me to play with capitalization or
other abbreviations of ordinals, e.g., "=O" or "=ord". Maybe Andrei can
comment, as he picked the current notation.

I don't know what "=o" stands for in the case of Set_Algebras.elt_set_eq (is
this a reference to the Oh-notation?) and why there is need for an alternative
notation for ∈. I believe the better textbooks are those that write "f ∈ O(g)"

Along similar lines, I find the notation "f
> I don’t suppose there’s any chance of using quotients to define actual
> cardinals and use ordinary equality?

Not really. "(=o) :: 'a rel ⇒ 'b rel ⇒ bool" is too polymorphic for this to
work properly.  (The relation arguments are ordinals represented by
well-orders.) One can quotient modulo a restricted relation "(=o) :: 'a rel ⇒
'a rel ⇒ bool", but then the equality on the quotient type won't allow us to
compare "|UNIV :: nat set| :: nat rel" to "|UNIV :: real set| :: real rel".

> And it still makes sense to introduce the actual notion of equipollence and
> similar relations.

This is the usual trade-off between many similar definitions with dedicated
reasoning support (transitivity, congruence, and monotonicity rules and such)
or a few core ones. Possibly an abbreviation is sufficient in this case.

Dmitriy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

```

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

```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).

Our ITP'14 paper explains the design of the library:

http://people.inf.ethz.ch/trayteld/papers/itp14-card/card.pdf

Dmitriy

> On 27 Dec 2018, at 13:31, Lawrence Paulson  wrote:
>
> I am inclined to introduce these definitions:
>
> definition lepoll :: "'a set ⇒ 'b set ⇒ bool" (infixl "≲" 50)
>where "lepoll A B ≡ ∃f. inj_on f A ∧ f ` A ⊆ B"
>
> definition eqpoll :: "'a set ⇒ 'b set ⇒ bool" (infixl "≈" 50)
>where "eqpoll A B ≡ ∃f. bij_betw f A B”
>
> They allow, for example, this:
>
> theorem Schroeder_Bernstein_eqpoll:
>  assumes "A ≲ B" "B ≲ A" shows "A ≈ B"
>  using assms unfolding eqpoll_def lepoll_def by (metis Schroeder_Bernstein)
>
> The names and syntax are borrowed from Isabelle/ZF, and they are needed for
> some HOL Light proofs.
>
> But do they exist in some form already? And are there any comments on those
> relation symbols?
>
> Larry
>
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

```