Email Gateway (Aug 19 2022 at 13:50): Email Gateway (Aug 19 2022 at 13:50):From: David Greenaway <david.greenaway@nicta.com.au>
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.
Email Gateway (Aug 19 2022 at 13:50):From: Dmitriy Traytel <traytel@in.tum.de>
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
Email Gateway (Aug 19 2022 at 13:50):From: David Greenaway <david.greenaway@nicta.com.au>
Hi Dmitriy,
On 14/02/14 17:50, Dmitriy Traytel wrote:
this looks like the finite_Collect simproc running havoc here again.
[...]
For Isabelle2013-2 you can disable the simproc using
[[simproc del: finite_Collect]]
Thanks for the hint! Turning off the simproc solves the problem both for
the minimal example and in the bigger proof I was working on.
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.
Last updated: Apr 19 2024 at 20:15 UTC