[isabelle-dev] lists of n elements

[Peter Lammich]

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}"
>>
The naming of the lemmas suggests that this function should be named 
lists, not list.

--

   Peter


>> 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
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev