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或fun命令通过公式递归来定义这样的函数。在Isabelle网站上有很多关于‘Programming and Proving‘ tutorial的例子.