1

假设我有一个引理mylem: foo ?a = bar ?a，我需要将它应用到一个目标上，该目标有两次出现foo，例如baz (foo (f p q)) (foo (g r s))，但只出现在其中一个位置上。我知道有两种方法可以做到这一点，而不必写出所有的p, q...，这可能是复杂的表达式。

  • 使用apply (subst mylem)后跟适当数量（此处为 0 或 1）的back命令。
  • 使用apply (subst mylem[where a = 'foo x y', standard]), wherex和y是未绑定的名称。

这里的使用subst只是为了演示；我真的很想修改引理，例如，rule当有多个可能的匹配项我想以这种方式消除歧义时使用它。

这两种方法对我来说都是不好的风格。有没有更好的方法来实现这一目标？

4

1 回答 1

1

您可以判断subst它应该替换哪个事件：在第 -th 匹配事件处subst (i) mylem展开。这可以节省您的步骤。您还可以列出多个职位，如。如果要在场所展开，请使用.mylemibacksubst (1 2) mylemmylemsubst (asm) (1 2) mylem

一般来说，我不知道在apply脚本中实现你想要的东西的方法。在理论层面上，您可以使用lemmaswithfor子句来概括局部引入的变量：

lemmas mylem' = mylem[where a="f x y"] for x y

在结构化证明中，您可以像这样明确地执行此操作：

{ fix x y note mylem[where a="f x y"] }
note mylem' = this
于 2013-04-09T11:43:57.613 回答