Up to index of Isabelle/HOL/ribbonproofs

theory Ribbons_Graphicalimports 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