*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] case-split in inductive spoils monotonicity*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Mon, 21 May 2012 11:59:13 +0200*In-reply-to*: <A26C7A82-DDFE-4CA0-9DEC-9C454360A117@cam.ac.uk>*References*: <A26C7A82-DDFE-4CA0-9DEC-9C454360A117@cam.ac.uk>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:12.0) Gecko/20120428 Thunderbird/12.0.1

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

**References**:**[isabelle] case-split in inductive spoils monotonicity***From:*John Wickerson

- Previous by Date: [isabelle] case-split in inductive spoils monotonicity
- Next by Date: [isabelle] Definition in jEdit
- Previous by Thread: [isabelle] case-split in inductive spoils monotonicity
- Next by Thread: [isabelle] Definition in jEdit
- Cl-isabelle-users May 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list