Stream: Beginner Questions

Topic: Shorthand for current subgoal?

view this post on Zulip Jiahong Lee (Dec 15 2022 at 06:01):

Hi, I'm proving a basic propositional theorem :

theorem "(p ⟶ (q ⟶ r)) = (p ∧ q ⟶ r)"
proof
  show "p ⟶ (q ⟶ r) ⟹ p ∧ q ⟶ r" (* <==== How to avoid typing this? *)
    by(rule thm2)
next
  show "p ∧ q ⟶ r ⟹ p ⟶ (q ⟶ r)"
    by(rule thm1)
qed

Is there a shorthand for current subgoal such that I can rewrite my proof as such?

theorem "(p ⟶ (q ⟶ r)) = (p ∧ q ⟶ r)"
proof
  show ?subgoal by(rule thm2)
next
  show ?subgoal by(rule thm1)
qed

Last updated: Dec 21 2024 at 16:20 UTC