Re: [isabelle] finite sets and code generation, once again


On 14/07/2010, at 11:09 PM, Peter Lammich wrote:

> What's about
>    d) Parameterize over choice-function (e.g. using a locale, fixing
> choice and assuming: "s~={} ==> choice s : s"), do your definition
> inside this locale
>        and then instantiate to concrete set implementation ?

I like this approach - thanks for sharing it.

However it seems a bit limited: locale-fixed functions ("choice") are monomorphic, right? In other words, I would need to instantiate this locale at every type I wanted to apply "choice" to. I guess I'm asking for the locale equivalent of the polymorphic SOME.

In any case I think the amount of proof-pain of eliminating choice is pretty much constant whatever the scaffolding is, having tried out a few approaches recently.



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