0

在我的 Isabelle 形式化中，我正在处理有限的自然数集，在这些集上我想考虑具有线性顺序属性的函数。

我看到图书馆中有几种不同的订单形式，但我不确定要重用哪一种。在大多数情况下，我想检查它们是否为线性顺序的那些函数将简单地通过使用库运算符（如<( less)）来定义，但在某些情况下，它们可能被定义为更复杂的库函数组合。

我试过HOL/Library/Order_Relation了，但似乎没有连接到<；例如，我无法自动证明以下引理：

lemma "linear_order_on {1::nat, 2} {(a::nat, b) . {a, b} ⊆ {1::nat, 2} ∧ a < b}"

（我确信有更好的方法将函数转换为关系，但这不是这里的重点。）

如果有一些现成的库可以让我知道，我会很感激。以数学上优雅的方式对此进行建模现在对我来说并不是最重要的，所以现在我正在考虑使用将有理数或实数分配给我的集合中的自然数的函数，然后<在这些有理数/实数上使用数字。

4

1 回答 1

2

我真的不知道是否有更好的理论可以使用，但是您给出的引理（仍然在修复之后）是错误的（给定的关系是反身的，而预期的关系应该是反身的）。以下是两个正确的版本：

lemma "linear_order_on {1::nat, 2} {(a::nat, b) . {a, b} ⊆ {1::nat, 2} ∧ a ≤ b}"
  unfolding linear_order_on_def partial_order_on_def preorder_on_def
    refl_on_def total_on_def trans_def antisym_def
  by auto

lemma "strict_linear_order_on {1::nat, 2} {(a::nat, b) . {a, b} ⊆ {1::nat, 2} ∧ a < b}"
  unfolding strict_linear_order_on_def partial_order_on_def preorder_on_def
    irrefl_def total_on_def trans_def antisym_def
  by auto
于 2013-05-22T11:16:40.190 回答