# Re: [isabelle] Free variables vs schematic variables

*To*: Makarius <makarius at sketis.net>
*Subject*: Re: [isabelle] Free variables vs schematic variables
*From*: Ramana Kumar <rk436 at cam.ac.uk>
*Date*: Tue, 3 Jul 2012 14:42:01 +0100
*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Steve Wong <s.wong.731 at gmail.com>
*In-reply-to*: <alpine.LNX.2.00.1206282253120.13196@macbroy21.informatik.tu-muenchen.de>
*References*: <CAFU+7wO5C8HePiPJOarcAVqDq+9LDFvp65HxoREvuzy6R41_xg@mail.gmail.com> <CAMej=2719H71FBUT90xtvON-q_8QQPTbHdqVBYmr5k1DMVVMFw@mail.gmail.com> <alpine.LNX.2.00.1206282253120.13196@macbroy21.informatik.tu-muenchen.de>
*Sender*: ramana.kumar at gmail.com

Could I summarise the difference between free and schematic variables like
this:
Free variables came from the statement you want to prove, whereas schematic
variables came from other facts that are already known to be true.
(Thus, free variables must be fixed during a proof, they cannot be
instantiated. Because they were never instantiated, they can become
arbitrary after the proof is completed. Schematic variables can be
instantiated at any time, because they came from some proof in which they
were originally treated as fixed.)
On Thu, Jun 28, 2012 at 9:55 PM, Makarius <makarius at sketis.net> wrote:
> On Wed, 13 Jun 2012, Ramana Kumar wrote:
>
> as I understand it, the distinction is fundamentally unavoidable because
>> one kind of variable is in the object-logic syntax and the other is a
>> meta-logic variable.
>>
>
> Both free and schematic variables belong to Isabelle/Pure, just like bound
> variables via !!x or %x. You could argue if Isabelle/HOL has actually
> variables on its own -- it just re-uses many things from Pure directly,
> including the type system, for example.
>
>
> Makarius
>

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