[isabelle-dev] lists of n elements

[Lawrence Paulson]

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?

Larry
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20220804/f5afa9cf/attachment.htm>