Email Gateway (Aug 18 2022 at 11:35): Email Gateway (Aug 18 2022 at 11:35):From: Tobias Nipkow <nipkow@in.tum.de>
The following (not widely advertised) feature may help. You can always
refer to subgoals i by "case goal<i>", which sets ?case to the actual
subgoal. Here is a (bad!) example:
lemma "P & Q"
proof(rule conjI)
case goal1
show ?case sorry
next
case goal2
show ?case sorry
qed
?case stands for P/Q in subgoal 1/2.
This feature does not yield readable proofs but helps in situations like
you describe.
Tobias
David Streader schrieb:
Email Gateway (Aug 18 2022 at 11:35):From: Makarius <makarius@sketis.net>
Maybe you just need the ?thesis abbreviation, which always refers to the
conclusion of the last goal statement in the text (not the proof state!).
Makarius
Last updated: Nov 21 2024 at 12:39 UTC