Re: [isabelle] Mutually recursive coinductive predicates



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

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