theory Scratch
imports Main
begin
primrec (nonexhaustive) head :: "'a list => 'a" where "head (v # _) = v"
primrec (nonexhaustive) tail :: "'a list => 'a list" where "tail (_ # x) = x"
theorem "x ~= [] ==> x = head x # tail x"
apply (cases x)
by simp_all
end