Stream: Beginner Questions

Topic: ✔ How can I shorten this simple Isar proof?

Adam Dingle (Apr 11 2026 at 14:38):

Consider this proof:

lemma "∀x :: nat. x > 3 ⟶ x > 2"
proof
  fix x :: nat
  show "x > 3 ⟶ x > 2"
  proof
    assume a: "x > 3"
    have "(3 :: nat) > 2" by auto
    with a show "x > 2" by auto
  qed
qed

And never mind that "auto" could prove the entire lemma, since really I'm asking about the block structure here. The proof seems too verbose, since fix x :: nat and show "x > 3 ⟶ x > 2" and assume a: "x > 3" all duplicate text that appear in the lemma statement. Is there some way to tell Isabelle to apply these automatically?

By the way, I know that if I omit ∀ in the lemma statement I can get this shorter proof:

lemma "(x :: nat) > 3 ⟶ x > 2"
proof
  assume a: "x > 3"
  have "(3 :: nat) > 2" by auto
  with a show "x > 2" by auto
qed

However that still seems too verbose, since I must explicitly write "assume". (And maybe I'd prefer to have ∀ in the lemma statement anyway.)

Adam Dingle (Apr 11 2026 at 14:43):

Aha, two minutes after posting this I realized I can write this:

lemma
  fixes x :: nat assumes a: "x > 3" shows "x > 2"
proof -
  have "(3 :: nat) > 2" by auto
  with a show "x > 2" by auto
qed

Is that the best/only way to shorten the proof?

Adam Dingle (Apr 11 2026 at 14:56):

Also, I noticed that if I write the last form above with "fixes" then I end up with a lemma with meta-level implication (?x > 3 ⟹ ?x > 2) rather than object-level implication (?x > 3 ⟶ ?x > 2). Presumably this doesn't matter since they are logically equivalent, but I'm still curious whether there is a compact way to write the proof that will produce the object-level version.

Kevin Kappelmann (Apr 11 2026 at 14:56):

lemma "(x :: nat) > 3 ⟹ x > 2" by simp

Adam Dingle (Apr 11 2026 at 14:56):

Kevin: as I wrote above "never mind that "auto" could prove the entire lemma, since really I'm asking about the block structure here".

Kevin Kappelmann (Apr 11 2026 at 14:58):

I don't understand how you further want to "shorten" the proof then.

Adam Dingle (Apr 11 2026 at 15:05):

This is a contrived example - I'm actually working on a more complex proof that has a similar block structure, and which "auto" or "simp" cannot solve automatically. It's not worth presenting the details of that proof here.

I'll rephrase my question as follows. Suppose that I have a proof of this form:

lemma "∀x :: nat. <P> ⟶ <Q>"
proof
  fix x :: nat
  show "<P> ⟶ <Q>"
  proof
    assume a: "<P>"
    ... have ...
    with a show "<Q>"
  qed
qed

How can I write the proof without repeating <P> and <Q> so many times?

As I wrote above, I realized I can write

lemma
  fixes x :: nat assumes a: "<P>" shows "<Q>"
proof -
    ... have ...
    with a show "<Q>"
qed

That's shorter, which is nice. Presumably this is the best way, then?

Kevin Kappelmann (Apr 11 2026 at 15:07):

Yes, use meta-level connectives for theorem statements.
And you can write show ?thesis instead of repeating your shows statement.
You can also use (is "<some patterns>") next to your assumptions and conclusion.

Adam Dingle (Apr 11 2026 at 15:12):

Thanks for the suggestions. Regarding meta-level connectives, I believe you are saying that theorem statements should generally use ⋀ and ⟹ rather than '∀' and '⟶'. Can you elaborate on this a bit? I'm not sure why/when I might prefer one form over the other. Will built-in proof methods sometimes work better with the meta-level connectives?

Kevin Kappelmann (Apr 11 2026 at 15:40):

Meta-level forall and implication are typically nicer to work with in Isar (Isabelle's structured proof language) and most proof methods. Rule of thumb: use them in theorem statements whenever you can.

Adam Dingle (Apr 11 2026 at 16:07):

OK, thanks for the advice.

Notification Bot (Apr 11 2026 at 16:07):

Adam Dingle has marked this topic as resolved.

Last updated: Apr 14 2026 at 09:21 UTC