theory Separation_Algebra

lemma foldl_map_filter:
  "f (foldl f z (map P (filter t xs))) (foldl f z (map P (filter (not t) xs))) = foldl f z (map P xs)" proof (induct xs) case Nil thus ?case by clarsimp next case (Cons x xs) hence IH:
    "foldl f z (map P xs) =  f (foldl f z (map P (filter t xs))) (foldl f z (map P [x\<leftarrow>xs . \<not> t x]))" by (simp only: eq_commute) have foldl_Cons':
    "\<And>x xs. foldl f z (x # xs) = f x (foldl f z xs)" by (simp, subst foldl_absorb1[symmetric], rule refl) { assume "t x" hence ?case by (auto simp del: foldl_Cons simp add: foldl_Cons' IH ac_simps) } moreover { assume "\<not> t x" hence ?case by (auto simp del: foldl_Cons simp add: foldl_Cons' IH ac_simps) } ultimately show ?case by blast qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. foldl (\<^bold>*) \<^bold>1 (map P (filter t xs)) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) xs)) = foldl (\<^bold>*) \<^bold>1 (map P xs) proof (state)
goal (2 subgoals):
 1. foldl (\<^bold>*) \<^bold>1 (map P (filter t [])) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) [])) = foldl (\<^bold>*) \<^bold>1 (map P [])
 2. \<And>a xs. foldl (\<^bold>*) \<^bold>1 (map P (filter t xs)) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) xs)) = foldl (\<^bold>*) \<^bold>1 (map P xs) \<Longrightarrow> foldl (\<^bold>*) \<^bold>1 (map P (filter t (a # xs))) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) (a # xs))) = foldl (\<^bold>*) \<^bold>1 (map P (a # xs)) proof (state)
this:


goal (2 subgoals):
 1. foldl (\<^bold>*) \<^bold>1 (map P (filter t [])) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) [])) = foldl (\<^bold>*) \<^bold>1 (map P [])
 2. \<And>a xs. foldl (\<^bold>*) \<^bold>1 (map P (filter t xs)) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) xs)) = foldl (\<^bold>*) \<^bold>1 (map P xs) \<Longrightarrow> foldl (\<^bold>*) \<^bold>1 (map P (filter t (a # xs))) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) (a # xs))) = foldl (\<^bold>*) \<^bold>1 (map P (a # xs)) proof (prove)
goal (1 subgoal):
 1. foldl (\<^bold>*) \<^bold>1 (map P (filter t [])) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) [])) = foldl (\<^bold>*) \<^bold>1 (map P []) proof (state)
this:
foldl (\<^bold>*) \<^bold>1 (map P (filter t [])) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) [])) = foldl (\<^bold>*) \<^bold>1 (map P [])

goal (1 subgoal):
 1. \<And>a xs. foldl (\<^bold>*) \<^bold>1 (map P (filter t xs)) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) xs)) = foldl (\<^bold>*) \<^bold>1 (map P xs) \<Longrightarrow> foldl (\<^bold>*) \<^bold>1 (map P (filter t (a # xs))) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) (a # xs))) = foldl (\<^bold>*) \<^bold>1 (map P (a # xs)) proof (state)
goal (1 subgoal):
 1. \<And>a xs. foldl (\<^bold>*) \<^bold>1 (map P (filter t xs)) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) xs)) = foldl (\<^bold>*) \<^bold>1 (map P xs) \<Longrightarrow> foldl (\<^bold>*) \<^bold>1 (map P (filter t (a # xs))) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) (a # xs))) = foldl (\<^bold>*) \<^bold>1 (map P (a # xs)) proof (state)
this:
foldl (\<^bold>*) \<^bold>1 (map P (filter t xs)) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) xs)) = foldl (\<^bold>*) \<^bold>1 (map P xs)

goal (1 subgoal):
 1. \<And>a xs. foldl (\<^bold>*) \<^bold>1 (map P (filter t xs)) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) xs)) = foldl (\<^bold>*) \<^bold>1 (map P xs) \<Longrightarrow> foldl (\<^bold>*) \<^bold>1 (map P (filter t (a # xs))) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) (a # xs))) = foldl (\<^bold>*) \<^bold>1 (map P (a # xs)) proof (prove)
using this:
foldl (\<^bold>*) \<^bold>1 (map P (filter t xs)) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) xs)) = foldl (\<^bold>*) \<^bold>1 (map P xs)

goal (1 subgoal):
 1. foldl (\<^bold>*) \<^bold>1 (map P xs) = foldl (\<^bold>*) \<^bold>1 (map P (filter t xs)) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>x. \<not> t x) xs)) proof (state)
this:
foldl (\<^bold>*) \<^bold>1 (map P xs) = foldl (\<^bold>*) \<^bold>1 (map P (filter t xs)) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>x. \<not> t x) xs))

goal (1 subgoal):
 1. \<And>a xs. foldl (\<^bold>*) \<^bold>1 (map P (filter t xs)) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) xs)) = foldl (\<^bold>*) \<^bold>1 (map P xs) \<Longrightarrow> foldl (\<^bold>*) \<^bold>1 (map P (filter t (a # xs))) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) (a # xs))) = foldl (\<^bold>*) \<^bold>1 (map P (a # xs)) proof (prove)
goal (1 subgoal):
 1. \<And>x xs. foldl (\<^bold>*) \<^bold>1 (x # xs) = x \<^bold>* foldl (\<^bold>*) \<^bold>1 xs proof (state)
this:
foldl (\<^bold>*) \<^bold>1 (?x # ?xs) = ?x \<^bold>* foldl (\<^bold>*) \<^bold>1 ?xs

goal (1 subgoal):
 1. \<And>a xs. foldl (\<^bold>*) \<^bold>1 (map P (filter t xs)) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) xs)) = foldl (\<^bold>*) \<^bold>1 (map P xs) \<Longrightarrow> foldl (\<^bold>*) \<^bold>1 (map P (filter t (a # xs))) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) (a # xs))) = foldl (\<^bold>*) \<^bold>1 (map P (a # xs)) proof (state)
this:
foldl (\<^bold>*) \<^bold>1 (?x # ?xs) = ?x \<^bold>* foldl (\<^bold>*) \<^bold>1 ?xs

goal (1 subgoal):
 1. \<And>a xs. foldl (\<^bold>*) \<^bold>1 (map P (filter t xs)) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) xs)) = foldl (\<^bold>*) \<^bold>1 (map P xs) \<Longrightarrow> foldl (\<^bold>*) \<^bold>1 (map P (filter t (a # xs))) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) (a # xs))) = foldl (\<^bold>*) \<^bold>1 (map P (a # xs)) proof (state)
this:
t x

goal (1 subgoal):
 1. \<And>a xs. foldl (\<^bold>*) \<^bold>1 (map P (filter t xs)) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) xs)) = foldl (\<^bold>*) \<^bold>1 (map P xs) \<Longrightarrow> foldl (\<^bold>*) \<^bold>1 (map P (filter t (a # xs))) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) (a # xs))) = foldl (\<^bold>*) \<^bold>1 (map P (a # xs)) proof (prove)
using this:
t x

goal (1 subgoal):
 1. foldl (\<^bold>*) \<^bold>1 (map P (filter t (x # xs))) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) (x # xs))) = foldl (\<^bold>*) \<^bold>1 (map P (x # xs)) proof (state)
this:
foldl (\<^bold>*) \<^bold>1 (map P (filter t (x # xs))) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) (x # xs))) = foldl (\<^bold>*) \<^bold>1 (map P (x # xs))

goal (1 subgoal):
 1. \<And>a xs. foldl (\<^bold>*) \<^bold>1 (map P (filter t xs)) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) xs)) = foldl (\<^bold>*) \<^bold>1 (map P xs) \<Longrightarrow> foldl (\<^bold>*) \<^bold>1 (map P (filter t (a # xs))) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) (a # xs))) = foldl (\<^bold>*) \<^bold>1 (map P (a # xs)) proof (state)
this:
t x \<Longrightarrow> foldl (\<^bold>*) \<^bold>1 (map P (filter t (x # xs))) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) (x # xs))) = foldl (\<^bold>*) \<^bold>1 (map P (x # xs))

goal (1 subgoal):
 1. \<And>a xs. foldl (\<^bold>*) \<^bold>1 (map P (filter t xs)) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) xs)) = foldl (\<^bold>*) \<^bold>1 (map P xs) \<Longrightarrow> foldl (\<^bold>*) \<^bold>1 (map P (filter t (a # xs))) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) (a # xs))) = foldl (\<^bold>*) \<^bold>1 (map P (a # xs)) proof (state)
this:
t x \<Longrightarrow> foldl (\<^bold>*) \<^bold>1 (map P (filter t (x # xs))) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) (x # xs))) = foldl (\<^bold>*) \<^bold>1 (map P (x # xs))

goal (1 subgoal):
 1. \<And>a xs. foldl (\<^bold>*) \<^bold>1 (map P (filter t xs)) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) xs)) = foldl (\<^bold>*) \<^bold>1 (map P xs) \<Longrightarrow> foldl (\<^bold>*) \<^bold>1 (map P (filter t (a # xs))) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) (a # xs))) = foldl (\<^bold>*) \<^bold>1 (map P (a # xs)) proof (state)
this:
t x \<Longrightarrow> foldl (\<^bold>*) \<^bold>1 (map P (filter t (x # xs))) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) (x # xs))) = foldl (\<^bold>*) \<^bold>1 (map P (x # xs))

goal (1 subgoal):
 1. \<And>a xs. foldl (\<^bold>*) \<^bold>1 (map P (filter t xs)) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) xs)) = foldl (\<^bold>*) \<^bold>1 (map P xs) \<Longrightarrow> foldl (\<^bold>*) \<^bold>1 (map P (filter t (a # xs))) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) (a # xs))) = foldl (\<^bold>*) \<^bold>1 (map P (a # xs)) proof (state)
this:
\<not> t x

goal (1 subgoal):
 1. \<And>a xs. foldl (\<^bold>*) \<^bold>1 (map P (filter t xs)) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) xs)) = foldl (\<^bold>*) \<^bold>1 (map P xs) \<Longrightarrow> foldl (\<^bold>*) \<^bold>1 (map P (filter t (a # xs))) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) (a # xs))) = foldl (\<^bold>*) \<^bold>1 (map P (a # xs)) proof (prove)
using this:
\<not> t x

goal (1 subgoal):
 1. foldl (\<^bold>*) \<^bold>1 (map P (filter t (x # xs))) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) (x # xs))) = foldl (\<^bold>*) \<^bold>1 (map P (x # xs)) proof (state)
this:
foldl (\<^bold>*) \<^bold>1 (map P (filter t (x # xs))) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) (x # xs))) = foldl (\<^bold>*) \<^bold>1 (map P (x # xs))

goal (1 subgoal):
 1. \<And>a xs. foldl (\<^bold>*) \<^bold>1 (map P (filter t xs)) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) xs)) = foldl (\<^bold>*) \<^bold>1 (map P xs) \<Longrightarrow> foldl (\<^bold>*) \<^bold>1 (map P (filter t (a # xs))) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) (a # xs))) = foldl (\<^bold>*) \<^bold>1 (map P (a # xs)) proof (state)
this:
\<not> t x \<Longrightarrow> foldl (\<^bold>*) \<^bold>1 (map P (filter t (x # xs))) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) (x # xs))) = foldl (\<^bold>*) \<^bold>1 (map P (x # xs))

goal (1 subgoal):
 1. \<And>a xs. foldl (\<^bold>*) \<^bold>1 (map P (filter t xs)) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) xs)) = foldl (\<^bold>*) \<^bold>1 (map P xs) \<Longrightarrow> foldl (\<^bold>*) \<^bold>1 (map P (filter t (a # xs))) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) (a # xs))) = foldl (\<^bold>*) \<^bold>1 (map P (a # xs)) proof (chain)
picking this:
t x \<Longrightarrow> foldl (\<^bold>*) \<^bold>1 (map P (filter t (x # xs))) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) (x # xs))) = foldl (\<^bold>*) \<^bold>1 (map P (x # xs))
\<not> t x \<Longrightarrow> foldl (\<^bold>*) \<^bold>1 (map P (filter t (x # xs))) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) (x # xs))) = foldl (\<^bold>*) \<^bold>1 (map P (x # xs)) proof (prove)
using this:
t x \<Longrightarrow> foldl (\<^bold>*) \<^bold>1 (map P (filter t (x # xs))) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) (x # xs))) = foldl (\<^bold>*) \<^bold>1 (map P (x # xs))
\<not> t x \<Longrightarrow> foldl (\<^bold>*) \<^bold>1 (map P (filter t (x # xs))) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) (x # xs))) = foldl (\<^bold>*) \<^bold>1 (map P (x # xs))

goal (1 subgoal):
 1. foldl (\<^bold>*) \<^bold>1 (map P (filter t (x # xs))) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) (x # xs))) = foldl (\<^bold>*) \<^bold>1 (map P (x # xs)) proof (state)
this:
foldl (\<^bold>*) \<^bold>1 (map P (filter t (x # xs))) \<^bold>* foldl (\<^bold>*) \<^bold>1 (map P (filter (\<lambda>s. \<not> t s) (x # xs))) = foldl (\<^bold>*) \<^bold>1 (map P (x # xs))

goal:
No subgoals!