[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 *)
      oops

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:
    {uu_.
     ∃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,
David


________________________________

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.