[isabelle] Mutually recursive coinductive predicates
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"
| "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 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
Thanks in advance for any help,
Karlsruher Institut für Technologie
Adenauerring 20a, Gebäude 50.41, Raum 023
Telefon: +49 721 608-8352
Fax: +49 721 608-8457
E-Mail: andreas.lochbihler at kit.edu
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