Re: [isabelle] Dealing with functions
Tobias Nipkow <nipkow at in.tum.de> writes:
>Because fun generates the right induction principle, the proof is a one-l=
>by (induct n xs ys rule: sv2vl.induct) auto
>See the documentation (eg Tutorial on Function Definitions or the new
>Programming and Proving tutorial) for more info.
>Of course you can also use this induction rule in more verbose Isar proof=
Thanks so much! I took a look at the documentation in question and
that clears things up, though I do not understand why the explicit
"rule" part is necessary. Why would it not automatically choose that
rule? Do you normally want the other induction rules instead of this
one in proofs?
Aaron W. Hsu | arcfide at sacrideo.us | http://www.sacrideo.us
Programming is just another word for the lost art of thinking.
This archive was generated by a fusion of
Pipermail (Mailman edition) and