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

On 01/08/2013 01:23 AM, Makarius wrote:
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 ;)
Sorry for the confusion. What I really meant was that after a successful proof

lemma "P x"


lemma "!!x. P x"

behave alike (for almost all purposes). I did not even consider what happens inside the corresponding proof. Your explanations are enlightening (though, maybe not the uninitiated ;)).



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

This is called "formal noise" in Isar terminology.  Here is the well-known
explicit way to avoid it:

     fixes x :: 'a
     shows "x = x"
   proof -

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 MHonArc.