Sollte ich universelle Quantifizierung in der Lemma-Formulierung verwenden?

Question

Für

datatype natural = Zero | Succ natural 

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

I

beweisen

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

Für mathematische zu sein, ist es wichtig, Allquantifizierung zu haben. Doch für die Nutzung dieser Tatsache in dem Vereinfacher, ist es besser, es zu tun, ohne:

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

Was ist die gemeinsame Weisheit über diese Versionen, die man soll ich unter welchen Umständen bevorzugen?

Answer 1

Isabelle/HOL hat drei Möglichkeiten, um universell Variablen in Lemma Aussagen zu quantifizieren über:

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

Zusätzlich werden frei Variablen in Lemma Anweisungen automatisch quantifiziert:

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

Lemmata 1, 2, und 4 ergeben den gleichen Satz, der später auf identische Weise verwendet werden kann. In Lemma 3 wird anstelle der Quantifizierung aus der Meta-Logik der HOL-Universalquantor verwendet. Daher ist zusätzliche Arbeit erforderlich, um den Quantifizierer in Lemma 3 zu instantiieren. Daher sollte diese Version nur unter besonderen Umständen verwendet werden.

Die Version in Lemma 1 stammt aus der Zeit, als die Isar-Sprache nicht in ihrem aktuellen Zustand war und daher etwas veraltet ist. Daher würde ich vorschlagen, Version 2 (wenn Sie die quantifizierten Variablen explizit erwähnen möchten) oder 4 (falls nicht) zu bevorzugen.