Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] lists of n elements

Email Gateway (Aug 04 2022 at 13:51):

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

Email Gateway (Aug 04 2022 at 14:32):

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_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@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
smime.p7s

Email Gateway (Aug 04 2022 at 15:49):

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.

Email Gateway (Aug 04 2022 at 16:03):

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

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

Email Gateway (Aug 04 2022 at 17:12):

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: Apr 28 2024 at 08:19 UTC