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
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