Theory 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"

  assumes sep_add_assoc:
    " 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)

lemma sep_add_left_commute:
  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
    by (simp add: sep_add_assoc[symmetric] sep_disj_commute)
  also have "... = a + b + c" using a
    by (simp add: sep_add_commute sep_disj_commute)
  also have "... = ?rhs" using a
    by (simp add: sep_add_assoc sep_disj_commute)
  finally show ?thesis .
qed

lemmas sep_add_ac = sep_add_assoc sep_add_commute sep_add_left_commute
                    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"


subsection ‹Disjunction/Addition Properties›

lemma disjoint_zero_sym [simp]: "0 ## x"
  by (simp add: sep_disj_commute)

lemma sep_add_zero_sym [simp]: "0 + x = x"
  by (simp add: sep_add_commute)

lemma sep_disj_addD2: " x ## y + z; y ## z   x ## z"
  by (metis sep_disj_addD1 sep_add_ac)

lemma sep_disj_addD: " x ## y + z; y ## z   x ## y  x ## z"
  by (metis sep_disj_addD1 sep_disj_addD2)

lemma sep_add_disjD: " x + y ## z; x ## y   x ## z  y ## z"
  by (metis sep_disj_addD sep_disj_commuteI)

lemma sep_disj_addI2:
  " x ## y + z; y ## z   x + z ## y"
  by (metis sep_add_ac sep_disj_addI1)

lemma sep_add_disjI1:
  " x + y ## z; x ## y   x + z ## y"
  by (metis sep_add_ac sep_add_disjD sep_disj_addI2)

lemma sep_add_disjI2:
  " x + y ## z; x ## y   z + y ## x"
  by (metis sep_add_ac sep_add_disjD sep_disj_addI2)

lemma sep_disj_addI3:
   "x + y ## z  x ## y  x ## y + z"
   by (metis sep_add_ac sep_add_disjD sep_add_disjI2)

lemma sep_disj_add:
  " y ## z; x ## y   x ## y + z = x + y ## z"
  by (metis sep_disj_addI1 sep_disj_addI3)


subsection ‹Substate Properties›

lemma sep_substate_disj_add:
  "x ## y  x  x + y"
  unfolding sep_substate_def by blast

lemma sep_substate_disj_add':
  "x ## y  x  y + x"
  by (simp add: sep_add_ac sep_substate_disj_add)


subsection ‹Separating Conjunction Properties›

lemma sep_conjD:
  "(P ∧* Q) h  x y. x ## y  h = x + y  P x  Q y"
  by (simp add: sep_conj_def)

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"
    by (simp add: sep_disj_add)
  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"
    by (fastforce elim!: sep_conjE simp: sep_add_ac dest: sep_disj_addD)
  thus "?lhs h"
    by (metis sep_conj_def sep_disj_addI1)
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"
  by (simp add: sep_empty_def)


subsection ‹Properties of sep_true› and sep_false›

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

lemma sep_conj_sep_true':
  "P h  (sep_true ** P) h"
  by (simp add: sep_conjI[where x=0])

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"
  by (simp add: sep_conj_def sep_empty_def)

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

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

lemma comm_monoid_add: "class.comm_monoid_add (**) "
  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)"
  by (simp add: sep_conj_assoc[symmetric])

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,
      simp add: sep_conj_ac)


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"
  by (simp add: pure_def)

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

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'))"
  by (simp add: conj_comms pure_conj_right)

lemma pure_conj_left: "((P' and Q') ∧* Q) = (P' and (Q' ∧* Q))"
  by (simp add: pure_conj_right sep_conj_ac)

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'

declare pure_conj[simp add]


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
    by (metis sep_add_disjI1 sep_disj_commute sep_conjI)
  ultimately show "(sep_true ∧* P) h'" using hzd
    by (auto simp: sep_conj_commute sep_add_ac dest!: sep_disj_addD)
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)
    apply (metis sep_add_assoc sep_add_disjD sep_disj_addI3 sep_implI)
    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
    by (metis sep_add_disjD)

  with ip px have "P (x + z)"
    by (fastforce elim: intuitionisticD sep_substate_disj_add)

  thus "(P ∧* 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

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
    by (metis sep_add_disjI1 sep_substate_def)

    with imp hzd iq px hzx
    have "Q (h + z + x)"
    by (metis intuitionisticD sep_add_assoc sep_add_ac sep_add_disjD sep_implE)
  }

  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))"
  by (fastforce intro!: ext sep_substate_disj_add
                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)
     apply (clarsimp simp: sep_add_ac sep_substate_disj_add)+
  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
            intro: sep_substate_disj_add)

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
            simp: sep_add_commute sep_add_assoc)

end

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

interpretation sep: comm_monoid_add "(**)" 
  by (rule comm_monoid_add)


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)"
  by (metis sep_add_disj_eq sep_disj_commute)

subclass sep_algebra by standard auto

end


section ‹Folding separating conjunction over lists of predicates›

lemma sep_list_conj_Nil [simp]: "⋀* [] = "
  by (simp add: sep_list_conj_def)

(* apparently these two are rarely used and had to be removed from List.thy *)
lemma (in semigroup_add) foldl_assoc:
shows "foldl (+) (x+y) zs = x + (foldl (+) y zs)"
by (induct zs arbitrary: y) (simp_all add:add.assoc)

lemma (in monoid_add) foldl_absorb0:
shows "x + (foldl (+) 0 zs) = foldl (+) x zs"
by (induct zs) (simp_all add:foldl_assoc)

lemma sep_list_conj_Cons [simp]: "⋀* (x#xs) = (x ** ⋀* xs)"
  by (simp add: sep_list_conj_def sep.foldl_absorb0)

lemma sep_list_conj_append [simp]: "⋀* (xs @ ys) = (⋀* xs ** ⋀* ys)"
  by (simp add: sep_list_conj_def sep.foldl_absorb0)

lemma (in comm_monoid_add) foldl_map_filter:
  "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 [xxs . ¬ 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)

lemma sep_add_cancel:
  "x ## z  y ## z  (x + z = y + z) = (x = y)"
  by (metis sep_add_cancelD)

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
        by (fastforce simp: sep_substate_disj_add' sep_disj_commute)
      from sxy' have ys': "y'  x' + y'" using xy'
        by (fastforce simp: sep_substate_disj_add' sep_disj_commute)

      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'
        by (fastforce dest!: sep_add_cancelD)

      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'
      by (fastforce simp: sep_add_ac)

    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
                    simp: sep_add_ac sep_add_cancel sep_conj_def)
  qed
qed

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

end

end