[isabelle-dev] typedef (open) legacy

[Brian Huffman]

On Thu, Oct 4, 2012 at 2:17 PM, Makarius <makarius at 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