theory Ribbons_Graphical imports
Ribbons_Basic
begin
text {* We introduce several concepts that are required for the soundness and completeness results (proved in ribbons_rast.thy, ribbons_completeness.thy and ribbons_soundness.thy). We introduce interfaces, the graphical syntax of diagrams, and how to extract commands and interfaces from diagrams. *}
subsection {* Syntax and semantics of interfaces *}
text {* An interface is obtained by extracting a single row from a diagram. *}
datatype interface =
Ribbon "assertion"
| HComp_int "interface" "interface" (infixr "\" 50)
| Emp_int
| Exists_int "string" "interface"
text {* An equivalence on interfaces. The first three rules make this an equivalence relation. The next three make it a congruence. The next two identify interfaces up to associativity and commutativity of HComp_int. The final two make Emp_int the left and right unit of HComp_int. *}
inductive
equiv_int :: "interface \ interface \ bool"
where
refl: "equiv_int P P"
| sym: "equiv_int P Q \ equiv_int Q P"
| trans: "\equiv_int P Q; equiv_int Q R\ \ equiv_int P R"
| cong_hcomp1: "equiv_int P Q \ equiv_int (P' \ P) (P' \ Q)"
| cong_hcomp2: "equiv_int P Q \ equiv_int (P \ P') (Q \ P')"
| cong_exists: "equiv_int P Q \ equiv_int (Exists_int x P) (Exists_int x Q)"
| hcomp_assoc: "equiv_int (P \ (Q \ R)) ((P \ Q) \ R)"
| hcomp_comm: "equiv_int (P \ Q) (Q \ P)"
| hcomp_unit1: "equiv_int (Emp_int \ P) P"
| hcomp_unit2: "equiv_int (P \ Emp_int) P"
text {* The semantics of an interface is an assertion. *}
primrec
ass :: "interface \ assertion"
where
"ass (Ribbon p) = p"
| "ass (P \ Q) = (ass P) \ (ass Q)"
| "ass (Emp_int) = Emp"
| "ass (Exists_int x P) = Exists x (ass P)"
text {* The equivalence on interfaces is sound for this semantics. *}
lemma equiv_int_sound:
"equiv_int P1 P2 \ ass P1 = ass P2"
proof -
fix P1 P2
assume "equiv_int P1 P2"
thus "ass P1 = ass P2"
proof (induct rule:equiv_int.induct)
case (hcomp_assoc P Q R)
thus ?case by (auto simp add: star_assoc)
next
case (hcomp_comm P Q)
thus ?case by (auto simp add: star_comm)
next
case (hcomp_unit1 P)
thus ?case by (auto simp add: emp_star)
next
case (hcomp_unit2 P)
thus ?case by (auto simp add: star_emp)
qed auto
qed
text {* Program variables mentioned in an interface. *}
primrec
rd_int :: "interface \ string set"
where
"rd_int (Ribbon p) = rd_ass p"
| "rd_int (P \ Q) = rd_int P \ rd_int Q"
| "rd_int (Emp_int) = {}"
| "rd_int (Exists_int x P) = rd_int P"
text {* The program variables read by an interface are the same as those read by its corresponding assertion. (In fact, this lemma would suffice as a definition of rd_int.) *}
lemma rd_int_is_rd_ass:
"rd_ass (ass P) = rd_int P"
by (induct P, auto simp add: rd_star rd_exists rd_emp)
subsection {* Syntax, provability and semantics of diagrams *}
subsubsection {* Some general purpose lemmas *}
lemma nth_in_set:
"\ i < length xs ; xs ! i = x \ \ x \ set xs" by auto
lemma exI3: "P a b c \ \a b c. P a b c" by auto
text {* Fix a type for node identifiers. Pick v01 and v02 as distinct nodes. *}
typedecl node
axiomatization
v01 :: node and v02 :: node
where
v01_neq_v02 [simp]: "v01 \ v02" and
v02_neq_v01 [simp]: "v02 \ v01"
text {* Syntax of diagrams *}
datatype assnode =
Rib "assertion"
| Exists_dia "string" "diagram"
and comnode =
Com "command"
| Choose_dia "diagram" "diagram"
| Loop_dia "diagram"
and diagram =
Graph "node list" "node \ assnode" "(node list \ comnode \ node list) list"
type_synonym labelling = "node \ assnode"
type_synonym edge = "node list \ comnode \ node list"
subsubsection {* Projection functions on triples *}
definition fst3 :: "'a \ 'b \ 'c \ 'a"
where "fst3 \ fst"
definition snd3 :: "'a \ 'b \ 'c \ 'b"
where "snd3 \ fst \ snd"
definition thd3 :: "'a \ 'b \ 'c \ 'c"
where "thd3 \ snd \ snd"
lemma fst3_comp:
"\f g h T. fst3 ((\(x,y,z). (f x, g y, h z)) T) = f (fst3 T)"
unfolding fst3_def by auto
lemma snd3_comp:
"\f g h T. snd3 ((\(x,y,z). (f x, g y, h z)) T) = g (snd3 T)"
unfolding snd3_def by auto
lemma thd3_comp:
"\f g h T. thd3 ((\(x,y,z). (f x, g y, h z)) T) = h (thd3 T)"
unfolding thd3_def by auto
lemma fst3_simp: "\a b c. fst3 (a,b,c) = a" unfolding fst3_def by auto
lemma snd3_simp: "\a b c. snd3 (a,b,c) = b" unfolding snd3_def by auto
lemma thd3_simp: "\a b c. thd3 (a,b,c) = c" unfolding thd3_def by auto
lemma tripleI:
fixes T U
assumes "fst3 T = fst3 U" and
"snd3 T = snd3 U" and
"thd3 T = thd3 U"
shows "T = U"
using assms
unfolding fst3_def snd3_def thd3_def
by (metis o_def surjective_pairing)
subsubsection {* Well formedness of graphs *}
definition acyclicity :: "edge list \ bool"
where
"acyclicity E \ acyclic (\e \ set E. \v \ set (fst3 e). \w \ set (thd3 e). {(v,w)})"
definition linearity :: "edge list \ bool"
where
"linearity E \
distinct E \ (\e \ set E. \f \ set E. e \ f \
set (fst3 e) \ set (fst3 f) = {} \
set (thd3 e) \ set (thd3 f) = {})"
inductive
wf_ass :: "assnode \ bool" and
wf_com :: "comnode \ 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_basic: "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: "\ distinct V; acyclicity E; linearity E;
\e. e \ set E \ distinct (fst3 e) \ set (fst3 e) \ set V ;
\e. e \ set E \ distinct (thd3 e) \ set (thd3 e) \ set V \
\ wf_dia (Graph V \ E)"
inductive_cases wf_dia_inv': "wf_dia (Graph V \ E)"
lemma wf_dia_inv:
fixes V \ E
assumes "wf_dia (Graph V \ E)"
shows "distinct V" and "acyclicity E" and "linearity E"
and "\e. e \ set E \ distinct (fst3 e) \ set (fst3 e) \ set V"
and "\e. e \ set E \ distinct (thd3 e) \ set (thd3 e) \ set V"
proof -
show "distinct V" using wf_dia_inv'[OF assms] by blast
next
show "acyclicity E" using wf_dia_inv'[OF assms] by blast
next
show "linearity E" using wf_dia_inv'[OF assms] by blast
next
show "\e. e \ set E \ distinct (fst3 e) \ set (fst3 e) \ set V"
using wf_dia_inv'[OF assms] unfolding fst3_def by blast
next
show "\e. e \ set E \ distinct (thd3 e) \ set (thd3 e) \ set V"
using wf_dia_inv'[OF assms] unfolding thd3_def comp_def by blast
qed
subsubsection {* Initial and terminal nodes *}
fun
initials :: "diagram \ node list"
where
"initials (Graph V _ E) = [v \ V. v \ set (concat (map thd3 E))]"
fun
terminals :: "diagram \ node list"
where
"terminals (Graph V _ E) = [v \ V. v \ set (concat (map fst3 E))]"
lemma no_edges_imp_all_nodes_initial:
"initials (Graph V \ []) = V"
by auto
lemma no_edges_imp_all_nodes_terminal:
"terminals (Graph V \ []) = V"
by auto
subsubsection {* Top and bottom interfaces *}
primrec
top_dia :: "diagram \ interface" and
top_ass :: "assnode \ interface"
where
"top_dia (Graph V \ E) = foldl (op \) Emp_int [ top_ass (\ v) . v \ initials (Graph V \ E) ]"
| "top_ass (Rib p) = Ribbon p"
| "top_ass (Exists_dia x G) = Exists_int x (top_dia G)"
primrec
bot_dia :: "diagram \ interface" and
bot_ass :: "assnode \ interface"
where
"bot_dia (Graph V \ E) = foldl (op \) Emp_int [ bot_ass (\ v) . v \ terminals (Graph V \ E) ]"
| "bot_ass (Rib p) = Ribbon p"
| "bot_ass (Exists_dia x G) = Exists_int x (bot_dia G)"
subsubsection {* Provability of diagrams *}
inductive
prov_dia :: "[diagram, interface, interface] \ bool" and
prov_com :: "[comnode, interface, interface] \ bool" and
prov_ass :: "assnode \ bool"
where
Skip: "prov_ass (Rib p)"
| Exists: "prov_dia G _ _ \ prov_ass (Exists_dia x G)"
| Basic: "prov_triple (ass P, c, ass 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: "\\v. v \ set V \ prov_ass (\ v) ;
\e. e \ set E \ prov_com (snd3 e)
(foldl (op \) Emp_int [bot_ass (\ v) . v \ fst3 e])
(foldl (op \) Emp_int [top_ass (\ v) . v \ thd3 e]) ;
wf_dia (Graph V \ E) \ \
prov_dia (Graph V \ E) (top_dia (Graph V \ E)) (bot_dia (Graph V \ E))"
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)"
subsubsection {* Extracting commands from diagrams *}
fun lins :: "diagram \ ((node + edge) list) set"
where
"lins (Graph V \ E) = {\ . (distinct \) \ (set \ = ((Inl ` (set V)) \ (Inr ` (set E)))) \ (\i j v e. i < length \ \ j < length \ \ \!i = Inl v \ \!j = Inr e \ v \ set (fst3 e) \ i (\j k w e. j < length \ \ k < length \ \ \!j = Inr e \ \!k = Inl w \ w \ set (thd3 e) \ j defn.
And the corresponding defn cannot be
proved to terminate. So we use the
defn that follows.
primrec
coms_dia :: "diagram \ command set" and
coms_ass :: "assnode \ command set" and
coms_com :: "comnode \ command set"
where
"coms_ass (Rib p) = {Skip}"
| "coms_ass (Exists_dia x G) = coms_dia G"
| "coms_com (Com c) = {c}"
| "coms_com (Choose_dia G H) = {Choose c d | c d .
c \ coms_dia G \ d \ coms_dia H}"
| "coms_com (Loop_dia G) = {Loop c | c . c \ coms_dia G}"
| "coms_dia (Graph V \ E) = { foldr (op ;;) cs Skip | cs .
\X \ lin (Graph V \ E) . \i (case (X!i) of
Inl A \ coms_ass A |
Inr C \ coms_com C) }"
*)
inductive
coms_dia :: "[diagram, command] \ bool" and
coms_ass :: "[assnode, command] \ bool" and
coms_com :: "[comnode, 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)"
(* In the following clause we would prefer to write...
\i. i \ (case (\!i) of
Inl v \ coms_ass (\ v) |
Inr e \ coms_com (snd3 e) ) (cs!i)
... or maybe even ...
\i. i \
(sum_case (coms_ass \ \) (coms_com \ snd3) (\!i)) (cs!i)
... but in either case, monotonicity fails. Need to help
via a lemma annotated as [mono].
*)
| coms_main: "\