1 (* Author: Gerwin Klein, 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 Logic, Alternative Definition"

     7 

     8 theory Separation_Algebra_Alt

     9 imports Main

    10 begin

    11 

    12 text {*

    13   This theory contains an alternative definition of speration algebra,

    14   following Calcagno et al very closely. While some of the abstract

    15   development is more algebraic, it is cumbersome to instantiate.

    16   We only use it to prove equivalence and to give an impression of how

    17   it would look like.

    18 *}

    19 

    20 (* The @{text "++"} notation is a horrible choice, but this theory is 

    21    only intended to show how the development would look like, not to 

    22    actually use it. We remove the notation for map-add so it doesn't

    23    conflict.

    24 *)

    25 no_notation map_add (infixl "++" 100)

    26 

    27 definition

    28   lift2 :: "('a => 'b => 'c option) \<Rightarrow> 'a option => 'b option => 'c option"

    29 where

    30   "lift2 f a b \<equiv> case (a,b) of (Some a, Some b) \<Rightarrow> f a b | _ \<Rightarrow> None"

    31 

    32 

    33 class sep_algebra_alt = zero +

    34   fixes add :: "'a => 'a => 'a option" (infixr "\<oplus>" 65)

    35 

    36   assumes add_zero [simp]: "x \<oplus> 0 = Some x"

    37   assumes add_comm: "x \<oplus> y = y \<oplus> x"

    38   assumes add_assoc: "lift2 add a (lift2 add b c) = lift2 add (lift2 add a b) c"

    39 

    40 begin

    41 

    42 definition

    43   disjoint :: "'a => 'a => bool" (infix "##" 60)

    44 where

    45   "a ## b \<equiv> a \<oplus> b \<noteq> None"

    46 

    47 lemma disj_com: "x ## y = y ## x"

    48   by (auto simp: disjoint_def add_comm)

    49 

    50 lemma disj_zero [simp]: "x ## 0"

    51   by (auto simp: disjoint_def)

    52 

    53 lemma disj_zero2 [simp]: "0 ## x"

    54   by (subst disj_com) simp

    55 

    56 lemma add_zero2 [simp]: "0 \<oplus> x = Some x"

    57   by (subst add_comm) auto

    58 

    59 definition

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

    61   "a \<preceq> b \<equiv> \<exists>c. a \<oplus> c = Some b"

    62 

    63 definition

    64   sep_conj :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)" (infixl "**" 61)

    65   where

    66   "P ** Q \<equiv> \<lambda>s. \<exists>p q. p \<oplus> q = Some s \<and> P p \<and> Q q"

    67 

    68 definition emp :: "'a \<Rightarrow> bool" ("\<box>") where

    69   "\<box> \<equiv> \<lambda>s. s = 0"

    70 

    71 definition

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

    73   where

    74   "P \<longrightarrow>\<^sup>* Q \<equiv> \<lambda>h. \<forall>h' h''. h \<oplus> h' = Some h'' \<and> P h' \<longrightarrow> Q h''"

    75 

    76 definition

    77   "sep_true \<equiv> \<lambda>s. True"

    78 

    79 definition

    80   "sep_false \<equiv> \<lambda>s. False"

    81 

    82 

    83 abbreviation

    84   add2 :: "'a option => 'a option => 'a option" (infixr "++" 65)

    85 where

    86   "add2 == lift2 add"

    87 

    88 

    89 lemma add2_comm:

    90   "a ++ b = b ++ a"

    91   by (simp add: lift2_def add_comm split: option.splits)

    92 

    93 lemma add2_None [simp]:

    94   "x ++ None = None"

    95   by (simp add: lift2_def split: option.splits)

    96 

    97 lemma None_add2 [simp]:

    98   "None ++ x = None"

    99   by (simp add: lift2_def split: option.splits)

   100 

   101 lemma add2_Some_Some:

   102   "Some x ++ Some y = x \<oplus> y"

   103   by (simp add: lift2_def)

   104 

   105 lemma add2_zero [simp]:

   106   "Some x ++ Some 0 = Some x"

   107   by (simp add: add2_Some_Some)

   108 

   109 lemma zero_add2 [simp]:

   110   "Some 0 ++ Some x = Some x"

   111   by (simp add: add2_Some_Some)

   112 

   113 

   114 lemma sep_conjE:

   115   "\<lbrakk> (P ** Q) s; \<And>p q. \<lbrakk> P p; Q q; p \<oplus> q = Some s \<rbrakk> \<Longrightarrow> X \<rbrakk> \<Longrightarrow> X"

   116   by (auto simp: sep_conj_def)

   117 

   118 lemma sep_conjI:

   119   "\<lbrakk> P p; Q q; p \<oplus> q = Some s \<rbrakk> \<Longrightarrow> (P ** Q) s"

   120   by (auto simp: sep_conj_def)

   121 

   122 lemma sep_conj_comI:

   123   "(P ** Q) s \<Longrightarrow> (Q ** P) s"

   124   by (auto intro!: sep_conjI elim!: sep_conjE simp: add_comm)

   125 

   126 lemma sep_conj_com:

   127   "P ** Q = Q ** P"

   128   by (auto intro: sep_conj_comI intro!: ext)

   129 

   130 lemma lift_to_add2:

   131   "\<lbrakk>z \<oplus> q = Some s; x \<oplus> y = Some q\<rbrakk> \<Longrightarrow> Some z ++ Some x ++ Some y = Some s"

   132   by (simp add: add2_Some_Some)

   133 

   134 lemma lift_to_add2':

   135   "\<lbrakk>q \<oplus> z = Some s; x \<oplus> y = Some q\<rbrakk> \<Longrightarrow> (Some x ++ Some y) ++ Some z = Some s"

   136   by (simp add: add2_Some_Some)

   137 

   138 lemma add2_Some:

   139   "(x ++ Some y = Some z) = (\<exists>x'. x = Some x' \<and> x' \<oplus> y = Some z)"

   140   by (simp add: lift2_def split: option.splits)

   141 

   142 lemma Some_add2:

   143   "(Some x ++ y = Some z) = (\<exists>y'. y = Some y' \<and> x \<oplus> y' = Some z)"

   144   by (simp add: lift2_def split: option.splits)

   145 

   146 lemma sep_conj_assoc:

   147   "P ** (Q ** R) = (P ** Q) ** R"

   148   unfolding sep_conj_def

   149   apply (rule ext)

   150   apply (rule iffI)

   151    apply clarsimp

   152    apply (drule (1) lift_to_add2)

   153    apply (subst (asm) add_assoc)

   154    apply (fastforce simp: add2_Some_Some add2_Some)

   155   apply clarsimp

   156   apply (drule (1) lift_to_add2')

   157   apply (subst (asm) add_assoc [symmetric])

   158   apply (fastforce simp: add2_Some_Some Some_add2)

   159   done

   160 

   161 lemma sep_true[simp]: "sep_true s" by (simp add: sep_true_def)

   162 lemma sep_false[simp]: "\<not>sep_false x" by (simp add: sep_false_def)

   163 

   164 lemma sep_conj_sep_true:

   165   "P s \<Longrightarrow> (P ** sep_true) s"

   166   by (auto simp: sep_conjI [where q=0])

   167 

   168 lemma sep_conj_sep_true':

   169   "P s \<Longrightarrow> (sep_true ** P) s"

   170   by (auto simp: sep_conjI [where p=0])

   171 

   172 lemma disjoint_submaps_exist:

   173   "\<exists>h\<^isub>0 h\<^isub>1. h\<^isub>0 \<oplus> h\<^isub>1 = Some h"

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

   175 

   176 lemma sep_conj_true[simp]:

   177   "(sep_true ** sep_true) = sep_true"

   178   unfolding sep_conj_def

   179   by (auto intro!: ext intro: disjoint_submaps_exist)

   180 

   181 lemma sep_conj_false_right[simp]:

   182   "(P ** sep_false) = sep_false"

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

   184 

   185 lemma sep_conj_false_left[simp]:

   186   "(sep_false ** P) = sep_false"

   187   by (subst sep_conj_com) (rule sep_conj_false_right)

   188 

   189 lemma sep_conj_left_com:

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

   191 proof -

   192   have "?x = ((Q ** R) ** P)" by (simp add: sep_conj_com)

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

   194   finally show ?thesis by (simp add: sep_conj_com)

   195 qed

   196 

   197 lemmas sep_conj_ac = sep_conj_com sep_conj_assoc sep_conj_left_com

   198 

   199 lemma empty_empty[simp]: "\<box> 0"

   200   by (simp add: emp_def)

   201 

   202 lemma sep_conj_empty[simp]:

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

   204   by (simp add: sep_conj_def emp_def)

   205 

   206   lemma sep_conj_empty'[simp]:

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

   208   by (subst sep_conj_com, rule sep_conj_empty)

   209 

   210 lemma sep_conj_sep_emptyI:

   211   "P s \<Longrightarrow> (P ** \<box>) s"

   212   by simp

   213 

   214 lemma sep_conj_true_P[simp]:

   215   "(sep_true ** (sep_true ** P)) = (sep_true ** P)"

   216   by (simp add: sep_conj_assoc)

   217 

   218 lemma sep_conj_disj:

   219   "((\<lambda>s. P s \<or> Q s) ** R) s = ((P ** R) s \<or> (Q ** R) s)" (is "?x = (?y \<or> ?z)")

   220   by (auto simp: sep_conj_def)

   221 

   222 lemma sep_conj_conj:

   223   "((\<lambda>s. P s \<and> Q s) ** R) s \<Longrightarrow> (P ** R) s \<and> (Q ** R) s"

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

   225 

   226 lemma sep_conj_exists1:

   227   "((\<lambda>s. \<exists>x. P x s) ** Q) s = (\<exists>x. (P x ** Q) s)"

   228   by (force intro: sep_conjI elim: sep_conjE)

   229 

   230 lemma sep_conj_exists2:

   231   "(P ** (\<lambda>s. \<exists>x. Q x s)) = (\<lambda>s. (\<exists>x. (P ** Q x) s))"

   232   by (force intro!: sep_conjI ext elim!: sep_conjE)

   233 

   234 lemmas sep_conj_exists = sep_conj_exists1 sep_conj_exists2

   235 

   236 lemma sep_conj_forall:

   237   "((\<lambda>s. \<forall>x. P x s) ** Q) s \<Longrightarrow> (P x ** Q) s"

   238   by (force intro: sep_conjI elim: sep_conjE)

   239 

   240 lemma sep_conj_impl:

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

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

   243 

   244 lemma sep_conj_impl1:

   245   assumes P: "\<And>s. P s \<Longrightarrow> I s"

   246   shows "(P ** R) s \<Longrightarrow> (I ** R) s"

   247   by (auto intro: sep_conj_impl P)

   248 

   249 lemma sep_conj_sep_true_left:

   250   "(P ** Q) s \<Longrightarrow> (sep_true ** Q) s"

   251   by (erule sep_conj_impl, simp+)

   252 

   253 lemma sep_conj_sep_true_right:

   254   "(P ** Q) s \<Longrightarrow> (P ** sep_true) s"

   255   by (subst (asm) sep_conj_com, drule sep_conj_sep_true_left,

   256       simp add: sep_conj_ac)

   257 

   258 lemma sep_globalise:

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

   260   by (fast elim: sep_conj_impl)

   261 

   262 lemma sep_implI:

   263   assumes a: "\<And>h' h''. \<lbrakk> h \<oplus> h' = Some h''; P h' \<rbrakk> \<Longrightarrow> Q h''"

   264   shows "(P \<longrightarrow>\<^sup>* Q) h"

   265   unfolding sep_impl_def by (auto elim: a)

   266 

   267 lemma sep_implD:

   268   "(x \<longrightarrow>\<^sup>* y) h \<Longrightarrow> \<forall>h' h''. h \<oplus> h' = Some h'' \<and> x h' \<longrightarrow> y h''"

   269   by (force simp: sep_impl_def)

   270 

   271 lemma sep_impl_sep_true[simp]:

   272   "(P \<longrightarrow>\<^sup>* sep_true) = sep_true"

   273   by (force intro!: sep_implI ext)

   274 

   275 lemma sep_impl_sep_false[simp]:

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

   277   by (force intro!: sep_implI ext)

   278 

   279 lemma sep_impl_sep_true_P:

   280   "(sep_true \<longrightarrow>\<^sup>* P) s \<Longrightarrow> P s"

   281   apply (drule sep_implD)

   282   apply (erule_tac x=0 in allE)

   283   apply simp

   284   done

   285 

   286 lemma sep_impl_sep_true_false[simp]:

   287   "(sep_true \<longrightarrow>\<^sup>* sep_false) = sep_false"

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

   289 

   290 lemma sep_conj_sep_impl:

   291   "\<lbrakk> P s; \<And>s. (P ** Q) s \<Longrightarrow> R s \<rbrakk> \<Longrightarrow> (Q \<longrightarrow>\<^sup>* R) s"

   292 proof (rule sep_implI)

   293   fix h' h h''

   294   assume "P h" and "h \<oplus> h' = Some h''" and "Q h'"

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

   296   moreover assume "\<And>s. (P ** Q) s \<Longrightarrow> R s"

   297   ultimately show "R h''" by simp

   298 qed

   299 

   300 lemma sep_conj_sep_impl2:

   301   "\<lbrakk> (P ** Q) s; \<And>s. P s \<Longrightarrow> (Q \<longrightarrow>\<^sup>* R) s \<rbrakk> \<Longrightarrow> R s"

   302   by (force dest: sep_implD elim: sep_conjE)

   303 

   304 lemma sep_conj_sep_impl_sep_conj2:

   305   "(P ** R) s \<Longrightarrow> (P ** (Q \<longrightarrow>\<^sup>* (Q ** R))) s"

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

   307 

   308 lemma sep_conj_triv_strip2:

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

   310 

   311 end

   312 

   313 end