kings-crown/FVELER_Isabelle huggingface dataset:
theory Extended_Separation_Algebra

lemma sep_elsewhereD:
  "(P -* sep_true) s \<Longrightarrow> (P \<longrightarrow>* (P \<leadsto>* R)) s \<Longrightarrow> R s" apply (drule (1) septract_sep_wand, simp add: pred_conj_def) using sep_septraction_snake by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P -* (\<lambda>s. True)) s; (P \<longrightarrow>* (P \<leadsto>* R)) s\<rbrakk> \<Longrightarrow> R s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P \<longrightarrow>* (P \<leadsto>* R)) s; (P -* (P \<leadsto>* R)) s\<rbrakk> \<Longrightarrow> R s proof (prove)
using this:
\<lbrakk>(?P -* ?Q) ?s; \<And>s. ?Q s \<Longrightarrow> (?P \<leadsto>* ?Q') s\<rbrakk> \<Longrightarrow> ?Q' ?s

goal (1 subgoal):
 1. \<lbrakk>(P \<longrightarrow>* (P \<leadsto>* R)) s; (P -* (P \<leadsto>* R)) s\<rbrakk> \<Longrightarrow> R s
theory Extended_Separation_Algebra

lemma sep_conj_coimplI:
  "(Q \<leadsto>* R) s \<Longrightarrow>  ((P \<and>* Q) \<leadsto>* (P -* R)) s  " by (metis sep_coimpl_def sep_coimpl_def' sep_conj_commuteI sep_mp_frame septraction_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (Q \<leadsto>* R) s \<Longrightarrow> (P \<and>* Q \<leadsto>* P -* R) s
theory Extended_Separation_Algebra

lemma sep_conj_septract_curry:
  "((P \<and>* Q) -* R) s \<Longrightarrow>  (P -* (Q -* R)) s" by (smt sep_antimp' sep_conj_coimplI sep_septraction_snake)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<and>* Q -* R) s \<Longrightarrow> (P -* (Q -* R)) s
theory Extended_Separation_Algebra

lemma sep_snake_boxI:
  "Q s \<Longrightarrow> (\<box> \<leadsto>* Q) s" by (simp add: pred_neg_def sep_coimpl_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Q s \<Longrightarrow> (\<box> \<leadsto>* Q) s
theory Extended_Separation_Algebra

lemma sep_snake_boxD:
  "(Q \<leadsto>* \<box>) s \<Longrightarrow> ((Q \<leadsto>* sep_false) or Q) s" apply (simp only: pred_disj_def) apply (safe) using Sep_Cancel_Set.sep_conj_empty' sep_coimpl_cancel by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (Q \<leadsto>* \<box>) s \<Longrightarrow> ((Q \<leadsto>* (\<lambda>s. False)) or Q) s proof (prove)
goal (1 subgoal):
 1. (Q \<leadsto>* \<box>) s \<Longrightarrow> (Q \<leadsto>* (\<lambda>s. False)) s \<or> Q s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(Q \<leadsto>* \<box>) s; \<not> Q s\<rbrakk> \<Longrightarrow> (Q \<leadsto>* (\<lambda>s. False)) s proof (prove)
using this:
(?P \<and>* \<box>) ?s \<Longrightarrow> ?P ?s
\<lbrakk>(?P \<leadsto>* ?Q) ?s; (?P \<and>* ?Q) ?s \<Longrightarrow> (?P \<leadsto>* ?Q') ?s\<rbrakk> \<Longrightarrow> (?P \<leadsto>* ?Q') ?s

goal (1 subgoal):
 1. \<lbrakk>(Q \<leadsto>* \<box>) s; \<not> Q s\<rbrakk> \<Longrightarrow> (Q \<leadsto>* (\<lambda>s. False)) s
theory Extended_Separation_Algebra

lemma septract_wandD:
  "(( R \<longrightarrow>* (not Q)) -* Q) s \<Longrightarrow> (not R) s" apply (erule sep_septraction_snake) using sep_antimp_contrapos by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((R \<longrightarrow>* not Q) -* Q) s \<Longrightarrow> (not R) s proof (prove)
goal (1 subgoal):
 1. \<And>s. Q s \<Longrightarrow> (R \<longrightarrow>* not Q \<leadsto>* not R) s proof (prove)
using this:
?R ?s \<Longrightarrow> (?P \<longrightarrow>* not ?R \<leadsto>* not ?P) ?s

goal (1 subgoal):
 1. \<And>s. Q s \<Longrightarrow> (R \<longrightarrow>* not Q \<leadsto>* not R) s
theory Extended_Separation_Algebra

lemma sep_neg_impl:
  "(not (R \<longrightarrow>* Q)) = (R -* (not Q)) " apply (clarsimp simp: pred_neg_def septraction_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (not (R \<longrightarrow>* Q)) = (R -* not Q) proof (prove)
goal:
No subgoals!
theory Extended_Separation_Algebra

lemma sep_coimpl_notempty:
  "(Q \<leadsto>* (not \<box>)) s \<Longrightarrow> (not Q) s" apply (clarsimp simp: sep_coimpl_def pred_neg_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (Q \<leadsto>* not \<box>) s \<Longrightarrow> (not Q) s proof (prove)
goal:
No subgoals!
theory Extended_Separation_Algebra

lemma septract_empty_empty:
  "(P -* \<box>) s \<Longrightarrow> \<box> (s :: 'a :: cancellative_sep_algebra)" apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def sep_empty_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P -* \<box>) s \<Longrightarrow> \<box> s proof (prove)
goal:
No subgoals!
theory Extended_Separation_Algebra

lemma septract_trivial:
  "P s \<Longrightarrow> (sep_true -* P) s" apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def sep_empty_def) using sep_disj_zero by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P s \<Longrightarrow> ((\<lambda>s. True) -* P) s proof (prove)
goal (1 subgoal):
 1. P s \<Longrightarrow> \<exists>h'. s ## h' \<and> P (s + h') proof (prove)
using this:
?x ## (0::?'a)

goal (1 subgoal):
 1. P s \<Longrightarrow> \<exists>h'. s ## h' \<and> P (s + h')
theory Extended_Separation_Algebra

lemma sep_empty_and_conj:
  "\<box> s \<Longrightarrow> (P \<and>* Q) s \<Longrightarrow> P (s :: 'a :: cancellative_sep_algebra)" by (metis sep_conj_def sep_disj_positive_zero sep_empty_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<box> s; (P \<and>* Q) s\<rbrakk> \<Longrightarrow> P s
theory Extended_Separation_Algebra

lemma sep_conj_coimpl_mp:
  "(P \<and>* R) s \<Longrightarrow> (P \<leadsto>* Q) s \<Longrightarrow> (P \<and>* (Q and R)) s" apply (drule (2) sep_coimpl_mp_gen, clarsimp simp: pred_conj_def conj_commute) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P \<and>* R) s; (P \<leadsto>* Q) s\<rbrakk> \<Longrightarrow> (P \<and>* (Q and R)) s proof (prove)
goal:
No subgoals!
theory Extended_Separation_Algebra

lemma sep_conj_coimpl_contrapos_mp:
  "(P \<and>* Q) s \<Longrightarrow> (R \<leadsto>* (not Q)) s \<Longrightarrow> (Q \<and>* (P and (not R))) s" apply (subst (asm) sep_coimpl_contrapos) apply (clarsimp simp: pred_neg_def) apply (sep_drule (direct) sep_conj_coimpl_mp[where P=Q], assumption) apply (clarsimp simp: pred_conj_def conj_commute) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P \<and>* Q) s; (R \<leadsto>* not Q) s\<rbrakk> \<Longrightarrow> (Q \<and>* (P and not R)) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P \<and>* Q) s; (not not Q \<leadsto>* not R) s\<rbrakk> \<Longrightarrow> (Q \<and>* (P and not R)) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P \<and>* Q) s; (Q \<leadsto>* (\<lambda>x. \<not> R x)) s\<rbrakk> \<Longrightarrow> (Q \<and>* (P and (\<lambda>x. \<not> R x))) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(Q \<leadsto>* (\<lambda>x. \<not> R x)) s; (Q \<and>* ((\<lambda>x. \<not> R x) and P)) s\<rbrakk> \<Longrightarrow> (Q \<and>* (P and (\<lambda>x. \<not> R x))) s proof (prove)
goal:
No subgoals!
theory Sep_Forward

lemma sep_conj_sep_impl_spec:
  "\<lbrakk>((Q -* R) \<and>* P) h; \<And>h. (Q -* R) h \<Longrightarrow> (P \<longrightarrow>* R') h\<rbrakk> \<Longrightarrow> R' h" by (metis (full_types) sep_conj_sep_impl2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((Q -* R) \<and>* P) h; \<And>h. (Q -* R) h \<Longrightarrow> (P \<longrightarrow>* R') h\<rbrakk> \<Longrightarrow> R' h
theory Sep_Forward

lemma sep_conj_coimpl_cancel'':
  "(\<And>s. pred_imp P Q s) \<Longrightarrow> (P \<and>* R) s \<Longrightarrow>  precise Q \<Longrightarrow>
   (\<And>s. R s \<Longrightarrow> R' s) \<Longrightarrow> (Q \<leadsto>* R') s" by (simp add: sep_conj_coimpl_cancel')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. P s \<longrightarrow> Q s; (P \<and>* R) s; precise Q; \<And>s. R s \<Longrightarrow> R' s\<rbrakk> \<Longrightarrow> (Q \<leadsto>* R') s
theory Sep_Forward

lemma sep_conj_coimpl_cancel''':
  "(\<And>s. pred_imp Q P s) \<Longrightarrow> (P \<and>* R) s  \<Longrightarrow> precise P \<Longrightarrow>
   (\<And>s. R s \<Longrightarrow> R' s) \<Longrightarrow> (Q \<leadsto>* R') s" by (simp add: sep_conj_coimpl_cancel)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. Q s \<longrightarrow> P s; (P \<and>* R) s; precise P; \<And>s. R s \<Longrightarrow> R' s\<rbrakk> \<Longrightarrow> (Q \<leadsto>* R') s
theory Sep_Forward

lemma sep_coimpl_cancel':
  "(\<And>s. pred_imp Q P s) \<Longrightarrow> (P \<leadsto>* R) s   \<Longrightarrow>
   (\<And>s. R s \<Longrightarrow> R' s) \<Longrightarrow> (Q \<leadsto>* R') s" by (metis sep_coimpl_weaken sep_snake_septraction septraction_snake_trivial)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. Q s \<longrightarrow> P s; (P \<leadsto>* R) s; \<And>s. R s \<Longrightarrow> R' s\<rbrakk> \<Longrightarrow> (Q \<leadsto>* R') s
theory Sep_Forward

lemma sep_conj_pointer_coimpl_cancel:
  "(P x \<and>* R) s  \<Longrightarrow> pointer P \<Longrightarrow>
   (\<And>s. R s \<Longrightarrow> y = x \<Longrightarrow>  R'  s) \<Longrightarrow> (P y \<leadsto>* R') s" apply (clarsimp simp: pointer_def) apply (erule_tac x=x in allE) apply (erule_tac x=y in allE) apply (erule_tac x=s in allE) apply (erule_tac x=R in allE) apply (clarsimp simp: pred_conj_def) apply (erule sep_coimpl_cancel'[rotated]; simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P x \<and>* R) s; pointer P; \<And>s. \<lbrakk>R s; y = x\<rbrakk> \<Longrightarrow> R' s\<rbrakk> \<Longrightarrow> (P y \<leadsto>* R') s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P x \<and>* R) s; \<forall>x y s R. (P x \<and>* R) s \<longrightarrow> (P y \<leadsto>* R and (\<lambda>s. x = y)) s; \<And>s. \<lbrakk>R s; y = x\<rbrakk> \<Longrightarrow> R' s\<rbrakk> \<Longrightarrow> (P y \<leadsto>* R') s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P x \<and>* R) s; \<And>s. \<lbrakk>R s; y = x\<rbrakk> \<Longrightarrow> R' s; \<forall>y s R. (P x \<and>* R) s \<longrightarrow> (P y \<leadsto>* R and (\<lambda>s. x = y)) s\<rbrakk> \<Longrightarrow> (P y \<leadsto>* R') s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P x \<and>* R) s; \<And>s. \<lbrakk>R s; y = x\<rbrakk> \<Longrightarrow> R' s; \<forall>s R. (P x \<and>* R) s \<longrightarrow> (P y \<leadsto>* R and (\<lambda>s. x = y)) s\<rbrakk> \<Longrightarrow> (P y \<leadsto>* R') s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P x \<and>* R) s; \<And>s. \<lbrakk>R s; y = x\<rbrakk> \<Longrightarrow> R' s; \<forall>R. (P x \<and>* R) s \<longrightarrow> (P y \<leadsto>* R and (\<lambda>s. x = y)) s\<rbrakk> \<Longrightarrow> (P y \<leadsto>* R') s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P x \<and>* R) s; \<And>s. \<lbrakk>R s; y = x\<rbrakk> \<Longrightarrow> R' s; (P x \<and>* R) s \<longrightarrow> (P y \<leadsto>* R and (\<lambda>s. x = y)) s\<rbrakk> \<Longrightarrow> (P y \<leadsto>* R') s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P x \<and>* R) s; \<And>s. \<lbrakk>R s; y = x\<rbrakk> \<Longrightarrow> R' s; (P y \<leadsto>* (\<lambda>xa. R xa \<and> x = y)) s\<rbrakk> \<Longrightarrow> (P y \<leadsto>* R') s proof (prove)
goal:
No subgoals!
theory Sep_Forward

lemma septract_impl_cancel: "(P -* Q) s  \<Longrightarrow> (\<And>s. Q s \<Longrightarrow> Q' s) \<Longrightarrow> strictly_exact P \<Longrightarrow> (P \<longrightarrow>* Q') s" apply (clarsimp simp: septraction_def sep_impl_def pred_neg_def strictly_exact_def) by (fastforce)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P -* Q) s; \<And>s. Q s \<Longrightarrow> Q' s; strictly_exact P\<rbrakk> \<Longrightarrow> (P \<longrightarrow>* Q') s proof (prove)
goal (1 subgoal):
 1. \<And>h' h'a. \<lbrakk>\<And>s. Q s \<Longrightarrow> Q' s; \<forall>h h'. P h \<and> P h' \<longrightarrow> h = h'; s ## h'; P h'; Q (s + h'); s ## h'a; P h'a\<rbrakk> \<Longrightarrow> Q' (s + h'a)
theory Sep_Forward

lemma septract_mp: "\<lbrakk>(R' \<and>* (R' -* R)) s; \<And>s. R s \<Longrightarrow> (R' \<and>* (R' \<longrightarrow>* R)) s; precise R'\<rbrakk> \<Longrightarrow> R s" apply (sep_invert) apply (atomize, erule allE, drule (1) mp) using precise_conj_coimpl by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(R' \<and>* (R' -* R)) s; \<And>s. R s \<Longrightarrow> (R' \<and>* (R' \<longrightarrow>* R)) s; precise R'\<rbrakk> \<Longrightarrow> R s proof (prove)
goal (1 subgoal):
 1. \<And>h s. \<lbrakk>\<And>s. R s \<Longrightarrow> (R' \<and>* (R' \<longrightarrow>* R)) s; precise R'; R s\<rbrakk> \<Longrightarrow> (R' \<leadsto>* R' \<longrightarrow>* R) s proof (prove)
goal (1 subgoal):
 1. \<And>h s. \<lbrakk>precise R'; R s; (R' \<and>* (R' \<longrightarrow>* R)) s\<rbrakk> \<Longrightarrow> (R' \<leadsto>* R' \<longrightarrow>* R) s proof (prove)
using this:
precise ?P \<Longrightarrow> \<forall>s R. (?P \<and>* R) s \<longrightarrow> (?P \<leadsto>* R) s

goal (1 subgoal):
 1. \<And>h s. \<lbrakk>precise R'; R s; (R' \<and>* (R' \<longrightarrow>* R)) s\<rbrakk> \<Longrightarrow> (R' \<leadsto>* R' \<longrightarrow>* R) s
theory Sep_Fold_Cancel

lemma sep_fold_cong1: "(\<And>x s. P x s = P' x s) \<Longrightarrow> sep_fold P Q R xs s \<Longrightarrow> sep_fold P' Q R xs s" apply (induct xs arbitrary: s; clarsimp simp: sep_fold_def) apply (erule sep_conj_impl, fastforce) apply (sep_cancel, sep_mp) by (clarsimp)

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

lemma sep_fold_cong2: "(\<And>x s. Q x s = Q' x s) \<Longrightarrow> sep_fold P Q R xs s \<Longrightarrow> sep_fold P Q' R xs s" apply (induct xs arbitrary: s; clarsimp simp: sep_fold_def) apply (erule sep_conj_impl, fastforce) apply (sep_cancel) apply (sep_drule (direct) sep_mp_gen) by (clarsimp)

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

lemma sep_fold_cong3: "(\<And> s. R s = R' s) \<Longrightarrow> sep_fold P Q R xs s \<Longrightarrow> sep_fold P Q R' xs s" apply (induct xs arbitrary: s; clarsimp simp: sep_fold_def) apply (erule sep_conj_impl, fastforce) apply (sep_cancel) apply (sep_drule (direct) sep_mp_gen) by (clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. R s = 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 (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 = 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 h. \<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 = R' s; (Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R) h\<rbrakk> \<Longrightarrow> (Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R') h proof (prove)
goal (1 subgoal):
 1. \<And>a xs s h sa. \<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 = R' s; ((Q a \<longrightarrow>* foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R) \<and>* Q a) sa\<rbrakk> \<Longrightarrow> foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R' sa proof (prove)
goal (2 subgoals):
 1. \<And>a xs s h 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 = R' s; Q a sb\<rbrakk> \<Longrightarrow> Q a sb
 2. \<And>a xs s h sa. \<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 = R' s; foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R sa\<rbrakk> \<Longrightarrow> foldr (\<lambda>x R. P x \<and>* (Q x \<longrightarrow>* R)) xs R' sa
theory Sep_Fold_Cancel

lemma sep_factor_foldI__:
  "(\<And>* map P xs \<and>* foldr (\<lambda>x R. Q x \<longrightarrow>* R) xs R) s \<Longrightarrow> sep_fold P Q R xs s" apply (clarsimp simp: sep_fold_def) apply (induct xs arbitrary: s; clarsimp) apply sep_cancel+ apply sep_mp apply (clarsimp simp: sep_conj_ac) done

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