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



Dear Florian,

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).
You are right, the datatype definition unfolds nested recursion into mutual recursion. However, since assoc_list builds on the list and product datatypes, the manual unfolding and repackaging could be automated some time. Essentially, assoc_list is just a (degenerated) quotient type over list with the PER xs ~ ys <--> xs = ys & distinct (map fst ys). The quotient package already offers some support for lifting quotients over other type constructors, but this still has to be done manually. Are there any plans to integrate more tightly datatypes, abstract code generator types and the quotient package?

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.
Since the above quotient construction can be lifted over to the trie datatype, I think the datatype as mentions above can be constructed manually with the free constructor Trie and an induction rule. However, doing all this manually is probably not worth the effort.

Cheers,
Andreas





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