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
illusory.

Cheers,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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