On Thu, Oct 4, 2012 at 2:17 PM, Makarius <makar...@sketis.net> 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.
Defining a set constant does not make sense for all typedefs. For example, type 'a word in HOL-Word is defined something like this: typedef (open) 'a word = "{(0::int) ..< 2^card (UNIV :: 'a set)}" It is not possible to define a single constant "word :: int set" that is equal to the given right-hand side for any 'a. Similar typedefs are also found in the HOLCF libraries. Here are the options we have for the typedef implementation: 1) typedef fails with an internal error on such definitions in its default (closed) mode 2) typedef includes special code to generate set definitions with extra type parameters, e.g. "word :: 'a itself => int set" 3) typedef uses (open) as the default mode, with closed definitions as an option 4) typedef supports only open set definitions Option 1 is how typedef worked until a few years ago; obviously the error message was undesirable. Option 2 is how it works now, but the special code complicates the package and the special behavior is a bit surprising when it happens. I think either option 3 or 4 would make sense, although I'd say 4 is preferable for a couple of reasons: First, it makes the implementation of typedef simpler. Second, it actually gives users more flexibility because if they want a set constant, they can use any definition package, not just "definition". The extra verbosity in some cases is a small price to pay. [...] > 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 ... I was reluctant to support "closed" type definitions at all in HOLCF's cpodef and friends, preferring to make (open) the default behavior; but in the end I decided it was more important to make the input syntax consistent with typedef. I would be more than happy to remove this feature from the HOLCF packages if typedef will be changed to match. - Brian _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev