isabelle - 以应用样式删除目标中的变量

Question

最近学习了如何在应用式证明中删除不需要的前提，我现在想知道如何删除不需要的变量。也就是说，假设我有目标

1. !!x y z. A ⟹ B ⟹ C

wherey没有出现在A,B或C中。如何将其转换为以下内容？

1. !!x z. A ⟹ B ⟹ C

Answer 1

triv_forall_equality确实是去除冗余参数的纯规则。prune_params_tac作为 ML 策略，它也适用于所有子目标。请注意，后者没有作为 Isar 证明方法公开，因为在实践中几乎不需要它：默认情况下，类似的工具simp已经auto包含它。

请注意，方法 via(simp only: triv_forall_equality)在许多情况下都有效，但也有一个障碍：onlyIsabelle/HOL 中的修饰符比“仅”使用给定的 simp 规则做得更多。它包括诸如算术求解器之类的东西，这可能会在某些情况下引起意外或混乱。

prune_params_tac为了在 Isar 方法语言中精确模仿，您可以使用，(unfold triv_forall_equality)尽管存在一个微小的概念障碍：它使用任意重写而不是仅仅折叠方程c = t只是一个历史事故。

Answer 2

一个简单的：

apply simp

会成功的。如果您不想对目标状态执行任何其他转换，可以尝试：

apply (simp only: triv_forall_equality)

这将删除不必要的元量词，但不会修改目标状态。