Theory Ribbons_Basic

section ‹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