与 Isabelle 一起证明时的智能构造函数模式

Question

在学习 Concrete Semantics 的第 3 章时，我的讲师提到其中的一些函数是使用智能构造函数模式构建的，并指出这种模式有利于定理证明。

我在 google 上搜索了智能构造函数，它们似乎用于 Haskell 我不熟悉的语言。此外，在定理证明中，智能构造函数的引用并不多。

那么，Isabelle 中的智能构造函数模式是什么，它如何帮助定理证明呢？也许你甚至可以用本书的第 3 章来解释它......

Answer 1

因此，该模式基本上包括在单独的函数中定义和证明函数的困难子情况，然后将它们组合到主函数中。这当然会简化证明。

您可以在教程的 AExp.thy 中看到此行为的示例。简化后的函数为：

fun plus :: "aexp ⇒ aexp ⇒ aexp" where
"plus (N i1) (N i2) = N(i1+i2)" |
"plus (N i) a = (if i = 0 then a else Plus (N i) a)" |
"plus a (N i) = (if i = 0 then a else Plus a (N i))" |
"plus a1 a2 = Plus a1 a2"

关于简单函数的一些定理是：

lemma aval_plus [simp]:
  "aval (plus a1 a2) s = aval a1 s + aval a2 s"
apply(induction a1 a2 rule: plus.induct)
apply auto
done

事实的组合发现于：

fun asimp :: "aexp ⇒ aexp" where
"asimp (N n) = N n" |
"asimp (V x) = V x" |
"asimp (Plus a1 a2) = plus (asimp a1) (asimp a2)"

最后的证明更简单：

theorem aval_asimp[simp]:
  "aval (asimp a) s = aval a s"
apply(induction a)
apply (auto)
done

与 Isabelle 一起证明时的智能构造函数模式

Smart constructor pattern while proving with Isabelle

design-patterns

theorem-proving

isabelle