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



Am 22/05/2013 19:16, schrieb Christoph LANGE:
> 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.

Most of the time, converting from sets to lists is a cloogy workaround because
of problems defining some function directly on fnite sets. I recommend to
understand and use the appropriate fold combinator on lists instead.

tobias




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