How to create appropriate lemmas to prove this lemma in Isabelle?

Question

fun intersperse :: " 'a list ⇒ 'a ⇒ 'a list" where
  "intersperse (x#y#xs) a = x#(a#(intersperse (y#xs) a))"|
  "intersperse xs _ = xs"

lemma target:"map f (intersperse xs a) = intersperse (map f xs) (f a)"

The lemma seems very intuitive, but I can't get Isabelle to prove the lemma. I tried induction on xs, but the sledgehammer still can't find a proof. Then I tried adding auxiliary lemmas, all of them are easy to prove but don't help much proving target. I will list my attempts below though:

lemma intersp_1: "interspserse (xs@[y,x]) a = (intersperse (xs@[y]) a) @ [a,x]"
...done

lemma intersp_2:"map f (intersperse (xs@[b,x]) a) = (map f (intersperse (xs@[b]) a)) @ [(f a),(f x)]"
...done

lemma intersp_3: "map f (intersperse (x#y#xs) a) = (f x)#(f a)#(map f (intersperse (y#xs) a))"
...done

As a new learner of Isabelle I'm kind of stuck here. The only solution that I can currently think of is to come up with an appropriate lemma that provides enough hint to the solver. However I don't know how to "appropriately" dispart the induction step of target (after applying induction on xs) into a supplementary lemma. The induction step is

goal (1 subgoal):
 1. ⋀aa xs.
       map f (intersperse xs a) = intersperse (map f xs) (f a) ⟹
       map f (intersperse (aa # xs) a) = intersperse (map f (aa # xs)) (f a)

Any help is appreciated!

Answer 1

Here's a proof:

lemma target: "map f (intersperse xs a) = intersperse (map f xs) (f a)"
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons x xs)
  consider "xs = []" | "∃y ys. xs = y # ys" by (meson list.exhaust)
  then show ?case using Cons by (cases; auto)
qed

The key here is that intersperse (x # []) a and intersperse (x # y # ys) a match different patterns, so by considering each case separately sledgehammer can easily find a proof.

Answer 2

Here is another option: Use the specialized induction rule for intersperse:

lemma target:"map f (intersperse xs a) = intersperse (map f xs) (f a)"
  by (induct "(map f xs)" "f a" arbitrary: xs rule: intersperse.induct) auto

The rule intersperse.induct contains three cases:

1. x#y#xs
2. []
3. [v]

These can then be solved by auto since they fit the simplification rules available for the function.

Since the parameters of intersperse in the lemma are not variables, it is necessary to give them explicitly to the induct method and use arbitrary to state what the variable parts are.