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
