*To*: Dmitriy Traytel <traytel at inf.ethz.ch>*Subject*: Re: [isabelle] Mutual coinduction*From*: Thomas Sternagel <Thomas.Sternagel at uibk.ac.at>*Date*: Mon, 26 Sep 2016 15:40:10 +0200*Cc*: Isabelle Users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <0B9F2600-D4FB-4CD2-98E9-68B7B8FE7552@inf.ethz.ch>*References*: <0B9F2600-D4FB-4CD2-98E9-68B7B8FE7552@inf.ethz.ch>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.3.0

Its a new development. Actually, I started with Isabelle/HOL 2016 where I encountered the 'old' rule you describe below, but could also not figure out how to use it, so I switched to development version d4b89572ae71, because the coinduction scheme looked more promising there. Thanks for the information, anyway. On 09/26/2016 03:28 PM, Dmitriy Traytel wrote: > 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

**References**:**Re: [isabelle] Mutual coinduction***From:*Dmitriy Traytel

- Previous by Date: Re: [isabelle] Mutual coinduction
- Next by Date: [isabelle] Open Ph.D. position in Formal Methods for Information Security at ETH Zurich
- Previous by Thread: Re: [isabelle] Mutual coinduction
- Next by Thread: [isabelle] Tactic failed for Friends
- 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