kings-crown/FVELER_Isabelle huggingface dataset:
theory Separation_Algebra

lemma sep_conj_commute:
  "(P ** Q) = (Q ** P)" by (rule ext) (auto intro: sep_conj_commuteI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<and>* Q) = (Q \<and>* P)
theory Separation_Algebra

lemma sep_conj_impl:
  "\<lbrakk> (P ** Q) h; \<And>h. P h \<Longrightarrow> P' h; \<And>h. Q h \<Longrightarrow> Q' h \<rbrakk> \<Longrightarrow> (P' ** Q') h" by (erule sep_conjE, auto intro!: sep_conjI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P \<and>* Q) h; \<And>h. P h \<Longrightarrow> P' h; \<And>h. Q h \<Longrightarrow> Q' h\<rbrakk> \<Longrightarrow> (P' \<and>* Q') h
theory Separation_Algebra

lemma sep_conj_impl1:
  assumes P: "\<And>h. P h \<Longrightarrow> I h"
  shows "(P ** R) h \<Longrightarrow> (I ** R) h" by (auto intro: sep_conj_impl P)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<and>* R) h \<Longrightarrow> (I \<and>* R) h
theory Separation_Algebra

lemma sep_globalise:
  "\<lbrakk> (P ** R) h; (\<And>h. P h \<Longrightarrow> Q h) \<rbrakk> \<Longrightarrow> (Q ** R) h" by (fast elim: sep_conj_impl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P \<and>* R) h; \<And>h. P h \<Longrightarrow> Q h\<rbrakk> \<Longrightarrow> (Q \<and>* R) h
theory Separation_Algebra

lemma sep_conj_trivial_strip1:
  "Q = R \<Longrightarrow> (P ** Q) = (P ** R)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Q = R \<Longrightarrow> (P \<and>* Q) = (P \<and>* R)
theory Separation_Algebra

lemma sep_conj_trivial_strip2:
  "Q = R \<Longrightarrow> (Q ** P) = (R ** P)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Q = R \<Longrightarrow> (Q \<and>* P) = (R \<and>* P)
theory Separation_Algebra

lemma disjoint_subheaps_exist:
  "\<exists>x y. x ## y \<and> h = x + y" by (rule_tac x=0 in exI, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>x y. x ## y \<and> h = x + y
theory Separation_Algebra

lemma sep_conj_left_commute: (* for permutative rewriting *)
  "(P ** (Q ** R)) = (Q ** (P ** R))" (is "?x = ?y") proof - have "?x = ((Q ** R) ** P)" by (simp add: sep_conj_commute) also have "\<dots> = (Q ** (R ** P))" by (subst sep_conj_assoc, simp) finally show ?thesis by (simp add: sep_conj_commute) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<and>* Q \<and>* R) = (Q \<and>* P \<and>* R) proof (state)
goal (1 subgoal):
 1. (P \<and>* Q \<and>* R) = (Q \<and>* P \<and>* R) proof (prove)
goal (1 subgoal):
 1. (P \<and>* Q \<and>* R) = ((Q \<and>* R) \<and>* P) proof (state)
this:
(P \<and>* Q \<and>* R) = ((Q \<and>* R) \<and>* P)

goal (1 subgoal):
 1. (P \<and>* Q \<and>* R) = (Q \<and>* P \<and>* R) proof (state)
this:
(P \<and>* Q \<and>* R) = ((Q \<and>* R) \<and>* P)

goal (1 subgoal):
 1. (P \<and>* Q \<and>* R) = (Q \<and>* P \<and>* R) proof (prove)
goal (1 subgoal):
 1. ((Q \<and>* R) \<and>* P) = (Q \<and>* R \<and>* P) proof (state)
this:
((Q \<and>* R) \<and>* P) = (Q \<and>* R \<and>* P)

goal (1 subgoal):
 1. (P \<and>* Q \<and>* R) = (Q \<and>* P \<and>* R) proof (chain)
picking this:
(P \<and>* Q \<and>* R) = (Q \<and>* R \<and>* P) proof (prove)
using this:
(P \<and>* Q \<and>* R) = (Q \<and>* R \<and>* P)

goal (1 subgoal):
 1. (P \<and>* Q \<and>* R) = (Q \<and>* P \<and>* R) proof (state)
this:
(P \<and>* Q \<and>* R) = (Q \<and>* P \<and>* R)

goal:
No subgoals!
theory Separation_Algebra

lemma sep_empty_zero [simp,intro!]: "\<box> 0" by (simp add: sep_empty_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<box> (0::'a)
theory Separation_Algebra

lemma sep_conj_sep_true:
  "P h \<Longrightarrow> (P ** sep_true) h" by (simp add: sep_conjI[where y=0])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P h \<Longrightarrow> (P \<and>* (\<lambda>s. True)) h
theory Separation_Algebra

lemma sep_conj_false_right [simp]:
  "(P ** sep_false) = sep_false" by (force elim: sep_conjE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<and>* (\<lambda>s. False)) = (\<lambda>s. False)
theory Separation_Algebra

lemma sep_conj_false_left [simp]:
  "(sep_false ** P) = sep_false" by (subst sep_conj_commute) (rule sep_conj_false_right)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>s. False) \<and>* P) = (\<lambda>s. False)
theory Separation_Algebra

lemma sep_conj_empty [simp]:
  "(P ** \<box>) = P" by (simp add: sep_conj_def sep_empty_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<and>* \<box>) = P
theory Separation_Algebra

lemma sep_conj_empty'[simp]:
  "(\<box> ** P) = P" by (subst sep_conj_commute, rule sep_conj_empty)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<box> \<and>* P) = P
theory Separation_Algebra

lemma sep_conj_sep_emptyI:
  "P h \<Longrightarrow> (P ** \<box>) h" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P h \<Longrightarrow> (P \<and>* \<box>) h
theory Separation_Algebra

lemma sep_conj_sep_emptyE:
  "\<lbrakk> P s; (P ** \<box>) s \<Longrightarrow> (Q ** R) s \<rbrakk> \<Longrightarrow> (Q ** R) s" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P s; (P \<and>* \<box>) s \<Longrightarrow> (Q \<and>* R) s\<rbrakk> \<Longrightarrow> (Q \<and>* R) s
theory Separation_Algebra

lemma sep_conj_true_P [simp]:
  "(sep_true ** (sep_true ** P)) = (sep_true ** P)" by (simp add: sep_conj_assoc[symmetric])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>s. True) \<and>* (\<lambda>s. True) \<and>* P) = ((\<lambda>s. True) \<and>* P)
theory Separation_Algebra

lemma sep_conj_disj:
  "((P or Q) ** R) = ((P ** R) or (Q ** R))" by (rule ext, auto simp: sep_conj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>s. P s \<or> Q s) \<and>* R) = (\<lambda>s. (P \<and>* R) s \<or> (Q \<and>* R) s)
theory Separation_Algebra

lemma sep_conj_sep_true_left:
  "(P ** Q) h \<Longrightarrow> (sep_true ** Q) h" by (erule sep_conj_impl, simp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<and>* Q) h \<Longrightarrow> ((\<lambda>s. True) \<and>* Q) h
theory Separation_Algebra

lemma sep_conj_sep_true_right:
  "(P ** Q) h \<Longrightarrow> (P ** sep_true) h" by (subst (asm) sep_conj_commute, drule sep_conj_sep_true_left,
      simp add: sep_conj_ac)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<and>* Q) h \<Longrightarrow> (P \<and>* (\<lambda>s. True)) h
theory Separation_Algebra

lemma sep_conj_conj:
  "((P and Q) ** R) h \<Longrightarrow> ((P ** R) and (Q ** R)) h" by (force intro: sep_conjI elim!: sep_conjE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>s. P s \<and> Q s) \<and>* R) h \<Longrightarrow> (P \<and>* R) h \<and> (Q \<and>* R) h
theory Separation_Algebra

lemma sep_conj_exists1:
  "((EXS x. P x) ** Q) = (EXS x. (P x ** Q))" by (force intro: sep_conjI elim: sep_conjE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>s. \<exists>x. P x s) \<and>* Q) = (\<lambda>s. \<exists>x. (P x \<and>* Q) s)
theory Separation_Algebra

lemma sep_conj_exists2:
  "(P ** (EXS x. Q x)) = (EXS x. P ** Q x)" by (force intro!: sep_conjI elim!: sep_conjE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<and>* (\<lambda>s. \<exists>x. Q x s)) = (\<lambda>s. \<exists>x. (P \<and>* Q x) s)
theory Separation_Algebra

lemma sep_conj_spec1:
  "((ALLS x. P x) ** Q) h \<Longrightarrow> (P x ** Q) h" by (force intro: sep_conjI elim: sep_conjE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>s. \<forall>x. P x s) \<and>* Q) h \<Longrightarrow> (P x \<and>* Q) h
theory Separation_Algebra

lemma sep_conj_spec2:
  "(P ** (ALLS x. Q x)) h \<Longrightarrow> (P ** Q x) h" by (force intro: sep_conjI elim: sep_conjE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<and>* (\<lambda>s. \<forall>x. Q x s)) h \<Longrightarrow> (P \<and>* Q x) h
theory Separation_Algebra

lemma sep_implI:
  assumes a: "\<And>h'. \<lbrakk> h ## h'; P h' \<rbrakk> \<Longrightarrow> Q (h + h')"
  shows "(P \<longrightarrow>* Q) h" unfolding sep_impl_def by (auto elim: a)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<longrightarrow>* Q) h proof (prove)
goal (1 subgoal):
 1. \<forall>h'. h ## h' \<and> P h' \<longrightarrow> Q (h + h')
theory Separation_Algebra

lemma sep_implE:
  "(x \<longrightarrow>* y) h \<Longrightarrow> (\<forall>h'. h ## h' \<and> x h' \<longrightarrow> y (h + h') \<Longrightarrow> Q) \<Longrightarrow> Q" by (auto dest: sep_implD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x \<longrightarrow>* y) h; \<forall>h'. h ## h' \<and> x h' \<longrightarrow> y (h + h') \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q
theory Separation_Algebra

lemma sep_impl_sep_true [simp]:
  "(P \<longrightarrow>* sep_true) = sep_true" by (force intro!: sep_implI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<longrightarrow>* (\<lambda>s. True)) = (\<lambda>s. True)
theory Separation_Algebra

lemma sep_impl_sep_false [simp]:
  "(sep_false \<longrightarrow>* P) = sep_true" by (force intro!: sep_implI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>s. False) \<longrightarrow>* P) = (\<lambda>s. True)
theory Separation_Algebra

lemma sep_impl_sep_true_P:
  "(sep_true \<longrightarrow>* P) h \<Longrightarrow> P h" by (clarsimp dest!: sep_implD elim!: allE[where x=0])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>s. True) \<longrightarrow>* P) h \<Longrightarrow> P h
theory Separation_Algebra

lemma sep_impl_sep_true_false [simp]:
  "(sep_true \<longrightarrow>* sep_false) = sep_false" by (force dest: sep_impl_sep_true_P)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>s. True) \<longrightarrow>* (\<lambda>s. False)) = (\<lambda>s. False)
theory Separation_Algebra

lemma sep_conj_sep_impl:
  "\<lbrakk> P h; \<And>h. (P ** Q) h \<Longrightarrow> R h \<rbrakk> \<Longrightarrow> (Q \<longrightarrow>* R) h" proof (rule sep_implI) fix h' h assume "P h" and "h ## h'" and "Q h'" hence "(P ** Q) (h + h')" by (force intro: sep_conjI) moreover assume "\<And>h. (P ** Q) h \<Longrightarrow> R h" ultimately show "R (h + h')" by simp qed

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

goal (1 subgoal):
 1. \<And>h'. \<lbrakk>P h; \<And>h. (P \<and>* Q) h \<Longrightarrow> R h; h ## h'; Q h'\<rbrakk> \<Longrightarrow> R (h + h') proof (prove)
using this:
P h
h ## h'
Q h'

goal (1 subgoal):
 1. (P \<and>* Q) (h + h') proof (state)
this:
(P \<and>* Q) (h + h')

goal (1 subgoal):
 1. \<And>h'. \<lbrakk>P h; \<And>h. (P \<and>* Q) h \<Longrightarrow> R h; h ## h'; Q h'\<rbrakk> \<Longrightarrow> R (h + h') proof (state)
this:
(P \<and>* Q) (h + h')

goal (1 subgoal):
 1. \<And>h'. \<lbrakk>P h; \<And>h. (P \<and>* Q) h \<Longrightarrow> R h; h ## h'; Q h'\<rbrakk> \<Longrightarrow> R (h + h') proof (state)
this:
(P \<and>* Q) ?h \<Longrightarrow> R ?h

goal (1 subgoal):
 1. \<And>h'. \<lbrakk>P h; \<And>h. (P \<and>* Q) h \<Longrightarrow> R h; h ## h'; Q h'\<rbrakk> \<Longrightarrow> R (h + h') proof (chain)
picking this:
(P \<and>* Q) (h + h')
(P \<and>* Q) ?h \<Longrightarrow> R ?h proof (prove)
using this:
(P \<and>* Q) (h + h')
(P \<and>* Q) ?h \<Longrightarrow> R ?h

goal (1 subgoal):
 1. R (h + h') proof (state)
this:
R (h + h')

goal:
No subgoals!
theory Separation_Algebra

lemma sep_conj_sep_impl_sep_conj2:
  "(P ** R) h \<Longrightarrow> (P ** (Q \<longrightarrow>* (Q ** R))) h" by (erule (1) sep_conj_impl, erule sep_conj_sep_impl, simp add: sep_conj_ac)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<and>* R) h \<Longrightarrow> (P \<and>* (Q \<longrightarrow>* Q \<and>* R)) h
theory Separation_Algebra

lemma pure_sep_true:
  "pure sep_true" by (simp add: pure_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pure (\<lambda>s. True)
theory Separation_Algebra

lemma pure_split:
  "pure P = (P = sep_true \<or> P = sep_false)" by (force simp: pure_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pure P = (P = (\<lambda>s. True) \<or> P = (\<lambda>s. False))
theory Separation_Algebra

lemma pure_sep_conj:
  "\<lbrakk> pure P; pure Q \<rbrakk> \<Longrightarrow> pure (P \<and>* Q)" by (force simp: pure_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pure P; pure Q\<rbrakk> \<Longrightarrow> pure (P \<and>* Q)
theory Separation_Algebra

lemma pure_sep_impl:
  "\<lbrakk> pure P; pure Q \<rbrakk> \<Longrightarrow> pure (P \<longrightarrow>* Q)" by (force simp: pure_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pure P; pure Q\<rbrakk> \<Longrightarrow> pure (P \<longrightarrow>* Q)
theory Separation_Algebra

lemma pure_conj_sep_conj:
  "\<lbrakk> (P and Q) h; pure P \<or> pure Q \<rbrakk> \<Longrightarrow> (P \<and>* Q) h" by (metis pure_def sep_add_zero sep_conjI sep_conj_commute sep_disj_zero)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P h \<and> Q h; pure P \<or> pure Q\<rbrakk> \<Longrightarrow> (P \<and>* Q) h
theory Separation_Algebra

lemma pure_sep_conj_conj:
  "\<lbrakk> (P \<and>* Q) h; pure P; pure Q \<rbrakk> \<Longrightarrow> (P and Q) h" by (force simp: pure_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P \<and>* Q) h; pure P; pure Q\<rbrakk> \<Longrightarrow> P h \<and> Q h
theory Separation_Algebra

lemma pure_conj_sep_conj_assoc:
  "pure P \<Longrightarrow> ((P and Q) \<and>* R) = (P and (Q \<and>* R))" by (auto simp: pure_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pure P \<Longrightarrow> ((\<lambda>s. P s \<and> Q s) \<and>* R) = (\<lambda>s. P s \<and> (Q \<and>* R) s)
theory Separation_Algebra

lemma pure_sep_impl_impl:
  "\<lbrakk> (P \<longrightarrow>* Q) h; pure P \<rbrakk> \<Longrightarrow> P h \<longrightarrow> Q h" by (force simp: pure_split dest: sep_impl_sep_true_P)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P \<longrightarrow>* Q) h; pure P\<rbrakk> \<Longrightarrow> P h \<longrightarrow> Q h
theory Separation_Algebra

lemma pure_impl_sep_impl:
  "\<lbrakk> P h \<longrightarrow> Q h; pure P; pure Q \<rbrakk> \<Longrightarrow> (P \<longrightarrow>* Q) h" by (force simp: pure_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P h \<longrightarrow> Q h; pure P; pure Q\<rbrakk> \<Longrightarrow> (P \<longrightarrow>* Q) h
theory Separation_Algebra

lemma pure_conj_right': "(Q \<and>* (P' and \<langle>Q'\<rangle>)) = (\<langle>Q'\<rangle> and (Q \<and>* P'))" by (simp add: conj_comms pure_conj_right)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (Q \<and>* (\<lambda>s. P' s \<and> Q')) = (\<lambda>s. Q' \<and> (Q \<and>* P') s)
theory Separation_Algebra

lemma pure_conj_left: "((\<langle>P'\<rangle> and Q') \<and>* Q) = (\<langle>P'\<rangle> and (Q' \<and>* Q))" by (simp add: pure_conj_right sep_conj_ac)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>s. P' \<and> Q' s) \<and>* Q) = (\<lambda>s. P' \<and> (Q' \<and>* Q) s)
theory Separation_Algebra

lemma pure_conj_left': "((P' and \<langle>Q'\<rangle>) \<and>* Q) = (\<langle>Q'\<rangle> and (P' \<and>* Q))" by (subst conj_comms, subst pure_conj_left, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>s. P' s \<and> Q') \<and>* Q) = (\<lambda>s. Q' \<and> (P' \<and>* Q) s)
theory Separation_Algebra

lemma pure_intuitionistic:
  "pure P \<Longrightarrow> intuitionistic P" by (clarsimp simp: intuitionistic_def pure_def, fast)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pure P \<Longrightarrow> intuitionistic P
theory Separation_Algebra

lemma intuitionistic_conj:
  "\<lbrakk> intuitionistic P; intuitionistic Q \<rbrakk> \<Longrightarrow> intuitionistic (P and Q)" by (force intro: intuitionisticI dest: intuitionisticD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>intuitionistic P; intuitionistic Q\<rbrakk> \<Longrightarrow> intuitionistic (\<lambda>s. P s \<and> Q s)
theory Separation_Algebra

lemma intuitionistic_disj:
  "\<lbrakk> intuitionistic P; intuitionistic Q \<rbrakk> \<Longrightarrow> intuitionistic (P or Q)" by (force intro: intuitionisticI dest: intuitionisticD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>intuitionistic P; intuitionistic Q\<rbrakk> \<Longrightarrow> intuitionistic (\<lambda>s. P s \<or> Q s)
theory Separation_Algebra

lemma intuitionistic_forall:
  "(\<And>x. intuitionistic (P x)) \<Longrightarrow> intuitionistic (ALLS x. P x)" by (force intro: intuitionisticI dest: intuitionisticD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. intuitionistic (P x)) \<Longrightarrow> intuitionistic (\<lambda>s. \<forall>x. P x s)
theory Separation_Algebra

lemma intuitionistic_exists:
  "(\<And>x. intuitionistic (P x)) \<Longrightarrow> intuitionistic (EXS x. P x)" by (force intro: intuitionisticI dest: intuitionisticD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. intuitionistic (P x)) \<Longrightarrow> intuitionistic (\<lambda>s. \<exists>x. P x s)
theory Separation_Algebra

lemma intuitionistic_sep_impl_sep_true:
  "intuitionistic (sep_true \<longrightarrow>* P)" proof (rule intuitionisticI) fix h h' assume imp: "(sep_true \<longrightarrow>* P) h" and hh': "h \<preceq> h'" from hh' obtain z where h': "h' = h + z" and hzd: "h ## z" by (clarsimp simp: sep_substate_def) show "(sep_true \<longrightarrow>* P) h'" using imp h' hzd apply (clarsimp dest!: sep_implD) apply (metis sep_add_assoc sep_add_disjD sep_disj_addI3 sep_implI) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. intuitionistic ((\<lambda>s. True) \<longrightarrow>* P) proof (state)
goal (1 subgoal):
 1. \<And>h h'. \<lbrakk>((\<lambda>s. True) \<longrightarrow>* P) h; h \<preceq> h'\<rbrakk> \<Longrightarrow> ((\<lambda>s. True) \<longrightarrow>* P) h' proof (state)
goal (1 subgoal):
 1. \<And>h h'. \<lbrakk>((\<lambda>s. True) \<longrightarrow>* P) h; h \<preceq> h'\<rbrakk> \<Longrightarrow> ((\<lambda>s. True) \<longrightarrow>* P) h' proof (state)
this:
((\<lambda>s. True) \<longrightarrow>* P) h
h \<preceq> h'

goal (1 subgoal):
 1. \<And>h h'. \<lbrakk>((\<lambda>s. True) \<longrightarrow>* P) h; h \<preceq> h'\<rbrakk> \<Longrightarrow> ((\<lambda>s. True) \<longrightarrow>* P) h' proof (chain)
picking this:
h \<preceq> h' proof (prove)
using this:
h \<preceq> h'

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>h' = h + z; h ## z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
h' = h + z
h ## z

goal (1 subgoal):
 1. \<And>h h'. \<lbrakk>((\<lambda>s. True) \<longrightarrow>* P) h; h \<preceq> h'\<rbrakk> \<Longrightarrow> ((\<lambda>s. True) \<longrightarrow>* P) h' proof (prove)
goal (1 subgoal):
 1. ((\<lambda>s. True) \<longrightarrow>* P) h' proof (prove)
using this:
((\<lambda>s. True) \<longrightarrow>* P) h
h' = h + z
h ## z

goal (1 subgoal):
 1. ((\<lambda>s. True) \<longrightarrow>* P) h' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h' = h + z; h ## z; \<forall>h'. h ## h' \<longrightarrow> P (h + h')\<rbrakk> \<Longrightarrow> ((\<lambda>s. True) \<longrightarrow>* P) (h + z) proof (prove)
goal:
No subgoals! proof (state)
this:
((\<lambda>s. True) \<longrightarrow>* P) h'

goal:
No subgoals!
theory Separation_Algebra

lemma intuitionistic_sep_conj:
  assumes ip: "intuitionistic (P::('a \<Rightarrow> bool))"
  shows "intuitionistic (P \<and>* Q)" proof (rule intuitionisticI) fix h h' assume sc: "(P \<and>* Q) h" and hh': "h \<preceq> h'" from hh' obtain z where h': "h' = h + z" and hzd: "h ## z" by (clarsimp simp: sep_substate_def) from sc obtain x y where px: "P x" and qy: "Q y"
                       and h: "h = x + y" and xyd: "x ## y" by (clarsimp simp: sep_conj_def) have "x ## z" using hzd h xyd by (metis sep_add_disjD) with ip px have "P (x + z)" by (fastforce elim: intuitionisticD sep_substate_disj_add) thus "(P \<and>* Q) h'" using h' h hzd qy xyd by (metis (full_types) sep_add_commute sep_add_disjD sep_add_disjI2
              sep_add_left_commute sep_conjI) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. intuitionistic (P \<and>* Q) proof (state)
goal (1 subgoal):
 1. \<And>h h'. \<lbrakk>(P \<and>* Q) h; h \<preceq> h'\<rbrakk> \<Longrightarrow> (P \<and>* Q) h' proof (state)
goal (1 subgoal):
 1. \<And>h h'. \<lbrakk>(P \<and>* Q) h; h \<preceq> h'\<rbrakk> \<Longrightarrow> (P \<and>* Q) h' proof (state)
this:
(P \<and>* Q) h
h \<preceq> h'

goal (1 subgoal):
 1. \<And>h h'. \<lbrakk>(P \<and>* Q) h; h \<preceq> h'\<rbrakk> \<Longrightarrow> (P \<and>* Q) h' proof (chain)
picking this:
h \<preceq> h' proof (prove)
using this:
h \<preceq> h'

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>h' = h + z; h ## z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
h' = h + z
h ## z

goal (1 subgoal):
 1. \<And>h h'. \<lbrakk>(P \<and>* Q) h; h \<preceq> h'\<rbrakk> \<Longrightarrow> (P \<and>* Q) h' proof (chain)
picking this:
(P \<and>* Q) h proof (prove)
using this:
(P \<and>* Q) h

goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>P x; Q y; h = x + y; x ## y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
P x
Q y
h = x + y
x ## y

goal (1 subgoal):
 1. \<And>h h'. \<lbrakk>(P \<and>* Q) h; h \<preceq> h'\<rbrakk> \<Longrightarrow> (P \<and>* Q) h' proof (prove)
goal (1 subgoal):
 1. x ## z proof (prove)
using this:
h ## z
h = x + y
x ## y

goal (1 subgoal):
 1. x ## z proof (state)
this:
x ## z

goal (1 subgoal):
 1. \<And>h h'. \<lbrakk>(P \<and>* Q) h; h \<preceq> h'\<rbrakk> \<Longrightarrow> (P \<and>* Q) h' proof (chain)
picking this:
intuitionistic P
P x
x ## z proof (prove)
using this:
intuitionistic P
P x
x ## z

goal (1 subgoal):
 1. P (x + z) proof (state)
this:
P (x + z)

goal (1 subgoal):
 1. \<And>h h'. \<lbrakk>(P \<and>* Q) h; h \<preceq> h'\<rbrakk> \<Longrightarrow> (P \<and>* Q) h' proof (prove)
using this:
P (x + z)

goal (1 subgoal):
 1. (P \<and>* Q) h' proof (prove)
using this:
P (x + z)
h' = h + z
h = x + y
h ## z
Q y
x ## y

goal (1 subgoal):
 1. (P \<and>* Q) h' proof (state)
this:
(P \<and>* Q) h'

goal:
No subgoals!
theory Separation_Algebra

lemma strongest_intuitionistic:
  "\<not>(\<exists>Q. (\<forall>h. (Q h \<longrightarrow> (P \<and>* sep_true) h)) \<and> intuitionistic Q \<and> Q \<noteq> (P \<and>* sep_true) \<and> (\<forall>h. P h \<longrightarrow> Q h))" by (fastforce intro!: ext sep_substate_disj_add dest!: sep_conjD intuitionisticD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<nexists>Q. (\<forall>h. Q h \<longrightarrow> (P \<and>* (\<lambda>s. True)) h) \<and> intuitionistic Q \<and> Q \<noteq> (P \<and>* (\<lambda>s. True)) \<and> (\<forall>h. P h \<longrightarrow> Q h)
theory Separation_Algebra

lemma intuitionistic_sep_conj_sep_true_simp:
  "intuitionistic P \<Longrightarrow> (P \<and>* sep_true) = P" by (fast intro!: sep_conj_sep_true
           elim: intuitionistic_sep_conj_sep_true_P)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. intuitionistic P \<Longrightarrow> (P \<and>* (\<lambda>s. True)) = P
theory Separation_Algebra

lemma intuitionistic_sep_impl_sep_true_P:
  "\<lbrakk> P h; intuitionistic P \<rbrakk> \<Longrightarrow> (sep_true \<longrightarrow>* P) h" by (force intro!: sep_implI dest: intuitionisticD
            intro: sep_substate_disj_add)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P h; intuitionistic P\<rbrakk> \<Longrightarrow> ((\<lambda>s. True) \<longrightarrow>* P) h