Isabelle 中的条件定义

Question

假设您想在 Isabelle 中形式化以下定义：

add a b = 
 if f(a,b) ≠ 0 then add_1 a b
 if g(a,b) ≠ 0 then add_2 a b

我不想给任何选项任何偏好。事实上，我需要证明的下一个属性是：

add 为任何输入至少分配一个值
add 定义明确

我应该用什么在 Isabelle 中为这个定义建模？也许是部分功能？

你可以在 this paper 上查看等式 (17) 和引理 4.3.4、4.3.4 以了解我在说什么引理。

Answer 1

您可以使用具有重叠方程和先决条件的 function 命令：

function add :: "..." where
  "add a b = add_1 a b" if "f a b ≠ 0"
| "add a b = add_2 a b" if "g a b ≠ 0"
apply(atomize_elim) (* makes the exhaustiveness goal more readable *)

这给了你一个证明义务，即案例确实详尽无遗，并且当它们重叠时，右侧的节点相同。一旦你展示了这个，你就必须展示终止（如果你的函数不是递归的，那么这很简单

termination by lexicographic_order

如果你的方程实际上并不详尽，那么你首先必须添加更多的情况。在此示例中，您可以添加

| "add a b = undefined a b" if "f a b = 0 & g a b = 0"

表示如果 f 和 g 都是 0，那么 add a b 应该表示一些未指定的值，并且对于每个这样的选择，这个值可能不同a 和 b.

Isabelle 中的条件定义

Conditional definition in Isabelle

isabelle