Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Code generation, abstract types and higher ord...


view this post on Zulip Email Gateway (Aug 19 2022 at 10:49):

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:

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