（更新：我開始就這些了，那麼別人給我工作相當多了後一個答案，所以我繼續前進，並提出了我做了什麼
。 什麼，我想知道排在了對方的回答，這是在證明使用term ?thesis，以幫助匹配的問題就是錯誤消息。
也許在這裏我的回答增添了些許的上下文爲其他答案。）
下面，我使用!!作爲元邏輯all，而不是\<And>。
您已經進入了神祕的元邏輯與對象邏輯區域。一點理解讓事情變得不那麼神祕。
下面，我給你一個方法來展示隱藏的Trueprop函數的使用，這將帶走一些神祕感。
- 稍微解釋一下關於3純元邏輯運算符，以及它們的OTO的HOL對象的邏輯關係，
- 給3種不同形式的
lemma的，從你的，
- 其中
show ?thesis的第三種形式最終被證明引擎接受。
我不會在這裏完全分類。對我自己而言，很多時候，我完全理解所有的東西並不重要，但重要的是，我並不完全瞭解正在使用的元邏輯和對象邏輯功能的類型，它們在心臟這一切。
HOL BOOL，純支柱，和Trueprop ::（布爾=>道具），以配合到HOL純
爲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，因爲您使用-->代替==>，輸出顯示，該系列含義是類型bool，並且它被強制爲propTrueprop，如符號:@T所示。
HOL邏輯連接詞類型爲bool。例如，純的
term "op --> :: (bool => bool => bool)"
term "A --> B :: bool"
3個主要運營商：當量（==），IMP（==>），以及所有（!!）
在這裏，我確認它們的類型。 CNTL - 點擊它們將你帶到他們。對涉及的類型有一點認識，可以使錯誤信息不那麼神祕。
term "Pure.eq :: 'a => 'a => prop"
term "Pure.imp :: prop => prop => prop"
term "Pure.all :: ('a => prop) => prop"
有太多的嘗試和說這一切。有人需要爲像我這樣的邏輯新手編寫一本教科書，從Pure開始解釋Isabelle/HOL的邏輯。
道具VS布爾
自由變量是隱式的，普遍量化，這樣我就可以擺脫使用!!的。結果是該術語的類型從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
今天沒有必要再讓我的大腦受傷。我們必須做的事情中有一些微妙之處，要按照自己想要的方式向發動機提供所需的事實證據。我可以看看其他的答案，並且弄清楚更多。