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



I believe that Isabelle cannot deal with data refinement involving
higher-order functions at the moment. It is an open issue both in theory and
in the implementation.

Tobias

Am 30/04/2013 10:00, schrieb Joachim Breitner:
> 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
> 




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