*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Two lemmas about lists constructed from finite sets that I'd like Isabelle to provide*From*: Lars Noschinski <noschinl at in.tum.de>*Date*: Wed, 22 May 2013 20:30:00 +0200*In-reply-to*: <519CFD75.3050506@gmail.com>*References*: <519CFD75.3050506@gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:10.0.12) Gecko/20130116 Icedove/10.0.12

On 22.05.2013 19:16, Christoph LANGE wrote:

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 ≠ []"

--------------------------------------------- lemma sorted_list_of_set_remove': assumes "finite A" "x ∈ A" shows "sorted_list_of_set A = insort x (sorted_list_of_set (A - {x}))" proof - from assms have "insert x (A - {x}) = A" by blast

by simp also have "... = insort x (sorted_list_of_set (A - {x}))" using assms by simp finally show ?thesis . qed --------------------------------------------- then your proof goes through with using assms by (auto simp: sorted_list_of_set_remove') 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')

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

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

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.

-- Lars

**Follow-Ups**:

**References**:

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