Re: [isabelle] Composable induction invariants



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

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



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