*To*: Lars Noschinski <noschinl at in.tum.de>, Brian Huffman <huffman.brian.c at gmail.com>*Subject*: Re: [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 21:45:29 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <519D0EA8.4080800@in.tum.de>*Organization*: University of Birmingham*References*: <519CFD75.3050506@gmail.com> <519D0EA8.4080800@in.tum.de>*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

Hi Lars, hi Brian, thanks for your quick help; let me answer all remaining points at once. 2013-05-22 19:30 Lars Noschinski: > I first wondered why you had problems with these proofs; then I > discovered that Florians rework of Big_Operators in the development > version added some crucial lemmas ;) Oh, I see. Sorry, I should have said that I'm using the Isabelle2013 release version. >> lemma sorted_list_of_set_not_empty [simp] : >> assumes "finite S" and "S ≠ {}" >> shows "sorted_list_of_set S ≠ []" > > Sledeghammer is able to find a proof after unfolding > sorted_list_of_set_def. That's indeed a good lesson for me as a, still, relative newbie. So far I had been doing this "unfolding some_def sledgehammer" step with definitions of my own, whereas I had never thought of doing it with definitions from the library. > A nicer proof however is … > then your proof goes through with … > BTW, a nicer lemma would be: > > lemma sorted_list_of_set_eq_Nil_iff: > assumes "finite S" > shows "sorted_list_of_set S = [] <-> S = []" > using assms by (auto simp: sorted_list_of_set_remove') Thanks (to Brian, too)! For now I copied these into my formalisation. Is it right that as soon as I switch to Isabelle2014 or to the development version I will be able to remove this code? >> lemma sorted_list_of_set_distinct [simp] : >> shows "distinct (sorted_list_of_set S)" >> sorry > > This property does not hold in Isabelle 2013, as Finite_Set.fold is only > defined for finite sets (i.e., we cannot prove anything about infinite > sets). So you need to district your lemma to finite sets. Then the proof > is easy: > > lemma sorted_list_of_set_distinct [simp] : > assumes "finite S" shows "distinct (sorted_list_of_set S)" > using assms sorted_list_of_set by auto > > (In the next version of Isabelle, Finite_Set.fold will probably return > the initial argument for infinite sets). Thanks, and thanks for pointing out that I had forgotten to assume "finite S". >> 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. > > As sets have no order, fold is only well-defined if the operation you > define is commutative. Indeed. Still I have no idea whether it will be _easy_ to use finite_ne_induct in my case. Folding is actually not applicable to my Max-like function, which is actually rather a variant of "arg max" in that it returns the index of the maximum component of a vector, where the index is an element of those finite "nat set"s that I'm using. – Anyway, just some thoughts. Your solutions work fine for me, and allow me to focus on my actual problem (proving that a certain auction formalisation determines a unique winner – soon to become public at http://www.cs.bham.ac.uk/research/projects/formare/code/auction-theory/). Cheers, 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**:

**References**:

- Previous by Date: [isabelle] Set of functions
- 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] Two lemmas about lists constructed from finite sets that I'd like Isabelle to provide
- 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