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.