Isabelle中双括号与分号的含义及jEdit输入报错排查

一、[[ ]]与分号的语义 #

• 双括号[[ ... ]]：Isabelle/HOL里的语法糖，用于批量组合多个前提假设，等价于用逻辑与∧连接所有内部命题。比如[[P; Q]] ==> R和P ∧ Q ==> R逻辑完全一致，但前者在多假设场景下可读性更强。
• 分号;：仅在[[ ]]内部生效，作用是分隔独立的假设命题，每个分号对应一个独立前提，顺序不影响最终逻辑推导。

二、jEdit中输入符号的方法 #

• [[/]]：直接连续按两次左/右方括号键即可，无需特殊快捷键；Isabelle/jEdit的自动补全功能也会在输入单个[时提示补全，但手动输入两次更高效。
• ;：直接按下键盘L键右侧的分号键即可。

三、教程代码报错的原因与解决 #

你遇到的「Inner syntax error⌂ Failed to parse prop」错误，本质是Isabelle版本的语法兼容性差异：

• 你参考的《Isabelle/HOL教程》3.1.5节对应的是旧版Isabelle，当时[[ ... ]]是默认支持的写法；但新版Isabelle（如Isabelle2023及以后）对语法做了调整，默认不再直接识别这种旧写法。
• 两种解决方式：
  1. 改用现代推荐的assumes语法（可读性更强，兼容新版）：

     lemma
       assumes "xs @ zs = ys @ xs"
       assumes "[] @ xs = [] @ []"
       shows "ys = zs"
     

  2. 若坚持使用旧写法，需确保你的Isabelle版本与教程版本一致，或在理论文件开头添加必要的语法声明（不推荐，因为旧写法逐渐被淘汰）。

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