Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Code generation for typedefs


view this post on Zulip Email Gateway (Aug 18 2022 at 15:57):

From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi all

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.

Best,
Peter

view this post on Zulip Email Gateway (Aug 18 2022 at 15:57):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Peter,

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,
Florian
signature.asc


Last updated: Mar 28 2024 at 12:29 UTC