Theory Ribbons_Graphical

section ‹Syntax and proof rules for graphical diagrams›

theory Ribbons_Graphical imports 
  Ribbons_Interfaces
begin

text ‹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 node

text ‹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 (⋃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 auto

lemma linearityD2:
  "linearity E ⟹ (∀e f. e ∈ set E ∧ f ∈ set E ∧ e ≠ f ⟶ 
    fst3 e |∩| fst3 f = {||} ∧
    thd3 e |∩| thd3 f = {||})"
unfolding linearity_def by auto

inductive
  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 assms
apply -  (* This acts as an intro rule for &&& *)
apply (elim wf_dia_inv', simp)+
done

subsection ‹Initial and terminal nodes›

definition
  initials :: "diagram ⇒ node fset"
where
  "initials G = ffilter (λv. (∀e ∈ set G^E. v |∉| thd3 e)) G^V"

definition
   terminals :: "diagram ⇒ node fset"
where
  "terminals G = ffilter (λ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)

lemma no_edges_imp_all_nodes_terminal:
  "terminals (Graph V Λ []) = V"
by (auto simp add: terminals_def)

lemma initials_in_vertices:
   "initials G |⊆| G^V"
unfolding initials_def by auto

lemma terminals_in_vertices:
   "terminals G |⊆| G^V"
unfolding terminals_def by auto

subsection ‹Top and bottom interfaces›

primrec
  top_ass :: "assertion_gadget ⇒ interface" and
  top_dia :: "diagram ⇒ interface"
where
  "top_dia (Graph V Λ E) = (⨂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) = (⨂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) 
      (⨂v |∈| fst3 e. bot_ass (G^Λ v))
      (⨂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 assms
apply -
apply (unfold lins_def Collect_iff)
apply (elim conjE, assumption)+
done

text ‹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 π. case_sum (coms_ass ∘ Λ) (coms_com ∘ snd3) (π!i) (cs!i)) 
  = 
  ((∀i. i<length π ∧ (∃v. (π!i) = Inl v) ⟶ 
    coms_ass (Λ (projl (π!i))) (cs!i)) ∧
  (∀i. i<length π ∧ (∃e. (π!i) = Inr e) ⟶ 
    coms_com (snd3 (projr (π!i))) (cs!i)))"
apply (intro iffI)
apply auto[1]
apply (intro allI impI, case_tac "π!i", auto)
done
    
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 π. case_sum (coms_ass ∘ Λ) (coms_com ∘ snd3) (π!i) (cs!i) ⟧ 
    ⟹ coms_dia (Graph V Λ E) (foldr (;;) cs Skip)"
monos 
  coms_mono_helper

inductive_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