Re: [isabelle] Casting records efficiently



Just noticed: The same problem exists for the other direction:
foo.truncate is also not executable.

- René


Am 03.12.2013 18:27, schrieb René Neumann:
> 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é
> 


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