# [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
```

```

• Follow-Ups:

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