Re: [isabelle] adding a looper to the simplifier
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] adding a looper to the simplifier
- From: Makarius <makarius at sketis.net>
- Date: Tue, 3 Aug 2010 20:34:35 +0200 (CEST)
- In-reply-to: <4C544FCB.firstname.lastname@example.org>
- References: <4C544FCB.email@example.com>
- User-agent: Alpine 1.10 (LNX 962 2008-03-14)
On Sat, 31 Jul 2010, Matthias Schmalz wrote:
(fn ss => ss addloop ("foo", Simplifier.simp_tac my_ss));
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!
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and