[isabelle] Defining Cases for your own custom Datatypes
I am building a type that does not use Datatype. I would like to be able to
do a cases statement on it for some of the constructors that I have made,
but it is not clear to me how best to do this? What theorems do I need to
prove to enable a Case statement to work? Specifically, I have arrays, and I
want to be able to do something like:
case A of
Empty => ... |
Scalar x => ... |
Array s m => ...
Where Empty is an array of shape  and has an empty Map, Scalar is an
array of shape  with a map [ mapto x], and Array s m is the general
I have Empty, Scalar and Array defined, but I am finding that it is really
annoying trying to get the appropriate elements s, m, and x out of the input
without a case construct, and I do not like writing all the if then
statements to dispatch on the type of array I have. I think my proofs would
be much easier if I could have some sort of case thing going on.
I am not using Datatype because the general Array constructor must have a
specific, constrained relationship between map and shape.
Aaron W. Hsu | arcfide at sacrideo.us | http://www.sacrideo.us
Programming is just another word for the lost art of thinking.
This archive was generated by a fusion of
Pipermail (Mailman edition) and