Re: [isabelle] Composable induction invariants



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
>




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.