Re: [isabelle] Code generation for typedefs

Hi Peter,

> I have the following situation, analogously to RBT.thy:
> datatype 'a MyStruc  = ...
> invar :: 'a MyStruc => bool
> operation :: 'a MyStruc => (MyStruc * 'a * MyStruc)
> ...
> typedef (open) 'a My = "{ m::'a MyStruc . invar m}"
> lemma [simp, code abstype]: "Abs_My (Rep_My t) = t"
> definition operation' :: 'a My => ('a My * 'a * 'a My)
> where "operation' t == (%(a,b,c). (Abs_My a,b,Abs_my c)) operation
> (Rep_My t)"
> lemma [code abstract]: "???????"
> *** How to formulate this lemma?
> Will
>    "(%(a,b,c). (Rep_My a,b,Rep_my c)) (operation' t) == operation
> (Rep_My t)"
> work?

> My problem is, that I do not want to split "operation" into many
> functions for efficiency reasons,
> as all results of the tuple are computed simultaneously.

we have indeed no direct solution for this; as a workaround, it should
be possible to define a separate type for the result (with concrete
instead of abstract types) and declare it as abstype, together with
suitable projections to decompose this result later;  for the abstract
components, these projections return abstract types instead of concrete
ones.  An example on pairs of abstract values:

A :: r => a
R :: a => r with !x. P (R x)

Define abstype a2 with
A2 :: r * r => a2
R2 :: a2 => r * r with !x. P (fst (R2 x)) && P (snd (R2 x))

Computation f yields result of type a2 such that
R2 (f ...) = ...

Define projection R' :: a2 => r * r such that
R (R' x) = R2 x

This is as least a sketch how I thought it could work, but I have never
exercised this in practice before.

Hope this helps,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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