Re: [isabelle] Problems with code-datatype
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
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"
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"
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,
University of Cambridge
This archive was generated by a fusion of
Pipermail (Mailman edition) and