Email Gateway (Aug 18 2022 at 15:36): Email Gateway (Aug 18 2022 at 15:36):From: Matthias Schmalz <mschmalz@inf.ethz.ch>
-----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-----
Email Gateway (Aug 18 2022 at 15:48):From: Makarius <makarius@sketis.net>
The looper is explained in section 9.2.9 of the Old Isabelle Reference
manual. You need to read that text with the historical context in mind.
Success or failure in terms of looper tactics is meant in the elementary
tactic sense. Simplifier.simp_tac always succeeds, even if there is no
progress. You may want to wrap it into the CHANGED tactical. Moreover,
recall Simplifier variants such as asm_full_simp_tac that operate with/on
local goal premises. Simplifier.simp_tac only operates on the conclusion
of a subgoal.
Makarius
Last updated: Apr 25 2024 at 04:18 UTC