Isabelle中类型参数量化归纳论证及证明义务消解方法问询

1. 针对类型参数的量化归纳论证构造方法 #

• 基于类型类的归纳：定义包含类型参数的类型类（如finite类），针对类中类型的共性性质制定归纳规则。例如，对所有有限类型，可先归纳类型的构造方式（如基本有限类型、乘积类型、和类型），再结合类的实例覆盖不同类型参数，完成量化归纳。
• 项层面间接量化：利用typerep库将类型映射为项层面的表示，把类型参数的量化转化为项的量化，在项层面执行归纳推理后，再关联回原类型的性质。这种方式绕开Isabelle元逻辑对类型直接量化的限制。
• 特定类型族的组合归纳：针对带参数的归纳类型（如list 'a），先对类型参数'a的结构（若'a属于归纳类型）做归纳，再结合容器类型（如list）自身的归纳规则，组合形成针对类型参数的完整归纳论证。

2. 类型长度证明义务的消解方案 #

核心前提 #

你对示意类型?'a“任意但固定”的判断是准确的：直接用?'a无法实现“对任意n存在对应类型”的推理，因为P (LENGTH('a)) ∧ n = LENGTH('a)并非对所有'a成立，关键在于最终结论是否依赖?'a。

无需自定义预言机的方法 #

• 利用有限类型存在性定理：Isabelle的HOL-Finite_Set与Type_Length库中内置定理∀n. ∃(T::finite itself). LENGTH T = n，可通过以下步骤消解义务：
  1. 将原目标P n转化为∃(T::finite itself). LENGTH T = n ∧ P (LENGTH T)；
  2. 调用上述存在性定理，结合unit^n（n次乘积类型）的长度性质LENGTH(unit^n) = n，完成存在实例的构造；
  3. 通过等价替换n = LENGTH T将P (LENGTH T)转化为P n，完成证明。
• 绕开示意类型的中间步骤：直接在证明中引入存在量化的类型变量，而非使用示意类型?'a，避免“固定类型”带来的限制。

现有可用工具/扩展 #

• Type_Length库：专门提供类型长度相关的存在性与构造性定理，可直接调用length_exists这类定理来生成任意长度的有限类型实例。
• finite类型类工具：内置的有限类型构造方法（如乘积、和类型的组合）可用于手动构造对应长度的类型，配合存在引入规则完成证明。

自定义预言机的健全性 #

你的预言机思路是健全的，只要满足以下约束：

• 构造的新类型严格满足LENGTH('a) = x；
• 最终证明结论不包含示意类型?'a（即结论与?'a的具体选择无关）；
• 所有子目标中无未约束的类型变量依赖?'a。
  这种方法本质是在证明中引入存在性的类型实例，且未引入额外的逻辑假设，符合Isabelle的元逻辑规则。

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