[isabelle] Composable induction invariants

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


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.


Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

Attachment: signature.asc
Description: This is a digitally signed message part

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