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