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 \<Rightarrow> assertion \<Rightarrow> assertion" (infixr "\<ast>" 55)
where
  star_comm: "p \<ast> q = q \<ast> p" and 
  star_assoc: "(p \<ast> q) \<ast> r = p \<ast> (q \<ast> r)" and 
  star_emp: "p \<ast> Emp = p" and
  emp_star: "Emp \<ast> p = p"

lemma star_rot: 
  "q \<ast> p \<ast> r = p \<ast> q \<ast> r" 
  using star_assoc star_comm by auto

consts 
  Exists :: "string \<Rightarrow> assertion \<Rightarrow> assertion"

text {* Set of program variables in an assertion. *}
axiomatization 
  rd_ass :: "assertion \<Rightarrow> string set"
where rd_emp: "rd_ass Emp = {}"
  and rd_star: "rd_ass (p \<ast> q) = rd_ass p \<union> 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 \<Rightarrow> command \<Rightarrow> command"
consts Loop :: "command \<Rightarrow> command"
consts Skip :: "command"

axiomatization
  Seq :: "command \<Rightarrow> command \<Rightarrow> 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 \<Rightarrow> string set"
where rd_com_choose: "rd_com (Choose c1 c2) = rd_com c1 \<union> 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 \<union> rd_com c2"

text {* Program variables written by a command. *}
axiomatization
  wr_com :: "command \<Rightarrow> string set"
where wr_com_choose: "wr_com (Choose c1 c2) = wr_com c1 \<union> 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 \<union> wr_com c2"

text {* Separation logic rules for proving Hoare triples. *}
inductive
  prov_triple :: "assertion \<times> command \<times> assertion \<Rightarrow> bool"
where
  exists: 
  "prov_triple (p, c, q) 
  \<Longrightarrow> prov_triple (Exists x p, c, Exists x q)"
| choose: 
  "\<lbrakk>prov_triple (p, c1, q); 
  prov_triple (p, c2, q)\<rbrakk> 
  \<Longrightarrow> prov_triple (p, Choose c1 c2, q)"
| loop: 
  "prov_triple (p, c, p) 
  \<Longrightarrow> prov_triple (p, Loop c, p)" 
| frame: 
  "\<lbrakk>prov_triple (p, c, q); wr_com(c) \<inter> rd_ass(r) = {}\<rbrakk> 
  \<Longrightarrow> prov_triple (p \<ast> r, c, q \<ast> r)"
| skip: 
  "prov_triple(p, Skip, p)"
| seq: 
  "\<lbrakk>prov_triple (p, c1, q); prov_triple (q, c2, r)\<rbrakk> 
  \<Longrightarrow> prov_triple (p, c1 ;; c2, r)"

text {* Derived proof rules used in ribbon tool *}

lemma choice_lemma:
  "\<lbrakk>prov_triple (p1,c1,q1); prov_triple (p2,c2,q2);
  p=p1; p1=p2; q=q1; q1=q2\<rbrakk>
  \<Longrightarrow> prov_triple (p, Choose c1 c2, q)"
using prov_triple.choose by auto

lemma loop_lemma:
  "\<lbrakk>prov_triple (p1,c,q1); p=p1; p1=q1; q1=q\<rbrakk>
  \<Longrightarrow> prov_triple (p, Loop c, q)"
using prov_triple.loop by auto

lemma seq_lemma:
  "\<lbrakk>prov_triple (p1,c1,q1); prov_triple (p2,c2,q2); q1=p2\<rbrakk>
  \<Longrightarrow> prov_triple (p1, c1 ;; c2, q2)"
using prov_triple.seq by auto

end