Re: [isabelle] Free variables vs schematic variables



On Wed, 13 Jun 2012, Steve Wong wrote:

Just a quick question: how come Isabelle keeps a distinction between free and schematic variables?

Free means "fixed" and schematic "arbitrary". In informal mathematics you say "let x be arbitrary, but fixed". Which means it is first made a local free/fixed thing, and in the result it can then be arbitrary.

In the Isar proof language you write down fixed things, and get potentially arbitrary results from it. The free vs. schematic marker implements that idea formally in the underlying logical framework.


It seems that free variables in a goal are converted to schematic anyway, so what are the benefits of keeping them distinct?

When you say "in a goal", you mean the so-called "eigen context" of a statement, e.g.

  theorem fixes x :: 'a shows "x = x" ..

Here 'a and x are fixed, and in the result everything is then schematic, at least in this example. In general, the context can still keep other things fixed (say via 'locale' or 'context' or within a nested proof).

In fact, a mixture of fixed and schematic variables characterizes genuine locality in Isabelle, as opposed to the old scheme from the 1980/1990-ies where everything was either free or schematic.


	Makarius





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