Theory Ribbons_Graphical_Soundness

section ‹Soundness for graphical diagrams›

theory Ribbons_Graphical_Soundness imports
  Ribbons_Graphical
  More_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 Ribbon_Proofs.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 ⇀⇩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) = σ ⊖ {|v|} ++⇩f [{|v|} |=> Bot]"
| "next_ps σ (Inr e) = σ ⊖ fst3 e ++⇩f [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 (⦃ σ ⦄ ⋅ x ⋅ Π) π = ⦃ σ ⦄ ⋅ 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 (auto simp add: 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 Ribbon_Proofs.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 ] ++⇩f [ 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 simp
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 ++⇩fdisjoint g"} is defined, when @{term f} and
  @{term g} have disjoint domains, as @{term "f ++⇩f g"}. Then, a well-formed
  proofstate chain consists of triples of the form @{term "(σ ++⇩fdisjoint
  [{| v |} |=> Top], Inl v, σ ++⇩fdisjoint [{| v |} |=> Bot])"}, where @{term v}
  is a node, or of the form @{term "(σ ++⇩fdisjoint [{| vs |} |=> Bot], Inr e,
  σ ++⇩fdisjoint [{| 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 |∉| fmdom σ
      ∧ fst3 T = [ {|v|} |=> Top ] ++⇩f σ
      ∧ thd3 T = [ {|v|} |=> Bot ] ++⇩f σ)
  | Inr e ⇒ (∃σ. (fst3 e |∪| thd3 e) |∩| fmdom σ = {||}
      ∧ fst3 T = [ fst3 e |=> Bot ] ++⇩f σ
      ∧ thd3 T = [ thd3 e |=> Top ] ++⇩f σ))"

lemma wf_ps_triple_nodeI:
  assumes "∃σ. v |∉| fmdom σ  ∧
    σ1 = [ {|v|} |=> Top ] ++⇩f σ ∧
    σ2 = [ {|v|} |=> Bot ] ++⇩f σ"
  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) |∩| fmdom σ = {||}
      ∧ σ1 = [ fst3 e |=> Bot ] ++⇩f σ
      ∧ σ2 = [ thd3 e |=> Top ] ++⇩f σ"
  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 ⊖ {|v|} ++⇩f [ {|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 ⊖ fst3 e ++⇩f [ 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"
  have "thd3 e |∩| initials G = {||}"
    by (auto simp add: initials_def G_def e_in_E)
  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)
  apply (unfold G_def G'_def V'_def E'_def)
  apply (unfold edges.simps vertices.simps)
  apply (simp add: less_eq_fset.rep_eq e_in_E)
  apply safe
  apply (insert ‹thd3 e |∩| initials G = {||}›)[1]
  apply (insert S_initials, fold fset_cong)[2]
  apply (unfold less_eq_fset.rep_eq initials_def filter_fset)
  apply (auto simp add: G_def e_in_E)[1]
  apply (auto simp add: G_def e_in_E)[1]
  apply (auto simp add: G_def e_in_E)[1]
  apply (insert wf_G)[1]
  apply (unfold G_def vertices.simps edges.simps)
  apply (drule wf_dia_inv(3))
  apply (unfold acyclicity_def)
  apply (metis fst_e_in_S inter_fset le_iff_inf subsetD)
  apply (insert wf_G)[1]
  apply (unfold G_def vertices.simps edges.simps)
  apply (drule wf_dia_inv(4))
  apply (drule linearityD2)
  apply (fold fset_cong, unfold inter_fset fset_simps)
  apply (insert e_in_E, blast)[1]
  apply (insert wf_G)[1]
  apply (unfold G_def vertices.simps edges.simps)
  apply (drule wf_dia_inv(3))
  apply (metis (lifting) e_in_E G_def empty_iff fset_simps(1)
    finter_iff linearityD(2) wf_G wf_dia_inv(4))
  apply (insert wf_G)[1]
  apply (unfold G_def vertices.simps edges.simps)
  apply (drule wf_dia_inv(4))
  apply (drule linearityD2)
  apply (fold fset_cong, unfold inter_fset fset_simps)
  apply (insert e_in_E, blast)[1]
  apply (insert wf_G)[1]
  apply (unfold G_def vertices.simps edges.simps)
  apply (drule wf_dia_inv(3))
  apply (metis (lifting) e_in_E G_def empty_iff fset_simps(1)
    finter_iff linearityD(2) wf_G wf_dia_inv(4))
  apply (insert wf_G)
  apply (unfold G_def vertices.simps edges.simps)
  apply (drule wf_dia_inv(5))
  apply (unfold less_eq_fset.rep_eq union_fset)
  apply auto[1]
  apply (drule wf_dia_inv(5))
  apply (unfold less_eq_fset.rep_eq union_fset)
  apply auto[1]
  apply (drule wf_dia_inv(5))
  apply (unfold less_eq_fset.rep_eq union_fset)
  apply (auto simp add: e_in_E)[1]
  apply (drule wf_dia_inv(5))
  apply (unfold less_eq_fset.rep_eq 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 less_eq_fset.rep_eq, simp)
    apply (unfold diff_diff_eq)
    proof -
      have "∀a aa b.
       insert (Inr (vs, c, ws)) (set π) = (fset V - fset S) <+> set E ⟶
       fset vs ⊆ fset S ⟶
       Inr (vs, c, ws) ∉ set π ⟶
       distinct π ⟶ (a, aa, b) ∈ set E ⟶ Inr (a, aa, b) ∉ set π ⟶ b = ws"
     by (metis (lifting) InrI List.set_simps(2)
      prod.inject set_ConsD sum.simps(2))

     moreover have "∀a aa b.
       insert (Inr (vs, c, ws)) (set π) = (fset V - fset S) <+> set E ⟶
       fset vs ⊆ fset S ⟶
       Inr (vs, c, ws) ∉ set π ⟶
       distinct π ⟶ (a, aa, b) ∈ set E ⟶ Inr (a, aa, b) ∉ set π ⟶ aa = c"
     by (metis (lifting) InrI List.set_simps(2)
      prod.inject set_ConsD sum.simps(2))

     moreover have "∀x. insert (Inr (vs, c, ws)) (set π) = (fset V - fset S) <+> set E ⟶
         fset vs ⊆ fset S ⟶
         Inr (vs, c, ws) ∉ set π ⟶
         distinct π ⟶ x ∈ set π ⟶ x ∈ (fset V - fset S) <+> set E - {(vs, c, ws)}"
      apply (unfold insert_is_Un[of _ "set π"])
      apply (fold assms(3))
      apply clarify
      apply (subgoal_tac "set π = ((fset V - fset S) <+> set E) - {Inr e}")
      by auto
    ultimately show "Inr (vs, c, ws) ∉ set π ∧ distinct π ⟹
      insert (Inr (vs, c, ws)) (set π) = (fset V - fset S) <+> set E ⟹
      fset vs ⊆ fset S ⟹ set π = (fset V - fset S) <+> set E - {(vs, c, ws)}"
    by blast
    qed
  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 "fcard G^V + length G^E = k + fcard 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 "fcard V ≤ fcard S"
    using "0.prems"(4)
    by (unfold G_def, auto)
  from fcard_seteq[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: "Π = ⦃ initial_ps2 S G ⦄"
    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_all)
  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 ⦃ initial_ps2 S G ⦄ π" 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)
    by (metis ‹S |⊆| V› less_eq_fset.rep_eq subset_antisym)

    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 (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 (simp only: G_def initials_def vertices.simps edges.simps)
      apply (simp only: fminus_iff)
      apply (simp only: conj_commute, intro conjI, rule v_notin_S)
      apply (subgoal_tac
        "v ∈ fset (ffilter (λv. ∀e∈set E. v |∉| thd3 e) V)")
      apply simp
      apply (simp only: filter_fset, simp, simp only: conj_commute)
      apply (intro conjI ballI notI)
      apply (insert v_in_V, simp)
      proof -
        fix e :: edge
        assume "v ∈ fset (thd3 e)"
        then have "v |∈| (thd3 e)" by auto
        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)
        with lins2(4)[OF this ‹v |∈| (thd3 e)›] show False by auto
      qed

      define S' where "S' = {|v|} |∪| S"

      define Π' where "Π' = mk_ps_chain ⦃ initial_ps2 S' G ⦄ π'"
      hence pre_Π': "pre Π' = initial_ps2 S' G"
      by (metis pre.simps(1) pre_mk_ps_chain)

      define σ where "σ = [ initials G - ({|v|} |∪| S) |=> Top ] ++⇩f [ 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 (metis fminus_iff v_initial_not_S)
        by (metis Suc.prems(1) fset_rev_mp)
     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)
        by (metis v_notin_S)
      next
        show "fcard G^V + length G^E = k + fcard S'"
         apply (unfold S'_def)
         by (auto simp add: Suc.prems(4) fcard_finsert_disjoint[OF v_notin_S])
      qed
      hence
        wf_Π': "wf_ps_chain Π'" and
        post_Π': "post Π' = [terminals G |=> Bot]"
      by auto

      show ?thesis
      proof (intro conjI)
        have 1: "fmdom [ {|v|} |=> Bot ]
        |∩| fmdom ([ initials G - ({|v|} |∪| S) |=> Top ] ++⇩f
     [ S |=> Bot ]) = {||}"
        by (metis (no_types) fdom_make_fmap fmdom_add
          bot_least funion_iff finter_finsert_left le_iff_inf
          fminus_iff finsert_fsubset sup_ge1 v_initial_not_S)
        show "wf_ps_chain Π"
        using [[unfold_abs_def = false]]
        apply (simp only: Π_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 fmdom_add fdom_make_fmap)
        apply (metis finsertI1 fminus_iff funion_iff v_notin_S)
        apply (unfold pre_Π' initial_ps2_def S'_def)
        apply (unfold fmap_add_commute[OF 1])
        apply (unfold fmadd_assoc)
        apply (fold fmadd_assoc[of _ "[ S |=> Bot ]"])
        apply (unfold make_fmap_union sup.commute[of "{|v|}"])
        apply (unfold fminus_funion)
        using v_initial_not_S apply auto
        by (metis (opaque_lifting, no_types) finsert_absorb finsert_fminus_single finter_fminus
            inf_commute inf_idem v_initial_not_S)
      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
      define vs where "vs = fst3 e"
      define ws where "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 less_eq_fset.rep_eq)
      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: a)
      qed

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

      define S' where "S' = S - vs"
      define V' where "V' = V - vs"
      define E' where "E' = removeAll e E"
      define G' where "G' = Graph V' Λ E'"

      define Π' where "Π' = mk_ps_chain ⦃ initial_ps2 S' G' ⦄ π'"
      hence pre_Π': "pre Π' = initial_ps2 S' G'"
      by (metis pre.simps(1) pre_mk_ps_chain)

      define σ where "σ = [ initials G - S |=> Top ] ++⇩f [ S - vs |=> Bot ]"

      have next_initial_ps2: "initial_ps2 S' G'
        = initial_ps2 S G ⊖ vs ++⇩f [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 less_eq_fset.rep_eq S'_def E'_def V'_def)
        apply auto
        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 less_eq_fset.rep_eq)
        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)
        by (simp only: vs_in_S e_def)+
      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 "fcard G'^V + length G'^E = k + fcard 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 fcard_funion_fsubset[OF ‹vs |⊆| V›])
        apply (unfold fcard_funion_fsubset[OF ‹vs |⊆| S›])
        apply (fold distinct_remove1_removeAll[OF ‹distinct E›])
        apply (unfold length_remove1)
        apply (simp add: e_in_E)
        apply (drule arg_cong[of _ _ "λx. x - fcard vs - 1"])
        apply (subst (asm) add_diff_assoc2[symmetric])
        apply (simp add: fcard_mono[OF ‹vs |⊆| V›])
        apply (subst add_diff_assoc, insert length_pos_if_in_set[OF e_in_E], arith, auto)
        apply (subst add_diff_assoc, auto simp add: fcard_mono[OF ‹vs |⊆| 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: e_in_E vs_def)
      done

      have 1: "fmdom [ fst3 e |=> Bot ] |∩|
        fmdom([ ffilter (λv. ∀e∈set E. v |∉| thd3 e) V - S |=> Top ]
        ++⇩f [ S - fst3 e |=> Bot ]) = {||}"
      apply (unfold fmdom_add fdom_make_fmap)
      apply (fold fset_cong)
      apply auto
      apply (metis in_mono less_eq_fset.rep_eq vs_def vs_in_S)
      done

      show ?thesis
      proof (intro conjI)
        show "wf_ps_chain Π"
        using [[unfold_abs_def = false]]
        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 less_eq_fset.rep_eq)[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 fmadd_assoc)
        apply (unfold make_fmap_union)
        apply (auto simp add: fdom_make_fmap e_in_E)[1]
        apply simp
        apply (unfold fmadd_assoc)
        apply (unfold make_fmap_union)
        apply (metis (lifting) funion_absorb2 vs_def vs_in_S)
        apply (intro arg_cong2[of _ _ "[ S - fst3 e |=> Bot ]"
            "[ S - fst3 e |=> Bot ]" "(++⇩f)"])
        apply (intro arg_cong2[of _ _ "Top" "Top" "make_fmap"])
        defer 1
        apply (simp, simp)
        apply (fold fset_cong)
        apply (unfold less_eq_fset.rep_eq, 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 (insert e_in_E lin(2))[1]
        apply (subst (asm) (2) fset_cong[symmetric])
        apply (elim conjE)
        apply (subst (asm) inter_fset)
        apply (subst (asm) fset_simps)
        apply (insert disjoint_iff_not_equal)[1]
        apply blast
        apply (metis G_def Suc(3) e_in_E subsetD less_eq_fset.rep_eq wf_dia_inv')
        prefer 2
        apply (metis (lifting) IntI Suc(2) ‹ws |∩| initials G = {||}›
            empty_iff fset_simps(1) in_mono inter_fset less_eq_fset.rep_eq ws_def)
        apply auto
        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))
by (auto simp add: assms(1) ps_chains_is_ps_chains2_with_empty_S fcard_fempty)


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 σ ≡
    ⨂v |∈| fmdom σ. case_topbot 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) ((case_sum (Inl ∘ G^Λ) (Inr ∘ snd3))) Π"

lemma ps_chain_to_int_chain_simp:
  "ps_chain_to_int_chain (Graph V Λ E) Π =
    chainmap (ps_to_int (Graph V Λ E)) ((case_sum (Inl ∘ Λ) (Inr ∘ 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 (⨂v|∈|fst3 e. bot_ass (Λ v)),c,asn (⨂v|∈|thd3 e. top_ass (Λ v)))"
    hence prov_edge: "⋀e c P Q F. ⟦ e ∈ set E ; coms_com (snd3 e) c ;
      P = ((⨂v|∈|fst3 e. bot_ass (Λ v)) ⊗ F) ;
      Q = ((⨂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 π.
      case_sum (coms_ass ∘ Λ) (coms_com ∘ snd3) (π ! i) (cs ! i)"
    hence π_cs: "⋀i. i < length π ⟹
      case_sum (coms_ass ∘ Λ) (coms_com ∘ snd3) (π ! i) (cs ! i)" by auto
    assume G_def: "G = Graph V Λ E"
    assume c_def: "c = foldr (;;) cs Skip"
    assume π_lin: "π ∈ lins (Graph V Λ E)"

    note lins = linsD[OF π_lin]

    define Π where "Π = mk_ps_chain ⦃ initial_ps G ⦄ π"

    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 (⨂v|∈|initials (Graph V Λ E). top_ass (Λ v)),
      foldr (;;) cs Skip, asn (⨂v|∈|terminals (Graph V Λ E). bot_ass (Λ v)))"
    using [[unfold_abs_def = false]]
    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) =
      case_topbot 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) =
      case_topbot 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 |∉| fmdom σ" and
          fst_Πi: "fst3 (nthtriple Π i) = [ {|v|} |=> Top ] ++⇩f σ" and
          thd_Πi: "thd3 (nthtriple Π i) = [ {|v|} |=> Bot ] ++⇩f σ" 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 fmdom_add fdom_make_fmap)
        apply (unfold finsert_is_funion[symmetric])
        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 (fmdom σ). case_topbot top_ass bot_ass
          (lookup ([ {|v|} |=> Top ] ++⇩f σ) va) (Λ va) =
          case_topbot top_ass bot_ass (lookup ([{|v|} |=> Bot] ++⇩f σ) va)(Λ va)")
        apply (unfold iter_hcomp_cong, simp)
        apply (metis 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 |∩| fmdom σ = {||}" and
          thd_e_disjoint_σ: "thd3 e |∩| fmdom σ = {||}" and
          fst_Πi: "fst3 (nthtriple Π i) = [ fst3 e |=> Bot ] ++⇩f σ" and
          thd_Πi: "thd3 (nthtriple Π i) = [ thd3 e |=> Top ] ++⇩f σ"
        by (auto simp add: inf_sup_distrib2)


        let ?F = "⨂v|∈|fmdom σ.
          case_topbot top_ass bot_ass (lookup ([ fst3 e |=> Bot ] ++⇩f σ) v) (Λ v)"

        show "prov_triple (asn (ps_to_int G (fst3 (nthtriple Π i))),
                   cs ! i, asn (ps_to_int G (thd3 (nthtriple Π i))))"
        proof (intro prov_edge[where e=e])
          show "e ∈ set E"
            apply (subgoal_tac "Inr e ∈ set π")
             apply (metis Inr_not_Inl PlusE edges.simps lins(2) sum.simps(2))
            by (metis Inr ‹i < length π› nth_mem)
        next
          show "coms_com (snd3 e) (cs ! i)"
            by (metis (no_types) Inr ‹i < length π› π_cs o_def sum.simps(6))
        next
          show "ps_to_int G (fst3 (nthtriple Π i)) = ((⨂v|∈|fst3 e. bot_ass (Λ v)) ⊗ ?F)"
            unfolding fst_Πi ps_to_int_def G_def labelling.simps fmdom_add fdom_make_fmap
            apply (insert fst_e_disjoint_σ)
            apply (unfold iter_hcomp_union)
            apply (subgoal_tac "∀v ∈ fset (fst3 e). case_topbot top_ass bot_ass
          (lookup ([ fst3 e |=> Bot ] ++⇩f σ) v) (Λ v) = bot_ass (Λ v)")
             apply (unfold iter_hcomp_cong)
             apply (simp)
            apply (intro ballI)
            apply (subgoal_tac "v |∉| fmdom σ")
             apply (unfold lookup_union2)
             apply (metis lookup_make_fmap topbot.simps(4))
            by (metis fempty_iff finterI)
        next
          show "ps_to_int G (thd3 (nthtriple Π i)) = ((⨂v|∈|thd3 e. top_ass (Λ v)) ⊗ ?F)"
            unfolding thd_Πi ps_to_int_def G_def labelling.simps fmdom_add fdom_make_fmap
            apply (insert thd_e_disjoint_σ)
            apply (unfold iter_hcomp_union)
            apply (subgoal_tac "∀v ∈ fset (thd3 e). case_topbot top_ass bot_ass
          (lookup ([ thd3 e |=> Top ] ++⇩f σ) v) (Λ v) = top_ass (Λ v)")
             apply (unfold iter_hcomp_cong)
             apply (subgoal_tac "∀v ∈ fset (fmdom σ). case_topbot top_ass bot_ass
          (lookup ([ thd3 e |=> Top ] ++⇩f σ) v) (Λ v) =
          case_topbot top_ass bot_ass (lookup ([fst3 e |=> Bot] ++⇩f σ) v) (Λ v)")
              apply (unfold iter_hcomp_cong)
              apply simp
            subgoal
              by (simp add: lookup_union1)
            subgoal
              by (simp add: fdisjoint_iff lookup_union2 lookup_make_fmap)
            done
        qed
      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