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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
