*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. Cheers, and thanks in advance for your help, 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. Work-in-progress deadline 7 June; http://cicm-conference.org/2013/ → OpenMath Workshop, 10 July, Bath, UK. Submission deadline 7 June; http://cicm-conference.org/2013/openmath/

**Follow-Ups**:**Re: [isabelle] Two lemmas about lists constructed from finite sets that I'd like Isabelle to provide***From:*Brian Huffman

**Re: [isabelle] Two lemmas about lists constructed from finite sets that I'd like Isabelle to provide***From:*Lars Noschinski

**Re: [isabelle] Two lemmas about lists constructed from finite sets that I'd like Isabelle to provide***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] Be nice to have short tutorials on Quotient Types and Lifting
- Next by Date: Re: [isabelle] Two lemmas about lists constructed from finite sets that I'd like Isabelle to provide
- Previous by Thread: Re: [isabelle] [isabelle-dev] The-operator
- Next by Thread: Re: [isabelle] Two lemmas about lists constructed from finite sets that I'd like Isabelle to provide
- Cl-isabelle-users May 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list