1

假设我有一个关于简单归纳定义集的引理：

inductive_set foo :: "'a ⇒ 'a list set" for x :: 'a where
  "[] ∈ foo x" | "[x] ∈ foo x"

lemma "⋀x y. y ∈ foo x ⟹ qux x y ⟹ baz x y"

（对我来说，保留“⋀x y”位很重要，因为引理实际上是在说明我的证明处于长应用链中间的状态。）

我在开始证明这个引理时遇到了麻烦。我想通过规则归纳来进行。

第一次尝试

我试着写

apply (induct rule: foo.induct)

但这不起作用：该induct方法失败。我发现我可以通过修复x并y明确地解决这个问题，然后调用该induct方法，如下所示：

proof -
  fix x :: 'a
  fix y :: "'a list"
  assume "y ∈ foo x" and "qux x y"
  thus "baz x y"
  apply (induct rule: foo.induct)
oops

但是，由于我实际上处于应用链的中间，因此我宁愿不输入结构化证明块。

第二次尝试

我尝试使用该induct_tac方法，但不幸induct_tac的是没有foo.induct以我想要的方式应用该规则。如果我输入

apply (induct_tac rule: foo.induct, assumption)

那么第一个子目标是

⋀x y. y ∈ foo x ⟹ qux x y ⟹ baz x []

这不是我想要的：我想要qux x []而不是qux x y. 该induct方法做到了这一点，但还有其他问题，如上所述。

4

1 回答 1

4

如果您首先将目标转换为如下所示：

⋀x y. y ∈ foo x ⟹ qux x y ⟶ baz x []

然后apply (induct_tac rule: foo.induct)将以您想要的方式实例化归纳规则。（它还将在结果目标中留下对象级别的影响，您需要对此进行处理apply (rule impI)。）

该induct方法自动执行这些额外的步骤来处理含义，这是它的主要优点之一。

另一方面，induct_tac rule: foo.induct除了apply (rule foo.induct). （一般来说，induct_tac可以匹配你指定的变量，并根据它们的类型自动选择一个归纳规则，但你在这里没有利用这些特性。）

我认为您最好的选择是继续在应用链的末尾使用证明块。如果您担心所有的fix,assume和show语句都过于冗长，那么您可以使用小广告case goaln功能：

apply ...
apply ...
proof -
  case goal1 thus ?case
    apply induct
    ...
qed
于 2013-12-19T18:25:52.320 回答