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:
fix x :: 'a
This is called "formal noise" in Isar terminology. Here is the well-known
explicit way to avoid it:
fixes x :: 'a
shows "x = x"
So you build up a context with fixed x, then you state "x = x", in the end
you get arbitrary "?x::?'a = ?x".
This archive was generated by a fusion of
Pipermail (Mailman edition) and