如何定义类型的线性排序？

Question

我正在尝试定义。在我的例子中，合取等价于 min 函数的线性顺序 false < error < null < true.

datatype bool4 = JF | JT | BN | BE

instantiation bool4 :: linear_order
begin

fun leq_bool4 :: "bool4 ⇒ bool4 ⇒ bool" where
  "leq_bool4 JF b = True"
| "leq_bool4 BE b = (b = BE ∨ b = BN ∨ b = JT)"
| "leq_bool4 BN b = (b = BN ∨ b = JT)"
| "leq_bool4 JT b = (b = JT)"

instance proof
  fix x y z :: bool4
  show "x ⊑ x"
    by (induct x) simp_all
  show "x ⊑ y ⟹ y ⊑ z ⟹ x ⊑ z"
    by (induct x; induct y) simp_all
  show "x ⊑ y ⟹ y ⊑ x ⟹ x = y"
    by (induct x; induct y) simp_all
  show "x ⊑ y ∨ y ⊑ x"
    by (induct x; induct y) simp_all
qed

end

definition and4 :: "bool4 ⇒ bool4 ⇒ bool4" where
  "and4 a b ≡ minimum a b"

我想在 Isabelle HOL 中一定有更简单的方法来定义线性顺序。你能建议简化理论吗？

Answer 1

您可以使用 "Datatype_Order_Generator" AFP entry.

然后就是简单的导入"$AFP/Datatype_Order_Generator/Order_Generator"和声明derive linorder "bool4"。请注意，在定义数据类型时，必须按照您希望的顺序声明构造函数。

可以找到有关如何在本地下载和使用 AFP 的详细信息here。

如何定义类型的线性排序？

How to define a linear ordering on a type?

isabelle