# Theory Ribbons_Graphical

Up to index of Isabelle/HOL/ribbonproofs

theory Ribbons_Graphical
imports Ribbons_Interfaces
`header {* Syntax and proof rules for graphical diagrams *}theory Ribbons_Graphical imports   Ribbons_Interfacesbegintext {* We introduce a graphical syntax for diagrams, describe how to extract   commands and interfaces, and give proof rules for graphical diagrams. *}subsection {* Syntax of graphical diagrams *}text {* Fix a type for node identifiers *}typedecl nodetext {* Note that this datatype is necessarily an overapproximation of   syntactically-wellformed diagrams, for the reason that we can't impose the   well-formedness constraints while maintaining admissibility of the datatype   declarations. So, we shall impose well-formedness in a separate definition.   *}datatype assertion_gadget =  Rib "assertion"| Exists_dia "string" "diagram"and command_gadget =   Com "command"| Choose_dia "diagram" "diagram"| Loop_dia "diagram"and diagram = Graph   "node fset"   "node => assertion_gadget"   "(node fset × command_gadget × node fset) list"type_synonym labelling = "node => assertion_gadget"type_synonym edge = "node fset × command_gadget × node fset"text {* Projecting components from a graph *}fun vertices :: "diagram => node fset" ("_^V" [1000] 1000)where "(Graph V Λ E)^V = V"term "this (is^V) = (a test)^V"fun labelling :: "diagram => labelling" ("_^Λ" [1000] 1000)where "(Graph V Λ E)^Λ = Λ"fun edges :: "diagram => edge list" ("_^E" [1000] 1000)where "(Graph V Λ E)^E = E"subsection {* Well formedness of graphical diagrams *}definition acyclicity :: "edge list => bool"where  "acyclicity E ≡ acyclic (\<Union>e ∈ set E. fset (fst3 e) × fset (thd3 e))"definition linearity :: "edge list => bool"where  "linearity E ≡     distinct E ∧ (∀e ∈ set E. ∀f ∈ set E. e ≠ f -->     fst3 e |∩| fst3 f = {||} ∧    thd3 e |∩| thd3 f = {||})"lemma linearityD:  assumes "linearity E"  shows "distinct E"  and "!!e f. [| e ∈ set E ; f ∈ set E ; e ≠ f |] ==>     fst3 e |∩| fst3 f = {||} ∧    thd3 e |∩| thd3 f = {||}"using assms unfolding linearity_def by autolemma linearityD2:  "linearity E ==> (∀e f. e ∈ set E ∧ f ∈ set E ∧ e ≠ f -->     fst3 e |∩| fst3 f = {||} ∧    thd3 e |∩| thd3 f = {||})"using assms unfolding linearity_def by autoinductive  wf_ass :: "assertion_gadget => bool" and  wf_com :: "command_gadget => bool" and  wf_dia :: "diagram => bool"where  wf_rib: "wf_ass (Rib p)" | wf_exists: "wf_dia G ==> wf_ass (Exists_dia x G)"| wf_com: "wf_com (Com c)"| wf_choice: "[| wf_dia G ; wf_dia H |] ==> wf_com (Choose_dia G H)"| wf_loop: "wf_dia G ==> wf_com (Loop_dia G)"| wf_dia: "[| ∀e ∈ set E. wf_com (snd3 e) ; ∀v ∈ fset V. wf_ass (Λ v) ;  acyclicity E ; linearity E ; ∀e ∈ set E. fst3 e |∪| thd3 e |⊆| V |] ==>   wf_dia (Graph V Λ E)"inductive_cases wf_dia_inv': "wf_dia (Graph V Λ E)"lemma wf_dia_inv:    assumes "wf_dia (Graph V Λ E)"  shows "∀v ∈ fset V. wf_ass (Λ v)"     and "∀e ∈ set E. wf_com (snd3 e)"     and "acyclicity E"     and "linearity E"     and "∀e ∈ set E. fst3 e |∪| thd3 e |⊆| V"using assmsapply -  (* This acts as an intro rule for &&& *)apply (elim wf_dia_inv', simp)+donesubsection {* Initial and terminal nodes *}definition  initials :: "diagram => node fset"where  "initials G = filter_fset (λv. (∀e ∈ set G^E. v |∉| thd3 e)) G^V"definition   terminals :: "diagram => node fset"where  "terminals G = filter_fset (λv. (∀e ∈ set G^E. v |∉| fst3 e)) G^V"lemma no_edges_imp_all_nodes_initial:  "initials (Graph V Λ []) = V"by (auto simp add: initials_def, descending, auto)lemma no_edges_imp_all_nodes_terminal:  "terminals (Graph V Λ []) = V"by (auto simp add: terminals_def, descending, auto)lemma initials_in_vertices:   "initials G |⊆| G^V"by (unfold initials_def, rule filter_subset)lemma terminals_in_vertices:   "terminals G |⊆| G^V"by (unfold terminals_def, rule filter_subset)subsection {* Top and bottom interfaces *}primrec  top_ass :: "assertion_gadget => interface" and  top_dia :: "diagram => interface"where  "top_dia (Graph V Λ E) = (\<Otimes>v |∈| initials (Graph V Λ E). top_ass (Λ v))"| "top_ass (Rib p) = Ribbon p"| "top_ass (Exists_dia x G) = Exists_int x (top_dia G)"primrec  bot_ass :: "assertion_gadget => interface" and  bot_dia :: "diagram => interface"where  "bot_dia (Graph V Λ E) = (\<Otimes>v |∈| terminals (Graph V Λ E). bot_ass (Λ v))"| "bot_ass (Rib p) = Ribbon p"| "bot_ass (Exists_dia x G) = Exists_int x (bot_dia G)"subsection {* Proof rules for graphical diagrams *}inductive  prov_dia :: "[diagram, interface, interface] => bool" and  prov_com :: "[command_gadget, interface, interface] => bool" and  prov_ass :: "assertion_gadget => bool"where  Skip: "prov_ass (Rib p)"| Exists: "prov_dia G _ _ ==> prov_ass (Exists_dia x G)"| Basic: "prov_triple (asn P, c, asn Q) ==> prov_com (Com c) P Q"| Choice: "[| prov_dia G P Q ; prov_dia H P Q |]     ==> prov_com (Choose_dia G H) P Q"| Loop: "prov_dia G P P ==> prov_com (Loop_dia G) P P"| Main: "[| wf_dia G ; !!v. v ∈ fset G^V ==> prov_ass (G^Λ v);    !!e. e ∈ set G^E ==> prov_com (snd3 e)       (\<Otimes>v |∈| fst3 e. bot_ass (G^Λ v))      (\<Otimes>v |∈| thd3 e. top_ass (G^Λ v))|]     ==> prov_dia G (top_dia G) (bot_dia G)"inductive_cases main_inv: "prov_dia (Graph V Λ E) P Q"inductive_cases loop_inv: "prov_com (Loop_dia G) P Q"inductive_cases choice_inv: "prov_com (Choose_dia G H) P Q"inductive_cases basic_inv: "prov_com (Com c) P Q"inductive_cases exists_inv: "prov_ass (Exists_dia x G)"inductive_cases skip_inv: "prov_ass (Rib p)"subsection {* Extracting commands from diagrams *}type_synonym lin = "(node + edge) list"text {* A linear extension (lin) of a diagram is a list of its nodes and edges  which respects the order of those nodes and edges. That is, if an edge  @{term e} goes from node @{term v} to node @{term w}, then @{term v} and   @{term e} and @{term w} must have strictly increasing positions in the list.   *}definition lins :: "diagram => lin set"where"lins G ≡ {π :: lin.     (distinct π)   ∧ (set π = (fset G^V) <+> (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 linsD:  assumes "π ∈ lins G"  shows "(distinct π)"     and "(set π = (fset G^V) <+> (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)"using assmsapply -apply (unfold lins_def Collect_iff)apply (elim conjE, assumption)+donetext {* The following lemma enables the inductive definition below to be  proved monotonic. It does this by showing how one of the premises of the  @{term coms_main} rule can be rewritten in a form that is more verbose but   easier to prove monotonic. *}lemma coms_mono_helper:  "(∀i<length π. sum_case (coms_ass o Λ) (coms_com o snd3) (π!i) (cs!i))   =   ((∀i. i<length π ∧ (∃v. (π!i) = Inl v) -->     coms_ass (Λ (Sum_Type.Projl (π!i))) (cs!i)) ∧  (∀i. i<length π ∧ (∃e. (π!i) = Inr e) -->     coms_com (snd3 (Sum_Type.Projr (π!i))) (cs!i)))"by (smt Projl.simps Projr.simps o_apply o_def   sum.exhaust sum.simps(5) sum.simps(6) sumE)text {* The @{term coms_dia} function extracts a set of commands from a   diagram. Each command in @{term "coms_dia G"} is obtained by extracting a   command from each of @{term G}'s nodes and edges (using @{term coms_ass} or   @{term coms_com} respectively), then picking a linear extension @{term π} of   these nodes and edges (using @{term lins}), and composing the extracted   commands in accordance with @{term π}.*}inductive  coms_dia :: "[diagram, command] => bool" and  coms_ass :: "[assertion_gadget, command] => bool" and  coms_com :: "[command_gadget, command] => bool"where  coms_skip: "coms_ass (Rib p) Skip"| coms_exists: "coms_dia G c ==> coms_ass (Exists_dia x G) c"| coms_basic: "coms_com (Com c) c"| coms_choice: "[| coms_dia G c; coms_dia H d |] ==>     coms_com (Choose_dia G H) (Choose c d)"| coms_loop: "coms_dia G c ==> coms_com (Loop_dia G) (Loop c)"| coms_main: "[| π ∈ lins (Graph V Λ E); length cs = length π;    ∀i<length π. sum_case (coms_ass o Λ) (coms_com o snd3) (π!i) (cs!i) |]     ==> coms_dia (Graph V Λ E) (foldr (op ;;) cs Skip)"monos   coms_mono_helperinductive_cases coms_skip_inv: "coms_ass (Rib p) c"inductive_cases coms_exists_inv: "coms_ass (Exists_dia x G) c"inductive_cases coms_basic_inv: "coms_com (Com c') c"inductive_cases coms_choice_inv: "coms_com (Choose_dia G H) c"inductive_cases coms_loop_inv: "coms_com (Loop_dia G) c"inductive_cases coms_main_inv: "coms_dia G c"end`