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
Proofchain
begin

text {* 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)
done

subsection {* 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 auto
next
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)
done
qed

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 auto

end