Re: [isabelle] Code generation with invariants and new data types

Hi Andreas,

> datatype ('k, 'v) trie =
>   Trie "'v option" "('k, ('k, 'v) trie) assoc_list"
> However, the datatype package complains that ('k, ('k, 'v) trie)
> assoc_list is a non-admissible type expression which must not be used in
> a nested recursion.

this restriction is not just a technical one: to be able to construct
the datatype representation, the datatype package must how to recurse
through other types involving recursion, and therefore these must
satisfay a couple of properties (which assoc_list doesn't).

> How can I define tries where all lists for the successor nodes are
> distinct? Do I really have to go back to lists and explicit data
> structure invariants and do the lifting all over again? I hope there is
> a much more elegant solution to this.

Without having an example at hand, I would deem that this is largely a
matter whether you are able to organize your proofs in a way that you
can reuse the already proven properties of assoc_list representations.
Experience however shows that fundamental constructions over datatypes
must consider the construction of the datatype anyway, so this might be




PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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