theory Sep_Fold_Cancel

lemma sep_fold_strengthen_final:
  "\<lbrakk>\<And>s. R s \<Longrightarrow> R' s;
    \<lparr>{P} \<and>* {Q} \<longrightarrow>* {R}\<rparr> xs s\<rbrakk>
   \<Longrightarrow> \<lparr>{P} \<and>* {Q} \<longrightarrow>* {R'}\<rparr> xs s" apply (induct xs arbitrary: s) apply (clarsimp simp: sep_fold_def) apply (clarsimp simp: sep_fold_def) apply (sep_cancel)+ apply (sep_mp) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. R s \<Longrightarrow> R' s; \<lparr>{P} \<and>* {Q} \<longrightarrow>* {R}\<rparr> xs s\<rbrakk> \<Longrightarrow> \<lparr>{P} \<and>* {Q} \<longrightarrow>* {R'}\<rparr> xs s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<And>s. R s \<Longrightarrow> R' s; \<lparr>{P} \<and>* {Q} \<longrightarrow>* {R}\<rparr> [] s\<rbrakk> \<Longrightarrow> \<lparr>{P} \<and>* {Q} \<longrightarrow>* {R'}\<rparr> [] s
 2. \<And>a xs s. \<lbrakk>\<And>s. \<lbrakk>\<And>s. R s \<Longrightarrow> R' s; \<lparr>{P} \<and>* {Q} \<longrightarrow>* {R}\<rparr> xs s\<rbrakk> \<Longrightarrow> \<lparr>{P} \<and>* {Q} \<longrightarrow>* {R'}\<rparr> xs s; \<And>s. R s \<Longrightarrow> R' s; \<lparr>{P} \<and>* {Q} \<longrightarrow>* {R}\<rparr> a # xs s\<rbrakk> \<Longrightarrow> \<lparr>{P} \<and>* {Q} \<longrightarrow>* {R'}\<rparr> a # xs s proof (prove)
goal (1 subgoal):
 1. \<And>a xs s. \<lbrakk>\<And>s. \<lbrakk>\<And>s. R s \<Longrightarrow> R' s; \<lparr>{P} \<and>* {Q} \<longrightarrow>* {R}\<rparr> xs s\<rbrakk> \<Longrightarrow> \<lparr>{P} \<and>* {Q} \<longrightarrow>* {R'}\<rparr> xs s; \<And>s. R s \<Longrightarrow> R' s; \<lparr>{P} \<and>* {Q} \<longrightarrow>* {R}\<rparr> a # xs s\<rbrakk> \<Longrightarrow> \<lparr>{P} \<and>* {Q} \<longrightarrow>* {R'}\<rparr> a # xs s proof (prove)
goal (1 subgoal):
 1. \<And>a xs s. \<lbrakk>\<And>s. foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R s \<Longrightarrow> foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R' s; \<And>s. R s \<Longrightarrow> R' s; (P a \<and>* (Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R)) s\<rbrakk> \<Longrightarrow> (P a \<and>* (Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R')) s proof (prove)
goal (1 subgoal):
 1. \<And>a xs s sa sb. \<lbrakk>\<And>s. foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R s \<Longrightarrow> foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R' s; \<And>s. R s \<Longrightarrow> R' s; ((Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R) \<and>* Q a) sb\<rbrakk> \<Longrightarrow> foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R' sb proof (prove)
goal (1 subgoal):
 1. \<And>a xs s sa sb. \<lbrakk>\<And>s. foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R s \<Longrightarrow> foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R' s; \<And>s. R s \<Longrightarrow> R' s; foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R sb\<rbrakk> \<Longrightarrow> foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R' sb proof (prove)
goal:
No subgoals!