我應該在引理公式中使用通用量化嗎？

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（如果不是）。