<div dir='auto'>Ok<div dir="auto"><br></div><div dir="auto">For lists only of a specified length, the name is a bit generic anyway.</div><div dir="auto"><br></div><div dir="auto">Peter </div></div><div class="gmail_extra"><br><div class="gmail_quote">On 4 Aug 2022 18:03, Tobias Nipkow <nipkow@in.tum.de> wrote:<br type="attribution" /><blockquote class="quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><p dir="ltr"> <br>
<br>
On 04/08/2022 17:49, Peter Lammich wrote: <br>
> In the AFP we have four separate copies of the definition <br>
>>> <br>
>>> definition list :: "nat \<Rightarrow> 'a set \<Rightarrow> 'a list set" <br>
>>> where <br>
>>>   "list n A = {xs. size xs = n \<and> set xs \<subseteq> A}" <br>
>>> <br>
> The naming of the lemmas suggests that this function should be named lists, not  <br>
> list. <br>
<br>
The motivation for "list" what is that in should mimic the name of the type  <br>
constructor "list". On the level of types of rules omitted, e.g. nat not nats. <br>
<br>
However I think these days I would also use the plural of the term level. <br>
<br>
Tobias <br>
<br>
> --  <br>
>  <br>
>    Peter <br>
>  <br>
>  <br>
>>> Interestingly, the exact same concept is coded in three different ways in the  <br>
>>> four definitions. We also have a number of theorems in the repository  <br>
>>> referring to this concept: <br>
>>> <br>
>>> finite_lists_length_eq <br>
>>> set_n_lists <br>
>>> card_lists_length_eq <br>
>>> lists_length_Suc_eq <br>
>>> <br>
>>> And we have three copies of Listn.thy in MicroJava and JinjaThreads. Could  <br>
>>> maybe some fragment of this, if not the whole thing, be moved into Library? <br>
>> <br>
>> Definitely, go ahead! (I obviously prefer the def you quoted above) <br>
>> <br>
>> Tobias <br>
>> <br>
>>> Larry <br>
>>> <br>
>>> _______________________________________________ <br>
>>> isabelle-dev mailing list <br>
>>> isabelle-dev@in.tum.de <br>
>>> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev <br>
>> <br>
>> _______________________________________________ <br>
>> isabelle-dev mailing list <br>
>> isabelle-dev@in.tum.de <br>
>> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev <br>
> _______________________________________________ <br>
> isabelle-dev mailing list <br>
> isabelle-dev@in.tum.de <br>
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev </p>
<p dir="ltr">_______________________________________________<br>
isabelle-dev mailing list<br>
isabelle-dev@in.tum.de<br>
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev<br>
</p>
</blockquote></div><br></div>