Re: [isabelle] case-split in inductive spoils monotonicity



You should be able prove some monotonicity lemma for "case" and tell inductive
about it - see the "mono" atribute in the Isar reference manual. But unless you
need this frequently, chances are that you will spend more time getting this
right than if you just worked with your alternative definition.

Tobias

Am 21/05/2012 11:43, schrieb John Wickerson:
> 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.