Email Gateway (Aug 18 2022 at 19:50): Email Gateway (Aug 18 2022 at 19:50):From: John Wickerson <jpw48@cam.ac.uk>
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
Email Gateway (Aug 18 2022 at 19:50):From: Tobias Nipkow <nipkow@in.tum.de>
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
Last updated: Apr 20 2024 at 12:26 UTC