Re: [isabelle] Defining Cases for your own custom Datatypes

If your type *behaves* like a datatype, then you can tunr it into a datatype via
the rep_datatype command. See the Isar Reference manual. A typical example is in
Nat.thy: nat is not defined via datatype but behaves like one. But beware that
you will have to prove all the properties expected from a datatype: injectivity
and distinctness of the constructors and the induction rule.


Am 22/05/2012 22:52, schrieb Aaron W. Hsu:
> 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.

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