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
fun pat_to_term ctxt t =
let
fun new_var vs T = case Variable.variant_frees ctxt vs [("x", T)] of
v::_ => (Free v :: vs, Free v);
fun go (v as Var (_,T)) (vs,assocs) =
(case AList.lookup op= assocs v of
NONE => (case new_var vs T of
(vs', v') => (vs', (v,v') :: assocs))
| _ => (vs,assocs))
| go _ (vs,assocs) = (vs,assocs);
val assocs = snd (Term.fold_aterms go t
(map Free (Term.add_frees t []), []));
in fst (yield_singleton (Variable.import_terms true)
(subst_atomic assocs t) ctxt)
end;
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
