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

> 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

  (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
    case (Suc n)
    thus ?thesis sorry

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.