*To*: Andreas Lochbihler <andreas.lochbihler at kit.edu>*Subject*: Re: [isabelle] Mutually recursive coinductive predicates*From*: Tambet <qtvali at gmail.com>*Date*: Tue, 27 Jul 2010 12:25:07 +0300*Cc*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <4C4D65FA.70308@kit.edu>*References*: <4C4D65FA.70308@kit.edu>

I replace ?X with function name "EO" and add some parentheses: [| EO ?x ?xa; !!x xa. EO x xa ==> ~ x & xa = 0 | (EX n. ~ x & xa = iSuc n & (EO True n | odd n)) | (EX n. x & xa = iSuc n & (EO False n | even n)) |] ==> even_odd ?x ?xa For me it seems that ?x is boolean and ?xa is number. Thus, I do the corresponding replacement (for readability, not compileability): [| EO isodd n; !!isodd n. EO isodd n ==> (~ isodd) & (n = 0) | (EX m. (~ isodd) & (n = iSuc m) & ((EO True m) | (odd m))) | (EX m. (isodd) & (n = iSuc m) & ((EO False m) | (even m))) |] ==> even_odd isodd n This ((EO True m) | (odd m)) is odd rule then, but it basically says that ((odd m+1) | (odd m)). As m+1 is n, it's also a conclusion (~(odd n - 1) ==> (EO True n)) or, in other words, (~(odd n - 1) ==> (odd n)). Tambet On 26 July 2010 13:39, Andreas Lochbihler <andreas.lochbihler at kit.edu>wrote: > Hello all, > > I am having trouble understanding the coinduction rule that the > (co)inductive package produces for mutually recursive definitions. Here's an > example: > > theory Test imports Nat_Infinity begin > > coinductive even :: "inat set" > and odd :: "inat set" > where > "even 0" > | "odd n ==> even (iSuc n)" > | "even n ==> odd (iSuc n)" > > > The only coinduction theorem I was able to find, was even_odd.coinduct, but > it looks like this: > > [| ?X ?x ?xa; > !!x xa. > ?X x xa > ==> ~ x & xa = 0 | > (EX n. ~ x & xa = iSuc n & (?X True n | odd n)) | > (EX n. x & xa = iSuc n & (?X False n | even n)) |] > ==> even_odd ?x ?xa > > Here are my troubles with this rule; > > 1. Why is there a boolean parameter x to even_odd and similarly to X? > (In case I have three mutually recursive predicates, there are even > more booleans floating around!) > > 2. How can I use this rule to ever prove anything about even or odd > (e.g. that Infty is both even and add)? > The conclusion only mentions the combined predicate even_odd. > Searching for "even" or "odd" with find_theorems does not produce any > theorems that relate even or odd with even_odd other than > even_odd.coinduct. > > Thanks in advance for any help, > > Andreas > -- > Karlsruher Institut für Technologie > IPD Snelting > > Andreas Lochbihler > wissenschaftlicher Mitarbeiter > Adenauerring 20a, Gebäude 50.41, Raum 023 > 76131 Karlsruhe > > Telefon: +49 721 608-8352 > Fax: +49 721 608-8457 > E-Mail: andreas.lochbihler at kit.edu > http://pp.info.uni-karlsruhe.de > KIT - Universität des Landes Baden-Württemberg und nationales > Großforschungszentrum in der Helmholtz-Gemeinschaft > >

**References**:**[isabelle] Mutually recursive coinductive predicates***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Finding the instantiation of a variable
- Next by Date: [isabelle] Postdoc at Uppsala University
- Previous by Thread: [isabelle] Mutually recursive coinductive predicates
- Next by Thread: [isabelle] Postdoc at Uppsala University
- Cl-isabelle-users July 2010 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