Isabelle locale内调用Sledgehammer报bad SMT term错误求解

该报错是Isabelle 2021年12月发行版的已知共性缺陷，和自定义理论与HOL内置理论重名的问题没有关联。
触发的典型报错信息如下：

"cvc4": Prover error:
exception TERM raised (line 457 of "~~/src/HOL/Tools/SMT/smt_translate.ML"): bad SMT term

该缺陷出在SMT证明链路的翻译模块：2021-12版本的翻译逻辑没有适配locale上下文的项结构，无法正确编码locale引入的固定参数、局部假设等带上下文依赖的项，因此所有依赖SMT翻译的后端证明器（cvc4、z3等Sledgehammer默认调用的求解器）都会在locale内触发上述异常，和具体选择哪个求解器无关。

• 最优方案：直接升级到Isabelle 2022及后续正式发行版。该缺陷在2022版本的SMT模块重构中已被修复，升级后locale上下文内的Sledgehammer调用逻辑和全局上下文完全一致，不需要修改已有证明脚本。
• 高性价比临时方案（无法升级版本时使用）：将需要Sledgehammer证明的目标拆分为独立的全局引理，把locale的固定参数、局部假设作为显式前提写在全局引理中，在全局上下文下调用Sledgehammer完成证明后，再回到locale内直接引用该已证的全局引理即可，不需要在locale上下文内直接触发SMT翻译流程。
• 低效率临时方案：在locale内调用Sledgehammer前手动执行interpret命令临时展开locale上下文，但该方法需要手动实例化所有locale参数，操作繁琐且容易引入额外的证明义务，非必要不使用。

内容的提问来源于stack exchange，提问作者Steven Obua