1 (* Authors: Gerwin Klein and Rafal Kolanski, 2012

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

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

     4 *)

     5 

     6 header "Abstract Separation Algebra"

     7 

     8 theory Separation_Algebra

     9 imports Main

    10 begin

    11 

    12 

    13 text {* This theory is the main abstract separation algebra development *}

    14 

    15 

    16 section {* Input syntax for lifting boolean predicates to separation predicates *}

    17 

    18 abbreviation (input)

    19   pred_and :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "and" 35) where

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

    21 

    22 abbreviation (input)

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

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

    25 

    26 abbreviation (input)

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

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

    29 

    30 abbreviation (input)

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

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

    33 

    34 abbreviation (input)

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

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

    37 

    38 (* abbreviation *)

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

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

    41 

    42 abbreviation (input)

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

    44   "ALLS x. P x \<equiv> \<lambda>s. \<forall>x. P x s"

    45 

    46 

    47 section {* Associative/Commutative Monoid Basis of Separation Algebras *}

    48 

    49 class pre_sep_algebra = zero + plus +

    50   fixes sep_disj :: "'a => 'a => bool" (infix "##" 60)

    51 

    52   assumes sep_disj_zero [simp]: "x ## 0"

    53   assumes sep_disj_commuteI: "x ## y \<Longrightarrow> y ## x"

    54 

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

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

    57 

    58   assumes sep_add_assoc:

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

    60 begin

    61 

    62 lemma sep_disj_commute: "x ## y = y ## x"

    63   by (blast intro: sep_disj_commuteI)

    64 

    65 lemma sep_add_left_commute:

    66   assumes a: "a ## b" "b ## c" "a ## c"

    67   shows "b + (a + c) = a + (b + c)" (is "?lhs = ?rhs")

    68 proof -

    69   have "?lhs = b + a + c" using a

    70     by (simp add: sep_add_assoc[symmetric] sep_disj_commute)

    71   also have "... = a + b + c" using a

    72     by (simp add: sep_add_commute sep_disj_commute)

    73   also have "... = ?rhs" using a

    74     by (simp add: sep_add_assoc sep_disj_commute)

    75   finally show ?thesis .

    76 qed

    77 

    78 lemmas sep_add_ac = sep_add_assoc sep_add_commute sep_add_left_commute

    79                     sep_disj_commute (* nearly always necessary *)

    80 

    81 end

    82 

    83 

    84 section {* Separation Algebra as Defined by Calcagno et al. *}

    85 

    86 class sep_algebra = pre_sep_algebra +

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

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

    89 begin

    90 

    91 subsection {* Basic Construct Definitions and Abbreviations *}

    92 

    93 definition

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

    95   where

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

    97 

    98 notation

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

   100 

   101 definition

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

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

   104 

   105 definition

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

   107   where

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

   109 

   110 definition

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

   112   "x \<preceq> y \<equiv> \<exists>z. x ## z \<and> x + z = y"

   113 

   114 (* We want these to be abbreviations not definitions, because basic True and

   115    False will occur by simplification in sep_conj terms *)

   116 abbreviation

   117   "sep_true \<equiv> \<langle>True\<rangle>"

   118 

   119 abbreviation

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

   121 

   122 definition

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

   124   "sep_list_conj Ps \<equiv> foldl (op **) \<box> Ps"

   125 

   126 

   127 subsection {* Disjunction/Addition Properties *}

   128 

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

   130   by (simp add: sep_disj_commute)

   131 

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

   133   by (simp add: sep_add_commute)

   134 

   135 lemma sep_disj_addD2: "\<lbrakk> x ## y + z; y ## z \<rbrakk> \<Longrightarrow> x ## z"

   136   by (metis sep_disj_addD1 sep_add_ac)

   137 

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

   139   by (metis sep_disj_addD1 sep_disj_addD2)

   140 

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

   142   by (metis sep_disj_addD sep_disj_commuteI)

   143 

   144 lemma sep_disj_addI2:

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

   146   by (metis sep_add_ac sep_disj_addI1)

   147 

   148 lemma sep_add_disjI1:

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

   150   by (metis sep_add_ac sep_add_disjD sep_disj_addI2)

   151 

   152 lemma sep_add_disjI2:

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

   154   by (metis sep_add_ac sep_add_disjD sep_disj_addI2)

   155 

   156 lemma sep_disj_addI3:

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

   158    by (metis sep_add_ac sep_add_disjD sep_add_disjI2)

   159 

   160 lemma sep_disj_add:

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

   162   by (metis sep_disj_addI1 sep_disj_addI3)

   163 

   164 

   165 subsection {* Substate Properties *}

   166 

   167 lemma sep_substate_disj_add:

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

   169   unfolding sep_substate_def by blast

   170 

   171 lemma sep_substate_disj_add':

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

   173   by (simp add: sep_add_ac sep_substate_disj_add)

   174 

   175 

   176 subsection {* Separating Conjunction Properties *}

   177 

   178 lemma sep_conjD:

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

   180   by (simp add: sep_conj_def)

   181 

   182 lemma sep_conjE:

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

   184   by (auto simp: sep_conj_def)

   185 

   186 lemma sep_conjI:

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

   188   by (auto simp: sep_conj_def)

   189 

   190 lemma sep_conj_commuteI:

   191   "(P ** Q) h \<Longrightarrow> (Q ** P) h"

   192   by (auto intro!: sep_conjI elim!: sep_conjE simp: sep_add_ac)

   193 

   194 lemma sep_conj_commute:

   195   "(P ** Q) = (Q ** P)"

   196   by (rule ext) (auto intro: sep_conj_commuteI)

   197 

   198 lemma sep_conj_assoc:

   199   "((P ** Q) ** R) = (P ** Q ** R)" (is "?lhs = ?rhs")

   200 proof (rule ext, rule iffI)

   201   fix h

   202   assume a: "?lhs h"

   203   then obtain x y z where "P x" and "Q y" and "R z"

   204                       and "x ## y" and "x ## z" and "y ## z" and "x + y ## z"

   205                       and "h = x + y + z"

   206     by (auto dest!: sep_conjD dest: sep_add_disjD)

   207   moreover

   208   then have "x ## y + z"

   209     by (simp add: sep_disj_add)

   210   ultimately

   211   show "?rhs h"

   212     by (auto simp: sep_add_ac intro!: sep_conjI)

   213 next

   214   fix h

   215   assume a: "?rhs h"

   216   then obtain x y z where "P x" and "Q y" and "R z"

   217                       and "x ## y" and "x ## z" and "y ## z" and "x ## y + z"

   218                       and "h = x + y + z"

   219     thm sep_disj_addD

   220     by (fastforce elim!: sep_conjE simp: sep_add_ac dest: sep_disj_addD)

   221   thus "?lhs h"

   222     by (metis sep_conj_def sep_disj_addI1)

   223 qed

   224 

   225 lemma sep_conj_impl:

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

   227   by (erule sep_conjE, auto intro!: sep_conjI)

   228 

   229 lemma sep_conj_impl1:

   230   assumes P: "\<And>h. P h \<Longrightarrow> I h"

   231   shows "(P ** R) h \<Longrightarrow> (I ** R) h"

   232   by (auto intro: sep_conj_impl P)

   233 

   234 lemma sep_globalise:

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

   236   by (fast elim: sep_conj_impl)

   237 

   238 lemma sep_conj_trivial_strip2:

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

   240 

   241 lemma disjoint_subheaps_exist:

   242   "\<exists>x y. x ## y \<and> h = x + y"

   243   by (rule_tac x=0 in exI, auto)

   244 

   245 lemma sep_conj_left_commute: (* for permutative rewriting *)

   246   "(P ** (Q ** R)) = (Q ** (P ** R))" (is "?x = ?y")

   247 proof -

   248   have "?x = ((Q ** R) ** P)" by (simp add: sep_conj_commute)

   249   also have "\<dots> = (Q ** (R ** P))" by (subst sep_conj_assoc, simp)

   250   finally show ?thesis by (simp add: sep_conj_commute)

   251 qed

   252 

   253 lemmas sep_conj_ac = sep_conj_commute sep_conj_assoc sep_conj_left_commute

   254 

   255 lemma ab_semigroup_mult_sep_conj: "class.ab_semigroup_mult op **"

   256   by (unfold_locales)

   257      (auto simp: sep_conj_ac)

   258 

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

   260   by (simp add: sep_empty_def)

   261 

   262 

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

   264 

   265 lemma sep_conj_sep_true:

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

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

   268 

   269 lemma sep_conj_sep_true':

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

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

   272 

   273 lemma sep_conj_true [simp]:

   274   "(sep_true ** sep_true) = sep_true"

   275   unfolding sep_conj_def

   276   by (auto intro!: ext intro: disjoint_subheaps_exist)

   277 

   278 lemma sep_conj_false_right [simp]:

   279   "(P ** sep_false) = sep_false"

   280   by (force elim: sep_conjE intro!: ext)

   281 

   282 lemma sep_conj_false_left [simp]:

   283   "(sep_false ** P) = sep_false"

   284   by (subst sep_conj_commute) (rule sep_conj_false_right)

   285 

   286 

   287 

   288 subsection {* Properties of zero (@{const sep_empty}) *}

   289 

   290 lemma sep_conj_empty [simp]:

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

   292   by (simp add: sep_conj_def sep_empty_def)

   293 

   294 lemma sep_conj_empty'[simp]:

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

   296   by (subst sep_conj_commute, rule sep_conj_empty)

   297 

   298 lemma sep_conj_sep_emptyI:

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

   300   by simp

   301 

   302 lemma sep_conj_sep_emptyE:

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

   304   by simp

   305 

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

   307   by (unfold_locales) (auto simp: sep_conj_ac)

   308 

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

   310   by (unfold_locales) (auto simp: sep_conj_ac)

   311 

   312 

   313 subsection {* Properties of top (@{text sep_true}) *}

   314 

   315 lemma sep_conj_true_P [simp]:

   316   "(sep_true ** (sep_true ** P)) = (sep_true ** P)"

   317   by (simp add: sep_conj_assoc[symmetric])

   318 

   319 lemma sep_conj_disj:

   320   "((P or Q) ** R) = ((P ** R) or (Q ** R))"

   321   by (auto simp: sep_conj_def intro!: ext)

   322 

   323 lemma sep_conj_sep_true_left:

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

   325   by (erule sep_conj_impl, simp+)

   326 

   327 lemma sep_conj_sep_true_right:

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

   329   by (subst (asm) sep_conj_commute, drule sep_conj_sep_true_left,

   330       simp add: sep_conj_ac)

   331 

   332 

   333 subsection {* Separating Conjunction with Quantifiers *}

   334 

   335 lemma sep_conj_conj:

   336   "((P and Q) ** R) h \<Longrightarrow> ((P ** R) and (Q ** R)) h"

   337   by (force intro: sep_conjI elim!: sep_conjE)

   338 

   339 lemma sep_conj_exists1:

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

   341   by (unfold pred_ex_def, force intro!: ext intro: sep_conjI elim: sep_conjE)

   342 

   343 lemma sep_conj_exists2:

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

   345   by (unfold pred_ex_def, force intro!: sep_conjI ext elim!: sep_conjE)

   346 

   347 lemmas sep_conj_exists = sep_conj_exists1 sep_conj_exists2

   348 

   349 lemma sep_conj_spec:

   350   "((ALLS x. P x) ** Q) h \<Longrightarrow> (P x ** Q) h"

   351   by (force intro: sep_conjI elim: sep_conjE)

   352 

   353 

   354 subsection {* Properties of Separating Implication *}

   355 

   356 lemma sep_implI:

   357   assumes a: "\<And>h'. \<lbrakk> h ## h'; P h' \<rbrakk> \<Longrightarrow> Q (h + h')"

   358   shows "(P \<longrightarrow>* Q) h"

   359   unfolding sep_impl_def by (auto elim: a)

   360 

   361 lemma sep_implD:

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

   363   by (force simp: sep_impl_def)

   364 

   365 lemma sep_implE:

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

   367   by (auto dest: sep_implD)

   368 

   369 lemma sep_impl_sep_true [simp]:

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

   371   by (force intro!: sep_implI ext)

   372 

   373 lemma sep_impl_sep_false [simp]:

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

   375   by (force intro!: sep_implI ext)

   376 

   377 lemma sep_impl_sep_true_P:

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

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

   380 

   381 lemma sep_impl_sep_true_false [simp]:

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

   383   by (force intro!: ext dest: sep_impl_sep_true_P)

   384 

   385 lemma sep_conj_sep_impl:

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

   387 proof (rule sep_implI)

   388   fix h' h

   389   assume "P h" and "h ## h'" and "Q h'"

   390   hence "(P ** Q) (h + h')" by (force intro: sep_conjI)

   391   moreover assume "\<And>h. (P ** Q) h \<Longrightarrow> R h"

   392   ultimately show "R (h + h')" by simp

   393 qed

   394 

   395 lemma sep_conj_sep_impl2:

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

   397   by (force dest: sep_implD elim: sep_conjE)

   398 

   399 lemma sep_conj_sep_impl_sep_conj2:

   400   "(P ** R) h \<Longrightarrow> (P ** (Q \<longrightarrow>* (Q ** R))) h"

   401   by (erule (1) sep_conj_impl, erule sep_conj_sep_impl, simp add: sep_conj_ac)

   402 

   403 

   404 subsection {* Pure assertions *}

   405 

   406 definition

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

   408   "pure P \<equiv> \<forall>h h'. P h = P h'"

   409 

   410 lemma pure_sep_true:

   411   "pure sep_true"

   412   by (simp add: pure_def)

   413 

   414 lemma pure_sep_false:

   415   "pure sep_true"

   416   by (simp add: pure_def)

   417 

   418 lemma pure_split:

   419   "pure P = (P = sep_true \<or> P = sep_false)"

   420   by (force simp: pure_def intro!: ext)

   421 

   422 lemma pure_sep_conj:

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

   424   by (force simp: pure_split)

   425 

   426 lemma pure_sep_impl:

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

   428   by (force simp: pure_split)

   429 

   430 lemma pure_conj_sep_conj:

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

   432   by (metis pure_def sep_add_zero sep_conjI sep_conj_commute sep_disj_zero)

   433 

   434 lemma pure_sep_conj_conj:

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

   436   by (force simp: pure_split)

   437 

   438 lemma pure_conj_sep_conj_assoc:

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

   440   by (auto simp: pure_split)

   441 

   442 lemma pure_sep_impl_impl:

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

   444   by (force simp: pure_split dest: sep_impl_sep_true_P)

   445 

   446 lemma pure_impl_sep_impl:

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

   448   by (force simp: pure_split)

   449 

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

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

   452      (erule sep_conj_impl, auto)

   453 

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

   455   by (simp add: conj_comms pure_conj_right)

   456 

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

   458   by (simp add: pure_conj_right sep_conj_ac)

   459 

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

   461   by (subst conj_comms, subst pure_conj_left, simp)

   462 

   463 lemmas pure_conj = pure_conj_right pure_conj_right' pure_conj_left

   464     pure_conj_left'

   465 

   466 declare pure_conj[simp add]

   467 

   468 

   469 subsection {* Intuitionistic assertions *}

   470 

   471 definition intuitionistic :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where

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

   473 

   474 lemma intuitionisticI:

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

   476   by (unfold intuitionistic_def, fast)

   477 

   478 lemma intuitionisticD:

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

   480   by (unfold intuitionistic_def, fast)

   481 

   482 lemma pure_intuitionistic:

   483   "pure P \<Longrightarrow> intuitionistic P"

   484   by (clarsimp simp: intuitionistic_def pure_def, fast)

   485 

   486 lemma intuitionistic_conj:

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

   488   by (force intro: intuitionisticI dest: intuitionisticD)

   489 

   490 lemma intuitionistic_disj:

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

   492   by (force intro: intuitionisticI dest: intuitionisticD)

   493 

   494 lemma intuitionistic_forall:

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

   496   by (force intro: intuitionisticI dest: intuitionisticD)

   497 

   498 lemma intuitionistic_exists:

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

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

   501 

   502 lemma intuitionistic_sep_conj_sep_true:

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

   504 proof (rule intuitionisticI)

   505   fix h h' r

   506   assume a: "(sep_true \<and>* P) h"

   507   then obtain x y where P: "P y" and h: "h = x + y" and xyd: "x ## y"

   508     by - (drule sep_conjD, clarsimp)

   509   moreover assume a2: "h \<preceq> h'"

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

   511     by (clarsimp simp: sep_substate_def)

   512 

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

   514     using P h hzd xyd

   515     by (metis sep_add_disjI1 sep_disj_commute sep_conjI)

   516   ultimately show "(sep_true \<and>* P) h'" using hzd

   517     by (auto simp: sep_conj_commute sep_add_ac dest!: sep_disj_addD)

   518 qed

   519 

   520 lemma intuitionistic_sep_impl_sep_true:

   521   "intuitionistic (sep_true \<longrightarrow>* P)"

   522 proof (rule intuitionisticI)

   523   fix h h'

   524   assume imp: "(sep_true \<longrightarrow>* P) h" and hh': "h \<preceq> h'"

   525 

   526   from hh' obtain z where h': "h' = h + z" and hzd: "h ## z"

   527     by (clarsimp simp: sep_substate_def)

   528   show "(sep_true \<longrightarrow>* P) h'" using imp h' hzd

   529     apply (clarsimp dest!: sep_implD)

   530     apply (metis sep_add_assoc sep_add_disjD sep_disj_addI3 sep_implI)

   531     done

   532 qed

   533 

   534 lemma intuitionistic_sep_conj:

   535   assumes ip: "intuitionistic (P::('a \<Rightarrow> bool))"

   536   shows "intuitionistic (P \<and>* Q)"

   537 proof (rule intuitionisticI)

   538   fix h h'

   539   assume sc: "(P \<and>* Q) h" and hh': "h \<preceq> h'"

   540 

   541   from hh' obtain z where h': "h' = h + z" and hzd: "h ## z"

   542     by (clarsimp simp: sep_substate_def)

   543 

   544   from sc obtain x y where px: "P x" and qy: "Q y"

   545                        and h: "h = x + y" and xyd: "x ## y"

   546     by (clarsimp simp: sep_conj_def)

   547 

   548   have "x ## z" using hzd h xyd

   549     by (metis sep_add_disjD)

   550 

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

   552     by (fastforce elim: intuitionisticD sep_substate_disj_add)

   553 

   554   thus "(P \<and>* Q) h'" using h' h hzd qy xyd

   555     by (metis (full_types) sep_add_commute sep_add_disjD sep_add_disjI2

   556               sep_add_left_commute sep_conjI)

   557 qed

   558 

   559 lemma intuitionistic_sep_impl:

   560   assumes iq: "intuitionistic Q"

   561   shows "intuitionistic (P \<longrightarrow>* Q)"

   562 proof (rule intuitionisticI)

   563   fix h h'

   564   assume imp: "(P \<longrightarrow>* Q) h" and hh': "h \<preceq> h'"

   565 

   566   from hh' obtain z where h': "h' = h + z" and hzd: "h ## z"

   567     by (clarsimp simp: sep_substate_def)

   568 

   569   {

   570     fix x

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

   572 

   573     have "h + x \<preceq> h + x + z" using hzx hzd

   574     by (metis sep_add_disjI1 sep_substate_def)

   575 

   576     with imp hzd iq px hzx

   577     have "Q (h + z + x)"

   578     by (metis intuitionisticD sep_add_assoc sep_add_ac sep_add_disjD sep_implE)

   579   }

   580 

   581   with imp h' hzd iq show "(P \<longrightarrow>* Q) h'"

   582     by (fastforce intro: sep_implI)

   583 qed

   584 

   585 lemma strongest_intuitionistic:

   586   "\<not> (\<exists>Q. (\<forall>h. (Q h \<longrightarrow> (P \<and>* sep_true) h)) \<and> intuitionistic Q \<and>

   587       Q \<noteq> (P \<and>* sep_true) \<and> (\<forall>h. P h \<longrightarrow> Q h))"

   588   by (fastforce intro!: ext sep_substate_disj_add

   589                 dest!: sep_conjD intuitionisticD)

   590 

   591 lemma weakest_intuitionistic:

   592   "\<not> (\<exists>Q. (\<forall>h. ((sep_true \<longrightarrow>* P) h \<longrightarrow> Q h)) \<and> intuitionistic Q \<and>

   593       Q \<noteq> (sep_true \<longrightarrow>* P) \<and> (\<forall>h. Q h \<longrightarrow> P h))"

   594   apply (clarsimp intro!: ext)

   595   apply (rule iffI)

   596    apply (rule sep_implI)

   597    apply (drule_tac h="x" and h'="x + h'" in intuitionisticD)

   598      apply (clarsimp simp: sep_add_ac sep_substate_disj_add)+

   599   done

   600 

   601 lemma intuitionistic_sep_conj_sep_true_P:

   602   "\<lbrakk> (P \<and>* sep_true) s; intuitionistic P \<rbrakk> \<Longrightarrow> P s"

   603   by (force dest: intuitionisticD elim: sep_conjE sep_substate_disj_add)

   604 

   605 lemma intuitionistic_sep_conj_sep_true_simp:

   606   "intuitionistic P \<Longrightarrow> (P \<and>* sep_true) = P"

   607   by (fast intro!: sep_conj_sep_true ext

   608            elim: intuitionistic_sep_conj_sep_true_P)

   609 

   610 lemma intuitionistic_sep_impl_sep_true_P:

   611   "\<lbrakk> P h; intuitionistic P \<rbrakk> \<Longrightarrow> (sep_true \<longrightarrow>* P) h"

   612   by (force intro!: sep_implI dest: intuitionisticD

   613             intro: sep_substate_disj_add)

   614 

   615 lemma intuitionistic_sep_impl_sep_true_simp:

   616   "intuitionistic P \<Longrightarrow> (sep_true \<longrightarrow>* P) = P"

   617   by (fast intro!: ext

   618            elim: sep_impl_sep_true_P intuitionistic_sep_impl_sep_true_P)

   619 

   620 

   621 subsection {* Strictly exact assertions *}

   622 

   623 definition strictly_exact :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where

   624   "strictly_exact P \<equiv> \<forall>h h'. P h \<and> P h' \<longrightarrow> h = h'"

   625 

   626 lemma strictly_exactD:

   627   "\<lbrakk> strictly_exact P; P h; P h' \<rbrakk> \<Longrightarrow> h = h'"

   628   by (unfold strictly_exact_def, fast)

   629 

   630 lemma strictly_exactI:

   631   "(\<And>h h'. \<lbrakk> P h; P h' \<rbrakk> \<Longrightarrow> h = h') \<Longrightarrow> strictly_exact P"

   632   by (unfold strictly_exact_def, fast)

   633 

   634 lemma strictly_exact_sep_conj:

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

   636   apply (rule strictly_exactI)

   637   apply (erule sep_conjE)+

   638   apply (drule_tac h="x" and h'="xa" in strictly_exactD, assumption+)

   639   apply (drule_tac h="y" and h'="ya" in strictly_exactD, assumption+)

   640   apply clarsimp

   641   done

   642 

   643 lemma strictly_exact_conj_impl:

   644   "\<lbrakk> (Q \<and>* sep_true) h; P h; strictly_exact Q \<rbrakk> \<Longrightarrow> (Q \<and>* (Q \<longrightarrow>* P)) h"

   645   by (force intro: sep_conjI sep_implI dest: strictly_exactD elim!: sep_conjE

   646             simp: sep_add_commute sep_add_assoc)

   647 

   648 end

   649 

   650 interpretation sep: ab_semigroup_mult "op **"

   651   by (rule ab_semigroup_mult_sep_conj)

   652 

   653 interpretation sep: comm_monoid_add "op **" \<box>

   654   by (rule comm_monoid_add)

   655 

   656 

   657 section {* Separation Algebra with Stronger, but More Intuitive Disjunction Axiom *}

   658 

   659 class stronger_sep_algebra = pre_sep_algebra +

   660   assumes sep_add_disj_eq [simp]: "y ## z \<Longrightarrow> x ## y + z = (x ## y \<and> x ## z)"

   661 begin

   662 

   663 lemma sep_disj_add_eq [simp]: "x ## y \<Longrightarrow> x + y ## z = (x ## z \<and> y ## z)"

   664   by (metis sep_add_disj_eq sep_disj_commute)

   665 

   666 subclass sep_algebra by default auto

   667 

   668 end

   669 

   670 

   671 section {* Folding separating conjunction over lists of predicates *}

   672 

   673 lemma sep_list_conj_Nil [simp]: "\<And>* [] = \<box>"

   674   by (simp add: sep_list_conj_def)

   675 

   676 (* apparently these two are rarely used and had to be removed from List.thy *)

   677 lemma (in semigroup_add) foldl_assoc:

   678 shows "foldl op+ (x+y) zs = x + (foldl op+ y zs)"

   679 by (induct zs arbitrary: y) (simp_all add:add_assoc)

   680 

   681 lemma (in monoid_add) foldl_absorb0:

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

   683 by (induct zs) (simp_all add:foldl_assoc)

   684 

   685 lemma sep_list_conj_Cons [simp]: "\<And>* (x#xs) = (x ** \<And>* xs)"

   686   by (simp add: sep_list_conj_def sep.foldl_absorb0)

   687 

   688 lemma sep_list_conj_append [simp]: "\<And>* (xs @ ys) = (\<And>* xs ** \<And>* ys)"

   689   by (simp add: sep_list_conj_def sep.foldl_absorb0)

   690 

   691 lemma (in comm_monoid_add) foldl_map_filter:

   692   "foldl op + 0 (map f (filter P xs)) +

   693      foldl op + 0 (map f (filter (not P) xs))

   694    = foldl op + 0 (map f xs)"

   695 proof (induct xs)

   696   case Nil thus ?case by clarsimp

   697 next

   698   case (Cons x xs)

   699   hence IH: "foldl op + 0 (map f xs) =

   700                foldl op + 0 (map f (filter P xs)) +

   701                foldl op + 0 (map f [x\<leftarrow>xs . \<not> P x])"

   702                by (simp only: eq_commute)

   703 

   704   have foldl_Cons':

   705     "\<And>x xs. foldl op + 0 (x # xs) = x + (foldl op + 0 xs)"

   706     by (simp, subst foldl_absorb0[symmetric], rule refl)

   707 

   708   { assume "P x"

   709     hence ?case by (auto simp del: foldl_Cons simp add: foldl_Cons' IH add_ac)

   710   } moreover {

   711     assume "\<not> P x"

   712     hence ?case by (auto simp del: foldl_Cons simp add: foldl_Cons' IH add_ac)

   713   }

   714   ultimately show ?case by blast

   715 qed

   716 

   717 

   718 section {* Separation Algebra with a Cancellative Monoid (for completeness) *}

   719 

   720 text {*

   721   Separation algebra with a cancellative monoid. The results of being a precise

   722   assertion (distributivity over separating conjunction) require this.

   723   although we never actually use this property in our developments, we keep

   724   it here for completeness.

   725   *}

   726 class cancellative_sep_algebra = sep_algebra +

   727   assumes sep_add_cancelD: "\<lbrakk> x + z = y + z ; x ## z ; y ## z \<rbrakk> \<Longrightarrow> x = y"

   728 begin

   729 

   730 definition

   731   (* In any heap, there exists at most one subheap for which P holds *)

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

   733   "precise P = (\<forall>h hp hp'. hp \<preceq> h \<and> P hp \<and> hp' \<preceq> h \<and> P hp' \<longrightarrow> hp = hp')"

   734 

   735 lemma "precise (op = s)"

   736   by (metis (full_types) precise_def)

   737 

   738 lemma sep_add_cancel:

   739   "x ## z \<Longrightarrow> y ## z \<Longrightarrow> (x + z = y + z) = (x = y)"

   740   by (metis sep_add_cancelD)

   741 

   742 lemma precise_distribute:

   743   "precise P = (\<forall>Q R. ((Q and R) \<and>* P) = ((Q \<and>* P) and (R \<and>* P)))"

   744 proof (rule iffI)

   745   assume pp: "precise P"

   746   {

   747     fix Q R

   748     fix h hp hp' s

   749 

   750     { assume a: "((Q and R) \<and>* P) s"

   751       hence "((Q \<and>* P) and (R \<and>* P)) s"

   752         by (fastforce dest!: sep_conjD elim: sep_conjI)

   753     }

   754     moreover

   755     { assume qs: "(Q \<and>* P) s" and qr: "(R \<and>* P) s"

   756 

   757       from qs obtain x y where sxy: "s = x + y" and xy: "x ## y"

   758                            and x: "Q x" and y: "P y"

   759         by (fastforce dest!: sep_conjD)

   760       from qr obtain x' y' where sxy': "s = x' + y'" and xy': "x' ## y'"

   761                            and x': "R x'" and y': "P y'"

   762         by (fastforce dest!: sep_conjD)

   763 

   764       from sxy have ys: "y \<preceq> x + y" using xy

   765         by (fastforce simp: sep_substate_disj_add' sep_disj_commute)

   766       from sxy' have ys': "y' \<preceq> x' + y'" using xy'

   767         by (fastforce simp: sep_substate_disj_add' sep_disj_commute)

   768 

   769       from pp have yy: "y = y'" using sxy sxy' xy xy' y y' ys ys'

   770         by (fastforce simp: precise_def)

   771 

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

   773         by (fastforce dest!: sep_add_cancelD)

   774 

   775       hence "((Q and R) \<and>* P) s" using sxy x x' yy y' xy'

   776         by (fastforce intro: sep_conjI)

   777     }

   778     ultimately

   779     have "((Q and R) \<and>* P) s = ((Q \<and>* P) and (R \<and>* P)) s" using pp by blast

   780   }

   781   thus "\<forall>Q R. ((Q and R) \<and>* P) = ((Q \<and>* P) and (R \<and>* P))" by (blast intro!: ext)

   782 

   783 next

   784   assume a: "\<forall>Q R. ((Q and R) \<and>* P) = ((Q \<and>* P) and (R \<and>* P))"

   785   thus "precise P"

   786   proof (clarsimp simp: precise_def)

   787     fix h hp hp' Q R

   788     assume hp: "hp \<preceq> h" and hp': "hp' \<preceq> h" and php: "P hp" and php': "P hp'"

   789 

   790     obtain z where hhp: "h = hp + z" and hpz: "hp ## z" using hp

   791       by (clarsimp simp: sep_substate_def)

   792     obtain z' where hhp': "h = hp' + z'" and hpz': "hp' ## z'" using hp'

   793       by (clarsimp simp: sep_substate_def)

   794 

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

   796       by (fastforce simp: sep_add_ac)

   797 

   798     from hhp hhp' a hpz hpz' h_eq

   799     have "\<forall>Q R. ((Q and R) \<and>* P) (z + hp) = ((Q \<and>* P) and (R \<and>* P)) (z' + hp')"

   800       by (fastforce simp: h_eq sep_add_ac sep_conj_commute)

   801 

   802     hence "((op = z and op = z') \<and>* P) (z + hp) =

   803            ((op = z \<and>* P) and (op = z' \<and>* P)) (z' + hp')" by blast

   804 

   805     thus  "hp = hp'" using php php' hpz hpz' h_eq

   806       by (fastforce dest!: iffD2 cong: conj_cong

   807                     simp: sep_add_ac sep_add_cancel sep_conj_def)

   808   qed

   809 qed

   810 

   811 lemma strictly_precise: "strictly_exact P \<Longrightarrow> precise P"

   812   by (metis precise_def strictly_exactD)

   813 

   814 end

   815 

   816 end