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): https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-November/msg00145.html

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]]).

Dmitry

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 *)
       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.