英文:
Trouble with extremely basic Isabelle/ISAR proofs
问题
我正在学习Isabelle/ISAR，我想尝试一些基本的逻辑证明。我遇到的核心问题是，即使我直接从指导手册中复制证明，我仍然会出现错误。我正在从以下pdf中复制：Isabelle 教程
这是一个非常基本的可以工作的证明：
lemma "A ⟶ A"
proof (rule impI)
assume a: "A"
show "A" by (rule a)
qed
然而，下面的证明尽管直接从文档幻灯片中复制，但会引发错误：
lemma "A ⟶ A"
proof
assume "A"
show "A" .
qed
同样的情况也适用于这个证明：
lemma "A ⟶ A ∧ A"
proof
assume "A"
show "A ∧ A" ..
qed
我不知道为什么直接从pdf中复制的证明不起作用。是因为我使用的Isabelle版本与pdf不同吗？还是我做错了什么？
英文:
I am just starting to learn Isabelle/ISAR, and I wanted to try some basic logic proofs. My core issue is that even when I copy proofs straight out of an instruction manual, I am still getting errors. I am copying from the following pdf: Isabelle Tutorial
Here is a very basic proof that works:
lemma "A ⟶ A"
proof (rule impI)
assume a: "A"
show "A" by(rule a)
qed
However, the following proof throws this error despite the fact that it is copied straight from a documentation slide.
lemma "A ⟶ A"
proof
assume "A"
show "A" .
qed
The same is the case with this proof.
lemma "A ⟶ A ∧ A"
proof
assume "A"
show "A ∧ A" ..
qed
I have no clue why proofs copied straight out of the pdf aren't working. Is it because I'm using a different version of Isabelle than the pdf? Or is there something I am doing wrong?
答案1
得分: 1
Please read the prog-prove instead of some old paper.
I don't know if the semantics changed since 2002 (which is possible), but show nowadays ignores the last fact. Instead you have to use thus or then show.
show A
(*no assumptions*)
while
then show A
(*we have the assumption "A"*)
英文:
Please read the prog-prove instead of some old paper.
I don't know if the semantics changed since 2002 (which is possible), but show nowadays ignores the last fact. Instead you have to use thus or then show.
assume A
show A
(*no assumptions*)
while
assume A
then show A
(*we have the assumption "A"*)
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论