在Isabelle中查找小于列表元素的首个索引

核心步骤与语法说明 #

1. 集合构造（Collect）的用法
   Isabelle 里用 {j. P j} 语法（等价于 Collect (λj. P j)）构造集合，其中 P j 是判断元素 j 是否满足条件的谓词。针对你的需求，需要先限定索引 j 是列表 L 的合法索引（即 j < length L），再加上 j < L ! j 的条件，所以集合 A 的定义应为：

definition A :: "nat set" where "A = {j. j < length L ∧ j < L ! j}"

这里的 L ! j 是 Isabelle 中列表的索引访问操作，取列表 L 中第 j 个元素（索引从0开始）。

2. 求集合的最小值
   用 Min 函数可以直接取非空集合的最小值。但要注意，Min 仅对非空集合有效，所以需要先证明集合 A 非空，才能安全使用。

针对你的示例的完整代码 #

(* 定义排序后的列表 L *)
definition L :: "nat list" where "L = sorted_list_of_set {7, 0, 4}"

(* 构造满足条件的索引集合 A *)
definition A :: "nat set" where "A = {j. j < length L ∧ j < L ! j}"

(* 证明 A 非空，确保 Min 操作合法 *)
lemma A_non_empty: "A ≠ {}"
  unfolding A_def L_def
  by (simp add: sorted_list_of_set_def)

(* 定义最小索引 m *)
definition m :: nat where "m = Min A"

(* 计算 m 的值，结果为 1 *)
value m

关键概念解释 #

• 成员关系：Isabelle 中用 ∈ 表示成员关系，比如 1 ∈ A 表示索引1是集合A的元素，对应你提到的“成员关系”。
• Collect 机制：{j. P j} 会遍历所有符合类型的元素（这里是自然数），将满足谓词 P j 的元素全部收集到集合中。加上 j < length L 的条件，是为了避免索引越界，确保 L ! j 的访问合法。

内容的提问来源于stack exchange，提问作者Squirtle