# [isabelle] Two lemmas about lists constructed from finite sets that I'd like Isabelle to provide

• To: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>
• Subject: [isabelle] Two lemmas about lists constructed from finite sets that I'd like Isabelle to provide
• From: Christoph LANGE <math.semantic.web at gmail.com>
• Date: Wed, 22 May 2013 18:16:37 +0100
• Organization: University of Birmingham
• Sender: Christoph Lange <allegristas at gmail.com>
• User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130518 Thunderbird/17.0.6

```Dear Isabelle community,

I am currently working with lists constructed from finite sets, and I'm
missing the following two lemmas that would really help me to get my
work done.  At the moment my Isabelle experience is not sufficient for
proving them myself, plus I think it would make sense if they were part
of the library (List.thy).

lemma sorted_list_of_set_not_empty [simp] :
assumes "finite S" and "S ≠ {}"
shows "sorted_list_of_set S ≠ []"
sorry

lemma sorted_list_of_set_distinct [simp] :
shows "distinct (sorted_list_of_set S)"
sorry

Would any of the developers feel up to proving them, or alternatively
teaching me how to do it?

BTW, for my work I actually don't need these lists-from-sets to be
_sorted_.  However sorted_list_of_set is the only result that

find_consts "'a set ⇒ 'a list"

gives me.  Efficient computation is not yet that crucial for my work,
but would it be possible to provide a list-from-set constructor that
does not guarantee sorting?  I mean something that simply rearranges the
internal data structure of a finite set (which is not guaranteed to be
sorted either) into a list.

Finally, lists-from-sets are probably not even what I need to get my
actual work done.  I.e. if you think that there is no good reason for me
using them, I'm willing to abandon them.  Originally I'm working with
finite sets, but I defined a custom Max-like operation on them, which
recursively folds the comparison of two elements over the whole
set/list.  As I'm not yet capable of understanding the internals behind

definition (in linorder) Max :: "'a set ⇒ 'a" where
"Max = fold1 max"

in Big_Operators.thy (which seem to depend on certain idempotence laws
that max satisfies), but wanted to prove some properties of my Max-like
operation and got stuck in my initial attempt to use finite_ne_induct, I
resorted to converting my finite sets to lists and using
list_nonempty_induct – which did the job, except for the two missing
lemmas mentioned above.

Christoph

--
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701

→ Intelligent Computer Mathematics, 8–12 July, Bath, UK.