# Theory Separation_Algebra.Separation_Algebra

```(* Authors: Gerwin Klein and Rafal Kolanski, 2012
Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au>
Rafal Kolanski <rafal.kolanski at nicta.com.au>
*)

section "Abstract Separation Algebra"

theory Separation_Algebra
imports Main
begin

text ‹This theory is the main abstract separation algebra development›

section ‹Input syntax for lifting boolean predicates to separation predicates›

abbreviation (input)
pred_and :: "('a ⇒ bool) ⇒ ('a ⇒ bool) ⇒ 'a ⇒ bool" (infixr "and" 35) where
"a and b ≡ λs. a s ∧ b s"

abbreviation (input)
pred_or :: "('a ⇒ bool) ⇒ ('a ⇒ bool) ⇒ 'a ⇒ bool" (infixr "or" 30) where
"a or b ≡ λs. a s ∨ b s"

abbreviation (input)
pred_not :: "('a ⇒ bool) ⇒ 'a ⇒ bool" ("not _" [40] 40) where
"not a ≡ λs. ¬a s"

abbreviation (input)
pred_imp :: "('a ⇒ bool) ⇒ ('a ⇒ bool) ⇒ 'a ⇒ bool" (infixr "imp" 25) where
"a imp b ≡ λs. a s ⟶ b s"

abbreviation (input)
pred_K :: "'b ⇒ 'a ⇒ 'b" ("⟨_⟩") where
"⟨f⟩ ≡ λs. f"

abbreviation (input)
pred_ex :: "('b ⇒ 'a ⇒ bool) ⇒ 'a ⇒ bool" (binder "EXS " 10) where
"EXS x. P x ≡ λs. ∃x. P x s"

abbreviation (input)
pred_all :: "('b ⇒ 'a ⇒ bool) ⇒ 'a ⇒ bool" (binder "ALLS " 10) where
"ALLS x. P x ≡ λs. ∀x. P x s"

section ‹Associative/Commutative Monoid Basis of Separation Algebras›

class pre_sep_algebra = zero + plus +
fixes sep_disj :: "'a => 'a => bool" (infix "##" 60)

assumes sep_disj_zero [simp]: "x ## 0"
assumes sep_disj_commuteI: "x ## y ⟹ y ## x"

assumes sep_add_zero [simp]: "x + 0 = x"
assumes sep_add_commute: "x ## y ⟹ x + y = y + x"

"⟦ x ## y; y ## z; x ## z ⟧ ⟹ (x + y) + z = x + (y + z)"
begin

lemma sep_disj_commute: "x ## y = y ## x"
by (blast intro: sep_disj_commuteI)

assumes a: "a ## b" "b ## c" "a ## c"
shows "b + (a + c) = a + (b + c)" (is "?lhs = ?rhs")
proof -
have "?lhs = b + a + c" using a
also have "... = a + b + c" using a
also have "... = ?rhs" using a
finally show ?thesis .
qed

sep_disj_commute (* nearly always necessary *)

end

section ‹Separation Algebra as Defined by Calcagno et al.›

class sep_algebra = pre_sep_algebra +
assumes sep_disj_addD1: "⟦ x ## y + z; y ## z ⟧ ⟹ x ## y"
assumes sep_disj_addI1: "⟦ x ## y + z; y ## z ⟧ ⟹ x + y ##  z"
begin

subsection ‹Basic Construct Definitions and Abbreviations›

definition
sep_conj :: "('a ⇒ bool) ⇒ ('a ⇒ bool) ⇒ ('a ⇒ bool)" (infixr "**" 35)
where
"P ** Q ≡ λh. ∃x y. x ## y ∧ h = x + y ∧ P x ∧ Q y"

notation
sep_conj (infixr "∧*" 35)

definition
sep_empty :: "'a ⇒ bool" ("□") where
"□ ≡ λh. h = 0"

definition
sep_impl :: "('a ⇒ bool) ⇒ ('a ⇒ bool) ⇒ ('a ⇒ bool)" (infixr "⟶*" 25)
where
"P ⟶* Q ≡ λh. ∀h'. h ## h' ∧ P h' ⟶ Q (h + h')"

definition
sep_substate :: "'a => 'a => bool" (infix "≼" 60) where
"x ≼ y ≡ ∃z. x ## z ∧ x + z = y"

(* We want these to be abbreviations not definitions, because basic True and
False will occur by simplification in sep_conj terms *)
abbreviation
"sep_true ≡ ⟨True⟩"

abbreviation
"sep_false ≡ ⟨False⟩"

definition
sep_list_conj :: "('a ⇒ bool) list ⇒ ('a ⇒ bool)"  ("⋀* _" [60] 90) where
"sep_list_conj Ps ≡ foldl (**) □ Ps"

lemma disjoint_zero_sym [simp]: "0 ## x"

lemma sep_add_zero_sym [simp]: "0 + x = x"

lemma sep_disj_addD2: "⟦ x ## y + z; y ## z ⟧ ⟹ x ## z"

lemma sep_disj_addD: "⟦ x ## y + z; y ## z ⟧ ⟹ x ## y ∧ x ## z"

lemma sep_add_disjD: "⟦ x + y ## z; x ## y ⟧ ⟹ x ## z ∧ y ## z"

"⟦ x ## y + z; y ## z ⟧ ⟹ x + z ## y"

"⟦ x + y ## z; x ## y ⟧ ⟹ x + z ## y"

"⟦ x + y ## z; x ## y ⟧ ⟹ z + y ## x"

"x + y ## z ⟹ x ## y ⟹ x ## y + z"

"⟦ y ## z; x ## y ⟧ ⟹ x ## y + z = x + y ## z"

subsection ‹Substate Properties›

"x ## y ⟹ x ≼ x + y"
unfolding sep_substate_def by blast

"x ## y ⟹ x ≼ y + x"

subsection ‹Separating Conjunction Properties›

lemma sep_conjD:
"(P ∧* Q) h ⟹ ∃x y. x ## y ∧ h = x + y ∧ P x ∧ Q y"

lemma sep_conjE:
"⟦ (P ** Q) h; ⋀x y. ⟦ P x; Q y; x ## y; h = x + y ⟧ ⟹ X ⟧ ⟹ X"
by (auto simp: sep_conj_def)

lemma sep_conjI:
"⟦ P x; Q y; x ## y; h = x + y ⟧ ⟹ (P ** Q) h"
by (auto simp: sep_conj_def)

lemma sep_conj_commuteI:
"(P ** Q) h ⟹ (Q ** P) h"
by (auto intro!: sep_conjI elim!: sep_conjE simp: sep_add_ac)

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

lemma sep_conj_assoc:
"((P ** Q) ** R) = (P ** Q ** R)" (is "?lhs = ?rhs")
proof (rule ext, rule iffI)
fix h
assume a: "?lhs h"
then obtain x y z where "P x" and "Q y" and "R z"
and "x ## y" and "x ## z" and "y ## z" and "x + y ## z"
and "h = x + y + z"
by (auto dest!: sep_conjD dest: sep_add_disjD)
moreover
then have "x ## y + z"
ultimately
show "?rhs h"
by (auto simp: sep_add_ac intro!: sep_conjI)
next
fix h
assume a: "?rhs h"
then obtain x y z where "P x" and "Q y" and "R z"
and "x ## y" and "x ## z" and "y ## z" and "x ## y + z"
and "h = x + y + z"
thus "?lhs h"
qed

lemma sep_conj_impl:
"⟦ (P ** Q) h; ⋀h. P h ⟹ P' h; ⋀h. Q h ⟹ Q' h ⟧ ⟹ (P' ** Q') h"
by (erule sep_conjE, auto intro!: sep_conjI)

lemma sep_conj_impl1:
assumes P: "⋀h. P h ⟹ I h"
shows "(P ** R) h ⟹ (I ** R) h"
by (auto intro: sep_conj_impl P)

lemma sep_globalise:
"⟦ (P ** R) h; (⋀h. P h ⟹ Q h) ⟧ ⟹ (Q ** R) h"
by (fast elim: sep_conj_impl)

lemma sep_conj_trivial_strip2:
"Q = R ⟹ (Q ** P) = (R ** P)" by simp

lemma disjoint_subheaps_exist:
"∃x y. x ## y ∧ h = x + y"
by (rule_tac x=0 in exI, auto)

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 "… = (Q ** (R ** P))" by (subst sep_conj_assoc, simp)
finally show ?thesis by (simp add: sep_conj_commute)
qed

lemmas sep_conj_ac = sep_conj_commute sep_conj_assoc sep_conj_left_commute

lemma ab_semigroup_mult_sep_conj: "class.ab_semigroup_mult (**)"
by (unfold_locales)
(auto simp: sep_conj_ac)

lemma sep_empty_zero [simp,intro!]: "□ 0"

subsection ‹Properties of ‹sep_true› and ‹sep_false››

lemma sep_conj_sep_true:
"P h ⟹ (P ** sep_true) h"

lemma sep_conj_sep_true':
"P h ⟹ (sep_true ** P) h"

lemma sep_conj_true [simp]:
"(sep_true ** sep_true) = sep_true"
unfolding sep_conj_def
by (auto intro!: ext intro: disjoint_subheaps_exist)

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

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

subsection ‹Properties of zero (@{const sep_empty})›

lemma sep_conj_empty [simp]:
"(P ** □) = P"

lemma sep_conj_empty'[simp]:
"(□ ** P) = P"
by (subst sep_conj_commute, rule sep_conj_empty)

lemma sep_conj_sep_emptyI:
"P h ⟹ (P ** □) h"
by simp

lemma sep_conj_sep_emptyE:
"⟦ P s; (P ** □) s ⟹ (Q ** R) s ⟧ ⟹ (Q ** R) s"
by simp

by (unfold_locales) (auto simp: sep_conj_ac)

by (unfold_locales) (auto simp: sep_conj_ac)

subsection ‹Properties of top (‹sep_true›)›

lemma sep_conj_true_P [simp]:
"(sep_true ** (sep_true ** P)) = (sep_true ** P)"

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

lemma sep_conj_sep_true_left:
"(P ** Q) h ⟹ (sep_true ** Q) h"
by (erule sep_conj_impl, simp+)

lemma sep_conj_sep_true_right:
"(P ** Q) h ⟹ (P ** sep_true) h"
by (subst (asm) sep_conj_commute, drule sep_conj_sep_true_left,

subsection ‹Separating Conjunction with Quantifiers›

lemma sep_conj_conj:
"((P and Q) ** R) h ⟹ ((P ** R) and (Q ** R)) h"
by (force intro: sep_conjI elim!: sep_conjE)

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

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

lemmas sep_conj_exists = sep_conj_exists1 sep_conj_exists2

lemma sep_conj_spec:
"((ALLS x. P x) ** Q) h ⟹ (P x ** Q) h"
by (force intro: sep_conjI elim: sep_conjE)

subsection ‹Properties of Separating Implication›

lemma sep_implI:
assumes a: "⋀h'. ⟦ h ## h'; P h' ⟧ ⟹ Q (h + h')"
shows "(P ⟶* Q) h"
unfolding sep_impl_def by (auto elim: a)

lemma sep_implD:
"(x ⟶* y) h ⟹ ∀h'. h ## h' ∧ x h' ⟶ y (h + h')"
by (force simp: sep_impl_def)

lemma sep_implE:
"(x ⟶* y) h ⟹ (∀h'. h ## h' ∧ x h' ⟶ y (h + h') ⟹ Q) ⟹ Q"
by (auto dest: sep_implD)

lemma sep_impl_sep_true [simp]:
"(P ⟶* sep_true) = sep_true"
by (force intro!: sep_implI ext)

lemma sep_impl_sep_false [simp]:
"(sep_false ⟶* P) = sep_true"
by (force intro!: sep_implI ext)

lemma sep_impl_sep_true_P:
"(sep_true ⟶* P) h ⟹ P h"
by (clarsimp dest!: sep_implD elim!: allE[where x=0])

lemma sep_impl_sep_true_false [simp]:
"(sep_true ⟶* sep_false) = sep_false"
by (force intro!: ext dest: sep_impl_sep_true_P)

lemma sep_conj_sep_impl:
"⟦ P h; ⋀h. (P ** Q) h ⟹ R h ⟧ ⟹ (Q ⟶* 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 "⋀h. (P ** Q) h ⟹ R h"
ultimately show "R (h + h')" by simp
qed

lemma sep_conj_sep_impl2:
"⟦ (P ** Q) h; ⋀h. P h ⟹ (Q ⟶* R) h ⟧ ⟹ R h"
by (force dest: sep_implD elim: sep_conjE)

lemma sep_conj_sep_impl_sep_conj2:
"(P ** R) h ⟹ (P ** (Q ⟶* (Q ** R))) h"
by (erule (1) sep_conj_impl, erule sep_conj_sep_impl, simp add: sep_conj_ac)

subsection ‹Pure assertions›

definition
pure :: "('a ⇒ bool) ⇒ bool" where
"pure P ≡ ∀h h'. P h = P h'"

lemma pure_sep_true:
"pure sep_true"

lemma pure_sep_false:
"pure sep_true"

lemma pure_split:
"pure P = (P = sep_true ∨ P = sep_false)"
by (force simp: pure_def intro!: ext)

lemma pure_sep_conj:
"⟦ pure P; pure Q ⟧ ⟹ pure (P ∧* Q)"
by (force simp: pure_split)

lemma pure_sep_impl:
"⟦ pure P; pure Q ⟧ ⟹ pure (P ⟶* Q)"
by (force simp: pure_split)

lemma pure_conj_sep_conj:
"⟦ (P and Q) h; pure P ∨ pure Q ⟧ ⟹ (P ∧* Q) h"
by (metis pure_def sep_add_zero sep_conjI sep_conj_commute sep_disj_zero)

lemma pure_sep_conj_conj:
"⟦ (P ∧* Q) h; pure P; pure Q ⟧ ⟹ (P and Q) h"
by (force simp: pure_split)

lemma pure_conj_sep_conj_assoc:
"pure P ⟹ ((P and Q) ∧* R) = (P and (Q ∧* R))"
by (auto simp: pure_split)

lemma pure_sep_impl_impl:
"⟦ (P ⟶* Q) h; pure P ⟧ ⟹ P h ⟶ Q h"
by (force simp: pure_split dest: sep_impl_sep_true_P)

lemma pure_impl_sep_impl:
"⟦ P h ⟶ Q h; pure P; pure Q ⟧ ⟹ (P ⟶* Q) h"
by (force simp: pure_split)

lemma pure_conj_right: "(Q ∧* (⟨P'⟩ and Q')) = (⟨P'⟩ and (Q ∧* Q'))"
by (rule ext, rule, rule, clarsimp elim!: sep_conjE)
(erule sep_conj_impl, auto)

lemma pure_conj_right': "(Q ∧* (P' and ⟨Q'⟩)) = (⟨Q'⟩ and (Q ∧* P'))"

lemma pure_conj_left: "((⟨P'⟩ and Q') ∧* Q) = (⟨P'⟩ and (Q' ∧* Q))"

lemma pure_conj_left': "((P' and ⟨Q'⟩) ∧* Q) = (⟨Q'⟩ and (P' ∧* Q))"
by (subst conj_comms, subst pure_conj_left, simp)

lemmas pure_conj = pure_conj_right pure_conj_right' pure_conj_left
pure_conj_left'

subsection ‹Intuitionistic assertions›

definition intuitionistic :: "('a ⇒ bool) ⇒ bool" where
"intuitionistic P ≡ ∀h h'. P h ∧ h ≼ h' ⟶ P h'"

lemma intuitionisticI:
"(⋀h h'. ⟦ P h; h ≼ h' ⟧ ⟹ P h') ⟹ intuitionistic P"
by (unfold intuitionistic_def, fast)

lemma intuitionisticD:
"⟦ intuitionistic P; P h; h ≼ h' ⟧ ⟹ P h'"
by (unfold intuitionistic_def, fast)

lemma pure_intuitionistic:
"pure P ⟹ intuitionistic P"
by (clarsimp simp: intuitionistic_def pure_def, fast)

lemma intuitionistic_conj:
"⟦ intuitionistic P; intuitionistic Q ⟧ ⟹ intuitionistic (P and Q)"
by (force intro: intuitionisticI dest: intuitionisticD)

lemma intuitionistic_disj:
"⟦ intuitionistic P; intuitionistic Q ⟧ ⟹ intuitionistic (P or Q)"
by (force intro: intuitionisticI dest: intuitionisticD)

lemma intuitionistic_forall:
"(⋀x. intuitionistic (P x)) ⟹ intuitionistic (ALLS x. P x)"
by (force intro: intuitionisticI dest: intuitionisticD)

lemma intuitionistic_exists:
"(⋀x. intuitionistic (P x)) ⟹ intuitionistic (EXS x. P x)"
by (force intro: intuitionisticI dest: intuitionisticD)

lemma intuitionistic_sep_conj_sep_true:
"intuitionistic (sep_true ∧* P)"
proof (rule intuitionisticI)
fix h h' r
assume a: "(sep_true ∧* P) h"
then obtain x y where P: "P y" and h: "h = x + y" and xyd: "x ## y"
by - (drule sep_conjD, clarsimp)
moreover assume a2: "h ≼ h'"
then obtain z where h': "h' = h + z" and hzd: "h ## z"
by (clarsimp simp: sep_substate_def)

moreover have "(P ∧* sep_true) (y + (x + z))"
using P h hzd xyd
ultimately show "(sep_true ∧* P) h'" using hzd
qed

lemma intuitionistic_sep_impl_sep_true:
"intuitionistic (sep_true ⟶* P)"
proof (rule intuitionisticI)
fix h h'
assume imp: "(sep_true ⟶* P) h" and hh': "h ≼ h'"

from hh' obtain z where h': "h' = h + z" and hzd: "h ## z"
by (clarsimp simp: sep_substate_def)
show "(sep_true ⟶* P) h'" using imp h' hzd
apply (clarsimp dest!: sep_implD)
done
qed

lemma intuitionistic_sep_conj:
assumes ip: "intuitionistic (P::('a ⇒ bool))"
shows "intuitionistic (P ∧* Q)"
proof (rule intuitionisticI)
fix h h'
assume sc: "(P ∧* Q) h" and hh': "h ≼ 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

with ip px have "P (x + z)"

thus "(P ∧* Q) h'" using h' h hzd qy xyd
qed

lemma intuitionistic_sep_impl:
assumes iq: "intuitionistic Q"
shows "intuitionistic (P ⟶* Q)"
proof (rule intuitionisticI)
fix h h'
assume imp: "(P ⟶* Q) h" and hh': "h ≼ h'"

from hh' obtain z where h': "h' = h + z" and hzd: "h ## z"
by (clarsimp simp: sep_substate_def)

{
fix x
assume px: "P x" and hzx: "h + z ## x"

have "h + x ≼ h + x + z" using hzx hzd

with imp hzd iq px hzx
have "Q (h + z + x)"
}

with imp h' hzd iq show "(P ⟶* Q) h'"
by (fastforce intro: sep_implI)
qed

lemma strongest_intuitionistic:
"¬ (∃Q. (∀h. (Q h ⟶ (P ∧* sep_true) h)) ∧ intuitionistic Q ∧
Q ≠ (P ∧* sep_true) ∧ (∀h. P h ⟶ Q h))"
dest!: sep_conjD intuitionisticD)

lemma weakest_intuitionistic:
"¬ (∃Q. (∀h. ((sep_true ⟶* P) h ⟶ Q h)) ∧ intuitionistic Q ∧
Q ≠ (sep_true ⟶* P) ∧ (∀h. Q h ⟶ P h))"
apply (clarsimp intro!: ext)
apply (rule iffI)
apply (rule sep_implI)
apply (drule_tac h="x" and h'="x + h'" in intuitionisticD)
done

lemma intuitionistic_sep_conj_sep_true_P:
"⟦ (P ∧* sep_true) s; intuitionistic P ⟧ ⟹ P s"
by (force dest: intuitionisticD elim: sep_conjE sep_substate_disj_add)

lemma intuitionistic_sep_conj_sep_true_simp:
"intuitionistic P ⟹ (P ∧* sep_true) = P"
by (fast intro!: sep_conj_sep_true ext
elim: intuitionistic_sep_conj_sep_true_P)

lemma intuitionistic_sep_impl_sep_true_P:
"⟦ P h; intuitionistic P ⟧ ⟹ (sep_true ⟶* P) h"
by (force intro!: sep_implI dest: intuitionisticD

lemma intuitionistic_sep_impl_sep_true_simp:
"intuitionistic P ⟹ (sep_true ⟶* P) = P"
by (fast intro!: ext
elim: sep_impl_sep_true_P intuitionistic_sep_impl_sep_true_P)

subsection ‹Strictly exact assertions›

definition strictly_exact :: "('a ⇒ bool) ⇒ bool" where
"strictly_exact P ≡ ∀h h'. P h ∧ P h' ⟶ h = h'"

lemma strictly_exactD:
"⟦ strictly_exact P; P h; P h' ⟧ ⟹ h = h'"
by (unfold strictly_exact_def, fast)

lemma strictly_exactI:
"(⋀h h'. ⟦ P h; P h' ⟧ ⟹ h = h') ⟹ strictly_exact P"
by (unfold strictly_exact_def, fast)

lemma strictly_exact_sep_conj:
"⟦ strictly_exact P; strictly_exact Q ⟧ ⟹ strictly_exact (P ∧* Q)"
apply (rule strictly_exactI)
apply (erule sep_conjE)+
apply (drule_tac h="x" and h'="xa" in strictly_exactD, assumption+)
apply (drule_tac h="y" and h'="ya" in strictly_exactD, assumption+)
apply clarsimp
done

lemma strictly_exact_conj_impl:
"⟦ (Q ∧* sep_true) h; P h; strictly_exact Q ⟧ ⟹ (Q ∧* (Q ⟶* P)) h"
by (force intro: sep_conjI sep_implI dest: strictly_exactD elim!: sep_conjE

end

interpretation sep: ab_semigroup_mult "(**)"
by (rule ab_semigroup_mult_sep_conj)

section ‹Separation Algebra with Stronger, but More Intuitive Disjunction Axiom›

class stronger_sep_algebra = pre_sep_algebra +
assumes sep_add_disj_eq [simp]: "y ## z ⟹ x ## y + z = (x ## y ∧ x ## z)"
begin

lemma sep_disj_add_eq [simp]: "x ## y ⟹ x + y ## z = (x ## z ∧ y ## z)"

subclass sep_algebra by standard auto

end

section ‹Folding separating conjunction over lists of predicates›

lemma sep_list_conj_Nil [simp]: "⋀* [] = □"

(* apparently these two are rarely used and had to be removed from List.thy *)
shows "foldl (+) (x+y) zs = x + (foldl (+) y zs)"

shows "x + (foldl (+) 0 zs) = foldl (+) x zs"

lemma sep_list_conj_Cons [simp]: "⋀* (x#xs) = (x ** ⋀* xs)"

lemma sep_list_conj_append [simp]: "⋀* (xs @ ys) = (⋀* xs ** ⋀* ys)"

"foldl (+) 0 (map f (filter P xs)) +
foldl (+) 0 (map f (filter (not P) xs))
= foldl (+) 0 (map f xs)"
proof (induct xs)
case Nil thus ?case by clarsimp
next
case (Cons x xs)
hence IH: "foldl (+) 0 (map f xs) =
foldl (+) 0 (map f (filter P xs)) +
foldl (+) 0 (map f [x←xs . ¬ P x])"
by (simp only: eq_commute)

have foldl_Cons':
"⋀x xs. foldl (+) 0 (x # xs) = x + (foldl (+) 0 xs)"
by (simp, subst foldl_absorb0[symmetric], rule refl)

{ assume "P x"
hence ?case by (auto simp del: foldl_Cons simp add: foldl_Cons' IH ac_simps)
} moreover {
assume "¬ P x"
hence ?case by (auto simp del: foldl_Cons simp add: foldl_Cons' IH ac_simps)
}
ultimately show ?case by blast
qed

section ‹Separation Algebra with a Cancellative Monoid (for completeness)›

text ‹
Separation algebra with a cancellative monoid. The results of being a precise
assertion (distributivity over separating conjunction) require this.
although we never actually use this property in our developments, we keep
it here for completeness.
›
class cancellative_sep_algebra = sep_algebra +
assumes sep_add_cancelD: "⟦ x + z = y + z ; x ## z ; y ## z ⟧ ⟹ x = y"
begin

definition
(* In any heap, there exists at most one subheap for which P holds *)
precise :: "('a ⇒ bool) ⇒ bool" where
"precise P = (∀h hp hp'. hp ≼ h ∧ P hp ∧ hp' ≼ h ∧ P hp' ⟶ hp = hp')"

lemma "precise ((=) s)"
by (metis (full_types) precise_def)

"x ## z ⟹ y ## z ⟹ (x + z = y + z) = (x = y)"

lemma precise_distribute:
"precise P = (∀Q R. ((Q and R) ∧* P) = ((Q ∧* P) and (R ∧* P)))"
proof (rule iffI)
assume pp: "precise P"
{
fix Q R
fix h hp hp' s

{ assume a: "((Q and R) ∧* P) s"
hence "((Q ∧* P) and (R ∧* P)) s"
by (fastforce dest!: sep_conjD elim: sep_conjI)
}
moreover
{ assume qs: "(Q ∧* P) s" and qr: "(R ∧* P) s"

from qs obtain x y where sxy: "s = x + y" and xy: "x ## y"
and x: "Q x" and y: "P y"
by (fastforce dest!: sep_conjD)
from qr obtain x' y' where sxy': "s = x' + y'" and xy': "x' ## y'"
and x': "R x'" and y': "P y'"
by (fastforce dest!: sep_conjD)

from sxy have ys: "y ≼ x + y" using xy
from sxy' have ys': "y' ≼ x' + y'" using xy'

from pp have yy: "y = y'" using sxy sxy' xy xy' y y' ys ys'
by (fastforce simp: precise_def)

hence "x = x'" using sxy sxy' xy xy'

hence "((Q and R) ∧* P) s" using sxy x x' yy y' xy'
by (fastforce intro: sep_conjI)
}
ultimately
have "((Q and R) ∧* P) s = ((Q ∧* P) and (R ∧* P)) s" using pp by blast
}
thus "∀Q R. ((Q and R) ∧* P) = ((Q ∧* P) and (R ∧* P))" by (blast intro!: ext)

next
assume a: "∀Q R. ((Q and R) ∧* P) = ((Q ∧* P) and (R ∧* P))"
thus "precise P"
proof (clarsimp simp: precise_def)
fix h hp hp' Q R
assume hp: "hp ≼ h" and hp': "hp' ≼ h" and php: "P hp" and php': "P hp'"

obtain z where hhp: "h = hp + z" and hpz: "hp ## z" using hp
by (clarsimp simp: sep_substate_def)
obtain z' where hhp': "h = hp' + z'" and hpz': "hp' ## z'" using hp'
by (clarsimp simp: sep_substate_def)

have h_eq: "z' + hp' = z + hp" using hhp hhp' hpz hpz'

from hhp hhp' a hpz hpz' h_eq
have "∀Q R. ((Q and R) ∧* P) (z + hp) = ((Q ∧* P) and (R ∧* P)) (z' + hp')"
by (fastforce simp: h_eq sep_add_ac sep_conj_commute)

hence "(((=) z and (=) z') ∧* P) (z + hp) =
(((=) z ∧* P) and ((=) z' ∧* P)) (z' + hp')" by blast

thus  "hp = hp'" using php php' hpz hpz' h_eq
by (fastforce dest!: iffD2 cong: conj_cong
qed
qed

lemma strictly_precise: "strictly_exact P ⟹ precise P"
by (metis precise_def strictly_exactD)

end

end
```