Email Gateway (Aug 18 2022 at 19:22): Email Gateway (Aug 18 2022 at 19:22):From: charmi panchal <charmipanchal2006@gmail.com>
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
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 18 2022 at 19:22):From: Tobias Nipkow <nipkow@in.tum.de>
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
Email Gateway (Aug 18 2022 at 19:22):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Dear Tobias,
Interesting! Will it be an update of "isabelle doc tutorial" or
something entirely new? I'd be happy to look through any draft version
of such a document.
cheers
chris
Last updated: Nov 21 2024 at 12:39 UTC