使用 where-attribute 实例化以数字结尾的变量 (Isabelle)

Question

在 Isabelle 中，给定一个带有自由变量 x 的定理（更准确地说，是一个示意图变量），可以使用 where 属性实例化 x。

例如，thm[where x=5]

如果变量名以数字结尾，例如 thm[where x1=5]，我将无法完成这项工作。这似乎是由于变量在定理中表示为“?x1.0”而不是“?x1”。

下面的理论给出了一个例子。

我的问题是：如何在这样的定理中实例化 x1？（例如，下面理论中的定理。）

"Solutions" 我知道： - 使用 thm[of 1] 而不是 thm[where x1=1]。这在某些情况下有效，但对于具有许多变量的定理，这变得非常笨重且不稳定（变量的顺序可能会改变）。 - 只使用不以数字结尾的变量名。那会起作用，但有时像 x1 这样的变量在给定的上下文中是非常自然的。

theory Tmp imports Main begin

lemma l1: "x+y=y+(x::nat)" by simp

thm l1[where x=1]
(* Prints: 1 + ?y = ?y + 1 *)

lemma l2: "x1+x2=x1+(x2::nat)" by simp

thm l2[where x1=1]
(* Prints: No such variable in theorem: "?x1" *)

thm l2
(* Prints: ?x1.0 + ?x2.0 = ?x1.0 + ?x2.0 *)

Answer 1

您必须使用包含问号的原理图变量全名：

thm l2[where ?x1.0 = 1]

使用 where-attribute 实例化以数字结尾的变量 (Isabelle)

Instantiating variables ending in a digit using where-attribute (Isabelle)

isabelle