# Re: [isabelle] Induction over n for a proposition ALL k <= n

I don't think there are hard and fast rules. Nesting is certainly not a
crime. I try to avoid auxiliary lemmas and split a proof up only if it
becomes too long or too indented.
Tobias
Am 27/12/2011 23:12, schrieb Lars Hupel:
>> I think you need less_induct, induction where you can assume the
>> property holds for all smaller values. It is used like this:
>> (induction k arbitrary: i rule: less_induct).
>
> Thanks, that worked. Now I have a question regarding the recommended
> style: Is it better to make a proof without `less_induct` but rather
> with an explicit premise and then prove the proposition as a corollary
> using
>
> by
> (induct n arbitrary: i nt rule: less_induct)
> (fact cyk_correct_helper)
>
> or by stating it as a single theorem, where the structure would look like
>
> proof (induct n arbitrary: i nt rule: less_induct)
> case (less n' i nt)
> thus ?case
> proof (cases n')
> case 0
> thus ?thesis sorry
> next
> case (Suc n)
> thus ?thesis sorry
> qed
> qed
>
> The more general question is whether it is good style to nest case
> distinction proofs.
>

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