On Fri, 26 Aug 2011, Brian Huffman wrote:
Here's one possible approach to the set-axiomatization/typedef issue:
As a new primitive, we could have something like a "pred_typedef"
operation that uses predicates. This would work just like the
new_type_definition facility of HOL4, etc.
The type "'a set" could be introduced definitionally using
"pred_typedef".
After type "'a set" has been defined, we can implement the "typedef"
command, preserving its current behavior, as a thin wrapper on top of
"pred_typedef".
This approach would let us avoid having to axiomatize the 'a set type.
Also, for those of us who like predicates, "pred_typedef" might be
rather useful as a user-level command.
What is gained from that apart from having two versions of typedef?
We have had that very discussion around 1994, when Tobias thought that
typedef could be a definitional primitive of Pure, but it turned out to be
non-conservative outside of its special HOL-ish semantic fitting.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
