Re: [isabelle] Mutual coinduction



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




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