[isabelle] adding a looper to the simplifier



-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Dear Isabelle users,

I am trying to add a looper to the simplifier to do some "risky"
simplifications that I cannot do with the splitter. I am stuck, because
the simplifier loops, and I do not understand why. Here is what I do:

ML {*
val my_ss = HOL_basic_ss;

(* At this place, I later intend to add some interesting simplification
procedures to my_ss. *)

(* Register a new looper *)
change_simpset
  (fn ss => ss addloop ("foo", Simplifier.simp_tac my_ss));
*}

lemma "False"
apply simp

On the last command, the simplifier loops. According to the trace it is
invoked again and again on "False". I would expect the simplifier to
fail on "False", because my newly added looper fails on "False".

Any explanations / comments / pointers are very welcome!

Matthias
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFMVE/LczhznXSdWggRAkWLAJ44u0Z7CxEGntFTfUrg81iVi81WvACeNspa
n3E+8Mt1SIPSdZ9oKIUYdss=
=OLgP
-----END PGP SIGNATURE-----





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.