Re: [isabelle] Unification bound exceeded on "show"



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


> On 9 Dec 2015, at 20:23, Giuliano Losa <giuliano at losa.fr> wrote:
> 
> 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"
> 
> 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.