[isabelle] apply simp: Tactic failed

I found another problem involving nested case expressions:

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

In both Isabelle2014 and Isabelle/adaa430fc0f7, this prints:

  Tactic failed
  The error(s) above occurred for the goal statementâ:
  set (if p then case q of (None, u) â [] | (_, u) â [] else []) =
  {x. âuu_ uua_. p â (uua_, uu_) = q â
                 x â set (case uua_ of None â [] | _ â [])}

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.


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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