theory Extended_Separation_Algebra

lemma conj_coimpl_precise:
  "(\<forall>s R. (P \<and>* R) s \<longrightarrow> (P \<leadsto>* R) s) \<Longrightarrow> precise P" apply (clarsimp simp: precise_def) apply (clarsimp simp: sep_substate_def) apply (rename_tac h h' z z') apply (erule_tac x="h + z" in allE) apply (erule_tac x="\<lambda>s. s= z" in allE) apply (drule mp) apply (clarsimp simp: sep_conj_def) apply (fastforce) apply (clarsimp simp: sep_coimpl_def sep_conj_def pred_neg_def) using sep_add_cancel by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s R. (P \<and>* R) s \<longrightarrow> (P \<leadsto>* R) s \<Longrightarrow> precise P proof (prove)
goal (1 subgoal):
 1. \<And>h hp hp'. \<lbrakk>\<forall>s R. (P \<and>* R) s \<longrightarrow> (P \<leadsto>* R) s; hp \<preceq> h; P hp; hp' \<preceq> h; P hp'\<rbrakk> \<Longrightarrow> hp = hp' proof (prove)
goal (1 subgoal):
 1. \<And>hp hp' z za. \<lbrakk>\<forall>s R. (P \<and>* R) s \<longrightarrow> (P \<leadsto>* R) s; P hp; P hp'; hp ## z; hp' ## za; hp' + za = hp + z\<rbrakk> \<Longrightarrow> hp = hp' proof (prove)
goal (1 subgoal):
 1. \<And>h h' z z'. \<lbrakk>\<forall>s R. (P \<and>* R) s \<longrightarrow> (P \<leadsto>* R) s; P h; P h'; h ## z; h' ## z'; h' + z' = h + z\<rbrakk> \<Longrightarrow> h = h' proof (prove)
goal (1 subgoal):
 1. \<And>h h' z z'. \<lbrakk>P h; P h'; h ## z; h' ## z'; h' + z' = h + z; \<forall>R. (P \<and>* R) (h + z) \<longrightarrow> (P \<leadsto>* R) (h + z)\<rbrakk> \<Longrightarrow> h = h' proof (prove)
goal (1 subgoal):
 1. \<And>h h' z z'. \<lbrakk>P h; P h'; h ## z; h' ## z'; h' + z' = h + z; (P \<and>* (\<lambda>s. s = z)) (h + z) \<longrightarrow> (P \<leadsto>* (\<lambda>s. s = z)) (h + z)\<rbrakk> \<Longrightarrow> h = h' proof (prove)
goal (2 subgoals):
 1. \<And>h h' z z'. \<lbrakk>P h; P h'; h ## z; h' ## z'; h' + z' = h + z\<rbrakk> \<Longrightarrow> (P \<and>* (\<lambda>s. s = z)) (h + z)
 2. \<And>h h' z z'. \<lbrakk>P h; P h'; h ## z; h' ## z'; h' + z' = h + z; (P \<leadsto>* (\<lambda>s. s = z)) (h + z)\<rbrakk> \<Longrightarrow> h = h' proof (prove)
goal (2 subgoals):
 1. \<And>h h' z z'. \<lbrakk>P h; P h'; h ## z; h' ## z'; h' + z' = h + z\<rbrakk> \<Longrightarrow> \<exists>x. x ## z \<and> h + z = x + z \<and> P x
 2. \<And>h h' z z'. \<lbrakk>P h; P h'; h ## z; h' ## z'; h' + z' = h + z; (P \<leadsto>* (\<lambda>s. s = z)) (h + z)\<rbrakk> \<Longrightarrow> h = h' proof (prove)
goal (1 subgoal):
 1. \<And>h h' z z'. \<lbrakk>P h; P h'; h ## z; h' ## z'; h' + z' = h + z; (P \<leadsto>* (\<lambda>s. s = z)) (h + z)\<rbrakk> \<Longrightarrow> h = h' proof (prove)
goal (1 subgoal):
 1. \<And>h h' z z'. \<lbrakk>P h; P h'; h ## z; h' ## z'; h' + z' = h + z; \<forall>x. P x \<longrightarrow> (\<forall>y. h + z = x + y \<longrightarrow> x ## y \<longrightarrow> y = z)\<rbrakk> \<Longrightarrow> h = h' proof (prove)
using this:
\<lbrakk>?x ## ?z; ?y ## ?z\<rbrakk> \<Longrightarrow> (?x + ?z = ?y + ?z) = (?x = ?y)

goal (1 subgoal):
 1. \<And>h h' z z'. \<lbrakk>P h; P h'; h ## z; h' ## z'; h' + z' = h + z; \<forall>x. P x \<longrightarrow> (\<forall>y. h + z = x + y \<longrightarrow> x ## y \<longrightarrow> y = z)\<rbrakk> \<Longrightarrow> h = h'