*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*: Wed, 9 Nov 2016 19:07:14 +0000*Accept-language*: en-GB, en-US*Authentication-results*: spf=none (sender IP is ) smtp.mailfrom=A.Popescu@mdx.ac.uk;*In-reply-to*: <ebc169a5-2315-336a-b200-16f91e6fff6c@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> <AM3PR01MB1313214A7E11EF6FDE1308AAB7A70@AM3PR01MB1313.eurprd01.prod.exchangelabs.com> <8155fe9a-4580-292f-810b-3e83ea583b21@in.tum.de> <AM3PR01MB1313820C90F620B12AE2E7ACB7A70@AM3PR01MB1313.eurprd01.prod.exchangelabs.com>, <ebc169a5-2315-336a-b200-16f91e6fff6c@in.tum.de>*Spamdiagnosticmetadata*: NSPM*Spamdiagnosticoutput*: 1:99*Thread-index*: AQHSONz1o/SKReAAJ0euxqjLWbQVXaDNZHMAgABc0ICAABlCEoAABmkAgAAHgqiAAQErAIACGN1K*Thread-topic*: [isabelle] coinduct_upto for coinductive predicates

Hi Manuel, I am sorry for the headache. But since you've come this far, I suggest giving the proof reuse idea another chance (at some point). :-) Here is what my previously stated facts (1)-(3) become for your simple example (theory also attached). The only considered operation here is g, but the closure can potentially have any set of operations (including the constant s). Notice how (3) is the mother of all interesting facts -- and how everything else is absolute routine. Looking into what most people call "the low level", e.g., the operators behind (co)inductive definitions, can be rewarding for reducing proof complexity. theory Test imports Main "~~/src/HOL/Library/BNF_Corec" "~~/src/HOL/Library/Stream" begin coinductive P :: "int stream ? bool" where "P xs ? x ? 0 ? P (x ## xs)" definition F :: "(int stream ? bool) ? int stream ? bool" where "F X xs ? ?xs' x. xs = x ## xs' ? X xs' ? x ? 0" lemma F_mono: "mono F" unfolding mono_def F_def by blast (* Note: *) lemma P: "P = gfp F" unfolding HOL.nitpick_unfold F_def .. corec (friend) g :: "int stream ? int stream" where "g x = (shd x + 1) ## g (stl x)" inductive g_closure :: "(int stream ? bool) ? int stream ? bool" for X where embed: "X xs ? g_closure X xs" |step: "g_closure X xs ? g_closure X (g xs)" (* The following three facts are all trivial: *) lemma g_closure_mono: assumes "X ? Y" shows "g_closure X ? g_closure Y" proof fix xs assume "g_closure X xs" thus "g_closure Y xs" using assms by (induct) (auto intro: g_closure.intros) qed lemma g_closure_ext: "X ? g_closure X" by (auto intro: embed) lemma g_closure_idem: "g_closure (g_closure X) = g_closure X" proof- {fix xs assume "g_closure (g_closure X) xs" hence "g_closure X xs" by (induction) (auto intro: g_closure.intros) } thus ?thesis by (simp add: antisym g_closure_ext predicate1I) qed (* The *only* non-routine fact: *) lemma 3: "g_closure (F X) ? F (g_closure X)" proof clarify fix xs assume "g_closure (F X) xs" thus "F (g_closure X) xs" apply induct using F_def embed apply auto[1] by (smt F_def g.code g_closure.step stream.sel) qed lemma 1: (* Follows routinely from 3 *) assumes "X ? F (g_closure X)" shows "X ? gfp F" proof- note g_closure_mono[OF assms] also have "g_closure (F (g_closure X)) ? F (g_closure (g_closure X))" using 3 by simp also have "... = F (g_closure X)" unfolding g_closure_idem .. finally have "g_closure X ? F (g_closure X)" . with gfp_upperbound have "g_closure X ? gfp F" by auto thus ?thesis by(auto intro: g_closure.intros) qed lemma P_coinduct_upto_g: (* is just the concrete version on 1 *) assumes *: "X xs" and step: "?xs. X xs ? ?xs' x. xs = x ## xs' ? g_closure X xs' ? x ? 0" shows "P xs" using 1 assms unfolding P F_def using predicate1I by blast (* Follows routinely from 1 and 3: *) lemma g_closure_P: "g_closure P ? P" unfolding P apply(rule 1) unfolding g_closure_idem apply(subst gfp_unfold[OF F_mono]) using 3 . (* An immediate consequence of g_closure_P *) lemma 2: "P xs ? P (g xs)" using g_closure_P by (auto intro: g_closure.intros) end Andrei ________________________________ From: Manuel Eberl <eberlm at in.tum.de> Sent: 08 November 2016 10:48 To: Andrei Popescu; cl-isabelle-users at lists.cam.ac.uk Subject: Re: [isabelle] coinduct_upto for coinductive predicates I think this probably answers my question. I have decided not to look into this any further at the moment, seeing as 1. it gives me a headache, 2. I have working proofs for now and 3. I'm quite eager to continue my formalisation elsewhere. Thanks a lot for your help (also to Andreas). I still have no idea what I actually did with these closures, but the proofs went relatively smoothly and everything works out. Cheers, Manuel

**Attachment:
Test.thy**

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

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

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

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

- Previous by Date: Re: [isabelle] Isabelle2016-1-RC1 processing theories twice
- Next by Date: [isabelle] Turning on tracing for mode inference?
- Previous by Thread: Re: [isabelle] coinduct_upto for coinductive predicates
- Next by Thread: [isabelle] Isabelle2016-1-RC1 sledgehammer "Try this: by presburger" fails
- 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