[isabelle] Splitting case-expressions automatically
given the following datatype
datatype test = A | B | C
how can I prove the following subgoal automatically with one (or a few)
apply statements. I want to avoid to make the proof explicit in Isar,
because of the writing overhead.
"[| !!t. x:(case t of A => s1 | B => s2 | C => s3) ==> P; x:s2 |] ==> P"
something like (auto split: test.splits) does not work, am I missing
some lemmas or is there a way to explicitly instantiating t ?
Thanks for any hints in advance,
This archive was generated by a fusion of
Pipermail (Mailman edition) and