Thm.SPEC appears to hang in certain degenerate conditions

[someplaceguy]

I've observed Thm.SPEC taking an unreasonable amount of time to complete in certain conditions experienced during the replay of a Z3 proof certificate which contains terms that, while containing a reasonable number of unique sub-terms, do cause a combinatorial explosion in the result of term_size.

The issue can be reproduced with the following artificial minimal example:

val _ = let fun f 0 t = t | f x t = f (x-1) (mk_disj(t, t)) in
  Thm.SPEC T (Thm.SPEC (f 256 T) (Thm.ASSUME ``!x y. x \/ y``)) end;

(Note: val _ = <expr> is used instead of just <expr> or val thm = <expr> to prevent the REPL from trying to print the resulting theorem, which by itself would also cause an apparent hang due to a similar but orthogonal issue affecting the pretty-printing of such degenerate theorems).

In the example above, it's the outer Thm.SPEC which appears to hang, although the remaining expression is required to reproduce the problem.

The underlying slowdown seems to occur due to Thm.SPEC calling beta_conv, which ends up traversing the entire tree of sub-terms in the conclusion of the theorem. This takes exponentially long when performed on such degenerate theorems, i.e. those which have an exponential term_size compared to the number of unique sub-terms.

A potential fix for the standard kernel might be to use lazy_beta_conv instead of beta_conv in the implementation of Thm.SPEC. The former implementation of beta reduction, unlike the latter, appears to delay the application of the reduction by creating (what appears to be) a closure in the underlying term representation.

This potential fix seems to completely solve the observed hang both in the minimal example above and also in the more realistic observed conditions experienced during the replay of the Z3 proof certificate; i.e. after applying the fix, Thm.SPEC finishes instantly instead of appearing to hang.

However, I suspect it might not be as easy to fix the experimental kernel because currently it does not seem to support such closures in the underlying term representation...