[isabelle] Code generation for typedefs



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






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