Re: [isabelle] Simplifier internal proof failure

Hello David,

this looks like the finite_Collect simproc running havoc here again. Problems with this simproc have been noticed before (but after the "feature freeze" for the release):

As the result we have deactivated the (unmaintained) simproc globally in the development version 31afce809794.

For Isabelle2013-2 you can disable the simproc using [[simproc del: finite_Collect]] (and symmetrically reenable it after 31afce809794 using [[simproc add: finite_Collect]]).


Am 14.02.2014 04:26, schrieb David Greenaway:
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.