[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 [0] and has an empty Map, Scalar is an 
array of shape [] with a map [[] mapto x], and Array s m is the general 
Array constructor.

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