theory Ribbons_Basic imports
Main
begin

This is the top-level of our Isabelle formalisation of ribbon proofs. We define a command language, assertions, the rules of separation logic, and 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.

## Commands, assertions and separation logic rules

Assertions, comprising (at least) an emp constant, a *-operator and existentially-quantified logical variables.

typedecl assertion

consts 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

consts
Exists :: string ⇒ assertion ⇒ assertion

Set of program variables 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

Commands, comprising (at least) non-deterministic choice, non-deterministic looping, skip and sequencing.

typedecl command
consts Choose :: command ⇒ command ⇒ command
consts Loop :: command ⇒ command
consts 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

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

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

Separation logic rules for proving Hoare triples.

inductive
prov_triple :: assertion × command × assertion ⇒ bool
where
prov_triple (p, c, q)
prov_triple (Exists x p, c, Exists x q)
prov_triple (p, c1, q);
prov_triple (p, c2, q)
prov_triple (p, Choose c1 c2, q)
prov_triple (p, c, p)
prov_triple (p, Loop c, p)
prov_triple (p, c, q); wr_com(c) ∩ rd_ass(r) = {}
prov_triple (p ∗ r, c, q ∗ r)
prov_triple(p, Skip, p)
prov_triple (p, c1, q); prov_triple (q, c2, r)
prov_triple (p, c1 ;; c2, r)

Derived proof rules used in ribbon tool

lemma choice_lemma:
prov_triple (p1,c1,q1); prov_triple (p2,c2,q2);
p=p1; p1=p2; q=q1; q1=q2
prov_triple (p, Choose c1 c2, q)
using prov_triple.choose by auto

lemma loop_lemma:
prov_triple (p1,c,q1); p=p1; p1=q1; q1=q
prov_triple (p, Loop c, q)
using prov_triple.loop by auto

lemma seq_lemma:
prov_triple (p1,c1,q1); prov_triple (p2,c2,q2); q1=p2
prov_triple (p1, c1 ;; c2, q2)
using prov_triple.seq by auto

end
HTML version automatically generated from ribbons_basic.thy by isa2html.