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=
>iner:

>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=
>s.

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 MHonArc.