Email Gateway (Aug 18 2022 at 19:53): Email Gateway (Aug 18 2022 at 19:53):From: "Aaron W. Hsu" <arcfide@sacrideo.us>
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.
Email Gateway (Aug 18 2022 at 19:54):From: Tobias Nipkow <nipkow@in.tum.de>
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.
Tobias
Last updated: Apr 20 2024 at 08:16 UTC