[isabelle] Code generation with invariants and new data types



Hello all,

since the code generator now can also handle invariants, I encapsulated the associative lists in the Isabelle/HOL library with the distinctness predicate as an abstract type

typedef (open) ('k, 'v) assoc_list =
  "{xs :: ('k × 'v) list. distinct (map fst xs)}"
  morphisms impl_of Assoc_List
by(rule exI[where x="[]"]) simp

and lifted all primitive operations and their correctness statements from ('k * 'v) list to ('k, 'v) assoc_list. Now, I would like to go one step further and define a trie which uses these associative lists to manage the successor nodes:

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.

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.

Best regards,
Andreas





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