*To*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] Fwd: Composable induction invariants*From*: Ramana Kumar <rk436 at cam.ac.uk>*Date*: Fri, 16 Nov 2012 17:20:36 +0000*In-reply-to*: <CAMej=24UThyitFyNqVsPN=TA-sqXQT-0Hfrr1ss+8bRAXyhzuw@mail.gmail.com>*References*: <1353078730.4051.16.camel@kirk> <CAMej=24Q8H5tWUL30NpNyaUatOQ5VKcbUiObMs5yfgnKMzcxiQ@mail.gmail.com> <CAMej=24UThyitFyNqVsPN=TA-sqXQT-0Hfrr1ss+8bRAXyhzuw@mail.gmail.com>*Sender*: ramana.kumar at gmail.com

(forwarding to list because I used the wrong email address) ---------- Forwarded message ---------- From: Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> Date: Fri, Nov 16, 2012 at 5:19 PM Subject: Re: [isabelle] Composable induction invariants To: Joachim Breitner <breitner at kit.edu> Cc: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk> Sorry, I meant the strong induction would give you: f1 x y ⇓ f2 x y in addition to Q (f1 x y) ==> Q (f2 x y) as hypotheses when trying to prove Q x ==> Q y in the inductive case. On Fri, Nov 16, 2012 at 5:16 PM, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>wrote: > I presume for Q_preserved the last consequent should be Q y rather than P > y? > > One approach is to use what in HOL4 we call a "strong" induction > principle, which gives you x ⇓ y as an induction hypothesis when trying to > prove Q (f1 x y) etc. Then you can apply your existing P_preserved theorem > to that. Would that give you everything you need? > > I think you can prove the strong induction from the induction Isabelle > automatically generates (although perhaps not just "by induction"). > > > > On Fri, Nov 16, 2012 at 3:12 PM, Joachim Breitner <breitner at kit.edu>wrote: > >> Dear List, >> >> I am stumbling over a pattern here that requires me to do duplicate a >> lot of proofs, and wondering if there there is a better approach. >> >> Say I have an inductive predicate defined like this: >> _____ >> x ⇓ x >> >> and >> >> f1 x y ⇓ f2 x y ; f3 x y ⇓ f4 x y >> ______ >> x ⇓ y >> >> and a predicate P on the x’s and y’s that for which I have proven >> P_preserved: x ⇓ y ==> P x ==> P y >> by showing (in the context opened by the induction method) >> P x ==> P (f1 x y) >> P (f2 x y) ==> P (f3 x y) >> P (f3 x y) ==> P y >> >> Next, I need to to prove that another predicate Q is preserved, at least >> when P holds: >> Q_preserved: x ⇓ y ==> Q x ==> P x ==> P y >> In this proof, to actually use the induction hypotheses, I again will >> have to show >> P x ==> P (f1 x y), >> will have to invoke P_preserved with >> f1 x y ⇓ f2 x y &&& P (f1 x y) >> and then, again, have to show >> P (f2 x y) ==> P (f3 x y) >> for the second induction hypothesis. >> >> Is there a pattern that would simplify this a bit? Ideally, in the >> induction proof for Q, the method will provide me with >> P x, P (f1 x y), P(f2 x y), P (f3 x y), P (f4 x y), P y >> as induction premises. And preferably something more automatic than >> stating the three implications in the proof of P_preserved as separate >> named lemmas before proving them. >> >> I know that it is not possible to derive that just from P_preserved. >> Maybe the inductive command could generate a definition that captures >> the notion of a predicate that, if it holds for one judgment, it holds >> for all judgments occurring along the derivation tree, and then the >> induct method could be made to use "hold_along_derivation_tree P" to >> inject the necessary premises at each step. >> >> >> Thanks, >> Joachim >> >> -- >> Dipl.-Math. Dipl.-Inform. Joachim Breitner >> Wissenschaftlicher Mitarbeiter >> http://pp.info.uni-karlsruhe.de/~breitner >> >> >

**References**:**[isabelle] Composable induction invariants***From:*Joachim Breitner

- Previous by Date: Re: [isabelle] Highlight sorry in jEdit
- Next by Date: Re: [isabelle] Composable induction invariants
- Previous by Thread: [isabelle] Composable induction invariants
- Next by Thread: Re: [isabelle] Composable induction invariants
- Cl-isabelle-users November 2012 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