Re: [isabelle] Casting records efficiently



Hi René.

it might be helpful if you could provide me with a small self-contained
example.

Cheers,
	Florian

On 03.12.2013 18:27, René Neumann wrote:
> 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
> constants).
> 
> 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é
> 

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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