theory Extended_Separation_Algebra

lemma septract_cancel_eq_precise:
  "(\<forall>s. ((P -* (P \<and>* R)) s \<longrightarrow> R s)) = (\<forall>s. (P \<and>* R) s \<longrightarrow> (P \<leadsto>* R) s)" apply (rule iffI) apply (clarsimp) apply (clarsimp simp: sep_conj_def sep_impl_def septraction_def pred_neg_def sep_coimpl_def) apply (rule ccontr) apply (rename_tac x y h h') apply (erule_tac x=h' in allE) apply (clarsimp) apply (erule_tac x=h in allE) apply (clarsimp simp: sep_disj_commute) apply (erule_tac x=x in allE) apply (clarsimp) apply (erule_tac x=y in allE) apply (clarsimp) apply (fastforce simp: sep_disj_commute sep_add_commute) apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def) by (metis pred_neg_def sep_coimpl_def sep_conjI sep_conj_commuteI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<forall>s. (P -* P \<and>* R) s \<longrightarrow> R s) = (\<forall>s. (P \<and>* R) s \<longrightarrow> (P \<leadsto>* R) s) proof (prove)
goal (2 subgoals):
 1. \<forall>s. (P -* P \<and>* R) s \<longrightarrow> R s \<Longrightarrow> \<forall>s. (P \<and>* R) s \<longrightarrow> (P \<leadsto>* R) s
 2. \<forall>s. (P \<and>* R) s \<longrightarrow> (P \<leadsto>* R) s \<Longrightarrow> \<forall>s. (P -* P \<and>* R) s \<longrightarrow> R s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<forall>s. (P -* P \<and>* R) s \<longrightarrow> R s; (P \<and>* R) s\<rbrakk> \<Longrightarrow> (P \<leadsto>* R) s
 2. \<forall>s. (P \<and>* R) s \<longrightarrow> (P \<leadsto>* R) s \<Longrightarrow> \<forall>s. (P -* P \<and>* R) s \<longrightarrow> R s proof (prove)
goal (2 subgoals):
 1. \<And>x y xa ya. \<lbrakk>\<forall>s. (\<exists>h'. s ## h' \<and> P h' \<and> (\<exists>x. P x \<and> (\<exists>y. s + h' = x + y \<and> x ## y \<and> R y))) \<longrightarrow> R s; x ## y; P x; R y; P xa; x + y = xa + ya; xa ## ya\<rbrakk> \<Longrightarrow> R ya
 2. \<forall>s. (P \<and>* R) s \<longrightarrow> (P \<leadsto>* R) s \<Longrightarrow> \<forall>s. (P -* P \<and>* R) s \<longrightarrow> R s proof (prove)
goal (2 subgoals):
 1. \<And>x y xa ya. \<lbrakk>\<forall>s. (\<exists>h'. s ## h' \<and> P h' \<and> (\<exists>x. P x \<and> (\<exists>y. s + h' = x + y \<and> x ## y \<and> R y))) \<longrightarrow> R s; x ## y; P x; R y; P xa; x + y = xa + ya; xa ## ya; \<not> R ya\<rbrakk> \<Longrightarrow> False
 2. \<forall>s. (P \<and>* R) s \<longrightarrow> (P \<leadsto>* R) s \<Longrightarrow> \<forall>s. (P -* P \<and>* R) s \<longrightarrow> R s proof (prove)
goal (2 subgoals):
 1. \<And>x y h h'. \<lbrakk>\<forall>s. (\<exists>h'. s ## h' \<and> P h' \<and> (\<exists>x. P x \<and> (\<exists>y. s + h' = x + y \<and> x ## y \<and> R y))) \<longrightarrow> R s; x ## y; P x; R y; P h; x + y = h + h'; h ## h'; \<not> R h'\<rbrakk> \<Longrightarrow> False
 2. \<forall>s. (P \<and>* R) s \<longrightarrow> (P \<leadsto>* R) s \<Longrightarrow> \<forall>s. (P -* P \<and>* R) s \<longrightarrow> R s proof (prove)
goal (2 subgoals):
 1. \<And>x y h h'. \<lbrakk>x ## y; P x; R y; P h; x + y = h + h'; h ## h'; \<not> R h'; (\<exists>h'a. h' ## h'a \<and> P h'a \<and> (\<exists>x. P x \<and> (\<exists>y. h' + h'a = x + y \<and> x ## y \<and> R y))) \<longrightarrow> R h'\<rbrakk> \<Longrightarrow> False
 2. \<forall>s. (P \<and>* R) s \<longrightarrow> (P \<leadsto>* R) s \<Longrightarrow> \<forall>s. (P -* P \<and>* R) s \<longrightarrow> R s proof (prove)
goal (2 subgoals):
 1. \<And>x y h h'. \<lbrakk>x ## y; P x; R y; P h; x + y = h + h'; h ## h'; \<not> R h'; \<forall>h'a. P h'a \<longrightarrow> h' ## h'a \<longrightarrow> (\<forall>x. P x \<longrightarrow> (\<forall>y. x ## y \<longrightarrow> h' + h'a = x + y \<longrightarrow> \<not> R y))\<rbrakk> \<Longrightarrow> False
 2. \<forall>s. (P \<and>* R) s \<longrightarrow> (P \<leadsto>* R) s \<Longrightarrow> \<forall>s. (P -* P \<and>* R) s \<longrightarrow> R s proof (prove)
goal (2 subgoals):
 1. \<And>x y h h'. \<lbrakk>x ## y; P x; R y; P h; x + y = h + h'; h ## h'; \<not> R h'; P h \<longrightarrow> h' ## h \<longrightarrow> (\<forall>x. P x \<longrightarrow> (\<forall>y. x ## y \<longrightarrow> h' + h = x + y \<longrightarrow> \<not> R y))\<rbrakk> \<Longrightarrow> False
 2. \<forall>s. (P \<and>* R) s \<longrightarrow> (P \<leadsto>* R) s \<Longrightarrow> \<forall>s. (P -* P \<and>* R) s \<longrightarrow> R s proof (prove)
goal (2 subgoals):
 1. \<And>x y h h'. \<lbrakk>x ## y; P x; R y; P h; x + y = h + h'; h ## h'; \<not> R h'; \<forall>x. P x \<longrightarrow> (\<forall>y. x ## y \<longrightarrow> h' + h = x + y \<longrightarrow> \<not> R y)\<rbrakk> \<Longrightarrow> False
 2. \<forall>s. (P \<and>* R) s \<longrightarrow> (P \<leadsto>* R) s \<Longrightarrow> \<forall>s. (P -* P \<and>* R) s \<longrightarrow> R s proof (prove)
goal (2 subgoals):
 1. \<And>x y h h'. \<lbrakk>x ## y; P x; R y; P h; x + y = h + h'; h ## h'; \<not> R h'; P x \<longrightarrow> (\<forall>y. x ## y \<longrightarrow> h' + h = x + y \<longrightarrow> \<not> R y)\<rbrakk> \<Longrightarrow> False
 2. \<forall>s. (P \<and>* R) s \<longrightarrow> (P \<leadsto>* R) s \<Longrightarrow> \<forall>s. (P -* P \<and>* R) s \<longrightarrow> R s proof (prove)
goal (2 subgoals):
 1. \<And>x y h h'. \<lbrakk>x ## y; P x; R y; P h; x + y = h + h'; h ## h'; \<not> R h'; \<forall>y. x ## y \<longrightarrow> h' + h = x + y \<longrightarrow> \<not> R y\<rbrakk> \<Longrightarrow> False
 2. \<forall>s. (P \<and>* R) s \<longrightarrow> (P \<leadsto>* R) s \<Longrightarrow> \<forall>s. (P -* P \<and>* R) s \<longrightarrow> R s proof (prove)
goal (2 subgoals):
 1. \<And>x y h h'. \<lbrakk>x ## y; P x; R y; P h; x + y = h + h'; h ## h'; \<not> R h'; x ## y \<longrightarrow> h' + h = x + y \<longrightarrow> \<not> R y\<rbrakk> \<Longrightarrow> False
 2. \<forall>s. (P \<and>* R) s \<longrightarrow> (P \<leadsto>* R) s \<Longrightarrow> \<forall>s. (P -* P \<and>* R) s \<longrightarrow> R s proof (prove)
goal (2 subgoals):
 1. \<And>x y h h'. \<lbrakk>x ## y; P x; R y; P h; x + y = h + h'; h ## h'; \<not> R h'; h' + h \<noteq> h + h'\<rbrakk> \<Longrightarrow> False
 2. \<forall>s. (P \<and>* R) s \<longrightarrow> (P \<leadsto>* R) s \<Longrightarrow> \<forall>s. (P -* P \<and>* R) s \<longrightarrow> R s proof (prove)
goal (1 subgoal):
 1. \<forall>s. (P \<and>* R) s \<longrightarrow> (P \<leadsto>* R) s \<Longrightarrow> \<forall>s. (P -* P \<and>* R) s \<longrightarrow> R s proof (prove)
goal (1 subgoal):
 1. \<And>s h'. \<lbrakk>\<forall>s. (P \<and>* R) s \<longrightarrow> (P \<leadsto>* R) s; s ## h'; P h'; (P \<and>* R) (s + h')\<rbrakk> \<Longrightarrow> R s