[isabelle] one function for two datatypes

Hi all,

Let's say I have two datatypes:

datatype 't t1 = C1a 't | C1b 't option

datatype 't t2 = C2a 't | C2b 't option

Then let's say that for a common 'y type, I have two elements e1 of type 'y t1  and e2 of type 'y t2.

let us finally say there is a value v such that e1 = C1a v and e2 = C2a v.

How could I define a "getval" function such that getval e1 = getval e2 is a admissible expression ? What type would it have ? It sounds like Java overloading, but I do not reckon there is such a thing in Isabelle, am I wrong ?

Secondly, is there any way I could say that some element e, which type could be either t1 or t2, is such that getval e = Some v, without having to say wether C1b or C2b was used to define it ?

Thanks in advance !

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