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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and