From: Joachim Breitner <breitner@kit.edu>
Dear list,
I am trying to work with the code generator and an abstract datatype
with invariants. What I learned so far is:
Code equations for functions returning values of the abstract type
are written in terms of the representation of the returned value and
if I have functions that return the abstract type in a container, I
need to introduce new abstract types that express the invariant for
all members.
But I am stuck with higher order functions. Say abs is my abstract type,
abs_list the abstract type for lists of abs representations. How would I
write the code equation for a combinator like
definition abs_list_all :: "(abs ⇒ bool) ⇒ abs_list ⇒ bool"
where "abs_list_all P l = list_all (λx. P (abs x)) (Rep_small_list l)"
when I cannot mention the abstraction morphism "abs" in the equation?
Example code for this can be found on
http://stackoverflow.com/questions/16273812/working-with-isabelles-code-generator-data-refinement-and-sets
Thanks in advance,
Joachim
signature.asc
Last updated: Mar 29 2024 at 04:18 UTC