theory Sep_Fold_Cancel

lemma sep_factor_foldI'':
  "(\<And>s. R s \<Longrightarrow> (R' \<and>* (R' \<longrightarrow>* R)) s) \<Longrightarrow>
   precise R' \<Longrightarrow>
   (R' \<and>* sep_fold P Q (R' -* R) xs) s \<Longrightarrow>
   sep_fold (\<lambda>x. R' \<and>* P x) (\<lambda>x. R' \<and>* Q x) R xs s" apply (induct xs arbitrary:s; clarsimp simp: sep_fold_def) apply (erule septract_mp[where R'=R']) apply (assumption)+ apply (clarsimp simp: sep_conj_ac) apply (sep_cancel)+ apply (sep_mp) by (clarsimp simp: sep_conj_ac)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. R s \<Longrightarrow> (R' \<and>* (R' \<longrightarrow>* R)) s; precise R'; (R' \<and>* \<lparr>{P} \<and>* {Q} \<longrightarrow>* {R' -* R}\<rparr> xs) s\<rbrakk> \<Longrightarrow> \<lparr>{\<lambda>x. R' \<and>* P x} \<and>* {\<lambda>x. R' \<and>* Q x} \<longrightarrow>* {R}\<rparr> xs s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<And>s. R s \<Longrightarrow> (R' \<and>* (R' \<longrightarrow>* R)) s; precise R'; (R' \<and>* (R' -* R)) s\<rbrakk> \<Longrightarrow> R s
 2. \<And>a xs s. \<lbrakk>\<And>s. (R' \<and>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs (R' -* R)) s \<Longrightarrow> foldr (\<lambda>x R. (R' \<and>* P x) \<and>* (R' \<and>* Q x \<longrightarrow>* R)) xs R s; \<And>s. R s \<Longrightarrow> (R' \<and>* (R' \<longrightarrow>* R)) s; precise R'; (R' \<and>* P a \<and>* (Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs (R' -* 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)) s proof (prove)
goal (3 subgoals):
 1. \<And>s sa. \<lbrakk>\<And>s. R s \<Longrightarrow> (R' \<and>* (R' \<longrightarrow>* R)) s; precise R'; R sa\<rbrakk> \<Longrightarrow> (R' \<and>* (R' \<longrightarrow>* R)) sa
 2. \<And>s. \<lbrakk>\<And>s. R s \<Longrightarrow> (R' \<and>* (R' \<longrightarrow>* R)) s; precise R'\<rbrakk> \<Longrightarrow> precise R'
 3. \<And>a xs s. \<lbrakk>\<And>s. (R' \<and>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs (R' -* R)) s \<Longrightarrow> foldr (\<lambda>x R. (R' \<and>* P x) \<and>* (R' \<and>* Q x \<longrightarrow>* R)) xs R s; \<And>s. R s \<Longrightarrow> (R' \<and>* (R' \<longrightarrow>* R)) s; precise R'; (R' \<and>* P a \<and>* (Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs (R' -* 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)) 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' -* R)) s \<Longrightarrow> foldr (\<lambda>x R. (R' \<and>* P x) \<and>* (R' \<and>* Q x \<longrightarrow>* R)) xs R s; \<And>s. R s \<Longrightarrow> (R' \<and>* (R' \<longrightarrow>* R)) s; precise R'; (R' \<and>* P a \<and>* (Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs (R' -* 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)) 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' -* R)) s \<Longrightarrow> foldr (\<lambda>x R. R' \<and>* P x \<and>* (R' \<and>* Q x \<longrightarrow>* R)) xs R s; \<And>s. R s \<Longrightarrow> (R' \<and>* (R' \<longrightarrow>* R)) s; precise R'; (R' \<and>* P a \<and>* (Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs (R' -* 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)) s proof (prove)
goal (1 subgoal):
 1. \<And>a xs s sa sb sc. \<lbrakk>\<And>s. (R' \<and>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs (R' -* R)) s \<Longrightarrow> foldr (\<lambda>x R. R' \<and>* P x \<and>* (R' \<and>* Q x \<longrightarrow>* R)) xs R s; \<And>s. R s \<Longrightarrow> (R' \<and>* (R' \<longrightarrow>* R)) s; precise R'; ((Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs (R' -* R)) \<and>* R' \<and>* Q a) sc\<rbrakk> \<Longrightarrow> foldr (\<lambda>x R. R' \<and>* P x \<and>* (R' \<and>* Q x \<longrightarrow>* R)) xs R sc proof (prove)
goal (1 subgoal):
 1. \<And>a xs s sa sb sc. \<lbrakk>\<And>s. (R' \<and>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs (R' -* R)) s \<Longrightarrow> foldr (\<lambda>x R. R' \<and>* P x \<and>* (R' \<and>* Q x \<longrightarrow>* R)) xs R s; \<And>s. R s \<Longrightarrow> (R' \<and>* (R' \<longrightarrow>* R)) s; precise R'; (foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs (R' -* R) \<and>* R') sc\<rbrakk> \<Longrightarrow> foldr (\<lambda>x R. R' \<and>* P x \<and>* (R' \<and>* Q x \<longrightarrow>* R)) xs R sc