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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and