On 04/08/2022 17:49, Peter Lammich 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}"
>>>
> The naming of the lemmas suggests that this function should be named lists, not
> list.
The motivation for "list" what is that in should mimic the name of the type
constructor "list". On the level of types of rules omitted, e.g. nat not nats.
However I think these days I would also use the plural of the term level.
Tobias
> --
>
> 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
>>> [email protected]
>>> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
>>
>> _______________________________________________
>> isabelle-dev mailing list
>> [email protected]
>> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
> _______________________________________________
> isabelle-dev mailing list
> [email protected]
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
