[isabelle] mutually recursive datatypes with records



I'm trying to create a mutually recursive datatype where one half of it is specified via the datatype keyword and the other half via a record keyword. There seems to be no way to combine regular datatypes and records unless I implement my own records out of datatypes, which seems clumsy and pointless given that Isabelle/HOL already has records. What can I do to specify the datatype I need? Below is an example of the kind of thing I want:
datatype type1 =
 foo |
 bar "type2 list"
and
record type2 =
 field1 :: nat
 field2 :: type1

The only thing I can think of at the moment is:
datatype type1 =
 foo |
 bar "type2 list"
and type2 = "nat * type1"

--
                            Greg Bronevetsky






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.