Theory Ribbons_Graphical_Soundness

Up to index of Isabelle/HOL/ribbonproofs

theory Ribbons_Graphical_Soundness
imports Ribbons_Graphical Finite_Map
header {* Soundness for graphical diagrams *}

theory Ribbons_Graphical_Soundness imports
Ribbons_Graphical
Finite_Map
begin

text {* We prove that the proof rules for graphical ribbon proofs are sound
with respect to the rules of separation logic.

We impose an additional assumption to achieve soundness: that the
Frame rule has no side-condition. This assumption is reasonable because there
are several separation logics that lack such a side-condition, such as
``variables-as-resource''.

We first describe how to extract proofchains from a diagram. This process is
similar to the process of extracting commands from a diagram, which was
described in @{theory Ribbons_Graphical}. When we extract a proofchain, we
don't just include the commands, but the assertions in between them. Our
main lemma for proving soundness says that each of these proofchains
corresponds to a valid separation logic proof.
*}


subsection {* Proofstate chains *}

text {* When extracting a proofchain from a diagram, we need to keep track
of which nodes we have processed and which ones we haven't. A
proofstate, defined below, maps a node to ``Top'' if it hasn't been
processed and ``Bot'' if it has. *}


datatype topbot = Top | Bot

type_synonym proofstate = "node \<rightharpoonup>f topbot"

text {* A proofstate chain contains all the nodes and edges of a graphical
diagram, interspersed with proofstates that track which nodes have been
processed at each point. *}


type_synonym ps_chain = "(proofstate, node + edge) chain"

text {* The @{term "next_ps σ"} function processes one node or one edge in a
diagram, given the current proofstate @{term σ}. It processes a node
@{term v} by replacing the mapping from @{term v} to @{term Top} with a
mapping from @{term v} to @{term Bot}. It processes an edge @{term e}
(whose source and target nodes are @{term vs} and @{term ws} respectively)
by removing all the mappings from @{term vs} to @{term Bot}, and adding
mappings from @{term ws} to @{term Top}. *}


fun next_ps :: "proofstate => node + edge => proofstate"
where
"next_ps σ (Inl v) = σ \<ominus> {|v|} ⊕ [{|v|} |=> Bot]"
| "next_ps σ (Inr e) = σ \<ominus> fst3 e ⊕ [thd3 e |=> Top]"

text {* The function @{term "mk_ps_chain Π π"} generates from @{term π}, which
is a list of nodes and edges, a proofstate chain, by interspersing the
elements of @{term π} with the appropriate proofstates. The first argument
@{term Π} is the part of the chain that has already been converted. *}


definition
mk_ps_chain :: "[ps_chain, (node + edge) list] => ps_chain"
where
"mk_ps_chain ≡ foldl (λΠ x. cSnoc Π x (next_ps (post Π) x))"

lemma mk_ps_chain_preserves_length:
fixes π Π
shows "chainlen (mk_ps_chain Π π) = chainlen Π + length π"
proof (induct π arbitrary: Π)
case Nil
show ?case by (unfold mk_ps_chain_def, auto)
next
case (Cons x π)
show ?case
apply (unfold mk_ps_chain_def list.size foldl.simps)
apply (fold mk_ps_chain_def)
apply (auto simp add: Cons len_snoc)
done
qed

text {* Distributing @{term mk_ps_chain} over @{term Cons}. *}
lemma mk_ps_chain_cons:
"mk_ps_chain Π (x # π) = mk_ps_chain (cSnoc Π x (next_ps (post Π) x)) π"
by (auto simp add: mk_ps_chain_def)

text {* Distributing @{term mk_ps_chain} over @{term snoc}. *}
lemma mk_ps_chain_snoc:
"mk_ps_chain Π (π @ [x])
= cSnoc (mk_ps_chain Π π) x (next_ps (post (mk_ps_chain Π π)) x)"

by (unfold mk_ps_chain_def, auto)

text {* Distributing @{term mk_ps_chain} over @{term cCons}. *}
lemma mk_ps_chain_ccons:
fixes π Π
shows "mk_ps_chain (\<lbrace> σ \<rbrace> · x · Π) π = \<lbrace> σ \<rbrace> · x · mk_ps_chain Π π "
by (induct π arbitrary: Π, auto simp add: mk_ps_chain_cons mk_ps_chain_def)

lemma pre_mk_ps_chain:
fixes Π π
shows "pre (mk_ps_chain Π π) = pre Π"
apply (induct π arbitrary: Π)
apply (auto simp add: mk_ps_chain_def mk_ps_chain_cons pre_snoc)
done

text {* A chain which is obtained from the list @{term π}, has @{term π}
as its list of commands. The following lemma states this in a slightly
more general form, that allows for part of the chain to have already
been processed. *}


lemma comlist_mk_ps_chain:
"comlist (mk_ps_chain Π π) = comlist Π @ π"
proof (induct π arbitrary: Π)
case Nil
thus ?case by (smt append_Nil2 foldl_Nil mk_ps_chain_def)
next
case (Cons x π')
show ?case
apply (unfold mk_ps_chain_def foldl.simps, fold mk_ps_chain_def)
apply (auto simp add: Cons comlist_snoc)
done
qed

text {* In order to perform induction over our diagrams, we shall wish
to obtain ``smaller'' diagrams, by removing nodes or edges. However, the
syntax and well-formedness constraints for diagrams are such that although
we can always remove an edge from a diagram, we cannot (in general) remove
a node -- the resultant diagram would not be a well-formed if an edge
connected to that node.

Hence, we consider ``partially-processed diagrams'' @{term "(G,S)"}, which
comprise a diagram @{term G} and a set @{term S} of nodes. @{term S} denotes
the subset of @{term G}'s initial nodes that have already been processed,
and can be thought of as having been removed from @{term G}.

We now give an updated version of the @{term "lins G"} function. This was
originally defined in @{theory Ribbons_Graphical}. We provide an extra
parameter, @{term S}, which denotes the subset of @{term G}'s initial nodes
that shouldn't be included in the linear extensions. *}


definition lins2 :: "[node fset, diagram] => lin set"
where
"lins2 S G ≡ {π :: lin .
(distinct π)
∧ (set π = (fset G^V - fset S) <+> set G^E)
∧ (∀i j v e. i < length π ∧ j < length π
∧ π!i = Inl v ∧ π!j = Inr e ∧ v |∈| fst3 e --> i<j)
∧ (∀j k w e. j < length π ∧ k < length π
∧ π!j = Inr e ∧ π!k = Inl w ∧ w |∈| thd3 e --> j<k) }"


lemma lins2D:
assumes "π ∈ lins2 S G"
shows "distinct π"
and "set π = (fset G^V - fset S) <+> set G^E"
and "!!i j v e. [| i < length π ; j < length π ;
π!i = Inl v ; π!j = Inr e ; v |∈| fst3 e |] ==> i<j"

and "!!i k w e. [| j < length π ; k < length π ;
π!j = Inr e ; π!k = Inl w ; w |∈| thd3 e |] ==> j<k"

using assms
apply (unfold lins2_def Collect_iff)
apply (elim conjE, assumption)+
apply blast+
done

lemma lins2I:
assumes "distinct π"
and "set π = (fset G^V - fset S) <+> set G^E"
and "!!i j v e. [| i < length π ; j < length π ;
π!i = Inl v ; π!j = Inr e ; v |∈| fst3 e |] ==> i<j"

and "!!j k w e. [| j < length π ; k < length π ;
π!j = Inr e ; π!k = Inl w ; w |∈| thd3 e |] ==> j<k"

shows "π ∈ lins2 S G"
using assms
apply (unfold lins2_def Collect_iff, intro conjI)
apply assumption+
apply blast+
done

text {* When @{term S} is empty, the two definitions coincide. *}
lemma lins_is_lins2_with_empty_S:
"lins G = lins2 {||} G"
by (unfold lins_def lins2_def, auto)

text {* The first proofstate for a diagram @{term G} is obtained by
mapping each of its initial nodes to @{term Top}. *}

definition
initial_ps :: "diagram => proofstate"
where
"initial_ps G ≡ [ initials G |=> Top ]"

text {* The first proofstate for the partially-processed diagram @{term G} is
obtained by mapping each of its initial nodes to @{term Top}, except those
in @{term S}, which are mapped to @{term Bot}. *}

definition
initial_ps2 :: "[node fset, diagram] => proofstate"
where
"initial_ps2 S G ≡ [ initials G - S |=> Top ] ⊕ [ S |=> Bot ]"

text {* When @{term S} is empty, the above two definitions coincide. *}
lemma initial_ps_is_initial_ps2_with_empty_S:
"initial_ps = initial_ps2 {||}"
apply (unfold fun_eq_iff, intro allI)
apply (unfold initial_ps_def initial_ps2_def)
apply (transfer, simp add: make_map_def)
done

text {* The following function extracts the set of proofstate chains from
a diagram. *}

definition
ps_chains :: "diagram => ps_chain set"
where
"ps_chains G ≡ mk_ps_chain (cNil (initial_ps G)) ` lins G"

text {* The following function extracts the set of proofstate chains from
a partially-processed diagram. Nodes in @{term S} are excluded from
the resulting chains. *}

definition
ps_chains2 :: "[node fset, diagram] => ps_chain set"
where
"ps_chains2 S G ≡ mk_ps_chain (cNil (initial_ps2 S G)) ` lins2 S G"

text {* When @{term S} is empty, the above two definitions coincide. *}
lemma ps_chains_is_ps_chains2_with_empty_S:
"ps_chains = ps_chains2 {||}"
apply (unfold fun_eq_iff, intro allI)
apply (unfold ps_chains_def ps_chains2_def)
apply (fold initial_ps_is_initial_ps2_with_empty_S)
apply (fold lins_is_lins2_with_empty_S)
apply auto
done

text {* We now wish to describe proofstates chain that are well-formed. First,
let us say that @{term "f ⊕disjoint g"} is defined, when @{term f} and
@{term g} have disjoint domains, as @{term "f ⊕ g"}. Then, a well-formed
proofstate chain consists of triples of the form @{term "(σ ⊕disjoint
[{| v |} |=> Top], Inl v, σ ⊕disjoint [{| v |} |=> Bot])"}, where @{term v}
is a node, or of the form @{term "(σ ⊕disjoint [{| vs |} |=> Bot], Inr e,
σ ⊕disjoint [{| ws |} |=> Top])"}, where @{term e} is an edge with source
and target nodes @{term vs} and @{term ws} respectively.

The definition below describes a well-formed triple; we then lift this
to complete chains shortly. *}


definition
wf_ps_triple :: "proofstate × (node + edge) × proofstate => bool"
where
"wf_ps_triple T = (case snd3 T of
Inl v => (∃σ. v |∉| fdom σ
∧ fst3 T = [ {|v|} |=> Top ] ⊕ σ
∧ thd3 T = [ {|v|} |=> Bot ] ⊕ σ)
| Inr e => (∃σ. (fst3 e |∪| thd3 e) |∩| fdom σ = {||}
∧ fst3 T = [ fst3 e |=> Bot ] ⊕ σ
∧ thd3 T = [ thd3 e |=> Top ] ⊕ σ))"


lemma wf_ps_triple_nodeI:
assumes "∃σ. v |∉| fdom σ ∧
σ1 = [ {|v|} |=> Top ] ⊕ σ ∧
σ2 = [ {|v|} |=> Bot ] ⊕ σ"

shows "wf_ps_triple (σ1, Inl v, σ2)"
using assms unfolding wf_ps_triple_def
by (auto simp add: fst3_simp snd3_simp thd3_simp)

lemma wf_ps_triple_edgeI:
assumes "∃σ. (fst3 e |∪| thd3 e) |∩| fdom σ = {||}
∧ σ1 = [ fst3 e |=> Bot ] ⊕ σ
∧ σ2 = [ thd3 e |=> Top ] ⊕ σ"

shows "wf_ps_triple (σ1, Inr e, σ2)"
using assms unfolding wf_ps_triple_def
by (auto simp add: fst3_simp snd3_simp thd3_simp)

definition
wf_ps_chain :: "ps_chain => bool"
where
"wf_ps_chain ≡ chain_all wf_ps_triple"

lemma next_initial_ps2_vertex:
"initial_ps2 ({|v|} |∪| S) G
= initial_ps2 S G \<ominus> {|v|} ⊕ [ {|v|} |=> Bot ]"

apply (unfold initial_ps2_def)
apply transfer
apply (auto simp add: make_map_def map_diff_def map_add_def restrict_map_def)
done

lemma next_initial_ps2_edge:
assumes "G = Graph V Λ E" and "G' = Graph V' Λ E'" and
"V' = V - fst3 e" and "E' = removeAll e E" and "e ∈ set E" and
"fst3 e |⊆| S" and "S |⊆| initials G" and "wf_dia G"
shows "initial_ps2 (S - fst3 e) G' =
initial_ps2 S G \<ominus> fst3 e ⊕ [ thd3 e |=> Top ]"

proof (insert assms, unfold initial_ps2_def, transfer)
fix G V Λ E G' V' E' e S
assume G_def: "G = Graph V Λ E" and G'_def: "G' = Graph V' Λ E'" and
V'_def: "V' = V - fst3 e" and E'_def: "E' = removeAll e E" and
e_in_E: "e ∈ set E" and fst_e_in_S: "fst3 e |⊆| S" and
S_initials: "S |⊆| initials G" and wf_G: "wf_dia G"
show "make_map (initials G' - (S - fst3 e)) Top ++ make_map (S - fst3 e) Bot
= map_diff (make_map (initials G - S) Top ++ make_map S Bot) (fst3 e)
++ make_map (thd3 e) Top"

apply (unfold make_map_def map_diff_def)
apply (unfold map_add_def restrict_map_def)
apply (unfold minus_fset)
apply (unfold fun_eq_iff initials_def, intro allI)
apply (unfold G_def G'_def V'_def E'_def)
apply (unfold edges.simps vertices.simps)
apply (simp add: subset_fset in_fset e_in_E)
apply (intro conjI impI)
apply (elim bexE conjE)
apply (rename_tac "f")
apply (subgoal_tac "thd3 e |∩| initials G = {||}")
apply (insert S_initials, fold fset_cong)
apply (unfold subset_fset initials_def filter_fset)
apply (auto simp add: in_fset G_def e_in_E)[1]
apply (auto simp add: in_fset G_def e_in_E)[1]
apply (auto simp add: in_fset G_def e_in_E)[1]
apply (auto simp add: in_fset G_def e_in_E)[1]
apply (elim conjE bexE)
apply (insert wf_G)[1]
apply (unfold G_def vertices.simps edges.simps)
apply (drule wf_dia_inv) back back
apply (unfold acyclicity_def)
apply (smt e_in_E fst_e_in_S inter_fset le_iff_inf set_mp)
apply (elim bexE DiffE)
apply (unfold singleton_iff)
apply (insert wf_G)[1]
apply (unfold G_def vertices.simps edges.simps)
apply (drule wf_dia_inv) back back back
apply (drule linearityD2)
apply (fold fset_cong, unfold inter_fset fset_simps)
apply (smt disjoint_iff_not_equal e_in_E)
apply (insert wf_G)[1]
apply (unfold G_def vertices.simps edges.simps)
apply (drule wf_dia_inv) back back
apply (metis (lifting) e_in_E Diff_iff G_def empty_iff fset_simps(1)
in_inter_fset insertCI linearityD(2) notin_fset wf_G wf_dia_inv(4))
apply (elim bexE DiffE)
apply (unfold singleton_iff)
apply (insert wf_G)[1]
apply (unfold G_def vertices.simps edges.simps)
apply (drule wf_dia_inv) back back back
apply (drule linearityD2)
apply (fold fset_cong, unfold inter_fset fset_simps)
apply (smt disjoint_iff_not_equal e_in_E)
apply (insert wf_G)[1]
apply (unfold G_def vertices.simps edges.simps)
apply (drule wf_dia_inv) back back
apply (metis (lifting) e_in_E Diff_iff G_def empty_iff fset_simps(1)
in_inter_fset insertCI linearityD(2) notin_fset wf_G wf_dia_inv(4))
apply (elim bexE)
apply (insert wf_G)
apply (unfold G_def vertices.simps edges.simps)
apply (drule wf_dia_inv) back back back back
apply (unfold subset_fset union_fset)
apply auto[1]
apply (drule wf_dia_inv) back back back back
apply (unfold subset_fset union_fset)
apply auto[1]
apply (drule wf_dia_inv) back back back back
apply (unfold subset_fset union_fset)
apply (auto simp add: e_in_E)[1]
apply (drule wf_dia_inv) back back back back
apply (unfold subset_fset union_fset)
apply (auto simp add: e_in_E)[1]
done
qed

lemma next_lins2_vertex:
assumes "Inl v # π ∈ lins2 S G"
assumes "v |∉| S"
shows "π ∈ lins2 ({|v|} |∪| S) G"
proof -
note lins2D = lins2D[OF assms(1)]
show ?thesis
proof (intro lins2I)
show "distinct π" using lins2D(1) by auto
next
have "set π = set (Inl v # π) - {Inl v}" using lins2D(1) by auto
also have "... = (fset G^V - fset ({|v|} |∪| S)) <+> set G^E"
using lins2D(2) by auto
finally show "set π = (fset G^V - fset ({|v|} |∪| S)) <+> set G^E"
by auto
next
fix i j v e
assume "i < length π" "j < length π" "π ! i = Inl v"
"π ! j = Inr e" "v |∈| fst3 e"
thus "i < j" using lins2D(3)[of "i+1" "j+1"] by auto
next
fix j k w e
assume "j < length π" "k < length π" "π ! j = Inr e"
"π ! k = Inl w" "w |∈| thd3 e"
thus "j < k" using lins2D(4)[of "j+1" "k+1"] by auto
qed
qed

lemma next_lins2_edge:
assumes "Inr e # π ∈ lins2 S (Graph V Λ E)"
and "vs |⊆| S"
and "e = (vs,c,ws)"
shows "π ∈ lins2 (S - vs) (Graph (V - vs) Λ (removeAll e E))"
proof -
note lins2D = lins2D[OF assms(1)]
show ?thesis
proof (intro lins2I, unfold vertices.simps edges.simps)
show "distinct π"
using lins2D(1) by auto
next
show "set π = (fset (V - vs) - fset (S - vs))
<+> set (removeAll e E)"

apply (insert lins2D(1) lins2D(2) assms(2))
apply (unfold assms(3) vertices.simps edges.simps subset_fset, simp)
apply (unfold diff_diff_eq)
apply auto
defer 1
apply (metis (lifting) InrI List.set.simps(2)
Pair_eq set_ConsD sum.simps(2))
apply (metis (lifting) InrI List.set.simps(2)
Pair_eq set_ConsD sum.simps(2))
apply (unfold insert_is_Un[of _ "set π"])
apply (fold assms(3))
apply (subgoal_tac "set π = ((fset V - fset S) <+> set E) - {Inr e}")
apply auto
done
next
fix i j v e
assume "i < length π" "j < length π" "π ! i = Inl v"
"π ! j = Inr e" "v |∈| fst3 e"
thus "i < j" using lins2D(3)[of "i+1" "j+1"] by auto
next
fix j k w e
assume "j < length π" "k < length π" "π ! j = Inr e"
"π ! k = Inl w" "w |∈| thd3 e"
thus "j < k" using lins2D(4)[of "j+1" "k+1"] by auto
qed
qed


text {* We wish to prove that every proofstate chain that can be obtained from
a linear extension of @{term G} is well-formed and has as its final
proofstate that state in which every terminal node in @{term G} is mapped
to @{term Bot}.

We first prove this for partially-processed diagrams, for
then the result for ordinary diagrams follows as an easy corollary.

We use induction on the size of the partially-processed diagram. The size of
a partially-processed diagram @{term "(G,S)"} is defined as the number of
nodes in @{term G}, plus the number of edges, minus the number of nodes in
@{term S}. *}


lemma wf_chains2:
fixes k
assumes "S |⊆| initials G"
and "wf_dia G"
and "Π ∈ ps_chains2 S G"
and "card_fset G^V + length G^E = k + card_fset S"
shows "wf_ps_chain Π ∧ (post Π = [ terminals G |=> Bot ])"
using assms
proof (induct k arbitrary: S G Π)
case 0
obtain V Λ E where G_def: "G = Graph V Λ E" by (metis diagram.exhaust)
have "S |⊆| V"
using "0.prems"(1) initials_in_vertices[of "G"]
by (auto simp add: G_def)
have "card_fset V ≤ card_fset S"
using "0.prems"(4)
by (unfold G_def, auto)
from card_subset_fset_eq[OF `S |⊆| V` this] have "S = V" by auto
hence "E = []" using "0.prems"(4) by (unfold G_def, auto)
have "initials G = V"
by (unfold G_def `E=[]`, rule no_edges_imp_all_nodes_initial)
have "terminals G = V"
by (unfold G_def `E=[]`, rule no_edges_imp_all_nodes_terminal)
have "{} <+> {} = {}" by auto
have "lins2 S G = { [] }"
apply (unfold G_def `S=V` `E=[]`)
apply (unfold lins2_def, auto simp add: `{} <+> {} = {}`)
done
hence Π_def: "Π = \<lbrace> initial_ps2 S G \<rbrace>"
using "0.prems"(3)
by (auto simp add: ps_chains2_def mk_ps_chain_def)
show ?case
apply (intro conjI)
apply (unfold Π_def wf_ps_chain_def, auto)
apply (unfold post.simps initial_ps2_def `initials G = V` `terminals G = V`)
apply (unfold `S=V`)
apply (subgoal_tac "V - V = {||}", simp)
apply (transfer, simp add: make_map_def)
apply (metis minus_in_fset remove_fset_cases)
done
next
case (Suc k)
obtain V Λ E where G_def: "G = Graph V Λ E" by (metis diagram.exhaust)
from Suc.prems(3) obtain π where
Π_def: "Π = mk_ps_chain \<lbrace> initial_ps2 S G \<rbrace> π" and
π_in: "π ∈ lins2 S G"
by (auto simp add: ps_chains2_def)
note lins2 = lins2D[OF π_in]
have "S |⊆| V"
using Suc.prems(1) initials_in_vertices[of "G"]
by (auto simp add: G_def)
show ?case
proof (cases π)
case Nil
from π_in have "V = S" "E = []"
apply (-, unfold `π = []` lins2_def, simp_all)
apply (unfold empty_eq_Plus_conv)
apply (unfold G_def vertices.simps edges.simps, auto)
apply (fold subset_fset, auto simp add: `S |⊆| V` order_antisym)
done
with Suc.prems(4) have False by (simp add: G_def)
thus ?thesis by auto
next
case (Cons x π')
note π_def = this
show ?thesis
proof (cases x)
case (Inl v)
note x_def = this

have "v |∉| S ∧ v |∈| V"
apply (subgoal_tac "v ∈ fset V - fset S")
apply (descending, simp)
apply (subgoal_tac "Inl v ∈ (fset V - fset S) <+> set E")
apply (metis Inl_inject Inr_not_Inl PlusE)
apply (metis lins2(1) lins2(2) Cons G_def Inl distinct.simps(2)
distinct_length_2_or_more edges.simps vertices.simps)
done
hence v_notin_S: "v |∉| S" and v_in_V: "v |∈| V" by auto

have v_initial_not_S: "v |∈| initials G - S"
apply (unfold G_def initials_def vertices.simps edges.simps)
apply (unfold minus_in_fset)
apply (unfold conj_commute, intro conjI, rule v_notin_S)
apply (subgoal_tac
"v ∈ fset (filter_fset (λv. ∀e∈set E. v |∉| thd3 e) V)")
apply (smt in_fset)
apply (unfold filter_fset, simp, unfold conj_commute)
apply (intro conjI ballI notI)
apply (insert v_in_V, descending, auto)
proof -
fix e :: edge
assume "v |∈| thd3 e"
assume "e ∈ set E"
hence "Inr e ∈ set π" using lins2(2) by (auto simp add: G_def)
then obtain j where
"j < length π" "0 < length π" "π!j = Inr e" "π!0 = Inl v"
by (metis π_def x_def in_set_conv_nth length_pos_if_in_set nth_Cons_0)
from lins2(4)[OF this `v |∈| thd3 e`] show False by auto
qed

def S' "{|v|} |∪| S"

def Π' "mk_ps_chain \<lbrace> initial_ps2 S' G \<rbrace> π'"
hence pre_Π': "pre Π' = initial_ps2 S' G"
by (metis pre.simps(1) pre_mk_ps_chain)

def σ "[ initials G - ({|v|} |∪| S) |=> Top ] ⊕ [ S |=> Bot ]"

have "wf_ps_chain Π' ∧ (post Π' = [terminals G |=> Bot])"
proof (intro Suc.hyps[of "S'"])
show "S' |⊆| initials G"
apply (unfold S'_def, auto)
apply (unfold subset_insert_fset, intro conjI)
apply (metis v_initial_not_S minus_in_fset)
apply (rule Suc(2))
done
next
show "wf_dia G" by (rule Suc.prems(2))
next
show "Π' ∈ ps_chains2 S' G"
apply (unfold ps_chains2_def Π'_def)
apply (intro imageI)
apply (unfold S'_def)
apply (intro next_lins2_vertex)
apply (fold x_def, fold π_def)
apply (rule π_in)
apply (metis in_minus_fset v_initial_not_S)
done
next
show "card_fset G^V + length G^E = k + card_fset S'"
by (unfold S'_def, auto simp add: v_notin_S Suc.prems(4))
qed
hence
wf_Π': "wf_ps_chain Π'" and
post_Π': "post Π' = [terminals G |=> Bot]"
by auto

show ?thesis
proof (intro conjI)
have 1: "fdom [ {|v|} |=> Bot ]
|∩| fdom ([ initials G - ({|v|} |∪| S) |=> Top ] ⊕
[ S |=> Bot ]) = {||}"

by (metis (no_types) fdom_make_fmap fdom_union
bot_least in_union_fset inter_insert_fset le_iff_inf
minus_in_fset subset_insert_fset sup_ge1 v_initial_not_S)
show "wf_ps_chain Π"
apply (unfold Π_def π_def x_def mk_ps_chain_cons)
apply simp
apply (unfold mk_ps_chain_ccons)
apply (fold next_initial_ps2_vertex S'_def)
apply (fold Π'_def)
apply (unfold wf_ps_chain_def chain_all.simps conj_commute)
apply (intro conjI)
apply (fold wf_ps_chain_def, rule wf_Π')
apply (intro wf_ps_triple_nodeI exI[of _ "σ"] conjI)
apply (unfold σ_def fdom_union fdom_make_fmap)
apply (metis v_notin_S in_minus_fset in_union_fset insert_fsetI1)
apply (unfold pre_Π' initial_ps2_def S'_def)
apply (unfold fmap_add_commute[OF 1])
apply (unfold fmap_add_assoc)
apply (fold fmap_add_assoc[of _ "[ S |=> Bot ]"])
apply (unfold make_fmap_union sup.commute[of "{|v|}"])
apply (unfold fset_diff_union)
apply (metis bot_least fset_diff_union2
subset_insert_fset v_initial_not_S)
apply simp
done
next
show "post Π = [ terminals G |=> Bot ]"
apply (unfold Π_def π_def x_def mk_ps_chain_cons, simp)
apply (unfold mk_ps_chain_ccons post.simps)
apply (fold next_initial_ps2_vertex S'_def)
apply (fold Π'_def, rule post_Π')
done
qed
next
case (Inr e)
note x_def = this
def vs "fst3 e"
def ws "thd3 e"

obtain c where e_def: "e = (vs, c, ws)"
by (metis vs_def ws_def fst3_simp thd3_simp prod_cases3)

have "linearity E" and "acyclicity E" and
e_in_V: "!!e. e ∈ set E ==> fst3 e |∪| thd3 e |⊆| V"
by (insert Suc.prems(2) wf_dia_inv, unfold G_def, blast)+
note lin = linearityD[OF this(1)]

have acy: "!!e. e ∈ set E ==> fst3 e |∩| thd3 e = {||}"
apply (fold fset_cong, insert `acyclicity E`)
apply (unfold acyclicity_def acyclic_def, auto)
done

note lins = lins2D[OF π_in]

have e_in_E: "e ∈ set E"
apply (subgoal_tac "set π = (fset G^V - fset S) <+> set G^E")
apply (unfold π_def x_def G_def edges.simps, auto)[1]
apply (simp add: lins(2))
done

have vs_in_S: "vs |⊆| S"
apply (insert e_in_V[OF e_in_E])
apply (unfold subset_fset)
apply (intro subsetI)
apply (unfold vs_def)
apply (rule ccontr)
apply (subgoal_tac "x ∈ fset V")
prefer 2
apply (auto)
proof -
fix v
assume a: "v ∈ fset (fst3 e)"
assume "v ∉ fset S" and "v ∈ fset V"
hence "Inl v ∈ set π"
by (metis (lifting) DiffI G_def InlI lins(2) vertices.simps)
then obtain i where
"i < length π" "0 < length π" "π!i = Inl v" "π!0 = Inr e"
by (metis Cons Inr in_set_conv_nth length_pos_if_in_set nth_Cons_0)
from lins(3)[OF this] show "False" by (auto simp add: in_fset a)
qed

have "ws |∩| (initials G) = {||}"
apply (insert e_in_V[OF e_in_E])
apply (unfold initials_def subset_fset in_fset, fold fset_cong)
apply (unfold ws_def G_def, auto simp add: e_in_E)
done

def S' "S - vs"
def V' "V - vs"
def E' "removeAll e E"
def G' "Graph V' Λ E'"

def Π' "mk_ps_chain \<lbrace> initial_ps2 S' G' \<rbrace> π'"
hence pre_Π': "pre Π' = initial_ps2 S' G'"
by (metis pre.simps(1) pre_mk_ps_chain)

def σ "[ initials G - S |=> Top ] ⊕ [ S - vs |=> Bot ]"

have next_initial_ps2: "initial_ps2 S' G'
= initial_ps2 S G \<ominus> vs ⊕ [ws |=> Top]"

using next_initial_ps2_edge[OF G_def _ _ _ e_in_E _ Suc.prems(1)
Suc.prems(2)] G'_def E'_def vs_def ws_def V'_def vs_in_S S'_def
by auto

have "wf_ps_chain Π' ∧ post Π' = [ terminals G' |=> Bot ]"
proof (intro Suc.hyps[of "S'"])
show "S' |⊆| initials G'"
apply (insert Suc.prems(1))
apply (unfold G'_def G_def initials_def)
apply (unfold subset_fset S'_def E'_def V'_def)
apply (auto simp add: in_fset)
done
next
from Suc.prems(2) have "wf_dia (Graph V Λ E)"
by (unfold G_def)
note wf_G = wf_dia_inv[OF this]
show "wf_dia G'"
apply (unfold G'_def V'_def E'_def)
apply (insert wf_G e_in_E vs_in_S Suc.prems(1))
apply (unfold vs_def)
apply (intro wf_dia)
apply (unfold linearity_def initials_def G_def)
apply (fold fset_cong, unfold subset_fset in_fset)
apply (simp, simp)
apply (unfold acyclicity_def, rule acyclic_subset)
apply (auto simp add: distinct_removeAll)
apply (metis (lifting) IntI empty_iff)
done
next
show "Π' ∈ ps_chains2 S' G'"
apply (unfold Π_def Π'_def ps_chains2_def)
apply (intro imageI)
apply (unfold S'_def G'_def V'_def E'_def)
apply (intro next_lins2_edge)
apply (metis π_def G_def x_def π_in)
apply (auto simp add: vs_in_S e_def)
done
next
have "vs |⊆| V" by (metis (lifting) `S |⊆| V` order_trans vs_in_S)
have "distinct E" using `linearity E` linearity_def by auto
show "card_fset G'^V + length G'^E = k + card_fset S'"
apply (insert Suc.prems(4))
apply (unfold G_def G'_def vertices.simps edges.simps)
apply (unfold V'_def E'_def S'_def)
apply (unfold card_minus_subset_fset[OF `vs |⊆| V`])
apply (unfold card_minus_subset_fset[OF `vs |⊆| S`])
apply (fold distinct_remove1_removeAll[OF `distinct E`])
apply (unfold length_remove1)
apply (simp add: e_in_E)
apply (smt `S |⊆| V` card_fset_mono e_def e_in_E length_0_conv
length_greater_0_conv length_pos_if_in_set vs_def vs_in_S)
done
qed
hence
wf_Π': "wf_ps_chain Π'" and
post_Π': "post Π' = [ terminals G' |=> Bot ]"
by auto

have terms_same: "terminals G = terminals G'"
apply (unfold G'_def G_def terminals_def edges.simps vertices.simps)
apply (unfold E'_def V'_def)
apply (fold fset_cong, auto simp add: in_fset e_in_E vs_def)
done

have 1: "fdom [ fst3 e |=> Bot ] |∩|
fdom([ filter_fset (λv. ∀e∈set E. v |∉| thd3 e) V - S |=> Top ]
⊕ [ S - fst3 e |=> Bot ]) = {||}"

apply (unfold fdom_union fdom_make_fmap)
apply (fold fset_cong)
apply (auto simp add: in_fset)
apply (metis in_mono subset_fset vs_def vs_in_S)
done

show ?thesis
proof (intro conjI)
show "wf_ps_chain Π"
apply (unfold Π_def π_def x_def mk_ps_chain_cons)
apply simp
apply (unfold mk_ps_chain_ccons)
apply (fold vs_def ws_def)
apply (fold next_initial_ps2)
apply (fold Π'_def)
apply (unfold wf_ps_chain_def chain_all.simps conj_commute)
apply (intro conjI)
apply (fold wf_ps_chain_def)
apply (rule wf_Π')
apply (intro wf_ps_triple_edgeI exI[of _ "σ"])
apply (unfold e_def fst3_simp thd3_simp σ_def, intro conjI)
apply (insert Suc.prems(1))
apply (unfold pre_Π' initial_ps2_def initials_def)
apply (insert vs_in_S acy[OF e_in_E])
apply (fold fset_cong)
apply (unfold subset_fset)[1]
apply (unfold G_def G'_def vs_def ws_def V'_def E'_def S'_def)
apply (unfold vertices.simps edges.simps)
apply (unfold fmap_add_commute[OF 1])
apply (fold fmap_add_assoc)
apply (unfold make_fmap_union)
apply (unfold fset_diff_union2)
apply (auto simp add: in_fset fdom_union fdom_make_fmap e_in_E)[1]
apply simp
apply (unfold fmap_add_assoc)
apply (unfold make_fmap_union)
apply (intro arg_cong2[of _ _ "[ S - fst3 e |=> Bot ]"
"[ S - fst3 e |=> Bot ]" "op ⊕"])
apply (intro arg_cong2[of _ _ "Top" "Top" "make_fmap"])
defer 1
apply (simp, simp)
apply (fold fset_cong)
apply (unfold subset_fset in_fset, simp)
apply (elim conjE)
apply (intro set_eqI iffI, simp_all)
apply (elim conjE, intro disjI conjI ballI, simp)
apply (case_tac "ea=e", simp_all)
apply (elim disjE conjE, intro conjI ballI impI, simp_all)
apply (smt disjoint_iff_not_equal e_in_E fset_simps(1) inter_fset lin(2))
apply (metis G_def Suc(3) e_in_E set_mp subset_fset wf_dia_inv')
apply (metis IntI empty_iff)
apply (metis (lifting) IntI Suc(2) `ws |∩| initials G = {||}`
empty_iff fset_simps(1) in_mono inter_fset subset_fset ws_def)
apply (metis set_mp)
done
next
show "post Π = [terminals G |=> Bot]"
apply (unfold Π_def π_def x_def mk_ps_chain_cons)
apply simp
apply (unfold mk_ps_chain_ccons post.simps)
apply (fold vs_def ws_def)
apply (fold next_initial_ps2)
apply (fold Π'_def)
apply (unfold terms_same)
apply (rule post_Π')
done
qed
qed
qed
qed



corollary wf_chains:
assumes "wf_dia G"
assumes "Π ∈ ps_chains G"
shows "wf_ps_chain Π ∧ post Π = [ terminals G |=> Bot ]"
apply (intro wf_chains2[of "{||}"], insert assms(2))
apply (auto simp add: assms(1) ps_chains_is_ps_chains2_with_empty_S)
done

subsection {* Interface chains *}

type_synonym int_chain = "(interface, assertion_gadget + command_gadget) chain"

text {* An interface chain is similar to a proofstate chain. However, where a
proofstate chain talks about nodes and edges, an interface chain talks about
the assertion-gadgets and command-gadgets that label those nodes and edges
in a diagram. And where a proofstate chain talks about proofstates, an
interface chain talks about the interfaces obtained from those proofstates.

The following functions convert a proofstate chain into an
interface chain. *}


definition
ps_to_int :: "[diagram, proofstate] => interface"
where
"ps_to_int G σ ≡
\<Otimes>v |∈| fdom σ. topbot_case top_ass bot_ass (lookup σ v) (G^Λ v)"


definition
ps_chain_to_int_chain :: "[diagram, ps_chain] => int_chain"
where
"ps_chain_to_int_chain G Π ≡
chainmap (ps_to_int G) ((sum_case (Inl o G^Λ) (Inr o snd3))) Π"


lemma ps_chain_to_int_chain_simp:
"ps_chain_to_int_chain (Graph V Λ E) Π =
chainmap (ps_to_int (Graph V Λ E)) ((sum_case (Inl o Λ) (Inr o snd3))) Π"

by (simp add: ps_chain_to_int_chain_def)

subsection {* Soundness proof *}

text {* We assume that @{term wr_com} always returns @{term "{}"}. This is
equivalent to changing our axiomatization of separation logic such that the
frame rule has no side-condition. One way to obtain a separation logic
lacking a side-condition on its frame rule is to use variables-as-
resource.

We proceed by induction on the proof rules for graphical diagrams. We
show that: (1) if a diagram @{term G} is provable w.r.t. interfaces
@{term P} and @{term Q}, then @{term P} and @{term Q} are the top and bottom
interfaces of @{term G}, and that the Hoare triple @{term "(asn P,
c, asn Q)"} is provable for each command @{term c} that can be extracted
from @{term G}; (2) if a command-gadget @{term C} is provable w.r.t.
interfaces @{term P} and @{term Q}, then the Hoare triple @{term "(asn P,
c, asn Q)"} is provable for each command @{term c} that can be extracted
from @{term C}; and (3) if an assertion-gadget @{term A} is provable, and if
the top and bottom interfaces of @{term A} are @{term P} and @{term Q}
respectively, then the Hoare triple @{term "(asn P, c, asn Q)"} is provable
for each command @{term c} that can be extracted from @{term A}. *}




lemma soundness_graphical_helper:
assumes no_var_interference: "!!c. wr_com c = {}"
shows
"(prov_dia G P Q -->
(P = top_dia G ∧ Q = bot_dia G ∧
(∀c. coms_dia G c --> prov_triple (asn P, c, asn Q))))
∧ (prov_com C P Q -->
(∀c. coms_com C c --> prov_triple (asn P, c, asn Q)))
∧ (prov_ass A -->
(∀c. coms_ass A c --> prov_triple (asn (top_ass A), c, asn (bot_ass A))))"

proof (induct rule: prov_dia_prov_com_prov_ass.induct)
case (Skip p)
thus ?case
apply (intro allI impI, elim conjE coms_skip_inv)
apply (auto simp add: prov_triple.skip)
done
next
case (Exists G P Q x)
thus ?case
apply (intro allI impI, elim conjE coms_exists_inv)
apply (auto simp add: prov_triple.exists)
done
next
case (Basic P c Q)
thus ?case
by (intro allI impI, elim conjE coms_basic_inv, auto)
next
case (Choice G P Q H)
thus ?case
apply (intro allI impI, elim conjE coms_choice_inv)
apply (auto simp add: prov_triple.choose)
done
next
case (Loop G P)
thus ?case
apply (intro allI impI, elim conjE coms_loop_inv)
apply (auto simp add: prov_triple.loop)
done
next
case (Main G)
thus ?case
apply (intro conjI)
apply (simp, simp)
apply (intro allI impI)
apply (elim coms_main_inv, simp)
proof -
fix c V Λ E
fix π::"lin"
fix cs::"command list"
assume wf_G: "wf_dia (Graph V Λ E)"
assume "!!v. v ∈ fset V ==> ∀c. coms_ass (Λ v) c -->
prov_triple (asn (top_ass (Λ v)), c, asn (bot_ass (Λ v)))"

hence prov_vertex: "!!v c P Q F. [| coms_ass (Λ v) c; v ∈ fset V;
P = (top_ass (Λ v) ⊗ F) ; Q = (bot_ass (Λ v) ⊗ F) |]
==> prov_triple (asn P, c, asn Q)"

by (auto simp add: prov_triple.frame no_var_interference)
assume "!!e. e ∈ set E ==> ∀c. coms_com (snd3 e) c --> prov_triple
(asn (\<Otimes>v|∈|fst3 e. bot_ass (Λ v)),c,asn (\<Otimes>v|∈|thd3 e. top_ass (Λ v)))"

hence prov_edge: "!!e c P Q F. [| e ∈ set E ; coms_com (snd3 e) c ;
P = ((\<Otimes>v|∈|fst3 e. bot_ass (Λ v)) ⊗ F) ;
Q = ((\<Otimes>v|∈|thd3 e. top_ass (Λ v)) ⊗ F) |]
==> prov_triple (asn P, c, asn Q)"

by (auto simp add: prov_triple.frame no_var_interference)
assume len_cs: "length cs = length π"
assume "∀i<length π.
sum_case (coms_ass o Λ) (coms_com o snd3) (π ! i) (cs ! i)"

hence π_cs: "!!i. i < length π ==>
sum_case (coms_ass o Λ) (coms_com o snd3) (π ! i) (cs ! i)"
by auto
assume G_def: "G = Graph V Λ E"
assume c_def: "c = foldr op ;; cs Skip"
assume π_lin: "π ∈ lins (Graph V Λ E)"

note lins = linsD[OF π_lin]

def Π "mk_ps_chain \<lbrace> initial_ps G \<rbrace> π"

have "Π ∈ ps_chains G" by (simp add: π_lin Π_def ps_chains_def G_def)
hence 1: "post Π = [ terminals G |=> Bot ]"
and 2: "chain_all wf_ps_triple Π"
by (insert wf_chains G_def wf_G, auto simp add: wf_ps_chain_def)

show "prov_triple (asn (\<Otimes>v|∈|initials (Graph V Λ E). top_ass (Λ v)),
foldr op ;; cs Skip, asn (\<Otimes>v|∈|terminals (Graph V Λ E). bot_ass (Λ v)))"

apply (intro seq_fold[of _ "ps_chain_to_int_chain G Π"])
apply (unfold len_cs)
apply (unfold ps_chain_to_int_chain_def chainmap_preserves_length Π_def)
apply (unfold mk_ps_chain_preserves_length, simp)
apply (unfold pre_chainmap post_chainmap)
apply (unfold pre_mk_ps_chain pre.simps)
apply (fold Π_def, unfold 1)
apply (unfold initial_ps_def)
apply (unfold ps_to_int_def)
apply (unfold fdom_make_fmap)
apply (unfold G_def labelling.simps, fold G_def)
apply (subgoal_tac "∀v ∈ fset (initials G). top_ass (Λ v) =
topbot_case top_ass bot_ass (lookup [ initials G |=> Top ] v) (Λ v)"
)
apply (unfold iter_hcomp_cong, simp)
apply (metis lookup_make_fmap topbot.simps(3))
apply (subgoal_tac "∀v ∈ fset (terminals G). bot_ass (Λ v) =
topbot_case top_ass bot_ass (lookup [ terminals G |=> Bot ] v) (Λ v)"
)
apply (unfold iter_hcomp_cong, simp)
apply (metis lookup_make_fmap topbot.simps(4), simp)
apply (unfold G_def, fold ps_chain_to_int_chain_simp G_def)
proof -
fix i
assume "i < length π"
hence "i < chainlen Π"
by (metis Π_def add_0_left chainlen.simps(1)
mk_ps_chain_preserves_length)
hence wf_Πi: "wf_ps_triple (nthtriple Π i)"
by (insert 2, simp add: chain_all_nthtriple)
show "prov_triple (asn (fst3 (nthtriple (ps_chain_to_int_chain G Π) i)),
cs ! i, asn (thd3 (nthtriple (ps_chain_to_int_chain G Π) i)))"

apply (unfold ps_chain_to_int_chain_def)
apply (unfold nthtriple_chainmap[OF `i < chainlen Π`])
apply (unfold fst3_simp thd3_simp)
proof (cases "π!i")
case (Inl v)

have "snd3 (nthtriple Π i) = Inl v"
apply (unfold snds_of_triples_form_comlist[OF `i < chainlen Π`])
apply (auto simp add: Π_def comlist_mk_ps_chain Inl)
done

with wf_Πi wf_ps_triple_def obtain σ where
v_notin_σ: "v |∉| fdom σ" and
fst_Πi: "fst3 (nthtriple Π i) = [ {|v|} |=> Top ] ⊕ σ" and
thd_Πi: "thd3 (nthtriple Π i) = [ {|v|} |=> Bot ] ⊕ σ"
by auto

show "prov_triple (asn (ps_to_int G (fst3 (nthtriple Π i))),
cs ! i, asn (ps_to_int G (thd3 (nthtriple Π i))))"

apply (intro prov_vertex[where v=v])
apply (metis (no_types) Inl `i < length π` π_cs o_def sum.simps(5))
apply (metis (lifting) Inl lins(2) Inl_not_Inr PlusE `i < length π`
nth_mem sum.simps(1) vertices.simps)
apply (unfold fst_Πi thd_Πi)
apply (unfold ps_to_int_def)
apply (unfold fdom_union fdom_make_fmap)
apply (unfold singleton_union_fset_left)
apply (insert v_notin_σ)
apply (unfold iter_hcomp_insert)
apply (unfold lookup_union2 lookup_make_fmap1)
apply (unfold G_def labelling.simps)
apply (subgoal_tac "∀va ∈ fset (fdom σ). topbot_case top_ass bot_ass
(lookup ([ {|v|} |=> Top ] ⊕ σ) va) (Λ va) =
topbot_case top_ass bot_ass (lookup ([{|v|} |=> Bot] ⊕ σ) va)(Λ va)"
)
apply (unfold iter_hcomp_cong, simp)
apply (metis in_fset lookup_union1, simp)
done
next
case (Inr e)
have "snd3 (nthtriple Π i) = Inr e"
apply (unfold snds_of_triples_form_comlist[OF `i < chainlen Π`])
apply (auto simp add: Π_def comlist_mk_ps_chain Inr)
done

with wf_Πi wf_ps_triple_def obtain σ where
fst_e_disjoint_σ: "fst3 e |∩| fdom σ = {||}" and
thd_e_disjoint_σ: "thd3 e |∩| fdom σ = {||}" and
fst_Πi: "fst3 (nthtriple Π i) = [ fst3 e |=> Bot ] ⊕ σ" and
thd_Πi: "thd3 (nthtriple Π i) = [ thd3 e |=> Top ] ⊕ σ"
by (smt sum.simps(6) inf_sup_distrib2 sup_eq_bot_iff)

show "prov_triple (asn (ps_to_int G (fst3 (nthtriple Π i))),
cs ! i, asn (ps_to_int G (thd3 (nthtriple Π i))))"

apply (intro prov_edge[where e=e])
apply (subgoal_tac "Inr e ∈ set π")
apply (metis Inr_not_Inl PlusE edges.simps lins(2) sum.simps(2))
apply (metis Inr `i < length π` nth_mem)
apply (metis (no_types) Inr `i < length π` π_cs o_def sum.simps(6))
apply (unfold fst_Πi thd_Πi)
apply (unfold ps_to_int_def)
apply (unfold G_def labelling.simps)
apply (unfold fdom_union fdom_make_fmap)
apply (insert fst_e_disjoint_σ)
apply (unfold iter_hcomp_union)
apply (subgoal_tac "∀v ∈ fset (fst3 e). topbot_case top_ass bot_ass
(lookup ([ fst3 e |=> Bot ] ⊕ σ) v) (Λ v) = bot_ass (Λ v)"
)
apply (unfold iter_hcomp_cong)
apply (simp)
apply (intro ballI)
apply (subgoal_tac "v |∉| fdom σ")
apply (unfold lookup_union2)
apply (metis lookup_make_fmap topbot.simps(4))
apply (metis fst_e_disjoint_σ in_inter_fset notin_empty_fset in_fset)
apply (insert thd_e_disjoint_σ)
apply (unfold iter_hcomp_union)
apply (subgoal_tac "∀v ∈ fset (thd3 e). topbot_case top_ass bot_ass
(lookup ([ thd3 e |=> Top ] ⊕ σ) v) (Λ v) = top_ass (Λ v)"
)
apply (unfold iter_hcomp_cong)
apply (subgoal_tac "∀v ∈ fset (fdom σ). topbot_case top_ass bot_ass
(lookup ([ thd3 e |=> Top ] ⊕ σ) v) (Λ v) =
topbot_case top_ass bot_ass (lookup ([fst3 e |=> Bot] ⊕ σ) v) (Λ v)"
)
apply (unfold iter_hcomp_cong)
apply simp
apply (intro ballI)
apply (subgoal_tac "v |∈| fdom σ")
apply (unfold lookup_union1, auto simp add: in_fset)
apply (subgoal_tac "v |∉| fdom σ")
apply (unfold lookup_union2)
apply (metis lookup_make_fmap topbot.simps(3))
apply (metis thd_e_disjoint_σ in_inter_fset notin_empty_fset in_fset)
done
qed
qed
qed
qed

text {* The soundness theorem states that any diagram provable using the
proof rules for ribbons can be recreated as a valid proof in separation
logic. *}


corollary soundness_graphical:
assumes "!!c. wr_com c = {}"
assumes "prov_dia G P Q"
shows "∀c. coms_dia G c --> prov_triple (asn P, c, asn Q)"
using soundness_graphical_helper[OF assms(1)] and assms(2) by auto

end