Re: [isabelle] adding a looper to the simplifier



On Sat, 31 Jul 2010, Matthias Schmalz wrote:

 (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!

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






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