*To*: Manuel Eberl <eberlm at in.tum.de>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] coinduct_upto for coinductive predicates*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Mon, 7 Nov 2016 12:35:50 +0100*In-reply-to*: <27160336-b7c8-8f83-117b-5258ea78da6e@in.tum.de>*References*: <27160336-b7c8-8f83-117b-5258ea78da6e@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.4.0

Hi Manuel,

inductive g_closure :: "(int stream â bool) â int stream â bool" for P where embed: "P xs â g_closure P xs" | step: "g_closure P xs â g_closure P (g xs)" lemma P_coinduct_upto_g: assumes *: "X xs" and step: "âxs. X xs â âx xs'. xs = x ## xs' â g_closure X xs' â 0 â x" shows "P xs" proof - from * have "g_closure X xs" by(rule g_closure.intros) then show ?thesis proof(coinduction arbitrary: xs) case (P xs) then have "âx xs'. xs = x ## xs' â g_closure X xs' â 0 â x" proof induction case (embed xs) from step[OF embed] show ?case by(auto) next case (step xs) then show ?case by(subst g.code)(auto intro: g_closure.step) qed then show ?case by blast qed qed A few more comments:

from * have "g_closure X xs" by(rule g_closure.intros) with from * have "g_closure (%xs. X xs \/ P xs) xs" by(rule g_closure.intros) and adjust the proof accordingly.

lemma P_coinduct_upto_g: assumes *: "X xs" and step: "âxs. X xs â g_closure (%xs. âx xs'. xs = x ## xs' â g_closure X xs' â 0 â x) xs" shows "P xs" You can derive that one from mine above by another induction. Hope this helps, Andreas On 07/11/16 10:52, Manuel Eberl wrote:

Hallo, I have a coinductive predicate P and I want to show that "P s" holds, where "s" is a corecursively-defined stream whose definition uses a friendly function, i.e. something like "s = 0 ## g s" where g is friendly. (see also attached theory) The problem is that P.coinduct then only allows me to use "P s" in the coinduction proof, but I need "P (g s)". I suppose what I really need here is something like "coinduction up to friends for coinductive predicates"; from what I read, something like this is already available for "normal" coinduction w.r.t. equality. How do I do something like this? (my actual coinductive predicate is, of course, much more complicated than this, so working with "normal" coinduction w.r.t. equality is not an option) Cheers, Manuel

**Follow-Ups**:**Re: [isabelle] coinduct_upto for coinductive predicates***From:*Andrei Popescu

**Re: [isabelle] coinduct_upto for coinductive predicates***From:*Manuel Eberl

**References**:**[isabelle] coinduct_upto for coinductive predicates***From:*Manuel Eberl

- Previous by Date: [isabelle] coinduct_upto for coinductive predicates
- Next by Date: Re: [isabelle] yet another simplifier question
- Previous by Thread: [isabelle] coinduct_upto for coinductive predicates
- Next by Thread: Re: [isabelle] coinduct_upto for coinductive predicates
- Cl-isabelle-users November 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