[isabelle-dev] typedef (open) legacy

[Makarius]

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