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

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

伊莎贝尔/ 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（如果不是）。