[isabelle] Code generation, abstract types and higher order function



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

-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



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