伊莎贝尔语中“case _ of _”是什么意思

在读的时候这个关于商类型的答案 https://stackoverflow.com/a/67237629/14656198，我偶然发现了这个结构“case _ of _ ⇒ _”。经检查手册 https://isabelle.in.tum.de/doc/isar-ref.pdf，没有这样的定义，但是“”有单独的定义case _“（§6.5.1）和”of _“（§6.4.3）。尽管如此，阅读这些定义只会让我对这个结构的含义更加困惑。

因此，我决定提出一个我可以证明的引理的简单版本，即：

lemma test: "(case n of (0::nat,0::nat) ⇒ (a,b) = n) ⟹ a = 0 ∧ b = 0"

在我看来，在分析了上述问题的上下文之后，这个陈述应该相当于"(a,b) = (0,0) ⟹ a = 0 ∧ b = 0"，这应该是微不足道的证明。出色地，大锤不敢苟同：

"cvc4": Timed out 
"z3": Timed out 
"e": Timed out 
"spass": Timed out 
"remote_vampire": The prover gave up

所以看来我误解了这个结构的含义。

鉴于此，该声明的含义是什么“case _ of _ ⇒ _“在伊莎贝尔？

在《伊莎贝尔》中，这种类型的陈述case _ of _ ⇒ _ | _ ⇒ _ | _ ⇒ _ | ... 是模式匹配的一种形式。

您可能想看看 §2.5.4伊莎贝尔的教程 https://isabelle.in.tum.de/doc/tutorial.pdf（§2.5.5 和 §2.5.6 也很有用）。这个关于模式匹配的问题 https://stackoverflow.com/questions/2502354/what-is-pattern-matching-in-functional-languages and 维基百科文章 https://en.wikipedia.org/wiki/Pattern_matching通常可以提供有关模式匹配的更多信息。

您缺少的是不能保证模式是详尽的。如果没有模式匹配，结果是undefined.

Nitpick 实际上会在你的引理上自动找到一个反例：

Nitpicking formula... 
Kodkod warning: Interrupt 
Nitpick found a counterexample:
  Free variables:
    a = 1
    b = 0
    n = (0, 1)

让我们插回 n 的值：

lemma ‹(case (0,1) of (0::nat,0::nat) ⇒ (a,b) = n)⟹ a = 0 ∧ b = 0›
  apply simp
(*
proof (prove)
goal (1 subgoal):
 1. undefined ⟹ a = 0 ∧ b = 0
*)

编辑，回答以下问题：(case (0,1) of (0::nat,0::nat) ⇒ (a,b) = n)大致意思是[1]：

(case_prod (0,1) of 
   (0::nat,0::nat) ⇒ (a,b) = n
 | _               ⇒ undefined)

where case_prod是对的析构函数。因此，如果不匹配任何模式，结果将是不确定的。

[1]完整输出：

ML ‹@{term ‹(case (0,1) of (0::nat,0::nat) ⇒ (a,b) = n)›}›