On Fri, 26 Aug 2011, Andreas Schropp wrote:
This is not really a problem, but complicates my conservativity argument.
Before local typedefs the proof of (EX x. x : A) was global. Actually
Makarius' attitude on this was that those non-emptiness proofs "should be
global most of the time", but he didn't want to introduce a check.
I don't understand this. Local typedefs are just a conjuring trick around
plain old global ones (in the above presentation) -- no changes of the
logical foundations here.
Formerly the non-emptiness proof was global, now its local!
locale bla =
assume "False"
typedef empty = {}
Yes, I now remember our state of discussion quite some time ago. It is
part of the conjuring to make it a bit unconstructive, but it still
follows the original spirit of Gordon/Pitts HOL typedefs as I've
understood them many years ago.
This does not mean there is no other way. Back then we just did not get
to the point where I had your translation running concretely, so it was
not continued. Where is your translation tool suite now? What is its
state concerning current Isabelle versions?
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
