From: Lawrence Paulson <lp15@cam.ac.uk>

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

From: Tobias Nipkow <nipkow@in.tum.de>

On 04/08/2022 15:50, Lawrence Paulson 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}"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_eqAnd 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@in.tum.de

https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

smime.p7s

From: Peter Lammich <lammich@in.tum.de>

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.

From: Tobias Nipkow <nipkow@in.tum.de>

On 04/08/2022 17:49, Peter Lammich wrote:

In the AFP we have four separate copies of the definition

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_eqAnd 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@in.tum.de

https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

isabelle-dev mailing list

isabelle-dev@in.tum.de

https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

isabelle-dev mailing list

isabelle-dev@in.tum.de

https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

smime.p7s

From: Peter Lammich <lammich@in.tum.de>

isabelle-dev mailing list

isabelle-dev@in.tum.de

https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Last updated: Mar 04 2024 at 10:08 UTC