[STATEMENT]
lemma prefixes_append: 
  "prefixes (xs @ ys) = prefixes xs @ map (\<lambda>ys'. xs @ ys') (tl (prefixes ys))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prefixes (xs @ ys) = prefixes xs @ map ((@) xs) (tl (prefixes ys))
[PROOF STEP]
proof (induction xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. prefixes ([] @ ys) = prefixes [] @ map ((@) []) (tl (prefixes ys))
 2. \<And>a xs. prefixes (xs @ ys) = prefixes xs @ map ((@) xs) (tl (prefixes ys)) \<Longrightarrow> prefixes ((a # xs) @ ys) = prefixes (a # xs) @ map ((@) (a # xs)) (tl (prefixes ys))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:


goal (2 subgoals):
 1. prefixes ([] @ ys) = prefixes [] @ map ((@) []) (tl (prefixes ys))
 2. \<And>a xs. prefixes (xs @ ys) = prefixes xs @ map ((@) xs) (tl (prefixes ys)) \<Longrightarrow> prefixes ((a # xs) @ ys) = prefixes (a # xs) @ map ((@) (a # xs)) (tl (prefixes ys))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prefixes ([] @ ys) = prefixes [] @ map ((@) []) (tl (prefixes ys))
[PROOF STEP]
by (cases ys) auto
[PROOF STATE]
proof (state)
this:
prefixes ([] @ ys) = prefixes [] @ map ((@) []) (tl (prefixes ys))

goal (1 subgoal):
 1. \<And>a xs. prefixes (xs @ ys) = prefixes xs @ map ((@) xs) (tl (prefixes ys)) \<Longrightarrow> prefixes ((a # xs) @ ys) = prefixes (a # xs) @ map ((@) (a # xs)) (tl (prefixes ys))
[PROOF STEP]
qed simp_all