[isabelle] Simplifier internal proof failure

Hello all,

In a bigger proof I discovered an "apply clarsimp" command internally
failing on Isabelle2013-2.

I managed to reduce the problem to the following:

    theory Foo imports Main begin

    lemma "finite (({(a, b). ∃(c, d)∈ A.  B a b c d}))"
      apply simp (* error *)

which gives the error message:

    Proof failed.
     1. ⋀a b aa ab ac ba ad bb ae bc af ag ah bd.
           ⟦(ah, bd) ∈ A; af ∈ UNIV; ag ∈ UNIV; B af ag ah bd⟧
           ⟹ case (ah, bd) of (x, xa) ⇒ B af ag x xa
    The error(s) above occurred for the goal statement:
     ∃a b x.
        uu_ = (a, b) ∧ x ∈ A ∧ (case x of (x, xa) ⇒ B a b x xa)} =
    (λ(a, b, x). (a, b)) `
    ((λ(x, a, b). (a, b, x)) ` (A × UNIV × UNIV) ∩
     (λ(a, b, x). (a, b, x)) `
     {(a, b, x). case x of (x, xa) ⇒ B a b x xa})

This is presumably a bug either somewhere in the simplifier itself or
(more likely) a simproc, but don't know how to track it down any
further, sorry.

Does anybody have any ideas about what might be causing this internal
proof error?

Thanks so much,


The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

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