（更新：我从这些开始，然后在我工作了很多之后其他人给出了答案，所以我继续并提出我所做的。
我想知道的是另一个答案，即term ?thesis在证明中的使用，以帮助将错误消息与问题所在的位置相匹配。
也许我在这里的回答为另一个答案增加了一点背景。）
下面，我使用!!for meta-logic all，而不是\<And>.
你进入了神秘的元逻辑与对象逻辑区域。一点点的了解会让事情变得不那么神秘。
下面，我给大家展示一下隐藏Trueprop功能的使用方法，这会带走一些谜团。
- 稍微解释一下 3 个纯元逻辑运算符，以及它们与 HOL 对象逻辑的关系，
- 给出 3 种不同形式的 your
lemma，从你的开始，
- 其中
show ?thesis第三种形式的 最终被证明引擎接受。
我在这里没有完全解决问题。对我自己来说，很多时候我完全理解一切并不重要，但重要的是我并不完全不了解正在使用的元逻辑和对象逻辑函数的类型，这是核心这一切。
HOL bool、Pure prop 和 Trueprop :: (bool => prop)，将 HOL 绑定到 Pure
该Trueprop函数的符号通常是隐藏的。您可以定义符号以查看它在输出面板中的应用位置。我notation在这里定义了一些声明：
notation (output) Trueprop ("_:@T" [1000] 999)
declare[[show_brackets=false, show_types, show_sorts=false, show_consts]]
这是 的类型Trueprop：
term "Trueprop :: bool => prop"
在您的lemma下面，因为您使用-->而不是==>，所以输出显示一系列含义是 type bool，并且它被强制转换prop为Trueprop，如符号 所示:@T。
HOL 逻辑连接词属于bool. 例如，
term "op --> :: (bool => bool => bool)"
term "A --> B :: bool"
Pure 的 3 个主要运算符：eq (==)、imp (==>) 和 all (!!)
在这里，我确认他们的类型。CNTL-单击它们将您带到它们。稍微了解所涉及的类型，可以使错误消息不那么神秘。
term "Pure.eq :: 'a => 'a => prop"
term "Pure.imp :: prop => prop => prop"
term "Pure.all :: ('a => prop) => prop"
关于这一切，有太多话要说。有人需要为像我这样的逻辑新手写一本教科书，解释 Isabelle/HOL 的逻辑，从 Pure 开始。
道具与布尔
自由变量是隐含的，普遍量化的，所以我可以摆脱使用!!. 结果是术语的类型从prop变为bool。打开类型信息有助于理解类型错误消息。
term "(!! d k l :: int. 0 < d --> ¬ 2 * k + 1 ≤ 2 * l --> 2 * l ≠ 1
--> -(2 * l) < 2 * k - 1 --> k ≤ l
--> d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)) :: prop"
term "(0 < (d::int) --> ¬ 2 * k + 1 ≤ 2 * l --> 2 * l ≠ 1
--> -(2 * l) < 2 * k - 1 --> k ≤ l
--> d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)) :: bool"
你的原创
你从?thesis ::int => int => int => bool` 开始。
declare[[show_types=false]]
lemma "!! d k l :: int. 0 < d --> ¬ 2 * k + 1 ≤ 2 * l --> 2 * l ≠ 1
--> -(2 * l) < 2 * k - 1 --> k ≤ l
--> d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)" (*
1. !!d k l. (0 < d --> ¬ 2 * k + 1 ≤ 2 * l --> 2 * l ≠ 1 -->
- (2 * l) < 2 * k - 1 --> k ≤ l -->
d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)):@T *)
proof -
fix d k l ::int
assume " ¬ 2 * k + 1 ≤ 2 * l" "k ≤ l"
then have "k = l" by simp
then have "d * (4 * l - 1) = d * (4 * k - 1) " by auto
moreover have "d * (2 * l - 2) + d * (2 * l) + d = d * (4 * l - 1)" by algebra
ultimately have "d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)" by auto
from this
term "?thesis" (*
"λd k l. 0 < d --> ¬ 2 * k + 1 ≤ 2 * l --> 2 * l ≠ 1
--> - (2 * l) < 2 * k - 1
--> k ≤ l --> d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)"
:: "int => int => int => bool" *)
show ?thesis (*
Type unification failed: Clash of types "_ => _" and "bool"
Type error in application: incompatible operand type
Operator: Trueprop :: bool => prop
Operand: ?thesis∷int => int => int => bool ::
int => int => int => bool
Coercion Inference:
Local coercion insertion on the operand failed:
No coercion known for type constructors: "fun" and "bool" *)
oops
摆脱显式使用!!
我摆脱了!!，现在我得到?thesis :: bool了 ，错误消息变成了一个非常常见的、令人沮丧的错误，“无法优化任何未决目标”。这意味着不知何故，我没有将我要达到show的目标与证明引擎视为目标的目标相匹配（我猜）。
lemma "0 < (d::int)
--> ¬ 2 * k + 1 ≤ 2 * l
--> 2 * l ≠ 1
--> - (2 * l) < 2 * k - 1 --> k ≤ l
--> d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)"
proof -
fix d k l ::int
assume " ¬ 2 * k + 1 ≤ 2 * l" "k ≤ l"
then have "k=l" by simp
then have "d * (4 * l - 1) = d * (4 * k - 1) " by auto
moreover have "d * (2 * l - 2) + d * (2 * l) + d = d * (4 * l - 1)" by algebra
ultimately have "d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)" by auto
from this
term "?thesis" (*
"0 < d --> ¬ 2 * k + 1 ≤ 2 * l --> 2 * l ≠ 1 --> - (2 * l) < 2 * k - 1
--> k ≤ l --> d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)"
:: "bool"
*)
show ?thesis (*
Failed to refine any pending goal
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
((¬ 2 * ?ka2 + 1 ≤ 2 * ?la2):@T) ==>
((?ka2 ≤ ?la2):@T) ==>
(0 < d --> ¬ 2 * k + 1 ≤ 2 * l --> 2 * l ≠ 1 --> - (2 * l) < 2 * k - 1
--> k ≤ l --> d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)):@T *)
oops
现在 ==> 代替 --> 和一个show ?thesis被接受的
现在我替换-->为==>. 的类型?thesis仍然是bool，它现在接受show ?thesis。
lemma "0 < (d::int)
==> ¬ 2 * k + 1 ≤ 2 * l
==> 2 * l ≠ 1
==> - (2 * l) < 2 * k - 1 ==> k ≤ l
==> d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)"
proof -
fix d k l ::int
assume " ¬ 2 * k + 1 ≤ 2 * l" "k ≤ l"
then have "k=l" by simp
then have "d * (4 * l - 1) = d * (4 * k - 1) " by auto
moreover have "d * (2 * l - 2) + d * (2 * l) + d = d * (4 * l - 1)" by algebra
ultimately have "d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)" by auto
from this
term "?thesis" (*
"d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)" :: "bool"*)
show ?thesis (*
goal (1 subgoal):
1. (d * ((2::int) * k - (2::int)) + d * ((2::int) * l) + d =
d * ((4::int) * k - (1::int))):@T *)
oops
今天不用再劳累我的大脑了。我们必须做的事情有一些微妙之处，以引擎想要的方式向证明引擎提供它想要的事实。我可以看看其他答案并弄清楚更多。