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_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 (\<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 auto

lemma 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 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 = 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 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 π. 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_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