Re: [isabelle] Unfixed variables in "define" command

On 22/02/2021 13:03, Manuel Eberl wrote:
> Prompted by a question from a student of mine, I am wondering why free
> argument variables on the left-hand side of a function definition with
> "define" have to be fixed manually with "for" for it to work:
> define a :: "nat ⇒ nat" where "a x = 2 * x"
> When writing it like this, the "x" is not fixed and therefore the
> "definition" does not work. When you add a "for x", it seems to work.
> Is there a reason for this behaviour? Would it be possible to fix such
> variables automatically, mirroring the behaviour of e.g. the
> "definition" command?

Such "auto fixes" only work for toplevel specification commands, and that is
already quite delicate and sometimes fragile.

Within the Isar proof languages with its arbitrary nesting of scopes, local
parameters need to be properly fixed. Note that the above "x" could be a
"constant" from an outer scope.

Further note that our ultra-flexible term syntax makes it impossible to say
e.g. that "a" wants to bind its argument (in contrast to ML: "fun a x = ...").

Much more could be said about the overall language design and resulting
decisions. In retrospect over more than 20-25 years, I would be now slightly
more explicit in the scopes: implicit variable declarations are often
confusing, both for the system and the human using it. (The more recent 'for'
context for various language elements make things more robust and flexible.)


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