[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.

Cheers
Lars

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



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