[isabelle] Casting records efficiently

Dear all,

when given a record hierarchy (let's take 'foo' and 'foo_bar', where
'foo_bar' extends 'foo'), I couldn't find a good way to "cast" a record
of type foo into one of type foo_bar, s.t. the construct is executable
(the additional fields of 'foo_bar' are going to be initialized with

I.e. I need a function "cast :: foo ⇒ foo_bar" or more generally
"cast :: 'a foo_scheme ⇒ 'b foo_scheme"

First attempt (not executable):

cast g = foo.extend g (foo_bar.fields arg1 arg2)

Second attempt (wrong type -- g here already needs to be of type foo_bar):

cast g = g(| arg1 := arg1, arg2 := arg2 |)

Third attempt (parsing error):

cast g = g(| … := (| arg1 = arg1, arg2 = arg2 |)|)

Fourth attempt (wrong type -- see 2nd):

cast g = foo.more_update (λ_. (| arg1 = arg1, arg2 = arg2 |)) g

Fifth attempt (working, but very clumsy):

function cast where
 "cast (| foo_1 = x1, foo_2 = x2, foo_3 = x3 |) = (| foo_1 = x1, foo_2 =
x2, foo_3 = x3, arg1 = arg1, arg2 = arg2 |)"
by (metis foo.cases) (metis foo.ext_inject)
termination by lexicographic_order

Is there some better alternative for this? Where I am not forced to
spell out all fields of 'foo', and proof trivial obligations?

Thanks a lot,

René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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