# Re: [isabelle] Happy New Year with Free/Bound Variables

On Fri, 4 Jan 2013, Christian Sternagel wrote:

lemma "P x"

`where "P" is some formula with the free variable "x". In this context, a
``helpful answer is that free variables are implicitly universally quantified.
``A more cautious answer would be something like:
`

`When writing a top-level lemma statement like 'lemma "P x"' Isabelle
``behaves as if the free variable "x" was universally quantified at the
``meta-level for almost all purposes ;)
`

I am not yet fully satisfied.
My preferred example is:
lemma "x = x"

`When you write that in a context with undeclared x and (and its implicitly
``inferred most general type 'a with undeclared 'a), the system will
``implicitly augment the proof context by fix x :: 'a (and fix type 'a
``beforehand as well).
`

`['a::TYPE, x::'a] is the so-called "Eigen-context" of the statement.
``There are two sides of this valuable coin:
`
(1) The proof context has its elements are fixed.
(2) The result (after export from the context) has makes them arbitrary.

`The example above includes the situation for types as well, since it hints
``at the important principle of implicit polymorphism in the manner of
``Hindley-Milner. The type language does not even have quantifiers, so
``there is no danger of claiming that they are introduced and eliminated
``somewhere in the belly of the logic -- they are simply not there.
`

`Nonetheless, there is a slight difference in free term variables and free
``type variables: terms need to be fixed explicitly if meant to be universal
``in the end, but types are fixed implicitly according to the possibilities
``of the syntactic context.
`
Instead, when you write
lemma "!!x :: 'a. x = x"

`you will have to fix the element in the proof before getting to the same
``proof context as before:
`
proof -
fix x :: 'a
...
qed
This is called "formal noise" in Isar terminology. Here is the well-known
explicit way to avoid it:
lemma
fixes x :: 'a
shows "x = x"
proof -
...
qed

`So you build up a context with fixed x, then you state "x = x", in the end
``you get arbitrary "?x::?'a = ?x".
`
Makarius

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*