Theory Separation_Algebra_Alt
section "Abstract Separation Logic, Alternative Definition"
theory Separation_Algebra_Alt
imports Main
begin
text ‹
This theory contains an alternative definition of speration algebra,
following Calcagno et al very closely. While some of the abstract
development is more algebraic, it is cumbersome to instantiate.
We only use it to prove equivalence and to give an impression of how
it would look like.
›
no_notation map_add (infixl "++" 100)
definition
lift2 :: "('a => 'b => 'c option) ⇒ 'a option => 'b option => 'c option"
where
"lift2 f a b ≡ case (a,b) of (Some a, Some b) ⇒ f a b | _ ⇒ None"
class sep_algebra_alt = zero +
fixes add :: "'a => 'a => 'a option" (infixr "⊕" 65)
assumes add_zero [simp]: "x ⊕ 0 = Some x"
assumes add_comm: "x ⊕ y = y ⊕ x"
assumes add_assoc: "lift2 add a (lift2 add b c) = lift2 add (lift2 add a b) c"
begin
definition
disjoint :: "'a => 'a => bool" (infix "##" 60)
where
"a ## b ≡ a ⊕ b ≠ None"
lemma disj_com: "x ## y = y ## x"
by (auto simp: disjoint_def add_comm)
lemma disj_zero [simp]: "x ## 0"
by (auto simp: disjoint_def)
lemma disj_zero2 [simp]: "0 ## x"
by (subst disj_com) simp
lemma add_zero2 [simp]: "0 ⊕ x = Some x"
by (subst add_comm) auto
definition
substate :: "'a => 'a => bool" (infix "≼" 60) where
"a ≼ b ≡ ∃c. a ⊕ c = Some b"
definition
sep_conj :: "('a ⇒ bool) ⇒ ('a ⇒ bool) ⇒ ('a ⇒ bool)" (infixl "**" 61)
where
"P ** Q ≡ λs. ∃p q. p ⊕ q = Some s ∧ P p ∧ Q q"
definition emp :: "'a ⇒ bool" ("□") where
"□ ≡ λs. s = 0"
definition
sep_impl :: "('a ⇒ bool) ⇒ ('a ⇒ bool) ⇒ ('a ⇒ bool)" (infixr "⟶⇧*" 25)
where
"P ⟶⇧* Q ≡ λh. ∀h' h''. h ⊕ h' = Some h'' ∧ P h' ⟶ Q h''"
definition (in -)
"sep_true ≡ λs. True"
definition (in -)
"sep_false ≡ λs. False"
abbreviation
add2 :: "'a option => 'a option => 'a option" (infixr "++" 65)
where
"add2 == lift2 add"
lemma add2_comm:
"a ++ b = b ++ a"
by (simp add: lift2_def add_comm split: option.splits)
lemma add2_None [simp]:
"x ++ None = None"
by (simp add: lift2_def split: option.splits)
lemma None_add2 [simp]:
"None ++ x = None"
by (simp add: lift2_def split: option.splits)
lemma add2_Some_Some:
"Some x ++ Some y = x ⊕ y"
by (simp add: lift2_def)
lemma add2_zero [simp]:
"Some x ++ Some 0 = Some x"
by (simp add: add2_Some_Some)
lemma zero_add2 [simp]:
"Some 0 ++ Some x = Some x"
by (simp add: add2_Some_Some)
lemma sep_conjE:
"⟦ (P ** Q) s; ⋀p q. ⟦ P p; Q q; p ⊕ q = Some s ⟧ ⟹ X ⟧ ⟹ X"
by (auto simp: sep_conj_def)
lemma sep_conjI:
"⟦ P p; Q q; p ⊕ q = Some s ⟧ ⟹ (P ** Q) s"
by (auto simp: sep_conj_def)
lemma sep_conj_comI:
"(P ** Q) s ⟹ (Q ** P) s"
by (auto intro!: sep_conjI elim!: sep_conjE simp: add_comm)
lemma sep_conj_com:
"P ** Q = Q ** P"
by (auto intro: sep_conj_comI intro!: ext)
lemma lift_to_add2:
"⟦z ⊕ q = Some s; x ⊕ y = Some q⟧ ⟹ Some z ++ Some x ++ Some y = Some s"
by (simp add: add2_Some_Some)
lemma lift_to_add2':
"⟦q ⊕ z = Some s; x ⊕ y = Some q⟧ ⟹ (Some x ++ Some y) ++ Some z = Some s"
by (simp add: add2_Some_Some)
lemma add2_Some:
"(x ++ Some y = Some z) = (∃x'. x = Some x' ∧ x' ⊕ y = Some z)"
by (simp add: lift2_def split: option.splits)
lemma Some_add2:
"(Some x ++ y = Some z) = (∃y'. y = Some y' ∧ x ⊕ y' = Some z)"
by (simp add: lift2_def split: option.splits)
lemma sep_conj_assoc:
"P ** (Q ** R) = (P ** Q) ** R"
unfolding sep_conj_def
apply (rule ext)
apply (rule iffI)
apply clarsimp
apply (drule (1) lift_to_add2)
apply (subst (asm) add_assoc)
apply (fastforce simp: add2_Some_Some add2_Some)
apply clarsimp
apply (drule (1) lift_to_add2')
apply (subst (asm) add_assoc [symmetric])
apply (fastforce simp: add2_Some_Some Some_add2)
done
lemma (in -) sep_true[simp]: "sep_true s" by (simp add: sep_true_def)
lemma (in -) sep_false[simp]: "¬sep_false x" by (simp add: sep_false_def)
lemma sep_conj_sep_true:
"P s ⟹ (P ** sep_true) s"
by (auto simp: sep_conjI [where q=0])
lemma sep_conj_sep_true':
"P s ⟹ (sep_true ** P) s"
by (auto simp: sep_conjI [where p=0])
lemma disjoint_submaps_exist:
"∃h⇩0 h⇩1. h⇩0 ⊕ h⇩1 = Some h"
by (rule_tac x=0 in exI, auto)
lemma sep_conj_true[simp]:
"(sep_true ** sep_true) = sep_true"
unfolding sep_conj_def
by (auto intro!: ext intro: disjoint_submaps_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_com) (rule sep_conj_false_right)
lemma sep_conj_left_com:
"(P ** (Q ** R)) = (Q ** (P ** R))" (is "?x = ?y")
proof -
have "?x = ((Q ** R) ** P)" by (simp add: sep_conj_com)
also have "… = (Q ** (R ** P))" by (subst sep_conj_assoc, simp)
finally show ?thesis by (simp add: sep_conj_com)
qed
lemmas sep_conj_ac = sep_conj_com sep_conj_assoc sep_conj_left_com
lemma empty_empty[simp]: "□ 0"
by (simp add: emp_def)
lemma sep_conj_empty[simp]:
"(P ** □) = P"
by (simp add: sep_conj_def emp_def)
lemma sep_conj_empty'[simp]:
"(□ ** P) = P"
by (subst sep_conj_com, rule sep_conj_empty)
lemma sep_conj_sep_emptyI:
"P s ⟹ (P ** □) s"
by simp
lemma sep_conj_true_P[simp]:
"(sep_true ** (sep_true ** P)) = (sep_true ** P)"
by (simp add: sep_conj_assoc)
lemma sep_conj_disj:
"((λs. P s ∨ Q s) ** R) s = ((P ** R) s ∨ (Q ** R) s)" (is "?x = (?y ∨ ?z)")
by (auto simp: sep_conj_def)
lemma sep_conj_conj:
"((λs. P s ∧ Q s) ** R) s ⟹ (P ** R) s ∧ (Q ** R) s"
by (force intro: sep_conjI elim!: sep_conjE)
lemma sep_conj_exists1:
"((λs. ∃x. P x s) ** Q) s = (∃x. (P x ** Q) s)"
by (force intro: sep_conjI elim: sep_conjE)
lemma sep_conj_exists2:
"(P ** (λs. ∃x. Q x s)) = (λs. (∃x. (P ** Q x) s))"
by (force intro!: sep_conjI ext elim!: sep_conjE)
lemmas sep_conj_exists = sep_conj_exists1 sep_conj_exists2
lemma sep_conj_forall:
"((λs. ∀x. P x s) ** Q) s ⟹ (P x ** Q) s"
by (force intro: sep_conjI elim: sep_conjE)
lemma sep_conj_impl:
"⟦ (P ** Q) s; ⋀s. P s ⟹ P' s; ⋀s. Q s ⟹ Q' s ⟧ ⟹ (P' ** Q') s"
by (erule sep_conjE, auto intro!: sep_conjI)
lemma sep_conj_impl1:
assumes P: "⋀s. P s ⟹ I s"
shows "(P ** R) s ⟹ (I ** R) s"
by (auto intro: sep_conj_impl P)
lemma sep_conj_sep_true_left:
"(P ** Q) s ⟹ (sep_true ** Q) s"
by (erule sep_conj_impl, simp+)
lemma sep_conj_sep_true_right:
"(P ** Q) s ⟹ (P ** sep_true) s"
by (subst (asm) sep_conj_com, drule sep_conj_sep_true_left,
simp add: sep_conj_ac)
lemma sep_globalise:
"⟦ (P ** R) s; (⋀s. P s ⟹ Q s) ⟧ ⟹ (Q ** R) s"
by (fast elim: sep_conj_impl)
lemma sep_implI:
assumes a: "⋀h' h''. ⟦ h ⊕ h' = Some h''; P h' ⟧ ⟹ Q h''"
shows "(P ⟶⇧* Q) h"
unfolding sep_impl_def by (auto elim: a)
lemma sep_implD:
"(x ⟶⇧* y) h ⟹ ∀h' h''. h ⊕ h' = Some h'' ∧ x h' ⟶ y h''"
by (force simp: sep_impl_def)
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) s ⟹ P s"
apply (drule sep_implD)
apply (erule_tac x=0 in allE)
apply simp
done
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 s; ⋀s. (P ** Q) s ⟹ R s ⟧ ⟹ (Q ⟶⇧* R) s"
proof (rule sep_implI)
fix h' h h''
assume "P h" and "h ⊕ h' = Some h''" and "Q h'"
hence "(P ** Q) h''" by (force intro: sep_conjI)
moreover assume "⋀s. (P ** Q) s ⟹ R s"
ultimately show "R h''" by simp
qed
lemma sep_conj_sep_impl2:
"⟦ (P ** Q) s; ⋀s. P s ⟹ (Q ⟶⇧* R) s ⟧ ⟹ R s"
by (force dest: sep_implD elim: sep_conjE)
lemma sep_conj_sep_impl_sep_conj2:
"(P ** R) s ⟹ (P ** (Q ⟶⇧* (Q ** R))) s"
by (erule (1) sep_conj_impl, erule sep_conj_sep_impl, simp add: sep_conj_ac)
lemma sep_conj_triv_strip2:
"Q = R ⟹ (Q ** P) = (R ** P)" by simp
end
end