I'm strongly in favour of an explicit set type.
I've been asked for advice by a number of novice Isabelle users and given the
same recommendation: go make the development type-check under the old rules.
Then the simplifier will start helping you rather than fighting you.
I suppose there might be an alternative strategy involving adapting the simpset
or similar to try to standardise blended terms on set operations or function
operations. But I don't think this is possible the way Isabelle works - if it
were not the default noone then it would not help, and if it were then it would
generate years of work in compatibility with the existing proof library.
Yours,
Thomas.
________________________________________
From: isabelle-dev-boun...@mailbroy.informatik.tu-muenchen.de
[isabelle-dev-boun...@mailbroy.informatik.tu-muenchen.de] On Behalf Of Lawrence
Paulson [l...@cam.ac.uk]
Sent: Thursday, August 11, 2011 11:09 PM
To: Florian Haftmann
Cc: DEV Isabelle Mailinglist
Subject: Re: [isabelle-dev] (Re-)introducing set as a type constructor rather
than as mere abbreviation
I hope that my position on this question is obvious. And if we decide to revert
to the former setup, I would be happy to help track down and fix some problems
in theories.
Larry
On 11 Aug 2011, at 13:43, Florian Haftmann wrote:
> Why (I think) the current state concerning sets is a bad idea:
> * There are two worlds (sets and predicates) which are logically the
> same but syntactically different. Although the logic construction
> suggests that you can switch easily between both, in practice you can't
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited accepts
no liability for any damage caused by this email or its attachments.
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
