how do i do this in isabelle?

failure.thy

(* how do i do this?? *)

function simplex_count :: "int⇒int⇒int" where
  "simplex_count 0 0 = 1" | 
  "simplex_count 0 1 = 0" |
  "simplex_count 1 0 = 2" |
  "simplex_count n k = (simplex_count (n-1) k + simplex_count n (k-1))"
  sorry

lemma simplex_count_lemma:
  assumes "n simplex S" fixes k assumes "0 ≤ k" and "k ≤ n"
  shows "k d_face_count S = simplex_count n k"
sorry