# [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.