[isabelle] Fwd: Composable induction invariants



(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
>>
>>
>




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