Re: [isabelle] apply simp: Tactic failed



On Sat, 14 Feb 2015, Florian Haftmann wrote:

A quick look into the simpset reveals that the simproc
'list_to_set_comprehension' is likely at fault. Indeed, after disabling
it, 'simp' goes through (doesn't solve the goal, though). Apparently the
simproc internally sets up some goal via 'Goal.prove' which it cannot solve.

This seems (again) an indication, that either somebody invests some time
to restore that simproc, or make it optional alternatively.

This old thread is still open.

I was at first confused, because the answer by Florian sounded like another routine breakdown of Set_Comprehension_Pointfree.simproce, but here it is List_to_Set_Comprehension.simproc, which looks much more canonical and robust.

Here is again the example causing the crash:

lemma "set (if p then case q of (None, u) â [] | (Some s, u) â [] else []) = {}"
  apply simp

The point of failure is here in the source http://isabelle.in.tum.de/repos/isabelle/annotate/879918f4ee0f/src/HOL/List.thy#l639 which may be easily seen by putting a print_tac before and after that step.


It is not immediately obvious to me, how to improve the simproc, but it should be possible, after 2-3 rounds of careful study of the source.

In any case this is not relevant for Isabelle2015: the same failure happens in Isabelle2014, so we don't have a regression.


	Makarius


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