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

[Makarius]

On Mon, 26 Mar 2012, Peter Lammich wrote:

> 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]
>      ctxt;
>    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)
>      (Arith_Data.prove_conv_nohyps
>        [simp_tac (HOL_basic_ss addsimps @{thms star_aci}) 1] ctxt
>        (redex,new_form)
>      );
>
>  in result
>  end;
>
> 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?

The warning is annoying, but not immediately harmful -- we have lived with 
such issues of "non-localized" simprocs for many years in main HOL, until 
Brian managed to isolate the last one 1-2 years ago.

I reckon that you merely need to use (Simplifier.context ctxt) or 
(Simplifier.inherit_context ss) on the nested simpset above to get rid of 
the warning.


 	Makarius