theory Ribbons_Basic imports Main begin text {* 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. *} subsection {* Commands, assertions and separation logic rules *} text {* 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" text {* 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" text {* 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" text {* 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 {* 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" text {* Separation logic rules for proving Hoare triples. *} 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 {* 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