# 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_Mapbegintext {* 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 | Bottype_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)  doneqedtext {* 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)  doneqedtext {* 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+donelemma 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+donetext {* 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)donetext {* 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 autodonetext {* 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_defby (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_defby (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 transferapply (auto simp add: make_map_def map_diff_def map_add_def restrict_map_def)donelemma 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]  doneqedlemma 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  qedqedlemma 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  qedqedtext {* 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)  donenext  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  qedqedcorollary 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)donesubsection {* 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)  donenext  case (Exists G P Q x)  thus ?case  apply (intro allI impI, elim conjE coms_exists_inv)  apply (auto simp add: prov_triple.exists)  donenext  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)  donenext  case (Loop G P)  thus ?case  apply (intro allI impI, elim conjE coms_loop_inv)  apply (auto simp add: prov_triple.loop)  donenext  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  qedqedtext {* 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 autoend`