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

2019-01-28 Thread Lawrence Paulson
Last January 24, I moved Fpow into Main and introduced Library/Equipollence.thy. Hope you like it. Larry > On 26 Jan 2019, at 15:14, Andrei Popescu wrote: > > Sorry for my late reply. I agree it makes sense to move such basic operators > (and facts) into Main. The Ordinals and Cardinals

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

2019-01-26 Thread Andrei Popescu
lanchette Cc: Traytel Dmitriy , isabelle-dev Subject: Re: [isabelle-dev] [Spam] cardinality primitives in Isabelle/HOL? Message-ID: Content-Type: text/plain; charset=utf-8 This makes perfect sense to me. I suggest moving at least the definition of Fpow into Main (it?s small, a

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

2019-01-23 Thread Lawrence Paulson
The question of dependency is tricky. I tried deleting the reference to HOL-Cardinals.Cardinals and found that most of the elementary results were easily provable using other library facts. But then there was this: lemma lepoll_trans1 [trans]: "⟦A ≈ B; B ≲ C⟧ ⟹ A ≲ C" by (meson card_of_ordLeq

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

2019-01-23 Thread 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

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

2019-01-22 Thread Lawrence Paulson
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

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

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

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

2018-12-28 Thread 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

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

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 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: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
> 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,