Theory Ribbons_Basic

Up to index of Isabelle/HOL/ribbonproofs

theory Ribbons_Basic
imports Main
header {* Assertions, commands, and separation logic proof rules *}

theory Ribbons_Basic imports

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

Emp :: "assertion"

Star :: "assertion => assertion => assertion" (infixr "∗" 55)
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

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

text {* Extracting the set of program variables mentioned in an assertion. *}
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

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

Loop :: "command => command"

Skip :: "command"

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. *}
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. *}
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. *}

prov_triple :: "assertion × command × assertion => bool"
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