Email Gateway (Aug 22 2022 at 15:10): Email Gateway (Aug 22 2022 at 15:10):From: Makarius <makarius@sketis.net>
On 02/03/17 16:03, Michel via Cl-isabelle-users wrote:
As a beginner, I tried another elementary proof with jedit.
Note that "jedit" is just a plain text editor written in Java. What you
mean is called "Isabelle/jEdit", "The Prover IDE" or just "PIDE".
thus "r" by (drule mp) When the cursor is on thus :
The old abbreviations "hence" and "thus" make the Isar language harder
to learn and to understand, and the average Isar proof longer (!).
It is better to expand "hence" ~> "then have" and "thus" ~> "then show".
Makarius
Email Gateway (Aug 22 2022 at 15:15):From: Michel via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
I am beginner in Isabelle and I try to understand isar. I have written
the following proof in jedit
1 lemma trivial2 : "p ⟶ (q ⟶ p)"
2 proof
3 assume p: "p"
4 then show "q ⟶ p"
5 proof
6 assume q:"q"
7 show "p" by assumption
8 qed
9 qed
On the line 6 I read in output panel :
goal : No subgoals
But on line 6, I have still a goal (who can't be refined)
On the line 7, with cursor after show I read in output panel :
goal : No subgoals
Failed to refine any pending goal
But on this line, I have the goal "p" which is solved by not still
discharged assumption p
Email Gateway (Aug 22 2022 at 15:18):From: Michel via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
As a beginner, I tried another elementary proof with jedit.
But during the proof, I have strange messages in the output window and 4
proof and only 3 qed.
lemma trivial3isar : "(p ⟶ (q ⟶ r)) ⟶ (q ⟶ (p ⟶ r))"
proof
assume "p ⟶ (q ⟶ r)"
show "q ⟶ (p ⟶ r)"
proof
assume "q"
show "p ⟶ r"
proof
assume "p"
show "r"
proof Here in output :
failed to apply proof method
then "q ⟶r" by (drule mp) When the cursor is on then :
Outer syntax error : command expected
thus "r" by (drule mp) When the cursor is on thus
: Failed to refine any pending goal
qed
qed
qed
Email Gateway (Aug 22 2022 at 15:19):From: Lawrence Paulson <lp15@cam.ac.uk>
It’s essential to understand that “proof” by itself will attempt to use the default proof method, but there is none for the formula r.
At this stage, you have two alternatives. One is to continue in this single-step style by feeding in one of your previous assumptions; the other is finally to use a little automation. So possibly this (note the introduced label):
lemma trivial3isar : "(p ⟶ (q ⟶ r)) ⟶ (q ⟶ (p ⟶ r))"
proof
assume 1: "p ⟶ (q ⟶ r)"
show "q ⟶ (p ⟶ r)"
proof
assume "q"
show "p ⟶ r"
proof
assume "p"
show "r"
using 1
proof
Alternatively, this:
show "r"
by (simp add: "1" ‹p› ‹q›)
Larry Paulson
Last updated: Apr 25 2024 at 12:23 UTC