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

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


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


The notation itself is quite generic, so it is worth spending more
thoughts on how can we keep reusable.  Maybe it would be worth a try to
put the syntax into a bundle (there are already some applications of
that pattern):

bundle set_relation_syntax
begin

notation …

end

bundle no_set_relation_syntax
begin

no_notation …

end

…

unbundle set_relation_syntax

…

unbundle no_set_relation_syntax

The input abbreviation gepoll should be added as well.

Anyway, I am uncertain about the name »poll«.

Cheers,
Florian


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





smime.p7s
Description: S/MIME Cryptographic Signature
___
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?

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
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


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 equipotent, equipollent, or 
> equinumerous. This relationship can also be denoted A ≈ B or A ~ B.”

I see.  Using »poll« is a stem, the canonical names would be

less_eq_poll
equiv_poll
greater_eq_poll

(I don't know how useful the strict versions less_poll, greater_poll
would be).

Florian



signature.asc
Description: OpenPGP digital signature
___
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?

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 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 equipotent, equipollent, or equinumerous. This 
relationship can also be denoted A ≈ B or A ~ B.”

Larry
___
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?

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

The notation itself is quite generic, so it is worth spending more
thoughts on how can we keep reusable.  Maybe it would be worth a try to
put the syntax into a bundle (there are already some applications of
that pattern):

bundle set_relation_syntax
begin

notation …

end

bundle no_set_relation_syntax
begin

no_notation …

end

…

unbundle set_relation_syntax

…

unbundle no_set_relation_syntax

The input abbreviation gepoll should be added as well.

Anyway, I am uncertain about the name »poll«.

Cheers,
Florian



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


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