引理中的自由变量与示意图变量

Question

这三个词之间有什么区别（在它们的含义上，在可能的用法上）？

  consts d::int
  consts e::int

  lemma  L1:"⟦2 dvd d; 2 dvd e⟧ ⟹ 2 dvd (d+e)" by simp

(* lemma L1: even d ⟹ even e ⟹ even (d + e) *)

  lemma  L2:"⋀(f::int) (g::int). ⟦2 dvd f; 2 dvd g⟧ ⟹ 2 dvd (f+g)" by simp

(* lemma L2: even ?f ⟹ even ?g ⟹ even (?f + ?g) *)

  lemma  L3:"⟦2 dvd (h::int); 2 dvd (i::int)⟧ ⟹ 2 dvd (h+i)" by simp

(* lemma L3: even ?h ⟹ even ?i ⟹ even (?h + ?i) *)

Answer 1

变量名称不同，但逻辑上是一样的。如果实例化原理图变量，差异就会发挥作用，在这种情况下，您必须使用定理中提供的名称。这就是为什么他们告诉我们使用不依赖于变量名称的证明技术。如果分发证明中的名称发生变化，则会破坏我们的证明。

查看标题为通用量词与示意图变量、奇怪错误消息，而x是一个特殊的变量，在这个月伊莎贝尔用户列表中的电子邮件：

lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-October/thread.html

自由变量被meta-all运算符隐式全称量化，前段时间C.Sternagel演示过一个教训。您显式量化 L2 的 f 和 g，其中 h 和 i 在 L3.

中隐式量化

在 2012-10 主题中，查看标题为 Free variables deadhorse beat... 和 [= 的电子邮件28=]新年快乐 Free/Bound 变量 如下：

引理中的自由变量与示意图变量

Free versus schematic variables in lemmas

isabelle

theorem-proving