Re: [isabelle] Mutually recursive coinductive predicates
I replace ?X with function name "EO" and add some parentheses:
[| EO ?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;
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
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
> theory Test imports Nat_Infinity begin
> coinductive even :: "inat set"
> and odd :: "inat set"
> "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
> Thanks in advance for any help,
> 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
> 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