theory Extended_Separation_Algebra

lemma disjointness_equiv:
  "(\<forall>P (s :: 'a :: sep_algebra). strictly_exact P \<longrightarrow> \<not>P 0 \<longrightarrow> (P \<leadsto>* (P \<leadsto>* sep_false)) s) =
   (\<forall>h :: 'a. h ## h \<longrightarrow> h = 0)" apply (rule iffI) apply (clarsimp) apply (erule_tac x="(=) h" in allE) apply (drule mp) apply (clarsimp simp: strictly_exact_def) apply (rule ccontr) apply (drule mp) apply (clarsimp) apply (erule_tac x="h + h" in allE) apply (clarsimp simp: sep_coimpl_def sep_conj_def pred_neg_def) apply (erule_tac x=h in allE, clarsimp) apply (erule_tac x=0 in allE, clarsimp) apply (clarsimp) apply (clarsimp simp: sep_coimpl_def sep_conj_def pred_neg_def strictly_exact_def) apply (erule_tac x=x in allE, erule_tac x=xa in allE, clarsimp simp: sep_empty_def) apply (erule_tac x=x in allE, clarsimp) using sep_disj_addD1 by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<forall>P s. strictly_exact P \<longrightarrow> \<not> P (0::'a) \<longrightarrow> (P \<leadsto>* (P \<leadsto>* (\<lambda>s. False))) s) = (\<forall>h. h ## h \<longrightarrow> h = (0::'a)) proof (prove)
goal (2 subgoals):
 1. \<forall>P s. strictly_exact P \<longrightarrow> \<not> P (0::'a) \<longrightarrow> (P \<leadsto>* (P \<leadsto>* (\<lambda>s. False))) s \<Longrightarrow> \<forall>h. h ## h \<longrightarrow> h = (0::'a)
 2. \<forall>h. h ## h \<longrightarrow> h = (0::'a) \<Longrightarrow> \<forall>P s. strictly_exact P \<longrightarrow> \<not> P (0::'a) \<longrightarrow> (P \<leadsto>* (P \<leadsto>* (\<lambda>s. False))) s proof (prove)
goal (2 subgoals):
 1. \<And>h. \<lbrakk>\<forall>P. strictly_exact P \<longrightarrow> \<not> P (0::'a) \<longrightarrow> (\<forall>s. (P \<leadsto>* (P \<leadsto>* (\<lambda>s. False))) s); h ## h\<rbrakk> \<Longrightarrow> h = (0::'a)
 2. \<forall>h. h ## h \<longrightarrow> h = (0::'a) \<Longrightarrow> \<forall>P s. strictly_exact P \<longrightarrow> \<not> P (0::'a) \<longrightarrow> (P \<leadsto>* (P \<leadsto>* (\<lambda>s. False))) s proof (prove)
goal (2 subgoals):
 1. \<And>h. \<lbrakk>h ## h; strictly_exact ((=) h) \<longrightarrow> h \<noteq> (0::'a) \<longrightarrow> (\<forall>s. ((=) h \<leadsto>* ((=) h \<leadsto>* (\<lambda>s. False))) s)\<rbrakk> \<Longrightarrow> h = (0::'a)
 2. \<forall>h. h ## h \<longrightarrow> h = (0::'a) \<Longrightarrow> \<forall>P s. strictly_exact P \<longrightarrow> \<not> P (0::'a) \<longrightarrow> (P \<leadsto>* (P \<leadsto>* (\<lambda>s. False))) s proof (prove)
goal (3 subgoals):
 1. \<And>h. h ## h \<Longrightarrow> strictly_exact ((=) h)
 2. \<And>h. \<lbrakk>h ## h; h \<noteq> (0::'a) \<longrightarrow> (\<forall>s. ((=) h \<leadsto>* ((=) h \<leadsto>* (\<lambda>s. False))) s)\<rbrakk> \<Longrightarrow> h = (0::'a)
 3. \<forall>h. h ## h \<longrightarrow> h = (0::'a) \<Longrightarrow> \<forall>P s. strictly_exact P \<longrightarrow> \<not> P (0::'a) \<longrightarrow> (P \<leadsto>* (P \<leadsto>* (\<lambda>s. False))) s proof (prove)
goal (2 subgoals):
 1. \<And>h. \<lbrakk>h ## h; h \<noteq> (0::'a) \<longrightarrow> (\<forall>s. ((=) h \<leadsto>* ((=) h \<leadsto>* (\<lambda>s. False))) s)\<rbrakk> \<Longrightarrow> h = (0::'a)
 2. \<forall>h. h ## h \<longrightarrow> h = (0::'a) \<Longrightarrow> \<forall>P s. strictly_exact P \<longrightarrow> \<not> P (0::'a) \<longrightarrow> (P \<leadsto>* (P \<leadsto>* (\<lambda>s. False))) s proof (prove)
goal (2 subgoals):
 1. \<And>h. \<lbrakk>h ## h; h \<noteq> (0::'a) \<longrightarrow> (\<forall>s. ((=) h \<leadsto>* ((=) h \<leadsto>* (\<lambda>s. False))) s); h \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> False
 2. \<forall>h. h ## h \<longrightarrow> h = (0::'a) \<Longrightarrow> \<forall>P s. strictly_exact P \<longrightarrow> \<not> P (0::'a) \<longrightarrow> (P \<leadsto>* (P \<leadsto>* (\<lambda>s. False))) s proof (prove)
goal (3 subgoals):
 1. \<And>h. \<lbrakk>h ## h; h \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> h \<noteq> (0::'a)
 2. \<And>h. \<lbrakk>h ## h; h \<noteq> (0::'a); \<forall>s. ((=) h \<leadsto>* ((=) h \<leadsto>* (\<lambda>s. False))) s\<rbrakk> \<Longrightarrow> False
 3. \<forall>h. h ## h \<longrightarrow> h = (0::'a) \<Longrightarrow> \<forall>P s. strictly_exact P \<longrightarrow> \<not> P (0::'a) \<longrightarrow> (P \<leadsto>* (P \<leadsto>* (\<lambda>s. False))) s proof (prove)
goal (2 subgoals):
 1. \<And>h. \<lbrakk>h ## h; h \<noteq> (0::'a); \<forall>s. ((=) h \<leadsto>* ((=) h \<leadsto>* (\<lambda>s. False))) s\<rbrakk> \<Longrightarrow> False
 2. \<forall>h. h ## h \<longrightarrow> h = (0::'a) \<Longrightarrow> \<forall>P s. strictly_exact P \<longrightarrow> \<not> P (0::'a) \<longrightarrow> (P \<leadsto>* (P \<leadsto>* (\<lambda>s. False))) s proof (prove)
goal (2 subgoals):
 1. \<And>h. \<lbrakk>h ## h; h \<noteq> (0::'a); ((=) h \<leadsto>* ((=) h \<leadsto>* (\<lambda>s. False))) (h + h)\<rbrakk> \<Longrightarrow> False
 2. \<forall>h. h ## h \<longrightarrow> h = (0::'a) \<Longrightarrow> \<forall>P s. strictly_exact P \<longrightarrow> \<not> P (0::'a) \<longrightarrow> (P \<leadsto>* (P \<leadsto>* (\<lambda>s. False))) s proof (prove)
goal (2 subgoals):
 1. \<And>h. \<lbrakk>h ## h; h \<noteq> (0::'a); \<forall>y. h + h = h + y \<longrightarrow> h ## y \<longrightarrow> (\<forall>ya. h ## ya \<longrightarrow> y \<noteq> h + ya)\<rbrakk> \<Longrightarrow> False
 2. \<forall>h. h ## h \<longrightarrow> h = (0::'a) \<Longrightarrow> \<forall>P s. strictly_exact P \<longrightarrow> \<not> P (0::'a) \<longrightarrow> (P \<leadsto>* (P \<leadsto>* (\<lambda>s. False))) s proof (prove)
goal (2 subgoals):
 1. \<And>h. \<lbrakk>h ## h; h \<noteq> (0::'a); \<forall>y. h ## y \<longrightarrow> h \<noteq> h + y\<rbrakk> \<Longrightarrow> False
 2. \<forall>h. h ## h \<longrightarrow> h = (0::'a) \<Longrightarrow> \<forall>P s. strictly_exact P \<longrightarrow> \<not> P (0::'a) \<longrightarrow> (P \<leadsto>* (P \<leadsto>* (\<lambda>s. False))) s proof (prove)
goal (1 subgoal):
 1. \<forall>h. h ## h \<longrightarrow> h = (0::'a) \<Longrightarrow> \<forall>P s. strictly_exact P \<longrightarrow> \<not> P (0::'a) \<longrightarrow> (P \<leadsto>* (P \<leadsto>* (\<lambda>s. False))) s proof (prove)
goal (1 subgoal):
 1. \<And>P s. \<lbrakk>\<forall>h. h ## h \<longrightarrow> h = (0::'a); strictly_exact P; \<not> P (0::'a)\<rbrakk> \<Longrightarrow> (P \<leadsto>* (P \<leadsto>* (\<lambda>s. False))) s proof (prove)
goal (1 subgoal):
 1. \<And>P x xa ya. \<lbrakk>\<forall>h. h ## h \<longrightarrow> h = (0::'a); \<forall>h h'. P h \<and> P h' \<longrightarrow> h = h'; \<not> P (0::'a); P x; x ## xa + ya; xa ## ya; P xa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>P x xa ya. \<lbrakk>\<not> P (0::'a); P x; x ## x + ya; x ## ya; x ## x \<longrightarrow> x = (0::'a); \<forall>h'. P h' \<longrightarrow> xa = h'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>P x ya. \<lbrakk>\<not> P (0::'a); P x; x ## x + ya; x ## ya; x ## x \<longrightarrow> x = (0::'a)\<rbrakk> \<Longrightarrow> False proof (prove)
using this:
\<lbrakk>?x ## ?y + ?z; ?y ## ?z\<rbrakk> \<Longrightarrow> ?x ## ?y

goal (1 subgoal):
 1. \<And>P x ya. \<lbrakk>\<not> P (0::'a); P x; x ## x + ya; x ## ya; x ## x \<longrightarrow> x = (0::'a)\<rbrakk> \<Longrightarrow> False