Свободные и условные переменные в леммах

Question

В чем разница между этими тремя леммами (по их смыслу, при возможном использовании)?

consts d::int 
    consts e::int 

    lemma L1:"⟦2 dvd d; 2 dvd e⟧ ⟹ 2 dvd (d+e)" by simp 

(* lemma L1: even d ⟹ even e ⟹ even (d + e) *) 

    lemma L2:"⋀(f::int) (g::int). ⟦2 dvd f; 2 dvd g⟧ ⟹ 2 dvd (f+g)" by simp 

(* lemma L2: even ?f ⟹ even ?g ⟹ even (?f + ?g) *) 

    lemma L3:"⟦2 dvd (h::int); 2 dvd (i::int)⟧ ⟹ 2 dvd (h+i)" by simp 

(* lemma L3: even ?h ⟹ even ?i ⟹ even (?h + ?i) *) 

Answer 1

Имена переменных разные, но они логически одинаковы. Разница вступает в игру, если вы создаете схемы переменных, и в этом случае вы должны использовать имена, указанные в теореме. Именно поэтому они говорят нам использовать методы доказательства, которые не зависят от имен переменных. Если имена будут изменены в доказательствах распространения, это нарушит наши доказательства.

Смотрите электронные письма под названием кванторов vs. схематические переменные, странное сообщение об ошибке и х специальная переменная, в этом месяцев писем на список пользователя Изабеллы:

• lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-October/thread.html

Свободные переменные неявно универсально количественно определяются оператором meta-all, уроком, продемонстрированным C.Sternagel некоторое время назад. Вы явно количественно определяете f и g из L2, где h и i неявно количественно определены в L3.

В 2012-10 нитей см письма под названием свободных переменных Дедхорс бить ... и С Новым годом с Free/Bound Переменные в следующем:

• lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-October/thread.html
• lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-December/date.html
• lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-January/thread.html