rename - 为什么元通用量化变量被重命名，如何防止？

Question

考虑下面这个愚蠢的例子

theory meta_all
imports Main
begin

lemma strict_subset: "⟦ A ⊂ B ⟧ ⟹ ∃a ∈ B. a ∉ A"
apply(blast)
done

lemma strict_subset2: "∀A B. A ⊂ B ⟶ (∃a ∈ B. a ∉ A)"
apply(blast)
done

lemma "¬ (∃A. A ⊂ A)"
apply(rule notI)
apply(erule exE)

接下来我想使用 strict_subset 引理并将 A 替换为 A 和 B，并且它会这样做，但会将现有的 A 重命名为 Aa，这完全违背了引入引理的目的。

apply(insert strict_subset [where A="A" and B="A"])

如果我使用派生引理 strict_subset2 一切正常，所以我相信我的推理是正确的。

apply(insert strict_subset2)
apply(erule_tac x="A" in allE, erule_tac x="A" in allE)
apply(drule mp, assumption)
apply(erule bexE, erule notE, assumption)
done

end

要点是，大多数标准引理都是 strict_subset 的形式，而不是 strict_subset2 的形式，Isabelle 的制作者不可能想让我自己制作 strict_subset2 首先是我自己，所以我一定是做错了什么。

我想明白为什么要重命名A？我认为这与类型系统有关，因为我认为我也看到过一些示例，其中只要类型完全正确，元通用量化就不是问题。

另一个问题是我是否可以通过某种方式阻止 A 的重命名？

当然，这两个问题很可能实际上与真正正确的答案无关，因为我对 Isabelle 还是很陌生。

附言。伊莎贝尔的漂亮符号也可以在这里得到吗？

Answer 1

这只是一个狭隘的技术答案，没有开始讨论这种实验路径是否有意义的问题。

在你的情况下

apply(insert strict_subset [where A="A" and B="A"])

有问题的子目标是这样的:

⋀A. A ⊂ A ⟹ False

但是局部绑定(bind)(绿色)A 是子目标的所谓“参数”，这意味着它隐藏在目标上下文中。 strict_subset [where A="A"and B="A"] 的使用指的是证明文本的上下文，而不是证明目标。所以你得到了不同的(免费的，未声明的)A，这也在证明者输出中通过特殊突出显示来指示。

有一组特殊的(非常老式的)策略允许在隐式目标上下文下潜入并进行一些实例化。这是一个例子:

apply(cut_tac A = A and B = A in strict_subset)

现在您在目标状态中有了绿色 A 的实例，但由于规则的形式以及这种奇怪的方式，它也被分成了太多子目标 cut_tac 有效。

请注意，Isabelle/Isar 证明方法基本上有以下几类:

• 结构化 Isar 证明步骤:特别是规则

• 带有推理方向指示的弱结构化步骤:erule、drule、frule

• 允许使用其参数进入隐式目标上下文的旧式战术仿真:rule_tac、erule_tac、drule_tac、 frule_tac

PS:您可以将 Isabelle/jEdit 的 unicode 输出复制粘贴到此文本编辑器中。