Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Mutually recursive coinductive predicates

Email Gateway (Aug 18 2022 at 15:45):

From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
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

Email Gateway (Aug 18 2022 at 15:45):

From: Tambet <qtvali@gmail.com>
I replace ?X with function name "EO" and add some parentheses:

[| EO ?x ?xa;
!!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;
!!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
n)).

Tambet

Last updated: Nov 21 2024 at 12:39 UTC