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.


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.