Isabelle中co-inductive定义exec的code_pred证明触发MATCH异常求助

• 我定义了互归纳（co-inductive）的exec和eval。对于eval，code_pred可自动生效，但exec无法自动工作。
• 我参照tranclp示例添加了[code_pred_intro]引理（因篇幅过长省略），并使用sledgehammer生成了以下证明脚本：

proof -
  case exec
  from this show thesis by (smt (verit) exec.cases)
qed

• 证明完成后无剩余目标，但在qed步骤触发了异常：exception MATCH raised (line 359 of "pattern.ML")。
• 我尝试将证明替换为：

apply (smt (verit) exec.cases)
done

以及：

by (smt (verit) exec.cases)

但仍出现相同异常。

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