(* Authors: Gerwin Klein and Rafal Kolanski, 2012

   Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au>

                Rafal Kolanski <rafal.kolanski at nicta.com.au>

*)

header "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 \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "and" 35) where

  "a and b \<equiv> \<lambda>s. a s \<and> b s"

abbreviation (input)

  pred_or :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "or" 30) where

  "a or b \<equiv> \<lambda>s. a s \<or> b s"

abbreviation (input)

  pred_not :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" ("not _" [40] 40) where

  "not a \<equiv> \<lambda>s. \<not>a s"

abbreviation (input)

  pred_imp :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "imp" 25) where

  "a imp b \<equiv> \<lambda>s. a s \<longrightarrow> b s"

abbreviation (input)

  pred_K :: "'b \<Rightarrow> 'a \<Rightarrow> 'b" ("\<langle>_\<rangle>") where

  "\<langle>f\<rangle> \<equiv> \<lambda>s. f"

(* was an abbreviation *)

  definition pred_ex :: "('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" (binder "EXS " 10) where

  "EXS x. P x \<equiv> \<lambda>s. \<exists>x. P x s"

abbreviation (input)

  pred_all :: "('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" (binder "ALLS " 10) where

  "ALLS x. P x \<equiv> \<lambda>s. \<forall>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 \<Longrightarrow> y ## x"

  assumes sep_add_zero [simp]: "x + 0 = x"

  assumes sep_add_commute: "x ## y \<Longrightarrow> x + y = y + x"

  assumes sep_add_assoc:

    "\<lbrakk> x ## y; y ## z; x ## z \<rbrakk> \<Longrightarrow> (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: "\<lbrakk> x ## y + z; y ## z \<rbrakk> \<Longrightarrow> x ## y"

  assumes sep_disj_addI1: "\<lbrakk> x ## y + z; y ## z \<rbrakk> \<Longrightarrow> x + y ##  z"

begin

subsection {* Basic Construct Definitions and Abbreviations *}

definition

  sep_conj :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)" (infixr "**" 35)

  where

  "P ** Q \<equiv> \<lambda>h. \<exists>x y. x ## y \<and> h = x + y \<and> P x \<and> Q y"

notation

  sep_conj (infixr "\<and>*" 35)

definition

  sep_empty :: "'a \<Rightarrow> bool" ("\<box>") where

  "\<box> \<equiv> \<lambda>h. h = 0"

definition

  sep_impl :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)" (infixr "\<longrightarrow>*" 25)

  where

  "P \<longrightarrow>* Q \<equiv> \<lambda>h. \<forall>h'. h ## h' \<and> P h' \<longrightarrow> Q (h + h')"

definition

  sep_substate :: "'a => 'a => bool" (infix "\<preceq>" 60) where

  "x \<preceq> y \<equiv> \<exists>z. x ## z \<and> 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 \<equiv> \<langle>True\<rangle>"

abbreviation

  "sep_false \<equiv> \<langle>False\<rangle>"

definition

  sep_list_conj :: "('a \<Rightarrow> bool) list \<Rightarrow> ('a \<Rightarrow> bool)"  ("\<And>* _" [60] 90) where

  "sep_list_conj Ps \<equiv> foldl (op **) \<box> 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: "\<lbrakk> x ## y + z; y ## z \<rbrakk> \<Longrightarrow> x ## z"

  by (metis sep_disj_addD1 sep_add_ac)

lemma sep_disj_addD: "\<lbrakk> x ## y + z; y ## z \<rbrakk> \<Longrightarrow> x ## y \<and> x ## z"

  by (metis sep_disj_addD1 sep_disj_addD2)

lemma sep_add_disjD: "\<lbrakk> x + y ## z; x ## y \<rbrakk> \<Longrightarrow> x ## z \<and> y ## z"

  by (metis sep_disj_addD sep_disj_commuteI)

lemma sep_disj_addI2:

  "\<lbrakk> x ## y + z; y ## z \<rbrakk> \<Longrightarrow> x + z ## y"

  by (metis sep_add_ac sep_disj_addI1)

lemma sep_add_disjI1:

  "\<lbrakk> x + y ## z; x ## y \<rbrakk> \<Longrightarrow> x + z ## y"

  by (metis sep_add_ac sep_add_disjD sep_disj_addI2)

lemma sep_add_disjI2:

  "\<lbrakk> x + y ## z; x ## y \<rbrakk> \<Longrightarrow> z + y ## x"

  by (metis sep_add_ac sep_add_disjD sep_disj_addI2)

lemma sep_disj_addI3:

   "x + y ## z \<Longrightarrow> x ## y \<Longrightarrow> x ## y + z"

   by (metis sep_add_ac sep_add_disjD sep_add_disjI2)

lemma sep_disj_add:

  "\<lbrakk> y ## z; x ## y \<rbrakk> \<Longrightarrow> x ## y + z = x + y ## z"

  by (metis sep_disj_addI1 sep_disj_addI3)

subsection {* Substate Properties *}

lemma sep_substate_disj_add:

  "x ## y \<Longrightarrow> x \<preceq> x + y"

  unfolding sep_substate_def by blast

lemma sep_substate_disj_add':

  "x ## y \<Longrightarrow> x \<preceq> y + x"

  by (simp add: sep_add_ac sep_substate_disj_add)

subsection {* Separating Conjunction Properties *}

lemma sep_conjD:

  "(P \<and>* Q) h \<Longrightarrow> \<exists>x y. x ## y \<and> h = x + y \<and> P x \<and> Q y"

  by (simp add: sep_conj_def)

lemma sep_conjE:

  "\<lbrakk> (P ** Q) h; \<And>x y. \<lbrakk> P x; Q y; x ## y; h = x + y \<rbrakk> \<Longrightarrow> X \<rbrakk> \<Longrightarrow> X"

  by (auto simp: sep_conj_def)

lemma sep_conjI:

  "\<lbrakk> P x; Q y; x ## y; h = x + y \<rbrakk> \<Longrightarrow> (P ** Q) h"

  by (auto simp: sep_conj_def)

lemma sep_conj_commuteI:

  "(P ** Q) h \<Longrightarrow> (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:

  "\<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)

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)

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)

lemma sep_conj_trivial_strip2:

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

lemma disjoint_subheaps_exist:

  "\<exists>x y. x ## y \<and> 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 "\<dots> = (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 op **"

  by (unfold_locales)

     (auto simp: sep_conj_ac)

lemma sep_empty_zero [simp,intro!]: "\<box> 0"

  by (simp add: sep_empty_def)

subsection {* Properties of @{text sep_true} and @{text sep_false} *}

lemma sep_conj_sep_true:

  "P h \<Longrightarrow> (P ** sep_true) h"

  by (simp add: sep_conjI[where y=0])

lemma sep_conj_sep_true':

  "P h \<Longrightarrow> (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 ** \<box>) = P"

  by (simp add: sep_conj_def sep_empty_def)

lemma sep_conj_empty'[simp]:

  "(\<box> ** P) = P"

  by (subst sep_conj_commute, rule sep_conj_empty)

lemma sep_conj_sep_emptyI:

  "P h \<Longrightarrow> (P ** \<box>) h"

  by simp

lemma sep_conj_sep_emptyE:

  "\<lbrakk> P s; (P ** \<box>) s \<Longrightarrow> (Q ** R) s \<rbrakk> \<Longrightarrow> (Q ** R) s"

  by simp

lemma monoid_add: "class.monoid_add (op **) \<box>"

  by (unfold_locales) (auto simp: sep_conj_ac)

lemma comm_monoid_add: "class.comm_monoid_add op ** \<box>"

  by (unfold_locales) (auto simp: sep_conj_ac)

subsection {* Properties of top (@{text 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 \<Longrightarrow> (sep_true ** Q) h"

  by (erule sep_conj_impl, simp+)

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)

subsection {* Separating Conjunction with Quantifiers *}

lemma sep_conj_conj:

  "((P and Q) ** R) h \<Longrightarrow> ((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 (unfold pred_ex_def, force intro!: ext intro: sep_conjI elim: sep_conjE)

lemma sep_conj_exists2:

  "(P ** (EXS x. Q x)) = (EXS x. P ** Q x)"

  by (unfold pred_ex_def, 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 \<Longrightarrow> (P x ** Q) h"

  by (force intro: sep_conjI elim: sep_conjE)

subsection {* Properties of Separating Implication *}

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)

lemma sep_implD:

  "(x \<longrightarrow>* y) h \<Longrightarrow> \<forall>h'. h ## h' \<and> x h' \<longrightarrow> y (h + h')"

  by (force simp: sep_impl_def)

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)

lemma sep_impl_sep_true [simp]:

  "(P \<longrightarrow>* sep_true) = sep_true"

  by (force intro!: sep_implI ext)

lemma sep_impl_sep_false [simp]:

  "(sep_false \<longrightarrow>* P) = sep_true"

  by (force intro!: sep_implI ext)

lemma sep_impl_sep_true_P:

  "(sep_true \<longrightarrow>* P) h \<Longrightarrow> P h"

  by (clarsimp dest!: sep_implD elim!: allE[where x=0])

lemma sep_impl_sep_true_false [simp]:

  "(sep_true \<longrightarrow>* sep_false) = sep_false"

  by (force intro!: ext dest: sep_impl_sep_true_P)

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

lemma sep_conj_sep_impl2:

  "\<lbrakk> (P ** Q) h; \<And>h. P h \<Longrightarrow> (Q \<longrightarrow>* R) h \<rbrakk> \<Longrightarrow> R h"

  by (force dest: sep_implD elim: sep_conjE)

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)

subsection {* Pure assertions *}

definition

  pure :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where

  "pure P \<equiv> \<forall>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 \<or> P = sep_false)"

  by (force simp: pure_def intro!: ext)

lemma pure_sep_conj:

  "\<lbrakk> pure P; pure Q \<rbrakk> \<Longrightarrow> pure (P \<and>* Q)"

  by (force simp: pure_split)

lemma pure_sep_impl:

  "\<lbrakk> pure P; pure Q \<rbrakk> \<Longrightarrow> pure (P \<longrightarrow>* Q)"

  by (force simp: pure_split)

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)

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)

lemma pure_conj_sep_conj_assoc:

  "pure P \<Longrightarrow> ((P and Q) \<and>* R) = (P and (Q \<and>* R))"

  by (auto simp: pure_split)

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)

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)

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

  by (rule ext, rule, rule, clarsimp elim!: sep_conjE)

     (erule sep_conj_impl, auto)

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)

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)

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)

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 \<Rightarrow> bool) \<Rightarrow> bool" where

  "intuitionistic P \<equiv> \<forall>h h'. P h \<and> h \<preceq> h' \<longrightarrow> P h'"

lemma intuitionisticI:

  "(\<And>h h'. \<lbrakk> P h; h \<preceq> h' \<rbrakk> \<Longrightarrow> P h') \<Longrightarrow> intuitionistic P"

  by (unfold intuitionistic_def, fast)

lemma intuitionisticD:

  "\<lbrakk> intuitionistic P; P h; h \<preceq> h' \<rbrakk> \<Longrightarrow> P h'"

  by (unfold intuitionistic_def, fast)

lemma pure_intuitionistic:

  "pure P \<Longrightarrow> intuitionistic P"

  by (clarsimp simp: intuitionistic_def pure_def, fast)

lemma intuitionistic_conj:

  "\<lbrakk> intuitionistic P; intuitionistic Q \<rbrakk> \<Longrightarrow> intuitionistic (P and Q)"

  by (force intro: intuitionisticI dest: intuitionisticD)

lemma intuitionistic_disj:

  "\<lbrakk> intuitionistic P; intuitionistic Q \<rbrakk> \<Longrightarrow> intuitionistic (P or Q)"

  by (force intro: intuitionisticI dest: intuitionisticD)

lemma intuitionistic_forall:

  "(\<And>x. intuitionistic (P x)) \<Longrightarrow> intuitionistic (ALLS x. P x)"

  by (force intro: intuitionisticI dest: intuitionisticD)

lemma intuitionistic_exists:

  "(\<And>x. intuitionistic (P x)) \<Longrightarrow> intuitionistic (EXS x. P x)"

  by (unfold pred_ex_def, force intro: intuitionisticI dest: intuitionisticD)

lemma intuitionistic_sep_conj_sep_true:

  "intuitionistic (sep_true \<and>* P)"

proof (rule intuitionisticI)

  fix h h' r

  assume a: "(sep_true \<and>* 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 \<preceq> h'"

  then obtain z where h': "h' = h + z" and hzd: "h ## z"

    by (clarsimp simp: sep_substate_def)

  moreover have "(P \<and>* sep_true) (y + (x + z))"

    using P h hzd xyd

    by (metis sep_add_disjI1 sep_disj_commute sep_conjI)

  ultimately show "(sep_true \<and>* 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 \<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)