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

I see... no obvious tricks are coming to my mind, but that doesn't mean there aren't any. Your approach to define a relation that carries the P around seems pretty good. One other approach would be to prove the three theorems you want to prove only once as separate lemmas independent of any induction. I.e., prove P x ==> P (f1 x y) (and add whatever extra hypotheses are necessary, which will always be provided in an induction context) as a standalone lemma, then use it whenever you need. (And similarly for the other two.) On Fri, Nov 16, 2012 at 5:34 PM, Joachim Breitner <breitner at kit.edu> wrote: > Dear Ramana, > > Am Freitag, den 16.11.2012, 17:19 +0000 schrieb Ramana Kumar: > > 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. > > Isabelle’s induct method already provides me "f1 x y ⇓ f2 x y", and I > can use this to prove what I need, but not without repeating the proofs > that I have done already inside P_preserves and using P_preserves > itself. > > I think one approach that does not involve too much copy’n’paste (but > still some would be this: I start with the normal inductive definition: > > f1 x y ⇓ f2 x y ; f3 x y ⇓ f4 x y > _____ _________________________________ > x ⇓ x x ⇓ y > > Then i copy’n’paste it to create a stronger version: > > P x f1 x y ⇓ f2 x y ; f3 x y ⇓ f4 x y; > P x; P y; P (f1 xy); P (f2 x y); > P (f3 x y; P (f4, x y) > ______ _________________________________ > x ⇓' x x ⇓' y > > An easy consequence will be: > x ⇓' y ==> P x &&& P y > > Now I prove this lemma: > x ⇓ y ==> P x ==> x ⇓' y > by induction over the definition of ⇓. In this proof, I will have to do > the steps that I want to avoid doing more than once, e.g. > P x ==> P (f1 x y) > P (f2 x y) ==> P (f3 x y) > P (f3 x y) ==> P y > > The lemma P_preserved is now an easy consequence of the the previous > two lemmas. > > Now to prove > Q_preserved: x ⇓ y ==> Q x ==> P x ==> P y > I first obtain x ⇓' y and then prove > x ⇓' y ==> Q y > by induction over ⇓'. At this point, Isabelle’s induct method will allow > me to assume all the "P something" statements that I need in the > inductive steps. > > > Disclaimer: I have not implemented this yet (currently, I have just > copied the proofs), but I guess I will before I copy them the second or > third time. > > Greetings, > Joachim > > -- > Dipl.-Math. Dipl.-Inform. Joachim Breitner > Wissenschaftlicher Mitarbeiter > http://pp.info.uni-karlsruhe.de/~breitner >

**Follow-Ups**:**Re: [isabelle] Composable induction invariants***From:*Joachim Breitner

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

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

- Previous by Date: Re: [isabelle] Composable induction invariants
- Next by Date: Re: [isabelle] Composable induction invariants
- Previous by Thread: Re: [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