theory Sep imports HoareAbort MapExtra begin text {* Define the heap *} types heap = "(nat \ nat option)" text {* The semantic definition of a few connectives: *} constdefs sep_emp :: "heap \ bool" ("\") "sep_emp h == h = empty" constdefs singl :: "nat \ nat \ heap \ bool" ("_ \ _" [56] 56) "singl x y h == dom h = {x} & h x = Some y" constdefs sep_conj :: "(heap \ bool) \ (heap \ bool) \ (heap \ bool)" (infixr "\\<^sup>*" 35) "sep_conj P Q == \h. \h1 h2. h = h1 ++ h2 \ h1 \ h2 \ P h1 \ Q h2" constdefs sep_impl :: "(heap \ bool) \ (heap \ bool) \ (heap \ bool)" (infixr "\\<^sup>*" 25) "sep_impl P Q == \h. \h'. h' \ h \ P h' \ Q(h++h')" constdefs "sep_true \ \s. True" constdefs "sep_false \ \s. False" text {* Simple test *} lemma "VARS x y z w h {sep_conj (singl x y) (singl z w) h} SKIP {x \ z}" apply vcg apply(auto simp:sep_conj_def map_disj_def singl_def) done lemma "VARS H x y z w {(x \ y \\<^sup>* z \ w) H} y := w {x \ z}" apply vcg apply (unfold sep_conj_def) apply clarsimp apply (clarsimp simp: map_disj_def singl_def) done lemma "VARS H x y z w {(x \ 3) H} H := H(x \ 4) {(x \ 4) H}" apply vcg apply (unfold singl_def) apply simp done text {* Rules of separation logic *} lemma sep_empD: "\ s \ s = empty" by (simp add: sep_emp_def) lemma sep_emp_empty [simp]: "\ empty" by (simp add: sep_emp_def) lemma sep_true [simp]: "sep_true s" by (simp add: sep_true_def) lemma sep_false [simp]: "\ sep_false s" by (simp add: sep_false_def) declare sep_false_def [symmetric, simp add] lemma sep_conjI: "\ P s\<^isub>0; Q s\<^isub>1; s\<^isub>0 \ s\<^isub>1; s = s\<^isub>1 ++ s\<^isub>0 \ \ (P \\<^sup>* Q) s" by (force simp: sep_conj_def map_add_ac) lemma sep_conjD: "(P \\<^sup>* Q) s \ \s\<^isub>0 s\<^isub>1. s\<^isub>0 \ s\<^isub>1 \ s = s\<^isub>1 ++ s\<^isub>0 \ P s\<^isub>0 \ Q s\<^isub>1" by (force simp: sep_conj_def map_add_ac) (* a law of separation logic *) lemma star_comm: "(P \\<^sup>* Q) = (Q \\<^sup>* P)" apply (rule ext) apply (rule iffI) apply (drule sep_conjD) apply clarsimp apply (rule sep_conjI) apply assumption apply assumption apply (simp add: map_disj_com) apply (simp add: map_add_ac) apply (drule sep_conjD) apply clarsimp apply (rule sep_conjI) apply assumption apply assumption apply (simp add: map_disj_com) apply (simp add: map_add_ac) done lemma "VARS H x y z w {(P \\<^sup>* Q) H} SKIP {(Q \\<^sup>* P) H}" apply (simp add: star_comm) apply vcg done end