[isabelle-dev] Invoking Simplifier inside simproc, ### Simplifier: renamed bound variable

Peter Lammich lammich at in.tum.de
Mon Mar 26 18:10:14 CEST 2012

Hi all,

Referring to Isabelle-2011-1
(If this post belongs to the users list, feel free to answer it there)

I want to write a simplification procedure, that gets in a term t,
does some transformations on it to obtain a term t', then invokes the
simplifier (with some customized simpset) to prove "t=t'" and returns it
as simplification lemma.

I tried to follow the approach done in the cancellation simprocs,
getting something like:

  fun assn_simproc_fun ss credex = let
    val ctxt = Simplifier.the_context ss
    val ([redex],ctxt') = Variable.import_terms true [term_of credex]
    val export = singleton (Variable.export ctxt' ctxt)

    fun do_transform t = [...]

    val new_form = do_transform redex;

    val result = Option.map (export o mk_meta_eq)
        [simp_tac (HOL_basic_ss addsimps @{thms star_aci}) 1] ctxt

  in result

Where do_transform does the job of transforming the term.
However, I get strange warning messages starting with 
"### Simplifier: renamed bound variable ...", I guess from the inner
call to the simplifier. When tracing the value of "redex", I find that
it may contain loose bound variables, and the warnings from the
simplifier seem to be related to "redex" containing loose bound vars. 

Now my question: Are these "renamed bound variable" - messages from the
simplifier harmful? What am I doing wrong, and how to do it properly?

Best and thanks in advance for any help,

More information about the isabelle-dev mailing list