[isabelle-dev] typedef (open) legacy
makarius at sketis.net
Thu Oct 4 14:17:48 CEST 2012
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
> 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
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 ...
More information about the isabelle-dev