我需要证明以下几点：
lemma "m = min_list(x#xs) ⟹ m ∈ set (x#xs)"
简单来说，我需要证明“min_list (x#xs)”的返回值始终是 (x#xs) 的成员
我试过了：
apply(induct xs)
apply(auto)
我还尝试使用以下方法为 min_list 重用现有的引理：
find_theorems min_list
此时的子目标太长了，我不知道如何进行。
我不是在寻找完整的答案，只是提示如何处理这个引理。此外，对于刚学习 Isabelle 的人来说，这个证明是简单的还是非常困难的？
【问题讨论】：
剧透：可以使用标准列表归纳和auto 来证明定理，即类似于by (induct xs ...) (auto simp: ...) 的东西。我特意省略了证明中的部分，让你自己填写。您需要考虑是否需要将任何变量（即m 或x）指定为arbitrary，并了解简化器可能需要哪些信息（在理论中的min_list 规范中寻找线索List)。
关于你关于问题难度的问题，我相信，难度是经验的函数。可以肯定的是，当我开始学习 Isabelle 时，我发现很难将类似于您问题中的证明形式化。在Isabelle 编码一段时间后（在回答这个问题时，我必须在Isabelle 积累相当于 4-5 个月的全职编码时间），这些问题似乎不再显着对我的挑战。当然，还有其他因素需要考虑，例如之前接受过数学或逻辑方面的培训以及之前的编码经验。
来自自学伊莎贝尔的人的一般建议（该建议可能与专业讲师通常推荐的方法不一致）
我相信，在证明类似结果时，重要的是要了解 Isabelle 主要是一种用于形式化“纸笔”证明的工具。因此，在尝试将其形式化之前，手头有“纸笔”证明是很重要的。在解决类似问题时，我建议采用以下一般方法：
Isar 将证明形式化，提供尽可能多的细节，而不是太在意证明的长度。此外，尽量不要依赖于自动推理工具（即auto、blast、meson、metis、fastforce），并尽可能多地使用rule 和intro 等直接方法可以。Isar 证明完成后，将自动推理工具（例如 auto、blast）应用于您的 Isar 证明，以尽可能简化您的证明。 当然，最终，随着您在学习伊莎贝尔方面取得进展，省略 1 和 2 会变得越来越容易。
我可以提供更多详细信息，例如完整的短证明和长证明的Isar 版本。
更新
根据您在 cmets 中的要求，我提供非正式证明。
引理。 m = min_list (x # xs) ⟹ m ∈ set (x # xs)。
备注。为了完整起见，我还提供了 min_list 的定义和一些关于 const set 的 cmets。 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/HOL 中定义 (Co) 数据类型和原始 (Co)recursive Functions”文件，如果伊莎贝尔）。特别是，它被称为数据类型的“设置函数”。 const set 的许多基本属性可以通过检查/搜索找到，例如find_theorems list.set。我认为定理thm list.set代表了constset的主要性质（我冒昧地重命名了定理中的示意图变量）：
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 证明。另外，请注意，证明可能并不理想——我稍后可能会对证明进行编辑。
【讨论】：