[STATEMENT]
lemma filtermap_list_all[simp]: "filtermap pred func tr = map func tr \<longleftrightarrow> list_all pred tr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Filtermap.filtermap pred func tr = map func tr) = list_all pred tr
[PROOF STEP]
proof(induction tr)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (Filtermap.filtermap pred func [] = map func []) = list_all pred []
 2. \<And>a tr. (Filtermap.filtermap pred func tr = map func tr) = list_all pred tr \<Longrightarrow> (Filtermap.filtermap pred func (a # tr) = map func (a # tr)) = list_all pred (a # tr)
[PROOF STEP]
case (Cons trn tr)
[PROOF STATE]
proof (state)
this:
(Filtermap.filtermap pred func tr = map func tr) = list_all pred tr

goal (2 subgoals):
 1. (Filtermap.filtermap pred func [] = map func []) = list_all pred []
 2. \<And>a tr. (Filtermap.filtermap pred func tr = map func tr) = list_all pred tr \<Longrightarrow> (Filtermap.filtermap pred func (a # tr) = map func (a # tr)) = list_all pred (a # tr)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(Filtermap.filtermap pred func tr = map func tr) = list_all pred tr

goal (1 subgoal):
 1. (Filtermap.filtermap pred func (trn # tr) = map func (trn # tr)) = list_all pred (trn # tr)
[PROOF STEP]
apply (cases "pred trn")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(Filtermap.filtermap pred func tr = map func tr) = list_all pred tr; pred trn\<rbrakk> \<Longrightarrow> (Filtermap.filtermap pred func (trn # tr) = map func (trn # tr)) = list_all pred (trn # tr)
 2. \<lbrakk>(Filtermap.filtermap pred func tr = map func tr) = list_all pred tr; \<not> pred trn\<rbrakk> \<Longrightarrow> (Filtermap.filtermap pred func (trn # tr) = map func (trn # tr)) = list_all pred (trn # tr)
[PROOF STEP]
by (simp_all) (metis impossible_Cons length_filtermap length_map)
[PROOF STATE]
proof (state)
this:
(Filtermap.filtermap pred func (trn # tr) = map func (trn # tr)) = list_all pred (trn # tr)

goal (1 subgoal):
 1. (Filtermap.filtermap pred func [] = map func []) = list_all pred []
[PROOF STEP]
qed auto