# [isabelle] Mutually recursive coinductive predicates

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
`

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*