Stream: Beginner Questions

Topic: ✔ Shorthand for current subgoal?

Johannes Neubrand (Dec 15 2022 at 07:33):

You can use something like:

lemma
  assumes "A ⟹ B" and "B ⟹ A"
  shows "A = B"
proof (standard, goal_cases)
  case 1
  then show ?case by (rule assms(1))
next
  case 2
  then show ?case by (rule assms(2))
qed

Jiahong Lee (Dec 15 2022 at 08:03):

Hmm, that's not quite what I'm looking for.

Jiahong Lee (Dec 15 2022 at 08:05):

My current best solution is

theorem "(p ⟶ (q ⟶ r)) = (p ∧ q ⟶ r)" (is "?A = ?B")
proof
  show "?A ⟹ ?B" by(rule thm2)
next
  show "?B ⟹ ?A" by(rule thm1)
qed

Jiahong Lee (Dec 15 2022 at 08:05):

That's good enough for now, thanks!

Notification Bot (Dec 15 2022 at 08:05):

Jiahong Lee has marked this topic as resolved.

Manuel Eberl (Dec 16 2022 at 09:30):

It is generally discouraged to have meta-level connectives appearing in have/show statements. You should either do assume ?A … show ?B or something like show ?B if ?A. I mean, don't worry, what you're doing works, too, and some people do it (and some would probably also disagree about it being discouraged). Just to let you know.

Wolfgang Jeltsch (Dec 16 2022 at 21:28):

Yeah, the Isabelle/Isar proof language, which is really great, let’s you write things in a style mathematicians would use and under the hood translates everything into Isabelle/Pure (meta-level) connectives.

Last updated: Apr 19 2024 at 04:17 UTC