What is the difference between these three lemmas (in their meaning, in possible usage)?
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) *)
The variables names are different, but they're logically the same. The difference comes into play if you instantiate the schematic variables, in which case you have to use the names provided in the theorem. It's why they tell us to use proof techniques which don't depend on names of variables. If the names change in the distribution proofs, it will break our proofs.
See the emails titled universal quantifiers vs. schematic variables, strange error message, and x is a special variable, in this months emails on the Isabelle user's list:
Free variables are implicitly universally quantified by the meta-all operator, a lesson demonstrated by C.Sternagel some time ago. You explicitly quantify f and g of L2, where h and i are implicitly quantified in L3.
In the 2012-10 threads, see emails titled Free variables deadhorse beat... and Happy New Year with Free/Bound Variables in the following: