We introduce several concepts that are required for the soundness and completeness results (proved in ribbons_rast, ribbons_completeness and ribbons_soundness). We introduce interfaces, the graphical syntax of diagrams, and how to extract commands and interfaces from diagrams.
Syntax and semantics of interfaces
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
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
equiv_int P P
equiv_int P Q
equiv_int Q P
equiv_int P Q; equiv_int Q R
equiv_int P R
equiv_int P Q
equiv_int (P' ⊗ P) (P' ⊗ Q)
equiv_int P Q
equiv_int (P ⊗ P') (Q ⊗ P')
equiv_int P Q
equiv_int (Exists_int x P) (Exists_int x Q)
equiv_int (P ⊗ (Q ⊗ R)) ((P ⊗ Q) ⊗ R)
equiv_int (P ⊗ Q) (Q ⊗ P)
equiv_int (Emp_int ⊗ P) P
equiv_int (P ⊗ Emp_int) P
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)
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
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
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)
Syntax, provability and semantics of diagrams
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
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
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
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)
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_ass (Rib p)
wf_dia G
wf_ass (Exists_dia x G)
wf_com (Com c)
wf_dia G; wf_dia H
wf_com (Choose_dia G H)
wf_dia G
wf_com (Loop_dia G)
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
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
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)
Provability of diagrams
inductive
prov_dia :: [diagram, interface, interface] ⇒ bool and
prov_com :: [comnode, interface, interface] ⇒ bool and
prov_ass :: assnode ⇒ bool
where
prov_ass (Rib p)
prov_dia G _ _
prov_ass (Exists_dia x G)
prov_triple (ass P, c, ass Q)
prov_com (Com c) P Q
prov_dia G P Q ; prov_dia H P Q
prov_com (Choose_dia G H) P Q
prov_dia G P P
prov_com (Loop_dia G) P P
⋀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)
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) ∧ (∀j k w e. j < length π ∧ k < length π ∧ π!j = Inr e ∧ π!k = Inl w ∧ w ∈ set (thd3 e) ⟶ j<k) }
inductive
coms_dia :: [diagram, command] ⇒ bool and
coms_ass :: [assnode, command] ⇒ bool and
coms_com :: [comnode, command] ⇒ bool
where
coms_ass (Rib p) Skip
coms_dia G c
coms_ass (Exists_dia x G) c
coms_com (Com c) c
coms_dia G c; coms_dia H d
coms_com (Choose_dia G H) (Choose c d)
coms_dia G c
coms_com (Loop_dia G) (Loop c)
| coms_main: ⟦ π ∈ lins (Graph V Λ E); length cs = length π;
⋀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) ⟧ ⟹
coms_dia (Graph V Λ E) (foldr (op ;;) cs Skip)
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
lemma coms_main_inv: fixes G c
assumes coms_dia G c
shows ∃V Λ E π cs.
(G = Graph V Λ E) ∧ (π ∈ lins (Graph V Λ E)) ∧
(length cs = length π) ∧
(∀i<length π. (∃v. (π!i) = Inl v) ⟶
coms_ass (Λ (Sum_Type.Projl (π!i))) (cs!i)) ∧
(∀i<length π. (∃e. (π!i) = Inr e) ⟶
coms_com (snd3 (Sum_Type.Projr (π!i))) (cs!i)) ∧
(c = foldr (op ;;) cs Skip)
proof -
have (coms_dia G c ⟶ (∃V Λ E π cs.
(G = Graph V Λ E) ∧ (π ∈ lins (Graph V Λ E)) ∧
(length cs = length π) ∧
(∀i<length π. (∃v. (π!i) = Inl v) ⟶
coms_ass (Λ (Sum_Type.Projl (π!i))) (cs!i)) ∧
(∀i<length π. (∃e. (π!i) = Inr e) ⟶
coms_com (snd3 (Sum_Type.Projr (π!i))) (cs!i)) ∧
(c = foldr (op ;;) cs Skip)))
∧ (coms_ass A c ⟶ True) ∧ (coms_com C c ⟶ True)
proof (induct rule: coms_dia_coms_ass_coms_com.induct)
qed (simp, simp, simp, simp, simp, metis)
with assms show ?thesis by auto
qed
end
