问题描述
我有这个 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 森林）。
解决方法
暂无找到可以解决该程序问题的有效方法，小编努力寻找整理中！
如果你已经找到好的解决方法，欢迎将解决方案带上本链接一起发送给小编。
小编邮箱:dio#foxmail.com (将#修改为@）