复制教程示例仍报错：基础Isabelle/ISAR证明问题咨询

你遇到的问题核心是Isabelle版本与参考教程不一致。你用的《Isabelle Tutorial》是早期版本（对应Isabelle2005左右），而现代Isabelle（如2023/2024版）对Isar证明的默认行为做了调整，导致旧语法无法直接运行。

具体差异说明 #

• 旧版Isabelle中，proof不带参数时，会自动根据目标的逻辑结构匹配对应的引入规则（比如针对蕴含式A ⟶ A，会自动调用impI规则）。
• 新版Isabelle里，无参数的proof默认使用standard证明方法，它不会自动选择引入规则，必须显式指定或者调整配置才能兼容旧写法。

两种解决方法 #

方法1：显式指定证明规则（推荐）

给proof加上规则参数，明确告诉Isabelle该用什么规则拆解目标，就像你能正常运行的示例那样：

对于第一个报错的例子：

lemma "A ⟶ A"
proof(rule impI)
  assume "A"
  show "A" .
qed

对于第二个例子：

lemma "A ⟶ A ∧ A"
proof(rule impI)
  assume "A"
  show "A ∧ A" ..
qed

方法2：启用旧版兼容模式

如果想完全沿用教程的写法，可以在你的理论文件开头添加以下声明，让proof恢复旧版的自动规则匹配行为：

declare [[proof_method = old]]

添加后，不带参数的proof就能像旧版Isabelle那样自动处理蕴含式目标了。

额外提示 #

现代Isabelle更推荐显式指定证明规则，这样代码可读性更强，也能避免版本兼容问题。后续学习时，建议优先参考你使用的Isabelle版本对应的官方文档，减少语法差异带来的困扰。

内容的提问来源于stack exchange，提问作者saltine