theory Ribbons_Rast imports
Ribbons_Graphical
begin

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.

## Rasterised diagrams

datatype rdiagram = RDiagram (cell × 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 ⇒ command and
com_cell :: cell ⇒ command
where
com_rdia (RDiagram D) = foldr (op ;;) (map (λ(γ,F). com_cell γ) 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 ⇒ string set and
wr_cell :: cell ⇒ string set
where
wr_rdia (RDiagram D) = (r ∈ 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 ∪ 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 γ = wr_com (com_cell γ))
and (r ∈ set (rs :: (cell × interface) list). wr_cell (fst r))
= wr_com (foldr (op ;;) (map (λ(γ,F). com_cell γ) rs) Skip)
and wr_cell (fst (p::cell × interface)) = wr_com (com_cell (fst p))
proof (induct D and γ 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] ⇒ bool and
prov_cell :: [cell × interface, interface, interface] ⇒ bool
where
prov_cell (Filler P, F) (P ⊗ F) (P ⊗ F)
prov_triple (ass P, c, ass Q) ; wr_com c ∩ rd_int F = {}
prov_cell (Basic P c Q, F) (P ⊗ F) (Q ⊗ F)
prov_rdia D P Q ; wr_rdia D ∩ rd_int F = {}
prov_cell (Exists_rdia x D, F) (Exists_int x P ⊗ F) (Exists_int x Q ⊗ F)
prov_rdia D P Q ; prov_rdia E P Q ; (wr_rdia D ∪ wr_rdia E) ∩ rd_int F = {}
prov_cell (Choose_rdia P D E Q, F) (P ⊗ F) (Q ⊗ F)
prov_rdia D P P ; wr_rdia D ∩ rd_int F = {}
prov_cell (Loop_rdia P D P, F) (P ⊗ F) (P ⊗ F)
lemma soundness_rast_helper:
(prov_rdia D P Q ⟶ prov_triple (ass P, com_rdia D, ass Q)) ∧
(prov_cell r P Q ⟶
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 ∩ 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) ∩ 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))
∩ 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)) ∩ 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
HTML version automatically generated from ribbons_rast.thy by isa2html.