似乎有些归纳谓词我不了解，因为我不断遇到问题。我最近的努力是使用具体语义学书籍第5章中基于ev的归纳定义谓词来理解案例分析。
假设我在证明
lemma
shows "ev n ⟹ ev (n - 2)"
我已经尝试立即在Isabelle / HOL中启动证明，但是当我尝试或给出奇怪目标时它会抱怨：
lemma
shows "ev n ⟹ ev (n - 2)"
proof (cases)
显示：
proof (state)
goal (2 subgoals):
1. ⟦ev n; ?P⟧ ⟹ ev (n - 2)
2. ⟦ev n; ¬ ?P⟧ ⟹ ev (n - 2)
这不是我期望的。
[当我将n传递给个案时，我们改为归纳自然数的定义（请注意，其他时候它正确地对ev进行归纳，请参阅后面的示例）：
lemma
shows "ev n ⟹ ev (n - 2)"
proof (cases n)
给予：
proof (state)
goal (2 subgoals):
1. ⟦ev n; n = 0⟧ ⟹ ev (n - 2)
2. ⋀nat. ⟦ev n; n = Suc nat⟧ ⟹ ev (n - 2)
这不是我期望的。但是请注意，即使使用ev作为参数，以下DOES仍起作用（即，它在n上归纳而不是自然数）：
lemma
shows "ev n ⟹ ev (n - 2)"
proof -
assume 0: "ev n"
from this show "ev (n - 2)"
proof (cases n)
[我意识到，首先假设ev n，然后声明显示ev (n-2)一定有魔术，否则不会发生错误。
我理解规则反演的思想（通过分析可能导致这种情况的情况得出相反的事实）。对于“偶数”谓词，规则倒置为：
ev n ==> n = 0 ∨ (∃k. n = Suc (Suc k) ∧ ev k)
这基于归纳定义的谓词很有意义：
inductive ev :: "nat ⇒ bool" where
ev0: "ev 0" |
evSS: "ev n ⟹ ev (Suc (Suc n))"
但是我不明白。为什么不直接处理案件呢？或为什么此语法无效：
proof (cases ev)
或此：
proof (cases ev.case)
等
我认为关键是，从本质上讲，我不知道在处理归纳定义谓词时，是否将此归纳应用于目标或假设，而是根据教科书的写作：
规则反转的名称强调了我们在进行倒推：通过哪些规则可以证明某些给定的事实？
我假设它正在对目标应用规则倒置，因为它说“可以通过某些规则证明某些给定事实”。
此外，由于示例和结论都涉及到ev ==> ev (n-2)，因此该示例ev不能使本书整洁。
[[带有规则反演的案例分析如何真正起作用，为什么我们需要首先承担一些事情才能让Isabelle给出明智的案例分析目标？
lemma
shows "ev n ⟹ ev (n - 2)"
proof (cases)
给您：
proof (state) goal (2 subgoals): 1. ⟦ev n; ?P⟧ ⟹ ev (n - 2) 2. ⟦ev n; ¬ ?P⟧ ⟹ ev (n - 2)
因为Isabelle在ev n的真相上有所分歧，即是非是。我相信您要查找的语法是：
proof (cases rule: ev.cases)
您通过哪种方式明确告诉伊莎贝拉，它应使用哪种规则进行案例证明。
proof (cases rule: ev.cases)
我也注意到了：
apply (rule ev.cases)
有效，但我认为通过一个小例子来查看明确列出的案例会有所帮助：考虑：
lemma "ev n ⟹ ev (n - 2)"
首先检查个案定理：
thm ev.cases ⟦ev ?a; ?a = 0 ⟹ ?P; ⋀n. ⟦?a = Suc (Suc n); ev n⟧ ⟹ ?P⟧ ⟹ ?P
然后，它统一了目标，并使用原始假设和案例的所有假设来引入新目标。这就是为什么所有人中都有一个ev n。
apply (rule ev.cases)
有目标：
proof (prove) goal (3 subgoals): 1. ev n ⟹ ev ?a 2. ⟦ev n; ?a = 0⟧ ⟹ ev (n - 2) 3. ⋀na. ⟦ev n; ?a = Suc (Suc na); ev na⟧ ⟹ ev (n - 2)
您可以做简单处理，然后像往常一样进行证明。