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 > [email protected] > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev -- _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
