Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Unexpected fact naming in induction tactic


view this post on Zulip Email Gateway (Aug 23 2022 at 08:40):

From: Dominique Unruh <unruh@ut.ee>
Hi,

when using "proof induction", I can use "case XXX" to refer to start
proving a specific case. All facts in this case are then available under
the name XXX, and the induction hypothesis under the name XXX.IH.

However, if my lemma contains == instead of = in the assumptions, then
the induction method still works, and the name XXX still contains all
facts, but XXX.IH is not defined.

This is illustrated by the attached theory (works with Isabelle2019 and
Isabelle2020-RC1).

Is this expected behavior? If so, what is the rationale?

Best wishes,
Dominique.
Scratch.thy


Last updated: Mar 29 2024 at 08:18 UTC