From c2d27da5b50150323442244054f8fd29114bd4df Mon Sep 17 00:00:00 2001 From: someplaceguy Date: Fri, 13 Sep 2024 01:33:30 +0000 Subject: [PATCH] Make Thm.SPEC use lazy_beta_conv instead of beta_conv The former, unlike the latter, avoids traversing the entire term, which can take exponentially long in certain degenerate conditions observed while replaying certain Z3 proof certificates. Unfortunately, this only fixes the issue for the standard kernel. The experimental kernel does not seem to be amenable to such a straightforward fix, as it does not seem to support closures in the term representation. Fixes #1300 --- src/thm/std-thm.ML | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/thm/std-thm.ML b/src/thm/std-thm.ML index d9f621bfa7..12c7a37046 100644 --- a/src/thm/std-thm.ML +++ b/src/thm/std-thm.ML @@ -563,7 +563,7 @@ fun SPEC t th = Assert (Name="!" andalso Thy="bool") "SPEC" "Theorem not universally quantified"; make_thm Count.Spec - (tag th, hypset th, beta_conv(mk_comb(Rand, t))) + (tag th, hypset th, lazy_beta_conv(mk_comb(Rand, t))) handle HOL_ERR _ => raise thm_err "SPEC" "Term argument's type not equal to bound variable's"