1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7(* Author: Gerwin Klein, 2012 8 Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au> 9 Rafal Kolanski <rafal.kolanski at nicta.com.au> 10*) 11 12chapter "Abstract Separation Logic, Alternative Definition" 13 14theory Separation_Algebra_Alt 15imports Main 16begin 17 18text \<open> 19 This theory contains an alternative definition of speration algebra, 20 following Calcagno et al very closely. While some of the abstract 21 development is more algebraic, it is cumbersome to instantiate. 22 We only use it to prove equivalence and to give an impression of how 23 it would look like. 24\<close> 25 26(* The @{text "++"} notation is a horrible choice, but this theory is 27 only intended to show how the development would look like, not to 28 actually use it. We remove the notation for map-add so it doesn't 29 conflict. 30*) 31no_notation map_add (infixl "++" 100) 32 33definition 34 lift2 :: "('a => 'b => 'c option) \<Rightarrow> 'a option => 'b option => 'c option" 35where 36 "lift2 f a b \<equiv> case (a,b) of (Some a, Some b) \<Rightarrow> f a b | _ \<Rightarrow> None" 37 38 39class sep_algebra_alt = zero + 40 fixes add :: "'a => 'a => 'a option" (infixr "\<oplus>" 65) 41 42 assumes add_zero [simp]: "x \<oplus> 0 = Some x" 43 assumes add_comm: "x \<oplus> y = y \<oplus> x" 44 assumes add_assoc: "lift2 add a (lift2 add b c) = lift2 add (lift2 add a b) c" 45 46begin 47 48definition 49 disjoint :: "'a => 'a => bool" (infix "##" 60) 50where 51 "a ## b \<equiv> a \<oplus> b \<noteq> None" 52 53lemma disj_com: "x ## y = y ## x" 54 by (auto simp: disjoint_def add_comm) 55 56lemma disj_zero [simp]: "x ## 0" 57 by (auto simp: disjoint_def) 58 59lemma disj_zero2 [simp]: "0 ## x" 60 by (subst disj_com) simp 61 62lemma add_zero2 [simp]: "0 \<oplus> x = Some x" 63 by (subst add_comm) auto 64 65definition 66 substate :: "'a => 'a => bool" (infix "\<preceq>" 60) where 67 "a \<preceq> b \<equiv> \<exists>c. a \<oplus> c = Some b" 68 69definition 70 sep_conj :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)" (infixl "**" 61) 71 where 72 "P ** Q \<equiv> \<lambda>s. \<exists>p q. p \<oplus> q = Some s \<and> P p \<and> Q q" 73 74definition emp :: "'a \<Rightarrow> bool" ("\<box>") where 75 "\<box> \<equiv> \<lambda>s. s = 0" 76 77definition 78 sep_impl :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)" (infixr "\<longrightarrow>\<^sup>*" 25) 79 where 80 "P \<longrightarrow>\<^sup>* Q \<equiv> \<lambda>h. \<forall>h' h''. h \<oplus> h' = Some h'' \<and> P h' \<longrightarrow> Q h''" 81 82definition 83 "sep_true \<equiv> \<lambda>s. True" 84 85definition 86 "sep_false \<equiv> \<lambda>s. False" 87 88 89abbreviation 90 add2 :: "'a option => 'a option => 'a option" (infixr "++" 65) 91where 92 "add2 == lift2 add" 93 94 95lemma add2_comm: 96 "a ++ b = b ++ a" 97 by (simp add: lift2_def add_comm split: option.splits) 98 99lemma add2_None [simp]: 100 "x ++ None = None" 101 by (simp add: lift2_def split: option.splits) 102 103lemma None_add2 [simp]: 104 "None ++ x = None" 105 by (simp add: lift2_def split: option.splits) 106 107lemma add2_Some_Some: 108 "Some x ++ Some y = x \<oplus> y" 109 by (simp add: lift2_def) 110 111lemma add2_zero [simp]: 112 "Some x ++ Some 0 = Some x" 113 by (simp add: add2_Some_Some) 114 115lemma zero_add2 [simp]: 116 "Some 0 ++ Some x = Some x" 117 by (simp add: add2_Some_Some) 118 119 120lemma sep_conjE: 121 "\<lbrakk> (P ** Q) s; \<And>p q. \<lbrakk> P p; Q q; p \<oplus> q = Some s \<rbrakk> \<Longrightarrow> X \<rbrakk> \<Longrightarrow> X" 122 by (auto simp: sep_conj_def) 123 124lemma sep_conjI: 125 "\<lbrakk> P p; Q q; p \<oplus> q = Some s \<rbrakk> \<Longrightarrow> (P ** Q) s" 126 by (auto simp: sep_conj_def) 127 128lemma sep_conj_comI: 129 "(P ** Q) s \<Longrightarrow> (Q ** P) s" 130 by (auto intro!: sep_conjI elim!: sep_conjE simp: add_comm) 131 132lemma sep_conj_com: 133 "P ** Q = Q ** P" 134 by (auto intro: sep_conj_comI) 135 136lemma lift_to_add2: 137 "\<lbrakk>z \<oplus> q = Some s; x \<oplus> y = Some q\<rbrakk> \<Longrightarrow> Some z ++ Some x ++ Some y = Some s" 138 by (simp add: add2_Some_Some) 139 140lemma lift_to_add2': 141 "\<lbrakk>q \<oplus> z = Some s; x \<oplus> y = Some q\<rbrakk> \<Longrightarrow> (Some x ++ Some y) ++ Some z = Some s" 142 by (simp add: add2_Some_Some) 143 144lemma add2_Some: 145 "(x ++ Some y = Some z) = (\<exists>x'. x = Some x' \<and> x' \<oplus> y = Some z)" 146 by (simp add: lift2_def split: option.splits) 147 148lemma Some_add2: 149 "(Some x ++ y = Some z) = (\<exists>y'. y = Some y' \<and> x \<oplus> y' = Some z)" 150 by (simp add: lift2_def split: option.splits) 151 152lemma sep_conj_assoc: 153 "P ** (Q ** R) = (P ** Q) ** R" 154 unfolding sep_conj_def 155 apply (rule ext) 156 apply (rule iffI) 157 apply clarsimp 158 apply (drule (1) lift_to_add2) 159 apply (subst (asm) add_assoc) 160 apply (fastforce simp: add2_Some_Some add2_Some) 161 apply clarsimp 162 apply (drule (1) lift_to_add2') 163 apply (subst (asm) add_assoc [symmetric]) 164 apply (fastforce simp: add2_Some_Some Some_add2) 165 done 166 167lemma sep_true[simp]: "sep_true s" by (simp add: sep_true_def) 168lemma sep_false[simp]: "\<not>sep_false x" by (simp add: sep_false_def) 169 170lemma sep_conj_sep_true: 171 "P s \<Longrightarrow> (P ** sep_true) s" 172 by (auto simp: sep_conjI [where q=0]) 173 174lemma sep_conj_sep_true': 175 "P s \<Longrightarrow> (sep_true ** P) s" 176 by (auto simp: sep_conjI [where p=0]) 177 178lemma disjoint_submaps_exist: 179 "\<exists>h\<^sub>0 h\<^sub>1. h\<^sub>0 \<oplus> h\<^sub>1 = Some h" 180 by (rule_tac x=0 in exI, auto) 181 182lemma sep_conj_true[simp]: 183 "(sep_true ** sep_true) = sep_true" 184 unfolding sep_conj_def 185 by (auto intro: disjoint_submaps_exist) 186 187lemma sep_conj_false_right[simp]: 188 "(P ** sep_false) = sep_false" 189 by (force elim: sep_conjE) 190 191lemma sep_conj_false_left[simp]: 192 "(sep_false ** P) = sep_false" 193 by (subst sep_conj_com) (rule sep_conj_false_right) 194 195lemma sep_conj_left_com: 196 "(P ** (Q ** R)) = (Q ** (P ** R))" (is "?x = ?y") 197proof - 198 have "?x = ((Q ** R) ** P)" by (simp add: sep_conj_com) 199 also have "\<dots> = (Q ** (R ** P))" by (subst sep_conj_assoc, simp) 200 finally show ?thesis by (simp add: sep_conj_com) 201qed 202 203lemmas sep_conj_ac = sep_conj_com sep_conj_assoc sep_conj_left_com 204 205lemma empty_empty[simp]: "\<box> 0" 206 by (simp add: emp_def) 207 208lemma sep_conj_empty[simp]: 209 "(P ** \<box>) = P" 210 by (simp add: sep_conj_def emp_def) 211 212 lemma sep_conj_empty'[simp]: 213 "(\<box> ** P) = P" 214 by (subst sep_conj_com, rule sep_conj_empty) 215 216lemma sep_conj_sep_emptyI: 217 "P s \<Longrightarrow> (P ** \<box>) s" 218 by simp 219 220lemma sep_conj_true_P[simp]: 221 "(sep_true ** (sep_true ** P)) = (sep_true ** P)" 222 by (simp add: sep_conj_assoc) 223 224lemma sep_conj_disj: 225 "((\<lambda>s. P s \<or> Q s) ** R) s = ((P ** R) s \<or> (Q ** R) s)" (is "?x = (?y \<or> ?z)") 226 by (auto simp: sep_conj_def) 227 228lemma sep_conj_conj: 229 "((\<lambda>s. P s \<and> Q s) ** R) s \<Longrightarrow> (P ** R) s \<and> (Q ** R) s" 230 by (force intro: sep_conjI elim!: sep_conjE) 231 232lemma sep_conj_exists1: 233 "((\<lambda>s. \<exists>x. P x s) ** Q) s = (\<exists>x. (P x ** Q) s)" 234 by (force intro: sep_conjI elim: sep_conjE) 235 236lemma sep_conj_exists2: 237 "(P ** (\<lambda>s. \<exists>x. Q x s)) = (\<lambda>s. (\<exists>x. (P ** Q x) s))" 238 by (force intro!: sep_conjI elim!: sep_conjE) 239 240lemmas sep_conj_exists = sep_conj_exists1 sep_conj_exists2 241 242lemma sep_conj_forall: 243 "((\<lambda>s. \<forall>x. P x s) ** Q) s \<Longrightarrow> (P x ** Q) s" 244 by (force intro: sep_conjI elim: sep_conjE) 245 246lemma sep_conj_impl: 247 "\<lbrakk> (P ** Q) s; \<And>s. P s \<Longrightarrow> P' s; \<And>s. Q s \<Longrightarrow> Q' s \<rbrakk> \<Longrightarrow> (P' ** Q') s" 248 by (erule sep_conjE, auto intro!: sep_conjI) 249 250lemma sep_conj_impl1: 251 assumes P: "\<And>s. P s \<Longrightarrow> I s" 252 shows "(P ** R) s \<Longrightarrow> (I ** R) s" 253 by (auto intro: sep_conj_impl P) 254 255lemma sep_conj_sep_true_left: 256 "(P ** Q) s \<Longrightarrow> (sep_true ** Q) s" 257 by (erule sep_conj_impl, simp+) 258 259lemma sep_conj_sep_true_right: 260 "(P ** Q) s \<Longrightarrow> (P ** sep_true) s" 261 by (subst (asm) sep_conj_com, drule sep_conj_sep_true_left, 262 simp add: sep_conj_ac) 263 264lemma sep_globalise: 265 "\<lbrakk> (P ** R) s; (\<And>s. P s \<Longrightarrow> Q s) \<rbrakk> \<Longrightarrow> (Q ** R) s" 266 by (fast elim: sep_conj_impl) 267 268lemma sep_implI: 269 assumes a: "\<And>h' h''. \<lbrakk> h \<oplus> h' = Some h''; P h' \<rbrakk> \<Longrightarrow> Q h''" 270 shows "(P \<longrightarrow>\<^sup>* Q) h" 271 unfolding sep_impl_def by (auto elim: a) 272 273lemma sep_implD: 274 "(x \<longrightarrow>\<^sup>* y) h \<Longrightarrow> \<forall>h' h''. h \<oplus> h' = Some h'' \<and> x h' \<longrightarrow> y h''" 275 by (force simp: sep_impl_def) 276 277lemma sep_impl_sep_true[simp]: 278 "(P \<longrightarrow>\<^sup>* sep_true) = sep_true" 279 by (force intro!: sep_implI) 280 281lemma sep_impl_sep_false[simp]: 282 "(sep_false \<longrightarrow>\<^sup>* P) = sep_true" 283 by (force intro!: sep_implI) 284 285lemma sep_impl_sep_true_P: 286 "(sep_true \<longrightarrow>\<^sup>* P) s \<Longrightarrow> P s" 287 apply (drule sep_implD) 288 apply (erule_tac x=0 in allE) 289 apply simp 290 done 291 292lemma sep_impl_sep_true_false[simp]: 293 "(sep_true \<longrightarrow>\<^sup>* sep_false) = sep_false" 294 by (force dest: sep_impl_sep_true_P) 295 296lemma sep_conj_sep_impl: 297 "\<lbrakk> P s; \<And>s. (P ** Q) s \<Longrightarrow> R s \<rbrakk> \<Longrightarrow> (Q \<longrightarrow>\<^sup>* R) s" 298proof (rule sep_implI) 299 fix h' h h'' 300 assume "P h" and "h \<oplus> h' = Some h''" and "Q h'" 301 hence "(P ** Q) h''" by (force intro: sep_conjI) 302 moreover assume "\<And>s. (P ** Q) s \<Longrightarrow> R s" 303 ultimately show "R h''" by simp 304qed 305 306lemma sep_conj_sep_impl2: 307 "\<lbrakk> (P ** Q) s; \<And>s. P s \<Longrightarrow> (Q \<longrightarrow>\<^sup>* R) s \<rbrakk> \<Longrightarrow> R s" 308 by (force dest: sep_implD elim: sep_conjE) 309 310lemma sep_conj_sep_impl_sep_conj2: 311 "(P ** R) s \<Longrightarrow> (P ** (Q \<longrightarrow>\<^sup>* (Q ** R))) s" 312 by (erule (1) sep_conj_impl, erule sep_conj_sep_impl, simp add: sep_conj_ac) 313 314lemma sep_conj_triv_strip2: 315 "Q = R \<Longrightarrow> (Q ** P) = (R ** P)" by simp 316 317end 318 319end 320