[isabelle-dev] typedef (open) legacy

[Christian Urban]

Thanks a lot for all replies!

Christian



On Thursday, October 4, 2012 at 14:17:48 (+0200), Makarius wrote:
 > 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-dev at in.tum.de
 > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

--