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:
"[| !t. x:(case t of A => s1 | B => s2 | C => s3) --> P; x:s2 |] ==> P"
by(auto split: test.splits)
Peter Lammich wrote:
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