我应该在引理公式中使用通用量化吗？

Question

为了

datatype natural = Zero | Succ natural

primrec add :: "natural ⇒ natural ⇒ natural"
where
  "add Zero m = m"
| "add (Succ n) m = Succ (add n m)"

我证明

lemma add_succ_right: "⋀ m n. add m (Succ n) = Succ (add m n)"

对于数学来说，通用量化很重要。但是，为了在简化器中使用这个事实，最好不要使用：

lemma add_succ_right_rewrite: "add m (Succ n) = Succ (add m n)"

关于这些版本的常识是什么？在什么情况下我应该更喜欢哪一个？

Answer 1

Isabelle/HOL 有三种方法可以通用地量化引理语句中的变量：

 lemma 1: "⋀m n. add m (Succ n) = Succ (add m n)"

 lemma 2:
   fixes m n
   shows "add m (Succ n) = Succ (add m n)"

 lemma 3: "∀m n. add m (Succ n) = Succ (add m n)"

此外，引理语句中的自由变量会自动量化：

 lemma 4: "add m (Succ n) = Succ (add m n)"

引理 1、2 和 4 产生相同的定理，以后可以以相同的方式使用。引理 3 使用 HOL 通用量词而不是元逻辑的量化。因此，需要额外的工作来实例化引理 3 中的量词。因此，此版本应仅在特殊情况下使用。

引理 1 中的版本可以追溯到 Isar 语言尚未处于当前状态时，因此有些过时。因此，我建议更喜欢版本 2（如果你想明确提及量化变量）或 4（如果不是）。

我应该在引理公式中使用通用量化吗？

Should I use universal quantification in lemma formulation?

isabelle