Re: [isabelle] Mutual coinduction



Hi Tom,

I fear that currently neither coinduct nor coinduction work properly with mutually coinductive predicates. Thus, in your example I would just use rule (+ goal_cases for the case names).

Note that few weeks ago the coinductive was generating a different (non-mutual) rule, that was exposing the internal construction (see NEWS). In your example this old rule looked like:

?X ?x ?xa â
(âx xa. ?X x xa â
         (ân. Â x â xa = Suc n â (?X True n â n â Y)) â
         (ân. x â xa = Suc n â (?X False n â n â X))) â
Xp_Yp ?x ?xa

This rule may have worked better with coinduct(ion), but getting from Xp_Yp to X and Y was tedious in turn.

When I changed coinductive to produce the new rule, I havenât seen any uses of mutually coinductive predicates in isabelle + AFP. Is your use-case a new development, or is it one that used to work with the old rule?

Cheers,
Dmitriy

> On 26 Sep 2016, at 13:01, Thomas Sternagel <Thomas.Sternagel at uibk.ac.at> wrote:
> 
> Dear List,
> 
> I'm trying to figure out mutual coinduction in a development version of
> Isabelle/HOL (d4b89572ae71). In particular I want to use the coinduction
> scheme for two sets defined by mutual coinduction, but I'm not even able
> to formulate my goal in a way that I can use 'coinduct'.
> Consider the following minimal example:
> 
> theory Tmp
> imports
>   Main
> begin
> 
> coinductive_set X and Y where
>   "n â Y â Suc n â X"
> | "n â X â Suc n â Y"
> 
> lemma tmp:
>   shows "(âx. P x â x â X) â (âx. Q x â x â Y)"
> proof (coinduct rule: X_Y.coinduct)
> sorry
> 
> end
> 
> In the first line of the proof of lemma 'tmp' the following exception is
> raised
> 
> exception TERM raised (line 80 of "Isar/rule_cases.ML"):
>   Expected 2 binop arguments
>   ân. B.0 = Suc n â (Q n â n â Y)
> 
> What am I doing wrong? What is 'B.0'? I don't understand what's
> happening here.
> 
> Tom




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.