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

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



Christoph Lange, School of Computer Science, University of Birmingham, Skype duke4701

→ Intelligent Computer Mathematics, 8–12 July, Bath, UK.
  Work-in-progress deadline 7 June;
→ OpenMath Workshop, 10 July, Bath, UK.
  Submission deadline 7 June;

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.