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