代码之家 › 专栏 › 技术社区 › user1868607

用Isabelle证明时的智能构造器模式

theorem-proving isabelle design-patterns

1

user1868607 · 技术社区 · 7 年前

在学习第三章的时候 Concrete Semantics 我的指导老师提到有些函数是使用智能构造函数模式构建的,并指出这种模式有利于定理证明。

那么,Isabelle中的智能构造函数模式是什么?它如何帮助定理证明呢?也许你可以用这本书的第三章来解释。。。

1 回复 | 直到 7 年前

1

0

user1868607 7 年前

因此,这种模式基本上是在单独的函数中定义和证明函数的困难子类,然后将它们组合成主函数。这当然会使证明更容易。

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