Re: [isabelle] Free variables vs schematic variables



The distinction is useful in the course of a proof. Free variables typically represent fixed parameters of the statement being proved. Schematic variables represent unknown quantities such as existential witnesses, where any single value might be supplied. If such a quantity is ?n, a natural number, then replacing ?n by 0 would be appropriate in a proof. However, if the statement being proved involves a natural number n as a parameter, it would not be acceptable to replace n by 0 and prove the much simpler statement resulting from that substitution.

Once the theorem has been proved, making all variables schematic makes it possible to apply the theorem for arbitrary values of n (which will now be ?n).

Larry Paulson


On 13 Jun 2012, at 12:55, Steve Wong wrote:

> Just a quick question: how come Isabelle keeps a distinction between free
> and schematic variables? It seems that free variables in a goal are
> converted to schematic anyway, so what are the benefits of keeping them
> distinct?






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