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

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20181227/94512e34/attachment.bin>