theory Ribbons_Rast imports 
  Ribbons_Graphical 
begin

text {* We define the syntax of rasterised diagrams. We give proof rules for rasterised diagrams, and prove them sound with respect to the rules of separation logic given in ribbons_basic.thy.  *}

subsection {* Rasterised diagrams *}

datatype rdiagram = RDiagram "(cell \<times> interface) list"
and cell = 
  Filler "interface"
| Basic "interface" "command" "interface"
| Exists_rdia "string" "rdiagram"
| Choose_rdia "interface" "rdiagram" "rdiagram" "interface"
| Loop_rdia "interface" "rdiagram" "interface"

fun
  com_rdia :: "rdiagram \<Rightarrow> command" and
  com_cell :: "cell \<Rightarrow> command"
where
  "com_rdia (RDiagram D) = foldr (op ;;) (map (\<lambda>(\<gamma>,F). com_cell \<gamma>) D) Skip"
| "com_cell (Filler P) = Skip"
| "com_cell (Basic P c Q) = c"
| "com_cell (Exists_rdia x D) = com_rdia D"
| "com_cell (Choose_rdia P D E Q) = Choose (com_rdia D) (com_rdia E)"
| "com_cell (Loop_rdia P D Q) = Loop (com_rdia D)"

fun
  wr_rdia :: "rdiagram \<Rightarrow> string set" and
  wr_cell :: "cell \<Rightarrow> string set" 
where
  "wr_rdia (RDiagram D) = (\<Union>r \<in> set D. wr_cell (fst r))"
| "wr_cell (Filler P) = {}"
| "wr_cell (Basic P c Q) = wr_com c"
| "wr_cell (Exists_rdia x D) = wr_rdia D"
| "wr_cell (Choose_rdia P D E Q) = wr_rdia D \<union> wr_rdia E"
| "wr_cell (Loop_rdia P D Q) = wr_rdia D"


lemma wr_rdia_is_wr_com:
  shows "(wr_rdia D = wr_com (com_rdia D))"
  and "(wr_cell \<gamma> = wr_com (com_cell \<gamma>))"
  and "(\<Union>r \<in> set (rs :: (cell \<times> interface) list). wr_cell (fst r)) 
    = wr_com (foldr (op ;;) (map (\<lambda>(\<gamma>,F). com_cell \<gamma>) rs) Skip)"
  and "wr_cell (fst (p::cell \<times> interface)) = wr_com (com_cell (fst p))"
proof (induct D and \<gamma> and rs and p 
    rule: rdiagram_cell.inducts)
qed (auto simp add: wr_com_skip wr_com_choose 
    wr_com_loop wr_com_seq split_def)


inductive 
  prov_rdia :: "[rdiagram, interface, interface] \<Rightarrow> bool" and
  prov_cell :: "[cell \<times> interface, interface, interface] \<Rightarrow> bool"
where
  RRibbon: "prov_cell (Filler P, F) (P \<otimes> F) (P \<otimes> F)"
| RBasic: "\<lbrakk> prov_triple (ass P, c, ass Q) ; wr_com c \<inter> rd_int F = {} \<rbrakk> 
  \<Longrightarrow> prov_cell (Basic P c Q, F) (P \<otimes> F) (Q \<otimes> F)"
| RExists: "\<lbrakk> prov_rdia D P Q ; wr_rdia D \<inter> rd_int F = {} \<rbrakk>
  \<Longrightarrow> prov_cell (Exists_rdia x D, F) (Exists_int x P \<otimes> F) (Exists_int x Q \<otimes> F)"
| RChoice: "\<lbrakk> prov_rdia D P Q ; prov_rdia E P Q ; (wr_rdia D \<union> wr_rdia E) \<inter> rd_int F = {} \<rbrakk> \<Longrightarrow> prov_cell (Choose_rdia P D E Q, F) (P \<otimes> F) (Q \<otimes> F)"
| RLoop: "\<lbrakk> prov_rdia D P P ; wr_rdia D \<inter> rd_int F = {} \<rbrakk> \<Longrightarrow> prov_cell (Loop_rdia P D P, F) (P \<otimes> F) (P \<otimes> F)"

lemma soundness_rast_helper:
  "(prov_rdia D P Q \<longrightarrow> prov_triple (ass P, com_rdia D, ass Q)) \<and>
  (prov_cell r P Q \<longrightarrow> 
  prov_triple (ass P, com_cell (fst r), ass Q))"
proof (induct rule: prov_rdia_prov_cell.induct)
  case (RRibbon P F)
  show ?case by (auto simp add: prov_triple.skip)
next
  case (RBasic P c Q F)
  from RBasic.hyps(2) have
    "wr_com c \<inter> rd_ass (ass F) = {}" 
    proof (fold rd_int_is_rd_ass) qed assumption
  with RBasic.hyps(1) and prov_triple.frame
  show ?case by auto
next
  case (RExists D P Q F x)
  from RExists.hyps(3) have
    fskru: "wr_com (com_rdia D) \<inter> rd_ass (ass F) = {}"
    proof (fold rd_int_is_rd_ass wr_rdia_is_wr_com) qed assumption
  from prov_triple.exists[OF RExists.hyps(2)]
  have "prov_triple (Exists x (ass P), com_rdia D, Exists x (ass Q))"
    by auto
  from prov_triple.frame[OF this fskru]
  show ?case by auto
next
  case (RChoice D P Q E F)
  from RChoice.hyps(5) have
    fskru: "wr_com (Choose (com_rdia D) (com_rdia E)) 
    \<inter> rd_ass (ass F) = {}" 
    by (auto simp add: rd_int_is_rd_ass 
      wr_rdia_is_wr_com wr_com_choose)
  from prov_triple.choose[OF RChoice.hyps(2) RChoice.hyps(4)]
  have "prov_triple (ass P, Choose (com_rdia D) (com_rdia E), ass Q)"
    by auto
  from prov_triple.frame[OF this fskru]
  show ?case by auto
next
  case (RLoop D P F)
  from RLoop.hyps(3) have
    fskru: "wr_com (Loop (com_rdia D)) \<inter> rd_ass (ass F) = {}"
    by (auto simp add: rd_int_is_rd_ass
    wr_rdia_is_wr_com wr_com_loop)
  from prov_triple.loop[OF RLoop.hyps(2)]
  have "prov_triple (ass P, Loop (com_rdia D), ass P)"
    by auto
  from prov_triple.frame[OF this fskru]
  show ?case by auto
qed

theorem soundness_rast:
  fixes D P Q
  assumes "prov_rdia D P Q"
  shows "prov_triple (ass P, com_rdia D, ass Q)"
using assms soundness_rast_helper by auto

end