# [isabelle] case-split in inductive spoils monotonicity

Dear Isabelle,
I have three mutually recursive datatypes (diagram, comnode and assnode), and three mutually inductive predicates:
inductive
coms_dia :: "[diagram, command] => bool" and
coms_ass :: "[assnode, command] => bool" and
coms_com :: "[comnode, command] => bool"
I want the third of these inductive predicates to be defined like so (sorry for all the unreadable \<...> symbols):
"[|
\<pi> \<in> lins (Graph V \<Lambda> E);
!!i. i < length \<pi> ==> (case (\<pi>!i) of
Inl v => coms_ass (\<Lambda> v) |
Inr e => coms_com (snd3 e) ) (cs!i)
|] ==>
coms_dia (Graph V \<Lambda> E) (foldl (op ;;) Skip cs)"
That is, I refer to coms_ass and coms_com inside a case-split. Unfortunately, the proof of monotonicity fails. So I remove the case-split, using Projl and Projr, like so:
"[| \<pi> \<in> lins (Graph V \<Lambda> E);
!!i. [| i<length \<pi> ; \<exists>v. (\<pi>!i) = Inl v |] ==>
coms_ass (\<Lambda> (Projl (\<pi>!i))) (cs!i) ;
!!i. [| i<length \<pi> ; \<exists>e. (\<pi>!i) = Inr e |] ==>
coms_com (snd3 (Projr (\<pi>!i))) (cs!i) |]
==>
coms_dia (Graph V \<Lambda> E) (foldl (op ;;) Skip cs)"
And now the proof of monotonicity succeeds. But the first one seemed, morally, perfectly monotonic to me. How can I convince Isabelle to accept my original definition?
Thanks very much.
John

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