Prove a recursive function in Isabelle

Question

I have defined the following recursive function:

primrec span :: "('a ⇒ bool) ⇒ 'a list ⇒ 'a list * 'a list" where
"span P [] = ([], [])"
| "span P (x#xs) = 
  (let (ys, zs) = span P xs in 
   if P x then (x#ys, zs) else (ys, x#zs))"

which splits a list into two sublists by a filter p and insert x in the middle.
Now I would like to prove the following lemma:

lemma invariant_length:
shows "length (fst (span P l)) + length (snd (span P l)) = length l"

I did the proof by induction

lemma invariant_length:
shows "length (fst (span P l)) + length (snd (span P l)) = length l"
proof (induction l)
case Nil
  then show ?case by auto
next
  case (Cons a l)
  show ?case
  proof(cases "P a")
    case True
    then have "span P (a # l) = (a # fst (span P l), snd (span P l))"
      by [where I stuck]
    then have "length (fst (span P (a # l))) + length (snd (span P (a # l))) 
               = length (a # fst (span P l)) + length(snd (span P l)) " 
      by simp
    then have "length (fst (span P (a # l))) + length (snd (span P (a # l))) 
               = Suc(length (fst (span P l))) + length(snd (span P l)) " 
      by simp
    with Cons have "length (fst (span P (a # l))) + length (snd (span P (a # l))) = Suc (length l)" 
      by simp
    then show ?thesis by simp
  next
    case False
        then have "span P (a # l) = (fst (span P l), a # snd (span P l))"
      by [where I stuck]
    then have "length (fst (span P (a # l))) + length (snd (span P (a # l))) 
               = length (fst (span P l)) + length(a # snd (span P l)) " 
      by simp
    then have "length (fst (span P (a # l))) + length (snd (span P (a # l))) 
               = length (fst (span P l)) + Suc(length(snd (span P l)))" 
      by simp
    with Cons have "length (fst (span P (a # l))) + length (snd (span P (a # l))) = Suc (length l)" 
      by simp
    then show ?thesis by simp
  qed
qed

I stuck at the first step of the two cases during the inductive step, where I have marked as [where I stuck]. I tried using auto or simp here but Isabelle says

Failed to finish proof⌂:
goal (1 subgoal):
 1. P a ⟹ (case span P l of (ys, x) ⇒ (a # ys, x)) = (a # fst (span P l), snd (span P l))

How can I proceed here?

Answer 1

lemma invariant_length:
  "length (fst (span P l)) + length (snd (span P l)) = length l"
  by (induction l; simp add: prod.case_eq_if)