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