theory Sep_Fold

lemma sep_factor_foldI:
  "(R' \<and>* (sep_fold P Q R xs)) s \<Longrightarrow>
   sep_fold (\<lambda>x. R' \<and>* P x) (\<lambda>x. R' \<and>* Q x) (R' \<and>* R) xs s" apply (induct xs arbitrary: s; clarsimp simp: sep_fold_def) apply (clarsimp simp: sep_conj_ac) apply (erule (1) sep_conj_impl) apply (erule (1) sep_conj_impl) apply (erule sep_conj_sep_impl) apply (clarsimp simp: sep_conj_ac) apply (drule (1) sep_conj_impl) apply (subst (asm) sep_conj_commute, erule (1) sep_conj_sep_impl2) by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (R' \<and>* \<lparr>{P} \<and>* {Q} \<longrightarrow>* {R}\<rparr> xs) s \<Longrightarrow> \<lparr>{\<lambda>x. R' \<and>* P x} \<and>* {\<lambda>x. R' \<and>* Q x} \<longrightarrow>* {R' \<and>* R}\<rparr> xs s proof (prove)
goal (1 subgoal):
 1. \<And>a xs s. \<lbrakk>\<And>s. (R' \<and>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R) s \<Longrightarrow> foldr (\<lambda>x R. (R' \<and>* P x) \<and>* (R' \<and>* Q x \<longrightarrow>* R)) xs (R' \<and>* R) s; (R' \<and>* P a \<and>* (Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R)) s\<rbrakk> \<Longrightarrow> ((R' \<and>* P a) \<and>* (R' \<and>* Q a \<longrightarrow>* foldr (\<lambda>x R. (R' \<and>* P x) \<and>* (R' \<and>* Q x \<longrightarrow>* R)) xs (R' \<and>* R))) s proof (prove)
goal (1 subgoal):
 1. \<And>a xs s. \<lbrakk>\<And>s. (R' \<and>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R) s \<Longrightarrow> foldr (\<lambda>x R. R' \<and>* P x \<and>* (R' \<and>* Q x \<longrightarrow>* R)) xs (R \<and>* R') s; (R' \<and>* P a \<and>* (Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R)) s\<rbrakk> \<Longrightarrow> (R' \<and>* P a \<and>* (R' \<and>* Q a \<longrightarrow>* foldr (\<lambda>x R. R' \<and>* P x \<and>* (R' \<and>* Q x \<longrightarrow>* R)) xs (R \<and>* R'))) s proof (prove)
goal (1 subgoal):
 1. \<And>a xs s h. \<lbrakk>\<And>s. (R' \<and>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R) s \<Longrightarrow> foldr (\<lambda>x R. R' \<and>* P x \<and>* (R' \<and>* Q x \<longrightarrow>* R)) xs (R \<and>* R') s; (P a \<and>* (Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R)) h\<rbrakk> \<Longrightarrow> (P a \<and>* (R' \<and>* Q a \<longrightarrow>* foldr (\<lambda>x R. R' \<and>* P x \<and>* (R' \<and>* Q x \<longrightarrow>* R)) xs (R \<and>* R'))) h proof (prove)
goal (1 subgoal):
 1. \<And>a xs s h ha. \<lbrakk>\<And>s. (R' \<and>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R) s \<Longrightarrow> foldr (\<lambda>x R. R' \<and>* P x \<and>* (R' \<and>* Q x \<longrightarrow>* R)) xs (R \<and>* R') s; (Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R) ha\<rbrakk> \<Longrightarrow> (R' \<and>* Q a \<longrightarrow>* foldr (\<lambda>x R. R' \<and>* P x \<and>* (R' \<and>* Q x \<longrightarrow>* R)) xs (R \<and>* R')) ha proof (prove)
goal (1 subgoal):
 1. \<And>a xs s h ha hb. \<lbrakk>\<And>s. (R' \<and>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R) s \<Longrightarrow> foldr (\<lambda>x R. R' \<and>* P x \<and>* (R' \<and>* Q x \<longrightarrow>* R)) xs (R \<and>* R') s; ((Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R) \<and>* R' \<and>* Q a) hb\<rbrakk> \<Longrightarrow> foldr (\<lambda>x R. R' \<and>* P x \<and>* (R' \<and>* Q x \<longrightarrow>* R)) xs (R \<and>* R') hb proof (prove)
goal (1 subgoal):
 1. \<And>a xs hb. \<lbrakk>\<And>s. (R' \<and>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R) s \<Longrightarrow> foldr (\<lambda>x R. R' \<and>* P x \<and>* (R' \<and>* Q x \<longrightarrow>* R)) xs (R \<and>* R') s; (R' \<and>* Q a \<and>* (Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R)) hb\<rbrakk> \<Longrightarrow> foldr (\<lambda>x R. R' \<and>* P x \<and>* (R' \<and>* Q x \<longrightarrow>* R)) xs (R \<and>* R') hb proof (prove)
goal (2 subgoals):
 1. \<And>a xs hb h. \<lbrakk>\<And>s. (R' \<and>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R) s \<Longrightarrow> foldr (\<lambda>x R. R' \<and>* P x \<and>* (R' \<and>* Q x \<longrightarrow>* R)) xs (R \<and>* R') s; (Q a \<and>* (Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R)) h\<rbrakk> \<Longrightarrow> ?Q'16 a xs hb h
 2. \<And>a xs hb. \<lbrakk>\<And>s. (R' \<and>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R) s \<Longrightarrow> foldr (\<lambda>x R. R' \<and>* P x \<and>* (R' \<and>* Q x \<longrightarrow>* R)) xs (R \<and>* R') s; (R' \<and>* ?Q'16 a xs hb) hb\<rbrakk> \<Longrightarrow> foldr (\<lambda>x R. R' \<and>* P x \<and>* (R' \<and>* Q x \<longrightarrow>* R)) xs (R \<and>* R') hb proof (prove)
goal (1 subgoal):
 1. \<And>a xs hb. \<lbrakk>\<And>s. (R' \<and>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R) s \<Longrightarrow> foldr (\<lambda>x R. R' \<and>* P x \<and>* (R' \<and>* Q x \<longrightarrow>* R)) xs (R \<and>* R') s; (R' \<and>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R) hb\<rbrakk> \<Longrightarrow> foldr (\<lambda>x R. R' \<and>* P x \<and>* (R' \<and>* Q x \<longrightarrow>* R)) xs (R \<and>* R') hb