theory Sep_Forward

lemma sep_conj_coimpl_cancel: "(P \<and>* R) s \<Longrightarrow> (\<And>s. Q s \<Longrightarrow> P s) \<Longrightarrow> precise P \<Longrightarrow>
                               (\<And>s. R s \<Longrightarrow> R' s) \<Longrightarrow> (Q \<leadsto>* R') s" apply (clarsimp simp: sep_conj_def sep_coimpl_def pred_neg_def) apply (clarsimp simp: precise_def) apply (erule_tac x=s in allE) apply (erule_tac x=x in allE) apply (erule_tac x=xa in allE) apply (clarsimp, drule mp) apply (intro conjI) apply (fastforce simp: sep_substate_def) apply (fastforce simp: sep_substate_def) apply (clarsimp) by (metis sep_add_cancelD sep_add_commute sep_disj_commuteI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P \<and>* R) s; \<And>s. Q s \<Longrightarrow> P s; precise P; \<And>s. R s \<Longrightarrow> R' s\<rbrakk> \<Longrightarrow> (Q \<leadsto>* R') s proof (prove)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>\<And>s. Q s \<Longrightarrow> P s; precise P; \<And>s. R s \<Longrightarrow> R' s; x ## y; s = xa + ya; P x; R y; Q xa; x + y = xa + ya; xa ## ya\<rbrakk> \<Longrightarrow> R' ya proof (prove)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>\<And>s. Q s \<Longrightarrow> P s; \<forall>h hp hp'. hp \<preceq> h \<and> P hp \<and> hp' \<preceq> h \<and> P hp' \<longrightarrow> hp = hp'; \<And>s. R s \<Longrightarrow> R' s; x ## y; s = xa + ya; P x; R y; Q xa; x + y = xa + ya; xa ## ya\<rbrakk> \<Longrightarrow> R' ya proof (prove)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>\<And>s. Q s \<Longrightarrow> P s; \<And>s. R s \<Longrightarrow> R' s; x ## y; s = xa + ya; P x; R y; Q xa; x + y = xa + ya; xa ## ya; \<forall>hp hp'. hp \<preceq> s \<and> P hp \<and> hp' \<preceq> s \<and> P hp' \<longrightarrow> hp = hp'\<rbrakk> \<Longrightarrow> R' ya proof (prove)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>\<And>s. Q s \<Longrightarrow> P s; \<And>s. R s \<Longrightarrow> R' s; x ## y; s = xa + ya; P x; R y; Q xa; x + y = xa + ya; xa ## ya; \<forall>hp'. x \<preceq> s \<and> P x \<and> hp' \<preceq> s \<and> P hp' \<longrightarrow> x = hp'\<rbrakk> \<Longrightarrow> R' ya proof (prove)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>\<And>s. Q s \<Longrightarrow> P s; \<And>s. R s \<Longrightarrow> R' s; x ## y; s = xa + ya; P x; R y; Q xa; x + y = xa + ya; xa ## ya; x \<preceq> s \<and> P x \<and> xa \<preceq> s \<and> P xa \<longrightarrow> x = xa\<rbrakk> \<Longrightarrow> R' ya proof (prove)
goal (2 subgoals):
 1. \<And>x y xa ya. \<lbrakk>\<And>s. Q s \<Longrightarrow> P s; \<And>s. R s \<Longrightarrow> R' s; x ## y; s = xa + ya; P x; R y; Q xa; x + y = xa + ya; xa ## ya\<rbrakk> \<Longrightarrow> x \<preceq> xa + ya \<and> xa \<preceq> xa + ya
 2. \<And>x y xa ya. \<lbrakk>\<And>s. Q s \<Longrightarrow> P s; \<And>s. R s \<Longrightarrow> R' s; x ## y; s = xa + ya; P x; R y; Q xa; x + y = xa + ya; xa ## ya; x = xa\<rbrakk> \<Longrightarrow> R' ya proof (prove)
goal (3 subgoals):
 1. \<And>x y xa ya. \<lbrakk>\<And>s. Q s \<Longrightarrow> P s; \<And>s. R s \<Longrightarrow> R' s; x ## y; s = xa + ya; P x; R y; Q xa; x + y = xa + ya; xa ## ya\<rbrakk> \<Longrightarrow> x \<preceq> xa + ya
 2. \<And>x y xa ya. \<lbrakk>\<And>s. Q s \<Longrightarrow> P s; \<And>s. R s \<Longrightarrow> R' s; x ## y; s = xa + ya; P x; R y; Q xa; x + y = xa + ya; xa ## ya\<rbrakk> \<Longrightarrow> xa \<preceq> xa + ya
 3. \<And>x y xa ya. \<lbrakk>\<And>s. Q s \<Longrightarrow> P s; \<And>s. R s \<Longrightarrow> R' s; x ## y; s = xa + ya; P x; R y; Q xa; x + y = xa + ya; xa ## ya; x = xa\<rbrakk> \<Longrightarrow> R' ya proof (prove)
goal (2 subgoals):
 1. \<And>x y xa ya. \<lbrakk>\<And>s. Q s \<Longrightarrow> P s; \<And>s. R s \<Longrightarrow> R' s; x ## y; s = xa + ya; P x; R y; Q xa; x + y = xa + ya; xa ## ya\<rbrakk> \<Longrightarrow> xa \<preceq> xa + ya
 2. \<And>x y xa ya. \<lbrakk>\<And>s. Q s \<Longrightarrow> P s; \<And>s. R s \<Longrightarrow> R' s; x ## y; s = xa + ya; P x; R y; Q xa; x + y = xa + ya; xa ## ya; x = xa\<rbrakk> \<Longrightarrow> R' ya proof (prove)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>\<And>s. Q s \<Longrightarrow> P s; \<And>s. R s \<Longrightarrow> R' s; x ## y; s = xa + ya; P x; R y; Q xa; x + y = xa + ya; xa ## ya; x = xa\<rbrakk> \<Longrightarrow> R' ya proof (prove)
goal (1 subgoal):
 1. \<And>y xa ya. \<lbrakk>\<And>s. Q s \<Longrightarrow> P s; \<And>s. R s \<Longrightarrow> R' s; xa ## y; s = xa + ya; R y; Q xa; xa + y = xa + ya; xa ## ya\<rbrakk> \<Longrightarrow> R' ya