Должен ли я использовать универсальную количественную оценку в формулировке леммы?

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)" 

Для того математического, важно иметь универсальные квантификации. Однако, для использования этого факта в Simplifier, то лучше сделать это без:

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 (если нет).