[isabelle-dev] lists of n elements

[Tobias Nipkow]

On 04/08/2022 15:50, Lawrence Paulson wrote:
> In the AFP we have four separate copies of the definition
> 
> definition list :: "nat \<Rightarrow> 'a set \<Rightarrow> 'a list set"
> where
>   "list n A = {xs. size xs = n \<and> set xs \<subseteq> A}"
> 
> Interestingly, the exact same concept is coded in three different ways in the 
> four definitions. We also have a number of theorems in the repository referring 
> to this concept:
> 
> finite_lists_length_eq
> set_n_lists
> card_lists_length_eq
> lists_length_Suc_eq
> 
> And we have three copies of Listn.thy in MicroJava and JinjaThreads. Could maybe 
> some fragment of this, if not the whole thing, be moved into Library?

Definitely, go ahead! (I obviously prefer the def you quoted above)

Tobias

> Larry
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5535 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20220804/4de916ab/attachment.bin>