[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.