会员证明
membership proof
我需要证明以下内容：
lemma "m = min_list(x#xs) ⟹ m ∈ set (x#xs)"
用简单的英语来说，我需要证明 "min_list (x#xs)" 中的 return 值始终是 (x#xs)
的成员
我试过了：
apply(induct xs)
apply(auto)
我还尝试通过以下方式为 min_list 重用现有引理：
find_theorems min_list
此时的子目标太长了，不知如何进行。
我不是在寻找一个完整的答案，只是在寻找如何处理这个引理的提示。此外，对于刚刚学习伊莎贝尔的人来说，这个证明是简单的还是非常困难的？
剧透：可以使用标准列表归纳法和 auto 来证明定理，即类似于 by (induct xs ...) (auto simp: ...) 的东西。我故意遗漏了证明中的部分供您自己填写。您需要考虑是否需要将任何变量（即 m 或 x）指定为 arbitrary，并了解简化器可能需要哪些信息（在规范中寻找线索min_list 理论上 List).
关于你关于问题难度的问题，我认为难度是经验的函数。最肯定的是，当我开始学习 Isabelle 时，我发现很难将类似于您问题中的证明形式化。在 Isabelle 编码一定时间后（在回答这个问题时，我一定已经积累了相当于 4-5 个月的 Isabelle 全职编码），这样的问题似乎不再存在对我提出重大挑战。当然，还有其他因素需要考虑，例如以前接受过数学或逻辑方面的培训以及以前的编码经验。
自学伊莎贝尔的人的一般建议（建议可能与专业教师通常推荐的方法不一致）
我相信，在证明类似结果时，重要的是要了解 Isabelle 主要是 'pen-and-paper' 证明形式化的工具。因此，在尝试将其形式化之前，手头有 'pen-and-paper' 证明很重要。在解决类似问题时，我建议采用以下通用方法：
- 把证明写在纸上。
- 使用
Isar 形式化证明，提供尽可能多的细节，不要太在意证明的长度。此外，尽量不要依赖自动推理工具（即 auto、blast、meson、metis、fastforce）并使用直接方法，如 rule 和 intro 尽可能多。
- 一旦您的
Isar 证明完成，将自动推理工具（例如 auto、blast）应用于您的 Isar 证明以尽可能简化您的证明。
当然，随着您在学习 Isabelle 方面的进步，最终省略 1 和 2 会变得越来越容易。
我可以提供更多详细信息，例如完整的简短证明和证明的长 Isar 版本。
更新
根据您在评论中的要求，我提供了一个非正式的证明。
引理。 m = min_list (x # xs) ⟹ m ∈ set (x # xs)。
备注。为了完整起见，我还提供了 min_list 的定义和一些关于常量 set 的注释。 min_list的定义可以在理论List:
中找到
fun min_list :: "'a::ord list ⇒ 'a" where
"min_list (x # xs) = (case xs of [] ⇒ x | _ ⇒ min x (min_list xs))"
const set 是隐式定义的，构成了 list 的 datatype 基础结构的一部分（如果 Isabelle，请参阅标准文档中的文档 "Defining (Co)datatypes and Primitively (Co)recursive Functions in Isabelle/HOL"）。特别是，它被称为数据类型的 'set function'。 const set 的许多基本属性可以通过 inspection/search 找到，例如find_theorems list.set。我认为定理 thm list.set 代表了 const set 的主要性质（我冒昧地重命名了定理中的示意图变量）：
set [] = {}
set (?x # ?xs) = insert ?x (set ?xs)
证明。证明是通过列表 xs 上的结构归纳得出的。归纳原理在理论的开头被表述为一个未命名的引理List。为了完整起见，我在下面重申归纳原理：
"P [] ⟹ (⋀a list. P list ⟹ P (a # list)) ⟹ P list"
基本情况：假设 xs = []，对所有 x 显示 m = min_list (x # xs) ⟹ m ∈ set (x # xs)。从 min_list 的定义中可以看出 min_list (x # []) = x。类似地，set (x # []) = {x} 可以直接从 const set 的属性中显示出来。代入上面的谓词，它仍然表明 m = x ⟹ m ∈ {x} 对所有 x。这是从基本集合论得出的。
归纳步骤：假设⋀x. m = min_list (x # xs) ⟹ m ∈ set (x # xs)，对所有a、x和xs显示m = min_list (a # x # xs) ⟹ m ∈ set (a # x # xs) .修复 a、x 和 xs。假设 m = min_list (a # x # xs)。那么剩下的就是证明m ∈ set (a # x # xs)。给定m = min_list (a # x # xs)，根据min_list的定义，很容易推导出m = a或m = min_list (x # xs)。明确考虑这些情况：
- 案例一：
m = a。 a ∈ set (a # x # xs) 遵循定义。然后，m ∈ set (a # x # xs)通过替换。
- 案例二：
m = min_list (x # xs)。然后，从假设 ⋀x. m = min_list (x # xs) ⟹ m ∈ set (x # xs) 得出 m ∈ set (x # xs)。因此，m ∈ set (a # x # xs) 遵循 set. 的属性
在所有可能的情况下m ∈ set (a # x # xs)，这是需要证明的。
至此，证明结束
结论。尝试将此非正式证明转换为 Isar 证明。另外，请注意证明可能并不理想——我可能会在稍后对证明进行编辑。
我需要证明以下内容：
lemma "m = min_list(x#xs) ⟹ m ∈ set (x#xs)"
用简单的英语来说，我需要证明 "min_list (x#xs)" 中的 return 值始终是 (x#xs)
的成员我试过了：
apply(induct xs)
apply(auto)
我还尝试通过以下方式为 min_list 重用现有引理：
find_theorems min_list
此时的子目标太长了，不知如何进行。
我不是在寻找一个完整的答案，只是在寻找如何处理这个引理的提示。此外，对于刚刚学习伊莎贝尔的人来说，这个证明是简单的还是非常困难的？
剧透：可以使用标准列表归纳法和 auto 来证明定理，即类似于 by (induct xs ...) (auto simp: ...) 的东西。我故意遗漏了证明中的部分供您自己填写。您需要考虑是否需要将任何变量（即 m 或 x）指定为 arbitrary，并了解简化器可能需要哪些信息（在规范中寻找线索min_list 理论上 List).
关于你关于问题难度的问题，我认为难度是经验的函数。最肯定的是，当我开始学习 Isabelle 时，我发现很难将类似于您问题中的证明形式化。在 Isabelle 编码一定时间后（在回答这个问题时，我一定已经积累了相当于 4-5 个月的 Isabelle 全职编码），这样的问题似乎不再存在对我提出重大挑战。当然，还有其他因素需要考虑，例如以前接受过数学或逻辑方面的培训以及以前的编码经验。
自学伊莎贝尔的人的一般建议（建议可能与专业教师通常推荐的方法不一致）
我相信，在证明类似结果时，重要的是要了解 Isabelle 主要是 'pen-and-paper' 证明形式化的工具。因此，在尝试将其形式化之前，手头有 'pen-and-paper' 证明很重要。在解决类似问题时，我建议采用以下通用方法：
- 把证明写在纸上。
- 使用
Isar形式化证明，提供尽可能多的细节，不要太在意证明的长度。此外，尽量不要依赖自动推理工具（即auto、blast、meson、metis、fastforce）并使用直接方法，如rule和intro尽可能多。 - 一旦您的
Isar证明完成，将自动推理工具（例如auto、blast）应用于您的 Isar 证明以尽可能简化您的证明。
当然，随着您在学习 Isabelle 方面的进步，最终省略 1 和 2 会变得越来越容易。
我可以提供更多详细信息，例如完整的简短证明和证明的长 Isar 版本。
更新
根据您在评论中的要求，我提供了一个非正式的证明。
引理。 m = min_list (x # xs) ⟹ m ∈ set (x # xs)。
备注。为了完整起见，我还提供了 min_list 的定义和一些关于常量 set 的注释。 min_list的定义可以在理论List:
fun min_list :: "'a::ord list ⇒ 'a" where
"min_list (x # xs) = (case xs of [] ⇒ x | _ ⇒ min x (min_list xs))"
const set 是隐式定义的，构成了 list 的 datatype 基础结构的一部分（如果 Isabelle，请参阅标准文档中的文档 "Defining (Co)datatypes and Primitively (Co)recursive Functions in Isabelle/HOL"）。特别是，它被称为数据类型的 'set function'。 const set 的许多基本属性可以通过 inspection/search 找到，例如find_theorems list.set。我认为定理 thm list.set 代表了 const set 的主要性质（我冒昧地重命名了定理中的示意图变量）：
set [] = {}
set (?x # ?xs) = insert ?x (set ?xs)
证明。证明是通过列表 xs 上的结构归纳得出的。归纳原理在理论的开头被表述为一个未命名的引理List。为了完整起见，我在下面重申归纳原理：
"P [] ⟹ (⋀a list. P list ⟹ P (a # list)) ⟹ P list"
基本情况：假设 xs = []，对所有 x 显示 m = min_list (x # xs) ⟹ m ∈ set (x # xs)。从 min_list 的定义中可以看出 min_list (x # []) = x。类似地，set (x # []) = {x} 可以直接从 const set 的属性中显示出来。代入上面的谓词，它仍然表明 m = x ⟹ m ∈ {x} 对所有 x。这是从基本集合论得出的。
归纳步骤：假设⋀x. m = min_list (x # xs) ⟹ m ∈ set (x # xs)，对所有a、x和xs显示m = min_list (a # x # xs) ⟹ m ∈ set (a # x # xs) .修复 a、x 和 xs。假设 m = min_list (a # x # xs)。那么剩下的就是证明m ∈ set (a # x # xs)。给定m = min_list (a # x # xs)，根据min_list的定义，很容易推导出m = a或m = min_list (x # xs)。明确考虑这些情况：
- 案例一：
m = a。a ∈ set (a # x # xs)遵循定义。然后，m ∈ set (a # x # xs)通过替换。 - 案例二：
m = min_list (x # xs)。然后，从假设⋀x. m = min_list (x # xs) ⟹ m ∈ set (x # xs)得出m ∈ set (x # xs)。因此，m ∈ set (a # x # xs)遵循set. 的属性
在所有可能的情况下m ∈ set (a # x # xs)，这是需要证明的。
至此，证明结束
结论。尝试将此非正式证明转换为 Isar 证明。另外，请注意证明可能并不理想——我可能会在稍后对证明进行编辑。