I’ve found some odd behavior of
match in connection with backtracking.
Consider the following complex approach of proving that
True is true:
lemma triviality: shows True by ( match TrueE FalseE in elimination: "P ⟹ _" for P ⇒ ‹ match TrueI in P ⇒ ‹succeed›, insert elimination [OF TrueI TrueI] › )
TrueE, resulting in
True ⟹ ?P ⟹ ?P and
True. The inner
match succeeds, since
elimination [OF TrueI TrueI] is inserted, which is
Now consider the following variant of the above code, which has an invocation of
lemma triviality: shows True by ( match TrueE FalseE in elimination: "P ⟹ _" for P ⇒ ‹ match TrueI in P ⇒ ‹succeed›, insert elimination [OF TrueI TrueI] ›, fail )
After the activities described above,
fail triggers backtracking. The outer
FalseE, resulting in
False ⟹ ?P and
False. The inner
match should now fail, causing the whole proof to fail.
However, that is not what happens. Instead, I get the following output:
exception THM 0 raised (line 309 of "drule.ML"): OF: no unifiers False ⟹ ?P7 True True
Apparently, what happens is the following: After backtracking, the inner
match is not re-executed, perhaps because it doesn’t depend on
elimination and its dependence on
P erroneously isn’t taken into account. As a result, Isabelle attempts to execute
insert elimination [OF TrueI TrueI], which has to fail as
False as its sole premise.
Is this really a bug or have I overlooked something?
I am not an expert in that area, but it also seems strange to me. I think this is something that you should post on the mailing list
I’ll report this as a bug to the developers.
Wolfgang Jeltsch has marked this topic as unresolved.
Wolfgang Jeltsch has marked this topic as resolved.
Last updated: Dec 07 2023 at 08:19 UTC