isabelle - 伊莎贝尔：验证重言式

Question

我想在 Isabelle 中创建一个给定公式的函数 F

       formula = pr int | neg formula | imp formula formula 

如果公式是重言式的，则返回 True，否则返回 False。

例如：

F( φ ⇒ φ ) = True
F( φ ⇒ (ψ ⇒ φ) ) = True
F( ψ ⇒ φ ) = False

谁能帮我？我发现很难理解 Isabelle 的文档，而且我找不到这样的功能（我认为它应该已经存在）。

Answer 1

在任何情况下，如果你想谈论公式的重言式（或公式的任何语义属性），你首先需要为你的公式定义语义，即一个函数eval :: formula ⇒ (int ⇒ bool) ⇒ bool（假设pr构造函数代表自由变量），它接受一个公式和变量赋值并返回公式是否适用于该赋值。

primrec您可以通过使用orfun命令对公式进行递归来定义这样的函数。Isabelle 网站上的“编程和证明”教程中有很多示例。