On Thu, 4 Oct 2012, Christian Urban wrote:
"Closed" type definitions with
typedef new_type = "some set"
are considered legacy. The warning message suggests
to use
typedef (open) new_type = "some set"
but as far as I can see, this does not introduce a definition for the
set underlying the type. For example the theorem
new_type_def
is not generated with open.
I have a number of lemmas that are of the form
f \<in> new_type ==> something
which require new_type_def. What is the received
wisdom to update those proofs?
I see that FinFun.thy goes around the problem
above by giving an explicit definition for the
set as in
definition new_type_set = something
typedef (open) new_type = new_type_set
Is this how it should be done nowadays? Looks to me more verbose than an
improvement.
The latter "verbose" version is the canonical way to upgrade old theories,
without changing their structure. If a bit more work is invested, in most
cases the very need for the new_type_set definition can be eliminated in
the concrete application, and then everything becomes simpler than before.
Historically, Larry introduced a certain "Gordon HOL typedef imitation
scheme" for Isabelle/HOL, which I imitated faithfully in the first version
of the typedef package, to generate exactly the same axiomatization with
the auxiliary new_type_set. Several years later, Brian Huffman pointed
out first that this is redundant in many situations. Some more years
later, I joined Brian in this observation --- after looking critically
through the existing library of theories and packages.
So today, the form with the extra definition is mostly irrelevant, but we
were a bit slow to remove the last remains of it from the typedef packages
(and some add-ons of it in HOLCF). It might be time now to do the purge
before the next release ...
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
