*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*: Andrei Popescu <A.Popescu at mdx.ac.uk>*Date*: Mon, 7 Nov 2016 18:47:35 +0000*Accept-language*: en-GB, en-US*Authentication-results*: spf=none (sender IP is ) smtp.mailfrom=A.Popescu@mdx.ac.uk;*Cc*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*In-reply-to*: <ffdc69e0-3dae-31d8-1452-91afb1a77fa2@in.tum.de>*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>*Spamdiagnosticmetadata*: NSPM*Spamdiagnosticoutput*: 1:99*Thread-index*: AQHSONz1o/SKReAAJ0euxqjLWbQVXaDNZHMAgABc0ICAABlCEg==*Thread-topic*: [isabelle] coinduct_upto for coinductive predicates

Hi Manuel, You can use Andreas's rule to prove that fact for any xs: lemma P_s: assumes "P xs" shows "P( g xs)" using assms apply(coinduction arbitrary: xs rule: P_coinduct_upto_g) by (smt P.cases embed g.code stream.sel(1) stream.sel(2)) (and, of course, you can also use it to immediately prove P(s), your original motivation) Andrei ________________________________ From: cl-isabelle-users-bounces at lists.cam.ac.uk <cl-isabelle-users-bounces at lists.cam.ac.uk> on behalf of Manuel Eberl <eberlm at in.tum.de> Sent: 07 November 2016 17:08 To: cl-isabelle-users at lists.cam.ac.uk Cc: Andreas Lochbihler Subject: Re: [isabelle] coinduct_upto for coinductive predicates Hallo, thanks for the explanation. I think I now managed to define the closure that I need and prove the corresponding coinduct_upto rule. I noticed that during the proof of this rule, I essentially needed to prove that all the friendly functions in the closure preserve the inductive predicate, i.e. in terms of the example theory from earlier, I needed to prove some generalised version of "P s ==> P (g s)". I then thought that once I have proven the coinduct_upto rule, I should be able to easily derive the fact "P s ==> P (g s)" from that, but I cannot see how. If I want to prove "P s ==> P (g s)", do I really have to do all the proof work again? Cheers, Manuel

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

**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

- Previous by Date: Re: [isabelle] Isabelle2016-1-RC2 cartouche vs quotation mark ML_file
- 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