Skip to content

Commit

Permalink
Make Thm.SPEC use lazy_beta_conv instead of beta_conv
Browse files Browse the repository at this point in the history
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
underlying term representation.

Partially fixes HOL-Theorem-Prover#1300
  • Loading branch information
someplaceguy committed Sep 13, 2024
1 parent 7bf55e0 commit c1a43f2
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/thm/std-thm.ML
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down

0 comments on commit c1a43f2

Please sign in to comment.