Email Gateway (Aug 22 2022 at 12:01): Email Gateway (Aug 22 2022 at 12:01):From: Giuliano Losa <giuliano@losa.fr>
Hello, I encountered a proof in which the processing of "show ?thesis"
would not terminate, displaying many "Unification bound exceeded" messages.
I reduced it to the following example, where the processing of "show
"P"" does not terminate.
Could anyone explain this behavior? Is it possible to reliably avoid it?
Removing the type annotation ::"'a ⇒ 'a ⇒ 'a" in the "fix" line resolves
the problem.
However, I don't understand why.
I'm using Isabelle 2015.
Thanks,
Giuliano
theory Test
imports Main
begin
notepad begin
have "⋀ Q (f::'a ⇒ 'a ⇒ 'a) P . (⋀s. Q (f s)) ⟹ P"
proof -
fix Q and f::"'a ⇒ 'a ⇒ 'a" and P
assume "⋀ s . Q (f s)"
show "P"
signature.asc
Email Gateway (Aug 22 2022 at 12:01):From: Lawrence Paulson <lp15@cam.ac.uk>
This certainly is most peculiar. The same behaviour occurs with the latest development version. Switching off “auto quickcheck” and “auto solve direct” didn’t help (and indeed I think they are only relevant at top level anyway).
I think it may lie deep in the Isar level and is connected with matching the statement that you want to show with the conjecture you stated earlier. Replacing “show” by “have” eliminates the problem, but that is no solution: obviously you need to show your result. It also works if you first declare as follows:
declare [[unify_search_bound = 5]]
Let’s hope somebody else has a more precise diagnosis and solution.
Larry Paulson
Last updated: Nov 21 2024 at 12:39 UTC