Theory Ribbons_Stratified

Up to index of Isabelle/HOL/ribbonproofs

theory Ribbons_Stratified
imports Ribbons_Interfaces
`header {* Syntax and proof rules for stratified diagrams *}theory Ribbons_Stratified imports   Ribbons_Interfaces  Proofchainbegintext {* We define the syntax of stratified diagrams. We give proof rules   for stratified diagrams, and prove them sound with respect to the   ordinary rules of separation logic. *}subsection {* Syntax of stratified diagrams *}datatype sdiagram = SDiagram "(cell × interface) list" and cell =   Filler "interface"| Basic "interface" "command" "interface"| Exists_sdia "string" "sdiagram"| Choose_sdia "interface" "sdiagram" "sdiagram" "interface"| Loop_sdia "interface" "sdiagram" "interface"type_synonym row = "cell × interface"text {* Extracting the command from a stratified diagram. *}fun  com_sdia :: "sdiagram => command" and  com_cell :: "cell => command"where  "com_sdia (SDiagram ρs) = foldr (op ;;) (map (com_cell o fst) ρs) Skip"| "com_cell (Filler P) = Skip"| "com_cell (Basic P c Q) = c"| "com_cell (Exists_sdia x D) = com_sdia D"| "com_cell (Choose_sdia P D E Q) = Choose (com_sdia D) (com_sdia E)"| "com_cell (Loop_sdia P D Q) = Loop (com_sdia D)"text {* Extracting the program variables written by a stratified diagram. *}fun  wr_sdia :: "sdiagram => string set" and  wr_cell :: "cell => string set" where  "wr_sdia (SDiagram ρs) = (\<Union>r ∈ set ρs. wr_cell (fst r))"| "wr_cell (Filler P) = {}"| "wr_cell (Basic P c Q) = wr_com c"| "wr_cell (Exists_sdia x D) = wr_sdia D"| "wr_cell (Choose_sdia P D E Q) = wr_sdia D ∪ wr_sdia E"| "wr_cell (Loop_sdia P D Q) = wr_sdia D"text {* The program variables written by a stratified diagram correspond to  those written by the commands therein. *}lemma wr_sdia_is_wr_com:  fixes ρs :: "row list"  and ρ :: row  shows "(wr_sdia D = wr_com (com_sdia D))"  and "(wr_cell γ = wr_com (com_cell γ))"  and "(\<Union>ρ ∈ set ρs. wr_cell (fst ρ))     = wr_com (foldr (op ;;) (map (λ(γ,F). com_cell γ) ρs) Skip)"  and "wr_cell (fst ρ) = wr_com (com_cell (fst ρ))"apply (induct D and γ and ρs and ρ rule: sdiagram_cell.inducts)apply (auto simp add: wr_com_skip wr_com_choose  wr_com_loop wr_com_seq split_def o_def)donesubsection {* Proof rules for stratified diagrams *}inductive   prov_sdia :: "[sdiagram, interface, interface] => bool" and  prov_row :: "[row, interface, interface] => bool" and  prov_cell :: "[cell, interface, interface] => bool"where  SRibbon: "prov_cell (Filler P) P P"| SBasic: "prov_triple (asn P, c, asn Q) ==> prov_cell (Basic P c Q) P Q"| SExists: "prov_sdia D P Q     ==> prov_cell (Exists_sdia x D) (Exists_int x P) (Exists_int x Q)"| SChoice: "[| prov_sdia D P Q ; prov_sdia E P Q |]     ==> prov_cell (Choose_sdia P D E Q) P Q"| SLoop: "prov_sdia D P P ==> prov_cell (Loop_sdia P D P) P P"| SRow: "[| prov_cell γ P Q ; wr_cell γ ∩ rd_int F = {} |]    ==> prov_row (γ, F) (P ⊗ F) (Q ⊗ F)"| SMain: "[| chain_all (λ(P,ρ,Q). prov_row ρ P Q) Π ; 0 < chainlen Π |]    ==> prov_sdia (SDiagram (comlist Π)) (pre Π) (post Π)"subsection {* Soundness *}lemma soundness_strat_helper:  "(prov_sdia D P Q --> prov_triple (asn P, com_sdia D, asn Q)) ∧   (prov_row ρ P Q --> prov_triple (asn P, com_cell (fst ρ), asn Q)) ∧   (prov_cell γ P Q --> prov_triple (asn P, com_cell γ, asn Q))"proof (induct rule: prov_sdia_prov_row_prov_cell.induct)  case (SRibbon P)  show ?case by (auto simp add: prov_triple.skip)next  case (SBasic P c Q)  thus ?case by autonext  case (SExists D P Q x)  thus ?case by (auto simp add: prov_triple.exists)next  case (SChoice D P Q E)  thus ?case by (auto simp add: prov_triple.choose)next  case (SLoop D P)  thus ?case by (auto simp add: prov_triple.loop)next  case (SRow γ P Q F)  thus ?case  by (smt prov_triple.frame rd_int_is_rd_ass asn_simps(2)     fst_conv wr_sdia_is_wr_com(2))next  case (SMain Π)  thus ?case  apply (unfold com_sdia.simps)  apply (intro seq_fold[of _ Π])  apply (simp_all add: len_comlist_chainlen)[3]  apply (induct Π, simp)  apply (case_tac i, auto simp add: fst3_simp thd3_simp)  doneqed  corollary soundness_strat:  assumes "prov_sdia D P Q"  shows "prov_triple (asn P, com_sdia D, asn Q)"using assms soundness_strat_helper by autoend`