Re: [isabelle] Code generation with invariants and new data types
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?
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).
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.
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and