Isabelle 函数查找关系成员的最长序列
Isabelle function to find the longest sequence of members of a relation
我有一个关系 R :: w => w => bool，它既是可传递的又是非自反的。
我有公理 Ax1："finite {x::w. True}"。因此，对于每个 x 总是有一个最长的序列 wn R ... R w2 R w1 R x.
我需要一个函数 F::w => nat，对于给定的 x - 返回此序列的 "lenght"（如果没有满足 xRy 的 y，则返回 0）。我将如何在 isabelle 中构建一个。
另外：Ax1 是公理化 "finiteness of type w" 的好方法还是有更好的方法？
首先，{x::w. True}更地道的写法是UNIV :: w set。我建议写 finite (UNIV :: w set)，或者可能使用 finite 类型 class，尽管这可能会使您的定理更难应用，因为您需要一个 finite 类型实例。我认为这对您的用例来说并不是真正必要或有帮助。
然后我建议采用以下方法：
在类型为 w list 的列表上定义一个归纳谓词（使用 inductive），声明第一个元素是 x 并且对于每两个连续的列表元素 y 和 z, R y z 成立，即列表是一个升序链 w.r.t。 R.
证明任何链表都必须有不同的元素（参见distinct :: 'a list ⇒ bool）。
证明有限集上有有限多个 distinct 列表。
使用 Max 运算符找到最大的 n 使得存在一个长度为 n 的列表是一个升序链 w.r.t . R。这项工作应该很容易，因为至少有一个这样的链，并且您已经证明只有有限多条链。
我有一个关系 R :: w => w => bool，它既是可传递的又是非自反的。
我有公理 Ax1："finite {x::w. True}"。因此，对于每个 x 总是有一个最长的序列 wn R ... R w2 R w1 R x.
我需要一个函数 F::w => nat，对于给定的 x - 返回此序列的 "lenght"（如果没有满足 xRy 的 y，则返回 0）。我将如何在 isabelle 中构建一个。
另外：Ax1 是公理化 "finiteness of type w" 的好方法还是有更好的方法？
首先，{x::w. True}更地道的写法是UNIV :: w set。我建议写 finite (UNIV :: w set)，或者可能使用 finite 类型 class，尽管这可能会使您的定理更难应用，因为您需要一个 finite 类型实例。我认为这对您的用例来说并不是真正必要或有帮助。
然后我建议采用以下方法：
在类型为
w list的列表上定义一个归纳谓词（使用inductive），声明第一个元素是x并且对于每两个连续的列表元素y和z,R y z成立，即列表是一个升序链 w.r.t。R.证明任何链表都必须有不同的元素（参见
distinct :: 'a list ⇒ bool）。证明有限集上有有限多个
distinct列表。使用
Max运算符找到最大的n使得存在一个长度为n的列表是一个升序链 w.r.t .R。这项工作应该很容易，因为至少有一个这样的链，并且您已经证明只有有限多条链。