Re: [isabelle] Dealing with functions



Am 06/09/2012 14:05, schrieb Aaron W. Hsu:
> 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?

There needs to be some indication which induction principle is wanted. Just
giving variable names indicates structural induction. Other induction principles
would need other hints. One could imagine writing something like "sv2vl n xs ys"
to indicate that, but that would be a significant extension of induction, and it
is already too complicated as it is.

Moreover you will find that the limiting factor in writing proofs is not stating
an induction rule.

Tobias





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