Re: [isabelle] [isabelle-dev] Difference between " induct " and " induct_tac "



The fact that induct_tac fails already indictates that you had better not use
it. It is less friendly and is required only if you want to induct on a variable
that the system has introduced during your proof. But such proofs (long chains
of applys) are best avoided in the first place.

So why does the Isabelle/HOL tutorial still advertise induct_tac? A historical
relic. A better tutorial will be ready very soon.

Please do not post to isabelle-dev unless you feel you are a developer or need
the help of a developer. Your question is a typical user question.

Tobias

Am 27/03/2012 10:14, schrieb charmi panchal:
> Hello,
> I am a beginner of Isabelle and practicing it  in JEdit.  I wish to understand
> the difference between "induct" and "induct_tac"
> e.g.
> 
> lemma zip1_zip2: "(zip1 xs ys) = (zip2 xs ys)"
>   apply (induct xs arbitrary: ys)
>   apply (case_tac ys)
>   apply auto
>   apply (case_tac ys)
>   apply auto
>   done
> 
> it shows error when induct_tac is used.
> 
> Thanks in advance,
> Charmi Panchal
> 
> 
> This body part will be downloaded on demand.





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