Re: [isabelle] Composable induction invariants



Hi,

Am Freitag, den 16.11.2012, 18:18 +0000 schrieb Ramana Kumar:
> 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.)

right, this is the straight-forward solution, but it does involve too
much copy’n’paste. In my case, x and f1 x y are somewhat large and
changing expressions, so just writing out these separate lammas (which
would also have to include any conditions on the induction rules) is
tedious, let alone coming up with good names for them :-)

Thanks for your input,
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.