*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] coinduct_upto for coinductive predicates*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Mon, 7 Nov 2016 20:01:22 +0100*Cc*: Andrei Popescu <A.Popescu at mdx.ac.uk>*In-reply-to*: <AM3PR01MB1313214A7E11EF6FDE1308AAB7A70@AM3PR01MB1313.eurprd01.prod.exchangelabs.com>*References*: <27160336-b7c8-8f83-117b-5258ea78da6e@in.tum.de> <2eac3394-b7da-ba90-7c18-0d4ad64145a5@inf.ethz.ch> <ffdc69e0-3dae-31d8-1452-91afb1a77fa2@in.tum.de> <AM3PR01MB1313214A7E11EF6FDE1308AAB7A70@AM3PR01MB1313.eurprd01.prod.exchangelabs.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.4.0

Hallo Andrei,

lemma P_s: assumes "P xs" shows "P( g xs)" using assms apply(coinduction arbitrary: xs) by (smt P.cases embed g.code stream.sel(1) stream.sel(2))

Cheers, Manuel

**Attachment:
Bar.thy**

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

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

**Re: [isabelle] coinduct_upto for coinductive predicates***From:*Andreas Lochbihler

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

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

- Previous by Date: Re: [isabelle] coinduct_upto for coinductive predicates
- Next by Date: Re: [isabelle] coinduct_upto for coinductive predicates
- Previous by Thread: Re: [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