I am currently working on AFP/Coinductive, which is full of the sort of thing.
Larry
On 19 Aug 2011, at 00:31, Gerwin Klein wrote:
Can't really quantify it, but I'm seeing this all the time from not-so-novice
users over here. Mixing sets and predicates (e.g. using intersection on
Hi all,
On 19.08.2011 01:38, Gerwin Klein wrote:
Should we ask a wider audience (isabelle-users) if anybody else has
good reasons against/for a change?
Another small advantage of set as an own datatype arises in the context
of subtyping.
We use map functions to lift coercions between base
Stefan Berghofer wrote:
Alexander Krauss wrote:
In particular, Stefan discovered that replacing inductive set
definitions by predicates was by no means as easy as everybody had
expected. One good example is the small-step relation from Jinja and
its various cousins. It had type ((expr * state)
On 08/19/2011 07:39 AM, Tobias Nipkow wrote:
Am 19/08/2011 00:00, schrieb Stefan Berghofer:
Alexander Krauss wrote:
I want to emphasize that the limitation of the code generator mentioned
here not only applies to sets-as-predicates but also to
maps-as-functions and other abstract types that
To avoid duplication of effort, note that I'm currently trying to convert the
AFP theories DataRefinementIBP and GraphMarkingIBP.
Larry
___
isabelle-dev mailing list
isabelle-...@in.tum.de
On 08/19/2011 01:31 AM, Gerwin Klein wrote:
On 19/08/2011, at 5:56 AM, Alexander Krauss wrote:
* Similarly, there is a vast proof search space for automated
tools which is not worth exploring since it leads to the »wrong
world«, making vain proof attempts lasting longer instead just
failing.
Hi again,
Indeed, I think a general point can be made here, and not just about code
generation. In the last couple of years, we've run into situations in
Quickcheck, Nitpick, the code generator, and perhaps more, where we felt the
need for sets as different from functions. However, there
