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

2018-12-27 Thread Traytel Dmitriy
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

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

2018-12-27 Thread Makarius
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

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

2018-12-27 Thread Florian Haftmann
> 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,

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

2018-12-27 Thread Lawrence Paulson
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,

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

2018-12-27 Thread Lawrence Paulson
> On 27 Dec 2018, at 12:39, Florian Haftmann > wrote: Thanks for the suggestions. > The input abbreviation gepoll should be added as well. > > Anyway, I am uncertain about the name »poll«. From https://en.wikipedia.org/wiki/Cardinality "Two sets A and B have the same cardinality if there

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

2018-12-27 Thread Florian Haftmann
>> Anyway, I am uncertain about the name »poll«. > > From https://en.wikipedia.org/wiki/Cardinality > > "Two sets A and B have the same cardinality if there exists a bijection from > A to B, that is, a function from A to B that is both injective and > surjective. Such sets are said to be

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

2018-12-27 Thread Lawrence Paulson
> On 27 Dec 2018, at 12:45, Florian Haftmann > wrote: > > (I don't know how useful the strict versions less_poll, greater_poll > would be). Strict versions do turn up in some places (both in HOL Light and Isabelle/ZF) ___ isabelle-dev mailing list

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

2018-12-27 Thread Tobias Nipkow
I agree with Florian wrt syntax. Tobias On 27/12/2018 13:39, Florian Haftmann 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"