[isabelle-dev] Replacing schematic/dummy variables in a term with fresh free variables

[Manuel Eberl]

Hallo,

I currently have the problem that I have a pattern, i.e. a term that may
contain schematic variables, schematic type variables and, in
particular,m schematic type variables originating from dummy variables.

I read this term using Proof_Context.read_term_pattern and the result
generally looks something like this:

Input: g x = Some _
Output: Const ("HOL.eq", "?'a option ⇒ ?'a option ⇒ bool") $
(Free ("g", "?'b ⇒ ?'a option") $ Free ("x", "?'b")) $
(Const ("Option.option.Some", "?'a ⇒ ?'a option") $
Var (("_dummy_", 1), "?'a"))

I now want to replace all the schematic variables (i.e. the "Var"s) with
fresh free variables and all schematic type variables with fresh normal
type variables. The names of these variables are irrelevant, but
"_dummy_" should, of course, be renamed to something more sensible, such
as "xa" in this case.

I have a solution for this that seems to work (see attachment), but it
is relatively complicated and I think that it should be a lot easier for
somebody who knows the library better than I do. In particular, I think
the function package does something similar, but I cannot seem to find
out where.

Does anybody have an idea how to solve this more elegantly?

Cheers,
Manuel
-------------- next part --------------
A non-text attachment was scrubbed...
Name: pat_to_term.ML
Type: text/x-ocaml
Size: 645 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130612/01c5f7c7/attachment.bin>