kings-crown/FVELER_Isabelle huggingface dataset:
theory Extended_Separation_Algebra

lemma intuitionistic_def':
  "intuitionistic P = (\<forall>s R. (P \<and>* R) s \<longrightarrow> P s)" apply (rule iffI) apply (clarsimp simp: intuitionistic_def) apply (clarsimp simp: sep_conj_def) using sep_substate_disj_add apply blast apply (clarsimp simp: intuitionistic_def) apply (erule_tac x=h' in allE) apply (drule mp) apply (rule_tac x=sep_true in exI) apply (clarsimp simp:sep_conj_def sep_substate_def, fastforce) apply (assumption) done

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

goal (2 subgoals):
 1. \<And>R x y. \<lbrakk>\<forall>h h'. P h \<and> h \<preceq> h' \<longrightarrow> P h'; x ## y; P x; R y\<rbrakk> \<Longrightarrow> P (x + y)
 2. \<forall>s R. (P \<and>* R) s \<longrightarrow> P s \<Longrightarrow> intuitionistic P proof (prove)
goal (1 subgoal):
 1. \<forall>s R. (P \<and>* R) s \<longrightarrow> P s \<Longrightarrow> intuitionistic P proof (prove)
goal (1 subgoal):
 1. \<And>h h'. \<lbrakk>\<forall>s. (\<exists>R. (P \<and>* R) s) \<longrightarrow> P s; P h; h \<preceq> h'\<rbrakk> \<Longrightarrow> P h' proof (prove)
goal (1 subgoal):
 1. \<And>h h'. \<lbrakk>P h; h \<preceq> h'; (\<exists>R. (P \<and>* R) h') \<longrightarrow> P h'\<rbrakk> \<Longrightarrow> P h' proof (prove)
goal (2 subgoals):
 1. \<And>h h'. \<lbrakk>P h; h \<preceq> h'\<rbrakk> \<Longrightarrow> \<exists>R. (P \<and>* R) h'
 2. \<And>h h'. \<lbrakk>P h; h \<preceq> h'; P h'\<rbrakk> \<Longrightarrow> P h' proof (prove)
goal (2 subgoals):
 1. \<And>h h'. \<lbrakk>P h; h \<preceq> h'\<rbrakk> \<Longrightarrow> (P \<and>* (\<lambda>s. True)) h'
 2. \<And>h h'. \<lbrakk>P h; h \<preceq> h'; P h'\<rbrakk> \<Longrightarrow> P h' proof (prove)
goal (1 subgoal):
 1. \<And>h h'. \<lbrakk>P h; h \<preceq> h'; P h'\<rbrakk> \<Longrightarrow> P h' proof (prove)
goal:
No subgoals!
theory Extended_Separation_Algebra

lemma saturated_split:
  "cointuitionistic P \<Longrightarrow> P s \<Longrightarrow> (Q \<and>* R) s \<Longrightarrow> ((P and Q) \<and>* (P and R)) s" apply (clarsimp simp: cointuitionistic_def sep_conj_def pred_conj_def) apply (rule_tac x=x in exI) apply (rule_tac x=y in exI) apply (clarsimp) using sep_disj_commuteI sep_substate_disj_add sep_substate_disj_add' by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cointuitionistic P; P s; (Q \<and>* R) s\<rbrakk> \<Longrightarrow> ((P and Q) \<and>* (P and R)) s proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>h h'. P h \<and> h' \<preceq> h \<longrightarrow> P h'; P (x + y); x ## y; s = x + y; Q x; R y\<rbrakk> \<Longrightarrow> \<exists>xa ya. xa ## ya \<and> x + y = xa + ya \<and> P xa \<and> Q xa \<and> P ya \<and> R ya proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>h h'. P h \<and> h' \<preceq> h \<longrightarrow> P h'; P (x + y); x ## y; s = x + y; Q x; R y\<rbrakk> \<Longrightarrow> \<exists>ya. x ## ya \<and> x + y = x + ya \<and> P x \<and> Q x \<and> P ya \<and> R ya proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>h h'. P h \<and> h' \<preceq> h \<longrightarrow> P h'; P (x + y); x ## y; s = x + y; Q x; R y\<rbrakk> \<Longrightarrow> x ## y \<and> x + y = x + y \<and> P x \<and> Q x \<and> P y \<and> R y proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>h h'. P h \<and> h' \<preceq> h \<longrightarrow> P h'; P (x + y); x ## y; s = x + y; Q x; R y\<rbrakk> \<Longrightarrow> P x \<and> P y proof (prove)
using this:
?x ## ?y \<Longrightarrow> ?y ## ?x
?x ## ?y \<Longrightarrow> ?x \<preceq> ?x + ?y
?x ## ?y \<Longrightarrow> ?x \<preceq> ?y + ?x

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>h h'. P h \<and> h' \<preceq> h \<longrightarrow> P h'; P (x + y); x ## y; s = x + y; Q x; R y\<rbrakk> \<Longrightarrow> P x \<and> P y
theory Extended_Separation_Algebra

lemma sep_wand_dne:
  "((P \<longrightarrow>* sep_false) \<longrightarrow>* sep_false) s \<Longrightarrow> \<exists>s. P s" apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def sep_conj_def sep_coimpl_def) apply (erule_tac x=0 in allE) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((P \<longrightarrow>* (\<lambda>s. False)) \<longrightarrow>* (\<lambda>s. False)) s \<Longrightarrow> \<exists>s. P s proof (prove)
goal (1 subgoal):
 1. \<forall>h'. s ## h' \<longrightarrow> (\<exists>h'a. h' ## h'a \<and> P h'a) \<Longrightarrow> \<exists>s. P s proof (prove)
goal (1 subgoal):
 1. s ## (0::'a) \<longrightarrow> (\<exists>h'. (0::'a) ## h' \<and> P h') \<Longrightarrow> \<exists>s. P s proof (prove)
goal:
No subgoals!
theory Extended_Separation_Algebra

lemma sep_snake_dne:
  "(sep_true \<leadsto>* P) s \<Longrightarrow> ((P \<leadsto>* sep_false) \<leadsto>* sep_false) s" apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def sep_conj_def sep_coimpl_def) apply (rename_tac x y) apply (erule_tac x=y in allE) apply (erule_tac x=x in allE) apply (rule_tac x=x in exI) apply (rule_tac x=0 in exI) apply (clarsimp) apply (fastforce simp: sep_disj_commute sep_add_commute) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>s. True) \<leadsto>* P) s \<Longrightarrow> ((P \<leadsto>* (\<lambda>s. False)) \<leadsto>* (\<lambda>s. False)) s proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>xa ya. x + y = xa + ya \<longrightarrow> xa ## ya \<longrightarrow> P ya; s = x + y; x ## y\<rbrakk> \<Longrightarrow> \<exists>xa y. x = xa + y \<and> xa ## y \<and> P xa proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>xa ya. x + y = xa + ya \<longrightarrow> xa ## ya \<longrightarrow> P ya; s = x + y; x ## y\<rbrakk> \<Longrightarrow> \<exists>xa y. x = xa + y \<and> xa ## y \<and> P xa proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>s = x + y; x ## y; \<forall>ya. x + y = y + ya \<longrightarrow> y ## ya \<longrightarrow> P ya\<rbrakk> \<Longrightarrow> \<exists>xa y. x = xa + y \<and> xa ## y \<and> P xa proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>s = x + y; x ## y; x + y = y + x \<longrightarrow> y ## x \<longrightarrow> P x\<rbrakk> \<Longrightarrow> \<exists>xa y. x = xa + y \<and> xa ## y \<and> P xa proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>s = x + y; x ## y; x + y = y + x \<longrightarrow> y ## x \<longrightarrow> P x\<rbrakk> \<Longrightarrow> \<exists>y. x = x + y \<and> x ## y \<and> P x proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>s = x + y; x ## y; x + y = y + x \<longrightarrow> y ## x \<longrightarrow> P x\<rbrakk> \<Longrightarrow> x = x + (0::'a) \<and> x ## (0::'a) \<and> P x proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>s = x + y; x ## y; x + y = y + x \<longrightarrow> y ## x \<longrightarrow> P x\<rbrakk> \<Longrightarrow> P x proof (prove)
goal:
No subgoals!
theory Extended_Separation_Algebra

lemma strictly_exactI:
  "(\<And>P s. ((P -* R) -* R) s \<Longrightarrow> P (s :: 'a :: cancellative_sep_algebra)) \<Longrightarrow> strictly_exact R" apply (atomize) apply (clarsimp simp: strictly_exact_def) apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def sep_conj_def sep_coimpl_def strictly_exact_def) apply (rename_tac h h') apply (erule_tac x="\<lambda>s. s = h" in allE) by (metis disjoint_zero_sym sep_add_commute sep_add_zero sep_disj_zero)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>P s. ((P -* R) -* R) s \<Longrightarrow> P s) \<Longrightarrow> strictly_exact R proof (prove)
goal (1 subgoal):
 1. \<forall>P s. ((P -* R) -* R) s \<longrightarrow> P s \<Longrightarrow> strictly_exact R proof (prove)
goal (1 subgoal):
 1. \<And>h h'. \<lbrakk>\<forall>P s. ((P -* R) -* R) s \<longrightarrow> P s; R h; R h'\<rbrakk> \<Longrightarrow> h = h' proof (prove)
goal (1 subgoal):
 1. \<And>h h'. \<lbrakk>\<forall>P s. (\<exists>h'. s ## h' \<and> (\<exists>h'a. h' ## h'a \<and> P h'a \<and> R (h' + h'a)) \<and> R (s + h')) \<longrightarrow> P s; R h; R h'\<rbrakk> \<Longrightarrow> h = h' proof (prove)
goal (1 subgoal):
 1. \<And>h h'. \<lbrakk>\<forall>P s. (\<exists>h'. s ## h' \<and> (\<exists>h'a. h' ## h'a \<and> P h'a \<and> R (h' + h'a)) \<and> R (s + h')) \<longrightarrow> P s; R h; R h'\<rbrakk> \<Longrightarrow> h = h' proof (prove)
goal (1 subgoal):
 1. \<And>h h'. \<lbrakk>R h; R h'; \<forall>s. (\<exists>h'. s ## h' \<and> (\<exists>h'a. h' ## h'a \<and> h'a = h \<and> R (h' + h'a)) \<and> R (s + h')) \<longrightarrow> s = h\<rbrakk> \<Longrightarrow> h = h'
theory Extended_Separation_Algebra

lemma strictly_exact_septractD:
  "strictly_exact R \<Longrightarrow> ((P -* R) -* R) s \<Longrightarrow> P (s :: 'a :: cancellative_sep_algebra)" apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def sep_conj_def sep_coimpl_def
                        strictly_exact_def) by (metis sep_add_cancel sep_add_commute sep_disj_commuteI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>strictly_exact R; ((P -* R) -* R) s\<rbrakk> \<Longrightarrow> P s proof (prove)
goal (1 subgoal):
 1. \<And>h' h'a. \<lbrakk>\<forall>h h'. R h \<and> R h' \<longrightarrow> h = h'; s ## h'; R (s + h'); h' ## h'a; P h'a; R (h' + h'a)\<rbrakk> \<Longrightarrow> P s
theory Extended_Separation_Algebra

lemma strictly_exact_def':
  "(\<forall>P s. ((P -* R) -* R) s \<longrightarrow> P (s :: 'a :: cancellative_sep_algebra)) = strictly_exact R" using strictly_exactI strictly_exact_septractD by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<forall>P s. ((P -* R) -* R) s \<longrightarrow> P s) = strictly_exact R proof (prove)
using this:
(\<And>P s. ((P -* ?R) -* ?R) s \<Longrightarrow> P s) \<Longrightarrow> strictly_exact ?R
\<lbrakk>strictly_exact ?R; ((?P -* ?R) -* ?R) ?s\<rbrakk> \<Longrightarrow> ?P ?s

goal (1 subgoal):
 1. (\<forall>P s. ((P -* R) -* R) s \<longrightarrow> P s) = strictly_exact R
theory Extended_Separation_Algebra

lemma copreciseI:
  "(\<forall>(s ) R. (P -* R) s \<longrightarrow> (P \<longrightarrow>* R) s) \<Longrightarrow> coprecise P" apply (clarsimp simp: coprecise_def) apply (clarsimp simp: sep_substate_def) apply (erule_tac x="0" in allE) apply (rename_tac s h h') apply (erule_tac x="\<lambda>s'. s' = s + h" in allE) apply (drule mp) apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def) apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s R. (P -* R) s \<longrightarrow> (P \<longrightarrow>* R) s \<Longrightarrow> coprecise P proof (prove)
goal (1 subgoal):
 1. \<And>s h h'. \<lbrakk>\<forall>s R. (P -* R) s \<longrightarrow> (P \<longrightarrow>* R) s; P h; P h'; s \<preceq> h; s \<preceq> h'; s \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> h = h' proof (prove)
goal (1 subgoal):
 1. \<And>s z za. \<lbrakk>\<forall>s R. (P -* R) s \<longrightarrow> (P \<longrightarrow>* R) s; P (s + z); P (s + za); s \<noteq> (0::'a); s ## z; s ## za\<rbrakk> \<Longrightarrow> s + z = s + za proof (prove)
goal (1 subgoal):
 1. \<And>s z za. \<lbrakk>P (s + z); P (s + za); s \<noteq> (0::'a); s ## z; s ## za; \<forall>R. (P -* R) (0::'a) \<longrightarrow> (P \<longrightarrow>* R) (0::'a)\<rbrakk> \<Longrightarrow> s + z = s + za proof (prove)
goal (1 subgoal):
 1. \<And>s h h'. \<lbrakk>P (s + h); P (s + h'); s \<noteq> (0::'a); s ## h; s ## h'; \<forall>R. (P -* R) (0::'a) \<longrightarrow> (P \<longrightarrow>* R) (0::'a)\<rbrakk> \<Longrightarrow> s + h = s + h' proof (prove)
goal (1 subgoal):
 1. \<And>s h h'. \<lbrakk>P (s + h); P (s + h'); s \<noteq> (0::'a); s ## h; s ## h'; (P -* (\<lambda>s'. s' = s + h)) (0::'a) \<longrightarrow> (P \<longrightarrow>* (\<lambda>s'. s' = s + h)) (0::'a)\<rbrakk> \<Longrightarrow> s + h = s + h' proof (prove)
goal (2 subgoals):
 1. \<And>s h h'. \<lbrakk>P (s + h); P (s + h'); s \<noteq> (0::'a); s ## h; s ## h'\<rbrakk> \<Longrightarrow> (P -* (\<lambda>s'. s' = s + h)) (0::'a)
 2. \<And>s h h'. \<lbrakk>P (s + h); P (s + h'); s \<noteq> (0::'a); s ## h; s ## h'; (P \<longrightarrow>* (\<lambda>s'. s' = s + h)) (0::'a)\<rbrakk> \<Longrightarrow> s + h = s + h' proof (prove)
goal (1 subgoal):
 1. \<And>s h h'. \<lbrakk>P (s + h); P (s + h'); s \<noteq> (0::'a); s ## h; s ## h'; (P \<longrightarrow>* (\<lambda>s'. s' = s + h)) (0::'a)\<rbrakk> \<Longrightarrow> s + h = s + h' proof (prove)
goal:
No subgoals!
theory Extended_Separation_Algebra

lemma sep_implI':
  "strictly_exact P \<Longrightarrow> (P -* R) s \<Longrightarrow> (P \<longrightarrow>* R) s" apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def coprecise_def strictly_exact_def) apply (fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>strictly_exact P; (P -* R) s\<rbrakk> \<Longrightarrow> (P \<longrightarrow>* R) s proof (prove)
goal (1 subgoal):
 1. \<And>h' h'a. \<lbrakk>\<forall>h h'. P h \<and> P h' \<longrightarrow> h = h'; s ## h'; P h'; R (s + h'); s ## h'a; P h'a\<rbrakk> \<Longrightarrow> R (s + h'a) proof (prove)
goal:
No subgoals!
theory Extended_Separation_Algebra

lemma strictly_exactI':
  "\<forall>s R. (P -* R) s \<longrightarrow> (P \<longrightarrow>* R) s \<Longrightarrow> strictly_exact P" apply (clarsimp simp: strictly_exact_def) apply (erule_tac x="0" in allE) apply (rename_tac h h') apply (erule_tac x="\<lambda>h. h = h'" in allE) apply (drule mp) apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def) apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s R. (P -* R) s \<longrightarrow> (P \<longrightarrow>* R) s \<Longrightarrow> strictly_exact P proof (prove)
goal (1 subgoal):
 1. \<And>h h'. \<lbrakk>\<forall>s R. (P -* R) s \<longrightarrow> (P \<longrightarrow>* R) s; P h; P h'\<rbrakk> \<Longrightarrow> h = h' proof (prove)
goal (1 subgoal):
 1. \<And>h h'. \<lbrakk>P h; P h'; \<forall>R. (P -* R) (0::'a) \<longrightarrow> (P \<longrightarrow>* R) (0::'a)\<rbrakk> \<Longrightarrow> h = h' proof (prove)
goal (1 subgoal):
 1. \<And>h h'. \<lbrakk>P h; P h'; \<forall>R. (P -* R) (0::'a) \<longrightarrow> (P \<longrightarrow>* R) (0::'a)\<rbrakk> \<Longrightarrow> h = h' proof (prove)
goal (1 subgoal):
 1. \<And>h h'. \<lbrakk>P h; P h'; (P -* (\<lambda>h. h = h')) (0::'a) \<longrightarrow> (P \<longrightarrow>* (\<lambda>h. h = h')) (0::'a)\<rbrakk> \<Longrightarrow> h = h' proof (prove)
goal (2 subgoals):
 1. \<And>h h'. \<lbrakk>P h; P h'\<rbrakk> \<Longrightarrow> (P -* (\<lambda>h. h = h')) (0::'a)
 2. \<And>h h'. \<lbrakk>P h; P h'; (P \<longrightarrow>* (\<lambda>h. h = h')) (0::'a)\<rbrakk> \<Longrightarrow> h = h' proof (prove)
goal (1 subgoal):
 1. \<And>h h'. \<lbrakk>P h; P h'; (P \<longrightarrow>* (\<lambda>h. h = h')) (0::'a)\<rbrakk> \<Longrightarrow> h = h' proof (prove)
goal:
No subgoals!
theory Extended_Separation_Algebra

lemma strictly_exact_def'':
  "(\<forall>s R. (P -* R) s \<longrightarrow> (P \<longrightarrow>* R) s) = strictly_exact P" using sep_implI' strictly_exactI' by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<forall>s R. (P -* R) s \<longrightarrow> (P \<longrightarrow>* R) s) = strictly_exact P proof (prove)
using this:
\<lbrakk>strictly_exact ?P; (?P -* ?R) ?s\<rbrakk> \<Longrightarrow> (?P \<longrightarrow>* ?R) ?s
\<forall>s R. (?P -* R) s \<longrightarrow> (?P \<longrightarrow>* R) s \<Longrightarrow> strictly_exact ?P

goal (1 subgoal):
 1. (\<forall>s R. (P -* R) s \<longrightarrow> (P \<longrightarrow>* R) s) = strictly_exact P
theory Extended_Separation_Algebra

lemma precise_conj_coimpl:
  "precise P \<Longrightarrow> (\<forall>s R. (P \<and>* R) s \<longrightarrow> (P \<leadsto>* R) s)" apply (clarsimp simp: precise_def) apply (clarsimp simp: sep_conj_def sep_coimpl_def pred_neg_def) by (metis cancellative_sep_algebra_class.sep_add_cancelD sep_add_commute
             sep_disj_commuteI sep_substate_disj_add)

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

lemma sep_coimpl_cancel:
  "(P \<leadsto>* Q) s \<Longrightarrow> ((P \<and>* Q) s \<Longrightarrow> (P \<leadsto>* Q') s) \<Longrightarrow> (P \<leadsto>* Q') s" apply (clarsimp simp: sep_coimpl_def pred_neg_def) apply (clarsimp simp: sep_conj_def) by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P \<leadsto>* Q) s; (P \<and>* Q) s \<Longrightarrow> (P \<leadsto>* Q') s\<rbrakk> \<Longrightarrow> (P \<leadsto>* Q') s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> (P \<and>* (\<lambda>x. \<not> Q x)) s; (P \<and>* Q) s \<Longrightarrow> False; (P \<and>* (\<lambda>x. \<not> Q' x)) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>xa. P xa \<longrightarrow> (\<forall>ya. x + y = xa + ya \<longrightarrow> xa ## ya \<longrightarrow> Q ya); \<exists>xa ya. xa ## ya \<and> x + y = xa + ya \<and> P xa \<and> Q ya \<Longrightarrow> False; x ## y; s = x + y; P x; \<not> Q' y\<rbrakk> \<Longrightarrow> False
theory Extended_Separation_Algebra

lemma sep_cases:
  "R s \<Longrightarrow> (P \<and>* (P -* R)) s \<or> (P \<leadsto>* (sep_false)) s" apply (safe) apply (clarsimp simp: sep_coimpl_def) apply (rule ccontr) by (meson sep_antimp' sep_conj_sep_true_right sep_snake_mp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. R s \<Longrightarrow> (P \<and>* (P -* R)) s \<or> (P \<leadsto>* (\<lambda>s. False)) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>R s; \<not> (P \<leadsto>* (\<lambda>s. False)) s\<rbrakk> \<Longrightarrow> (P \<and>* (P -* R)) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>R s; (P \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> (P \<and>* (P -* R)) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>R s; (P \<and>* (\<lambda>s. True)) s; \<not> (P \<and>* (P -* R)) s\<rbrakk> \<Longrightarrow> False
theory Extended_Separation_Algebra

lemma contra:
  "(\<forall>s. P s \<longrightarrow> Q s) \<Longrightarrow> (\<forall>s. \<not> Q s \<longrightarrow> \<not> P s )" apply (safe) by (fastforce)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. P s \<longrightarrow> Q s \<Longrightarrow> \<forall>s. \<not> Q s \<longrightarrow> \<not> P s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>s. P s \<longrightarrow> Q s; \<not> Q s; P s\<rbrakk> \<Longrightarrow> False
theory Extended_Separation_Algebra

lemma sep_coimpl_contra:
  "(R \<leadsto>* (not Q)) s \<Longrightarrow> (R \<leadsto>* Q) s \<Longrightarrow> (R \<leadsto>* sep_false) s" apply (drule sep_coimpl_comb, assumption) apply (clarsimp simp: pred_neg_def pred_conj_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(R \<leadsto>* not Q) s; (R \<leadsto>* Q) s\<rbrakk> \<Longrightarrow> (R \<leadsto>* (\<lambda>s. False)) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(R \<leadsto>* Q) s; (R \<leadsto>* not Q and Q) s\<rbrakk> \<Longrightarrow> (R \<leadsto>* (\<lambda>s. False)) s proof (prove)
goal:
No subgoals!
theory Extended_Separation_Algebra

lemma sep_comb':
  "((not Q) \<leadsto>* P) s \<Longrightarrow> (Q \<leadsto>* R) s \<Longrightarrow> ((R or P) \<and>* sep_true) s" apply (clarsimp simp: sep_coimpl_def sep_conj_def pred_neg_def) by (metis (full_types) disjoint_zero_sym pred_disj_def sep_add_zero sep_add_zero_sym sep_disj_zero)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(not Q \<leadsto>* P) s; (Q \<leadsto>* R) s\<rbrakk> \<Longrightarrow> ((R or P) \<and>* (\<lambda>s. True)) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x y. s = x + y \<longrightarrow> x ## y \<longrightarrow> Q x \<or> P y; \<forall>x. Q x \<longrightarrow> (\<forall>y. s = x + y \<longrightarrow> x ## y \<longrightarrow> R y)\<rbrakk> \<Longrightarrow> \<exists>x y. x ## y \<and> s = x + y \<and> (R x \<or> P x)
theory Extended_Separation_Algebra

lemma sep_coimpl_dne:
  "((R \<leadsto>* sep_false) \<leadsto>* sep_false) s \<Longrightarrow> (R \<and>* sep_true) s" by (metis sep_coimpl_def sep_conj_sep_true_right sep_neg_not)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((R \<leadsto>* (\<lambda>s. False)) \<leadsto>* (\<lambda>s. False)) s \<Longrightarrow> (R \<and>* (\<lambda>s. True)) s
theory Extended_Separation_Algebra

lemma sep_antimp_contrapos:
  " (R) s \<Longrightarrow> ((P \<longrightarrow>* not R) \<leadsto>* (not P)) s " by (metis pred_neg_def sep_coimpl_def' sep_mp_gen)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. R s \<Longrightarrow> (P \<longrightarrow>* not R \<leadsto>* not P) s
theory Extended_Separation_Algebra

lemma sep_snake_trivial:
  "(sep_true \<leadsto>* Q) s \<Longrightarrow> Q s" by (metis pred_neg_def sep_coimpl_def sep_conj_sep_true')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>s. True) \<leadsto>* Q) s \<Longrightarrow> Q s
theory Extended_Separation_Algebra

lemma min_predD:
  "(R \<leadsto>* \<box>) s \<Longrightarrow> (R \<and>* sep_true) s  \<Longrightarrow> R s" using Sep_Cancel_Set.sep_conj_empty' sep_coimpl_dne sep_snake_mp by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(R \<leadsto>* \<box>) s; (R \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> R s proof (prove)
using this:
(?P \<and>* \<box>) ?s \<Longrightarrow> ?P ?s
((?R \<leadsto>* (\<lambda>s. False)) \<leadsto>* (\<lambda>s. False)) ?s \<Longrightarrow> (?R \<and>* (\<lambda>s. True)) ?s
\<lbrakk>(?P \<leadsto>* ?Q) ?s; (?P \<and>* (\<lambda>s. True)) ?s\<rbrakk> \<Longrightarrow> (?P \<and>* ?Q) ?s

goal (1 subgoal):
 1. \<lbrakk>(R \<leadsto>* \<box>) s; (R \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> R s
theory Extended_Separation_Algebra

lemma septract_sep_wand:
  "(P -* R) s \<Longrightarrow> (P \<longrightarrow>* Q) s \<Longrightarrow> (P -* (Q and R)) s" apply (clarsimp simp: sep_impl_def septraction_def pred_neg_def) by (fastforce simp: pred_conj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P -* R) s; (P \<longrightarrow>* Q) s\<rbrakk> \<Longrightarrow> (P -* Q and R) s proof (prove)
goal (1 subgoal):
 1. \<And>h'. \<lbrakk>\<forall>h'. s ## h' \<and> P h' \<longrightarrow> Q (s + h'); s ## h'; P h'; R (s + h')\<rbrakk> \<Longrightarrow> \<exists>h'. s ## h' \<and> P h' \<and> Q (s + h') \<and> R (s + h')