[isabelle] Splitting case-expressions automatically



Hi all,

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







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