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

[Peter Lammich]

On Mo, 2012-04-02 at 13:45 +0200, Makarius wrote:
> 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.

Thank you. Using the simpset 
"Simplifier.inherit_context ss (HOL_basic_ss addsimps @{thms star_aci})"
did the job!

Cheers,
  Peter