概括结构归纳证明中的声明，以便能够使用归纳假设

Question

我想证明以下内容

lemma
  fixes pi :: "'a path" and T :: "'a ts"
  shows "valid_path T pi s ⟹ ∀ op ∈ set pi. valid_operator T op"

通过对圆周率的归纳，其中

fun valid_path :: "'a ts ⇒ 'a path ⇒ 'a state ⇒ bool" where
"valid_path T [] s = True" |
"valid_path T (op#ops) s = (valid_operator T op ∧ valid_path T ops (effect op s))

路径只是运算符列表的类型同义词。其他定义不应该对证明起作用。

基本案例工作正常。

问题是，非正式地，对于 pi = (x # xs) 的归纳步骤，我假设

if valid_path T xs s
then ∀ op ∈ set xs. valid_operator T op

我必须证明这意味着

if valid_path T (x#xs) s
then ∀ op ∈ set (x#xs). valid_operator T op

我可以在这里使用valid_path的定义，所以最后这个表达式等价于

if valid_path T (xs) (effect x s)
then ∀ op ∈ set (x#xs). valid_operator T op

如果我能够在 valid_path T (xs) (effect x s) 上使用归纳假设，我就完成了。

我不能，因为假设只适用于 valid_path T (xs) s 而不是 valid_path T xs (effect x s)。

但这并不重要，因为 if 语句的谓词根本不依赖于 s！

但是伊莎贝尔不知道所以它抱怨。

如何才能将归纳假设应用于 valid_path T (xs) (effect x s)？我有一种感觉，我必须使声明更普遍，以便我可以在证明中使用假设，但我不知道如何。

Answer 1

在归纳中必须概括某些术语是很常见的。在 induct 方法中使用关键字 arbitrary。

proof (induct pi arbitrary: s)

这在 Programming and Proving in Isabelle/HOL 的第 2.4 章中有解释。

概括结构归纳证明中的声明，以便能够使用归纳假设

Generalize a claim in a structural induction proof to be able to use the induction hypothesis

induction

isabelle