*To*: <Thomas.Sternagel at uibk.ac.at>*Subject*: Re: [isabelle] Mutual coinduction*From*: Dmitriy Traytel <traytel at inf.ethz.ch>*Date*: Mon, 26 Sep 2016 15:28:07 +0200*Cc*: Isabelle Users <isabelle-users at cl.cam.ac.uk>

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

**Follow-Ups**:**Re: [isabelle] Mutual coinduction***From:*Thomas Sternagel

- Previous by Date: Re: [isabelle] Tactic failed for Friends
- Next by Date: Re: [isabelle] Mutual coinduction
- Previous by Thread: [isabelle] Mutual coinduction
- Next by Thread: Re: [isabelle] Mutual coinduction
- Cl-isabelle-users September 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list