Re: [isabelle] Splitting case-expressions automatically

The problem are the deeply nested meta-logical symbols that the split facility seems unable to cope with. If you reformulate it a bit, it works:

lemma [rule_format]:
"[| !t. x:(case t of A => s1 | B => s2 | C => s3) --> P; x:s2 |] ==> P"
by(auto split: test.splits)


Peter Lammich wrote:
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,

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