header {* Assertions, commands, and separation logic proof rules *}

theory Ribbons_Basic imports

Main

begin

text {* We define a command language, assertions, and the rules of separation

logic, plus some derived rules that are used by our tool. This is the only

theory file that is loaded by the tool. We keep it as small as possible.

*}

subsection {* Assertions *}

text {* The language of assertions includes (at least) an emp constant,

a star-operator, and existentially-quantified logical variables. *}

typedecl assertion

axiomatization

Emp :: "assertion"

axiomatization

Star :: "assertion => assertion => assertion" (infixr "∗" 55)

where

star_comm: "p ∗ q = q ∗ p" and

star_assoc: "(p ∗ q) ∗ r = p ∗ (q ∗ r)" and

star_emp: "p ∗ Emp = p" and

emp_star: "Emp ∗ p = p"

lemma star_rot:

"q ∗ p ∗ r = p ∗ q ∗ r"

using star_assoc star_comm by auto

axiomatization

Exists :: "string => assertion => assertion"

text {* Extracting the set of program variables mentioned in an assertion. *}

axiomatization

rd_ass :: "assertion => string set"

where rd_emp: "rd_ass Emp = {}"

and rd_star: "rd_ass (p ∗ q) = rd_ass p ∪ rd_ass q"

and rd_exists: "rd_ass (Exists x p) = rd_ass p"

subsection {* Commands *}

text {* The language of commands comprises (at least) non-deterministic

choice, non-deterministic looping, skip and sequencing. *}

typedecl command

axiomatization

Choose :: "command => command => command"

axiomatization

Loop :: "command => command"

axiomatization

Skip :: "command"

axiomatization

Seq :: "command => command => command" (infixr ";;" 55)

where seq_assoc: "c1 ;; (c2 ;; c3) = (c1 ;; c2) ;; c3"

and seq_skip: "c ;; Skip = c"

and skip_seq: "Skip ;; c = c"

text {* Extracting the set of program variables read by a command. *}

axiomatization

rd_com :: "command => string set"

where rd_com_choose: "rd_com (Choose c1 c2) = rd_com c1 ∪ rd_com c2"

and rd_com_loop: "rd_com (Loop c) = rd_com c"

and rd_com_skip: "rd_com (Skip) = {}"

and rd_com_seq: "rd_com (c1 ;; c2) = rd_com c1 ∪ rd_com c2"

text {* Extracting the set of program variables written by a command. *}

axiomatization

wr_com :: "command => string set"

where wr_com_choose: "wr_com (Choose c1 c2) = wr_com c1 ∪ wr_com c2"

and wr_com_loop: "wr_com (Loop c) = wr_com c"

and wr_com_skip: "wr_com (Skip) = {}"

and wr_com_seq: "wr_com (c1 ;; c2) = wr_com c1 ∪ wr_com c2"

subsection {* Separation logic proof rules *}

text {* Note that the frame rule has a side-condition concerning program

variables. When proving the soundness of our graphical formalisation of

ribbon proofs, we shall omit this side-condition. *}

inductive

prov_triple :: "assertion × command × assertion => bool"

where

exists: "prov_triple (p, c, q) ==> prov_triple (Exists x p, c, Exists x q)"

| choose: "[| prov_triple (p, c1, q); prov_triple (p, c2, q) |]

==> prov_triple (p, Choose c1 c2, q)"

| loop: "prov_triple (p, c, p) ==> prov_triple (p, Loop c, p)"

| frame: "[| prov_triple (p, c, q); wr_com(c) ∩ rd_ass(r) = {} |]

==> prov_triple (p ∗ r, c, q ∗ r)"

| skip: "prov_triple (p, Skip, p)"

| seq: "[| prov_triple (p, c1, q); prov_triple (q, c2, r) |]

==> prov_triple (p, c1 ;; c2, r)"

text {* Here are some derived proof rules, which are used in our

ribbon-checking tool. *}

lemma choice_lemma:

assumes "prov_triple (p1, c1, q1)" and "prov_triple (p2, c2, q2)"

and "p = p1" and "p1 = p2" and "q = q1" and "q1 = q2"

shows "prov_triple (p, Choose c1 c2, q)"

using assms prov_triple.choose by auto

lemma loop_lemma:

assumes "prov_triple (p1, c, q1)" and "p = p1" and "p1 = q1" and "q1 = q"

shows "prov_triple (p, Loop c, q)"

using assms prov_triple.loop by auto

lemma seq_lemma:

assumes "prov_triple (p1, c1, q1)" and "prov_triple (p2, c2, q2)"

and "q1 = p2"

shows "prov_triple (p1, c1 ;; c2, q2)"

using assms prov_triple.seq by auto

end