Stream: Beginner Questions

Topic: Hypothesis not showing in Isabelle/jEdit

Mario Xerxes Castelán Castro (Oct 10 2026 at 03:16):

Why do I get this, and not p and q as proved facts?

Mario Xerxes Castelán Castro (Oct 10 2026 at 03:27):

How can I get the proof state to show in Isabelle/jEdit, like it shows in vscodium for Lean?

Mathias Fleury (Oct 10 2026 at 05:27):

Mario Xerxes Castelán Castro said:

How can I get the proof state to show in Isabelle/jEdit, like it shows in vscodium for Lean?

You do not want to: Nice forward proofs don't work like that. If you use apply style (backward proofs), then it works. But again, you do not want that: those proofs are fragile and hard to understand and maintain.

Also: we can discuss that Isabelle has more text here, but the version you have is identical to the lean version. And The Isabelle version is clearer, because you do need to know the h to see what is happening -- on this example, this would be stupid, but on long proofs, knowing locally what is happening is important.

Mathias Fleury (Oct 10 2026 at 05:32):

Mario Xerxes Castelán Castro said:

Why do I get this, and not p and q as proved facts?

lemma
  ‹p ∧ q ⟶ q ∧ p›
proof (intro impI, elim conjE)
  assume ‹q› and ‹p›
  then show ‹q ∧ p› by (rule conjI)
qed

but the natural way in Isabelle is to write:

lemma
  assumes ‹p› and  ‹q›
  shows ‹q∧p›

Kevin Kappelmann (Oct 10 2026 at 08:40):

Mario Xerxes Castelán Castro said:

Why do I get this, and not p and q as proved facts?

You put your cursor just after having proved q. this always refer to the last result produced in the text. Hence the output. See https://isabelle.in.tum.de/doc/isar-ref.pdf for a reference manual on Isabelle's input language Isar.

Kevin Kappelmann (Oct 10 2026 at 08:45):

Mario Xerxes Castelán Castro said:

How can I get the proof state to show in Isabelle/jEdit, like it shows in vscodium for Lean?

You could write a new print mode and use it instead of the default one. But note that there is a big difference between lean and Isabelle: the former always scopes a unique goal and its commands act on it while in Isabelle you can have several open goals in scope and solve them in any order you want. In Isar, only once you use show, unification will be used to decide which of the open goals you solved.

Lukas Stevens (Oct 10 2026 at 09:00):

There is also the Print Context menu in the Query panel. This allows you to show the local facts and bindings (e.g. ?thesis).

Last updated: Oct 19 2026 at 03:46 UTC