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.