我应该使用哪个箭头来暗示引理，目的是避免 Isabelle 中的假设子句？这种使用的后果呢？

如何解决我应该使用哪个箭头来暗示引理，目的是避免 Isabelle 中的假设子句？这种使用的后果呢？

我有这个 Isabelle/HOL 理论和 2 个引理——第一个（它的证明很好），第二个在语法上是不正确的：

theory Max_Of_Two_Integers_Real
  imports Main
    "HOL-Library.Multiset"
    "HOL-Library.Code_Target_Numeral"
    "HOL-Library.Code_Target_Nat"
    "HOL-Library.Code_Abstract_Nat"
begin

deFinition two_integer_max_case_def :: "nat ⇒ nat ⇒ nat" where
"two_integer_max_case_def a b = (case a > b of True ⇒ a | False ⇒ b)"

lemma spec_final:
  fixes a :: nat and b :: nat
  assumes "a > b" (* and "b < a" *)
  shows "two_integer_max_case_def a b = a"
  using assms by (simp add: two_integer_max_case_def_def) 

lemma spec_final_1:
  fixes a :: nat and b :: nat
  shows "a > b → two_integer_max_case_def a b = a"
  using assms by (simp add: two_integer_max_case_def_def)

在第二个引理中使用箭头有错误信息：

Inner lexical error⌂
Failed to parse prop

我的目的是避免使用引理的假设子句，并在显示子句中形成一个冗长的字符串。我应该在显示从句中使用什么箭头来表示含义？当假设被蕴涵取代时，这样的引理是否发生了变化？例如。也许有一些语义微妙之处？如果假设的内容移到 show 子句中，Isabelle 的证明可能会以不同的方式进行（需要不同的策略）？

修复条款呢？我可以将它们也移到 show 从句中吗（在先行词中形成连词？）？

我的目的是为机器学习编码引理，我认为形成一个字符串可能会更好。这只是为了方便。我的机器学习管道也可以接受多个字符串（不同字符串的 AST 森林）。