*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Composable induction invariants*From*: Joachim Breitner <breitner at kit.edu>*Date*: Fri, 16 Nov 2012 16:12:10 +0100

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

**Attachment:
signature.asc**

- Previous by Date: Re: [isabelle] Introduction rule for quantifiers over sets of pairs
- Next by Date: Re: [isabelle] Highlight sorry in jEdit
- Previous by Thread: Re: [isabelle] isabelle mailing lists
- Next by Thread: [isabelle] Fwd: 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