在 Isabelle 中创建具有不等式的数据类型

Question

我是 Isabelle 的新手，我正在尝试实现一种数据类型，例如

数据类型水果=苹果|香蕉|哈密瓜

（这里的单词选择很空洞，以免与尝试做其他事情混淆）

但是，重要的是要注意苹果≤香蕉≤哈密瓜。

在 Isabelle 中实施的最佳方式是什么？数据类型合适吗？

额外问题：如何将变量实例化为这 3 个选项之一？

Answer 1

关于你的主要问题。

我假设您想手动指定一个顺序，即您想要拼出所有情况。如果您对标准词典顺序感到满意，可以使用 AFP entry 自动执行此操作。

是的，实现所需内容的正确方法是从数据类型开始。然后，您需要定义 ≤ 运算符。为此，您需要 实例化一个 class。 documentation of type classes 中的前两节将让您了解其工作原理。对于您的示例，它看起来像这样：

instantiation fruit :: linorder begin

fun less_fruit where
"Apple < Apple ⟷ False" |
"Apple < _ ⟷ True" |
"Banana < Apple ⟷ False" |
"Banana < Banana ⟷ False" |
"Banana < _ ⟷ True" |
"Cantaloupe < _ ⟷ False"

definition less_eq_fruit :: "fruit ⇒ fruit ⇒ bool" where
[simp]: "less_eq_fruit x y ⟷ x = y ∨ x < y"

instance sorry

end

最后，你还得进行实例证明，即：你需要证明你定义的算子确实是线性排列的。在上面的示例中，我使用 sorry 命令作弊。

正确的做法直接导致你的奖金问题。

您可以使用 cases 策略实例化变量。查看实例证明的实际效果：

instance proof
  fix x y :: fruit
  show "(x < y) = (x ≤ y ∧ ¬ y ≤ x)"
    by (cases x; cases y; simp)
next
   (* more stuff to prove here *)
qed

cases方法采用变量名，并将当前目标拆分为多个案例（此处为三个）。 ;（顺序组合）运算符将应用第一种方法并将第二种方法应用于所有新的子目标。最后，一切都可以用simp.

来解决

在 Isabelle 中创建具有不等式的数据类型

Creating a datatype with inequalities in Isabelle

isabelle