我想证明以下Isabelle/HOL定理：
lemma involution:
"∀P h. (∀x. ¬P x ⟶ P (h x)) ⟶ (∃x. P x ∧ P (h (h x)))"
但到目前为止，我还没有找到正确的推理规则来证明它。我相信它直接来自于推理规则的应用，因为metis可以琐碎地证明它。
我的校对脚本只有以下内容：
apply (rule allI; rename_tac P; rule allI; rename_tac h; rule impI)
apply (rule exI; rule conjI)
留给我的目标是：
proof (prove)
goal (2 subgoals):
- ⋀P h. ∀x. ¬ P x ⟶ P (h x) ⟹
P (?x17 P h)
- ⋀P h. ∀x. ¬ P x ⟶ P (h x) ⟹
P (h (h (?x17 P h)))
在那之后，我对如何继续感到困惑。我可能需要援引被排除在外的中间人的法律，我尝试了两者：
P x / ~ P x(P x / ~ P (h x)) / ~(P x / ~P (h x))
无效。
我比Isabelle/HOL更熟悉Coq，但即使在那里我也无法证明它(即使有P的自变量类型是有人居住的额外假设和classic公理(。
任何线索都将不胜感激。
首先，正如您已经提到的，您的引理可以通过一些Isabelle的内置证明方法进行琐碎的证明，例如Isabelle2021-1中的blast。然而，由于我想你正在寻找一个更具教学意义的答案，我将对此进行详细说明
在处理一个非琐碎结果的证明之前，通常先有一个纸笔证明草图是有用的。这是我脑海中浮现的一个(也许有一个更简单的，但出于说明的目的，我认为它就足够了(：
我的证据是根据具体情况而定的。设a为任意但固定的值。然后，下表显示了所有需要考虑的案件以及满足结论的相关证人：
Case # P a P (h a) P (h (h a)) P (h (h (h a))) P (h (h (h (h a)))) Witness
----------------------------------------------------------------------------------
1 T ? T ? ? a
2 T F -----> T ? ? a
3 T T F ---------> T ? h a
4 F -> T ? T ? h a
5 F -> T F ---------> T ? h a
6 F -> T T F -------------> T h (h a)
在上表中，T、F和?代表True、False和"3"；不在乎"虚线箭头表示具有特定值x的房屋∀x. ¬P x ⟶ P (h x)的实例化。我们的证明草图到此结束。
关于你引理的Isabelle/HOL证明，我认为有几点意见是正确的：
由于最外层的通用量词是多余的，我将从引理语句中删除它们，并使用自由变量。
*如今，
_tac策略被认为是过时的，Isabelle/Isar(即结构化(证明比apply脚本更受欢迎(除了证明的实验阶段(。有关更多详细信息，请参阅Isabelle/Isar参考手册。
现在，请在上面的证明草图的基础上，在下面找到引理的结构化证明。出于教学目的，我试图将证明分解为最基本的步骤，并在代码中包含内联注释，以帮助读者：
lemma involution:
assumes "∀x. ¬P x ⟶ P (h x)"
shows "∃x. P x ∧ P (h (h x))"
proof -
fix a (* an arbitrary but fixed value *)
show ?thesis
proof (cases "P a")
case True
then consider
("Case #1") "P (h (h a))"
| ("Case #2") "¬P (h a)"
| ("Case #3") "P (h a)" and "¬P (h (h a))"
by blast
then show ?thesis
proof cases
case "Case #1"
from ‹P a› and ‹P (h (h a))› have "P a ∧ P (h (h a))"
by (intro conjI)
then show ?thesis
by (intro exI) (* `exI` using `a` as witness *)
next
case "Case #2"
have "¬P (h a)"
by fact (* assumption of case #2 *)
moreover have "¬P (h a) ⟶ P (h (h a))"
by (rule assms [THEN spec]) (* instantiation of premise with `h a` *)
ultimately have "P (h (h a))"
by (rule rev_mp) (* modus ponens *)
(* NOTE: The three steps above can be replaced by `then have "P (h (h a))" using assms by simp` *)
from ‹P a› and ‹P (h (h a))› have "P a ∧ P (h (h a))"
by (intro conjI)
then show ?thesis
by (intro exI) (* `exI` using `a` as witness *)
next
case "Case #3"
then have "P (h (h (h a)))" (* use of shortcut explained above *)
using assms by simp (* instantiation of premise with `h (h a)` *)
from ‹P (h a)› and ‹P (h (h (h a)))› have "P (h a) ∧ P (h (h (h a)))"
by (intro conjI)
then show ?thesis
by (intro exI) (* `exI` using `h a` as witness *)
qed
next
case False (* i.e., `¬P a` *)
then have "P (h a)"
using assms by simp (* instantiation of premise with `a` *)
then consider
("Case #4") "P (h (h (h a)))"
| ("Case #5") "¬P (h (h a))"
| ("Case #6") "P (h (h a))" and "¬P (h (h (h a)))"
by blast
then show ?thesis
sorry (* proof omitted, similar to cases #1, #2, and #3 *)
qed
qed