Re: [isabelle] Code generation, abstract types and higher order function
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] Code generation, abstract types and higher order function
- From: Tobias Nipkow <nipkow at in.tum.de>
- Date: Wed, 01 May 2013 03:27:21 +0200
- In-reply-to: <1367308803.4218.13.camel@kirk>
- References: <1367308803.4218.13.camel@kirk>
- User-agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.8; rv:17.0) Gecko/20130328 Thunderbird/17.0.5
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.
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
> Thanks in advance, Joachim
This archive was generated by a fusion of
Pipermail (Mailman edition) and