theory Extended_Separation_Algebra

lemma sep_snake_sep_impl:
  "(P \<longrightarrow>* R) s \<Longrightarrow> (\<And> s. R s \<Longrightarrow> (P \<leadsto>* sep_false) s) \<Longrightarrow> (not P \<and>* (not (P -* R))) s" apply (drule sep_impl_impl[where Q'="(P \<leadsto>* sep_false)"]) apply (atomize) apply (erule allE, drule mp, assumption) apply (assumption) apply (erule contrapos_pp) apply (clarsimp simp: sep_impl_def sep_coimpl_def sep_conj_def pred_neg_def septraction_def) apply (erule_tac x=0 in allE) apply (erule_tac x=s in allE) apply (clarsimp) apply (rule_tac x=0 in exI) apply (clarsimp) by (metis (full_types) disjoint_zero_sym sep_add_commute sep_add_zero_sym sep_disj_commuteI)

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