Re: [isabelle] Correct handling of fixed and free variables



On Wed, 5 Jun 2013, Lars Noschinski wrote:

On 04.06.2013 23:07, Lars Hupel wrote:
To summarize the constraints: I'd like to have a `Proof.context`-aware
term parsing, which works correctly for existing schematic and locally
fixed variables. Lars Noschinski also pointed out that care needs to be
taken of these two different kinds of fixed variables:

notepad begin
    { have P sorry } note A = this
    { fix P have P sorry } note B = this
end

These are two separate issues: if we want to use schematic variables as"holes" in the breakpoint, we need a method, whichv handles both bound and unbound schematic variables.

If on the other hand we want to use free variables for the holes then there is this issue which variables are too be generalized.

The usual way to do the latter is to specify the "eigen context" excplicitly via some 'for' specification.

The general scheme looks like this:

  foobar for x y z

So you augment the local context by additional fixes, read/process foobar (whatever that is exactly), and export the result into the original context. Thus there will be certain new schematic variables originating from eigen-variables x y z. This is similar to Pure quantification !!x y z. foobar within the language of propositions, but works for arbitrary things within some Proof.context.

See for example the method "ind_cases" in Isabelle/HOL. (Note that in Isabelle/jEdit you can hover-click over some proof text that uses it, to get quickly to the ML definition of it. Or you say 'print_methods' and hover-click over "ind_cases" in its output.)


	Makarius




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