Adam Dingle (Apr 11 2026 at 14:38): 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.
Alex Mobius (Apr 21 2026 at 17:28):Worth noting that you can also write proof (intro allI impI) to do both introduction steps at once, if you need to work with atomized objects.
David Wang (Apr 22 2026 at 16:14):Alex Mobius said:
Worth noting that you can also write
proof (intro allI impI)to do both introduction steps at once, if you need to work with atomized objects.
There is a nice rule combining these two as well: (intro strip).
Ant S. (Apr 22 2026 at 21:18):David Wang said:
Alex Mobius said:
Worth noting that you can also write
proof (intro allI impI)to do both introduction steps at once, if you need to work with atomized objects.There is a nice rule combining these two as well:
(intro strip).
Is it specifically those two rules its introducing, or does it do more? How can I check? (Could also be useful for the meta tips threads I'm trying to prop up in #**General** )
Mathias Fleury (Apr 23 2026 at 04:22):thm strip
Ant S. (Apr 23 2026 at 09:51):oh oops lol I shoulda checked that
Maximilian Schäffeler (Apr 23 2026 at 12:10):proof safe is also a very common pattern.
David Wang (Apr 23 2026 at 21:45):Ant S. said:
David Wang said:
Alex Mobius said:
Worth noting that you can also write
proof (intro allI impI)to do both introduction steps at once, if you need to work with atomized objects.There is a nice rule combining these two as well:
(intro strip).Is it specifically those two rules its introducing, or does it do more? How can I check? (Could also be useful for the meta tips threads I'm trying to prop up in #**General** )
Good idea.
Last updated: May 05 2026 at 02:56 UTC