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