# 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.*