Isabelle 中有类似 subst_tac 的规则吗？

Question

我有引理

lemma ex1_variable: "(∃x. ∀z. x = y z) = (∃!x. ∀z. x = y z)"

我在证明中有一个中间陈述

"∀a. ∃P. ∀z. P = Q z a"

我想展示

"∀a. ∃!P. ∀z. P = Q z a".

由于∀a，我无法直接使用by (rule ex1_variable)。但是，我觉得应该可以使用 subst 方法，例如

from `∀a. ∃P. ∀z. P = Q z a` have "∀a. ∃!P. ∀z. P = Q z a"
  by (subst_tac ?x="P" and ?y="λx. Q x a" and ?z="z" in ex1_variable)

以便 ex1_variable 在当前目标中被替换，但仅在实例化之后。这个特定的例子不起作用，但有没有类似的东西？

Answer 1

无需显式实例化引理 ex1_variable，高阶统一将为您完成。由于 ex1_variable 是一个等式语句，您实际上可以使用普通的 subst 来证明用实例化的右侧替换左侧的实例。但是你必须告诉 subst 查看假设，因为这是你的子目标中左侧实例出现的地方。所以以下应该有效：

lemma ex1_variable: "(∃x. ∀z. x = y z) = (∃!x. ∀z. x = y z)" sorry

notepad begin
  fix Q
  have "∀a. ∃P. ∀z. P = Q z a" sorry
  then have "∀a. ∃!P. ∀z. P = Q z a"
    by(subst (asm) ex1_variable)
end

或者，您可以翻转定理的边并将 subst 应用于结论：

by(subst ex1_variable[symmetric])

Isabelle 中有类似 subst_tac 的规则吗？

Is there anything like a subst_tac rule in Isabelle?

substitution

isabelle