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 \ 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 RRibbon: "prov_cell (Filler P, F) (P \ F) (P \ F)" | RBasic: "\ prov_triple (ass P, c, ass Q) ; wr_com c \ rd_int F = {} \ \ prov_cell (Basic P c Q, F) (P \ F) (Q \ F)" | RExists: "\ 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)" | RChoice: "\ 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)" | RLoop: "\ 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