Theory Ribbons_Stratified

section ‹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"

datatype_compat sdiagram cell

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 (;;) (map (com_cell ∘ 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) = (⋃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 "(⋃ρ ∈ set ρs. wr_cell (fst ρ)) 
    = wr_com (foldr (;;) (map (λ(γ,F). com_cell γ) ρs) Skip)"
  and "wr_cell (fst ρ) = wr_com (com_cell (fst ρ))"
apply (induct D and γ and ρs and ρ rule: compat_sdiagram.induct compat_cell.induct
  compat_cell_interface_prod_list.induct compat_cell_interface_prod.induct)
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 (simp add: prov_triple.frame rd_int_is_rd_ass 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