# 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   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 assertionaxiomatization  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 autoaxiomatization   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 commandaxiomatization   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 autolemma 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 autolemma 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 autoend`