What does "case _ of _" mean in Isabelle

Question

While reading this answer on quotient types, I stumbled upon the construct "case _ of _ ⇒ _". Upon checking the manual, there's no such definition, but there are separate definitions for "case _" (§6.5.1) and "of _" (§6.4.3). Nonetheless, reading these definitions only confused me more about the meaning of this construct.

Consequently, I decided to come up with a simpler version of the lemma that I might be able to prove, which was this one:

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

In my head, after analyzing the context of the mentioned question, this statement should be equivalent to "(a,b) = (0,0) ⟹ a = 0 ∧ b = 0", which should be trivial to prove. Well, sledgehammer begs to differ:

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

So it seems like I'm misunderstanding what this construct is meant to represent.

In light of that, what is the meaning of the statement "case _ of _ ⇒ _" in Isabelle?

Answer 1

In Isabelle, a statement of the type case _ of _ ⇒ _ | _ ⇒ _ | _ ⇒ _ | ... is a form of pattern matching.

You might want to take a look at §2.5.4 of Isabelle's tutorial (§2.5.5 and §2.5.6 are also useful). This question on pattern matching and the Wikipedia article may provide more information about pattern matching in general.

What you are missing is that there not guarantee that the patterns are exhaustive. If no pattern matches, the result is undefined.

Nitpick actually finds a counter-example automatically on your lemma:

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

Let's plugin back the value of 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
*)

EDIT, to answer the question below: (case (0,1) of (0::nat,0::nat) ⇒ (a,b) = n) means roughly [1]:

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

where case_prod is the destructor for pairs. Hence, if you don't match any of the patterns, the result is undefined.

[1] full output:

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