isabelle

How can I use a size parameter for datatype definitions

I want to use the word type from "HOL-Library.Word" in a datatype where I don't want to fix the size of the word.

datatype 's Foo = Foo1 "'s word" | Foo2 "'s word"

But this does not work, Isabelle complains with

Type definition with open dependencies, use "typedef (overloaded)" or enable configuration option "typedef_overloaded" in the context.
Type: 's Foo.Foo_IITN_Foo
Deps: len_of('s)
The error(s) above occurred in typedef "Foo.Foo_IITN_Foo"

If it was a record, I could use overloaded like this

record(overloaded) 's Bar =
  bar1 :: "'s word"

But if I try to use overloaded for a datatype

datatype(overloaded) 's Foo = Foo1 "'s word" | Foo2 "'s word"

Then I get the error

Outer syntax error⌂: type variable expected,
but keyword overloaded⌂ was found

How can I define a datatype that uses word of a size that is not fixed?

Solution

  • I do not know the details of typedef_overloaded, but it does appear in the AFP, so the following should be okay:

    context notes [[typedef_overloaded]] begin
datatype 's Foo = Foo1 "'s::len word" | Foo2 "'s word"
end

    Or, if you prefer not using it, want to be extra safe, just create a bnf without the word and create new abbreviation that work only with words...

    
datatype 's Foo_tmp = Foo1_tmp 's  | Foo2_tmp 's 

type_synonym 's Foo = "'s word Foo_tmp"
abbreviation Foo1 :: ‹_ ⇒ 's word Foo_tmp›where
"Foo1 ≡ Foo1_tmp"
abbreviation Foo2 :: ‹_ ⇒ 's word Foo_tmp›where
"Foo2 ≡ Foo2_tmp"