Re: [isabelle] Problems with code-datatype

Dear René,

Reading the manual on code-generation and "Data Refinement in Isabelle/HOL", I realized that page 109 it is mentioned that for abstract type A and concrete type C one can lift a function f :: C => (C)? => C to a function f whose type should be A => (A)? => A. So does that mean that I won't be able to define my function create_foo as essentially it is
of type C => A?

This is not quite true, as you can define

lift_definition g:: "test => no_B "
  is "% t. if t = B then A else t"
  by auto

and the code generation works fine. In terms of

lift_definition get_no_B :: "test => no_B option"
  is "% t. if t = B then None else Some t"
  by auto

I think the problem is with

get_no_B.rep_eq: map_option Rep_no_B (get_no_B ?x) = (if ?x = B then None else Some ?x)

An ideal code abstract equation for type no_B is of the form

Rep_no_B (f ...) = ...

so that code equations that preserve invariants of no_B could be derived for f. Lemma get_no_B.rep_eq does not match such format, and I guess that is why code generation fails for get_no_B (although in theory I think we can still derive code equations in such cases). Experts on data refinements should be able to comment more ;-)

Hope this helps,

Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge

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