<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>