theory Ribbons imports Main Interleave
begin
subsection {* Commands, assertions and separation logic rules *}
text {* Assertions, comprising (at least) an emp constant, a *-operator and existentially-quantified logical variables. *}
typedecl assertion
consts Emp :: "assertion"
axiomatization
Star :: "assertion \ assertion \ assertion"
where star_comm: "Star p q = Star q p"
and star_assoc: "Star (Star p q) r = Star p (Star q r)"
and star_emp: "Star p Emp = p"
and emp_star: "Star Emp p = p"
consts Exists :: "string \ assertion \ assertion"
text {* Set of program variables in an assertion. *}
axiomatization
rd_ass :: "assertion \ string set"
where rd_emp: "rd_ass Emp = {}"
and rd_star: "rd_ass (Star p q) = rd_ass p \ rd_ass q"
and rd_exists: "rd_ass (Exists x p) = rd_ass p"
text {* Commands, comprising (at least) non-deterministic choice, non-deterministic looping, skip and sequencing. *}
typedecl command
consts Choose :: "command \ command \ command"
consts Loop :: "command \ command"
consts Skip :: "command"
axiomatization
Seq :: "command \ command \ command"
where seq_assoc: "Seq c1 (Seq c2 c3) = (Seq (Seq c1 c2) c3)"
and seq_skip: "Seq c Skip = c"
and skip_seq: "Seq Skip c = c"
text {* Program variables read by a command. *}
axiomatization
rd_com :: "command \ string set"
where rd_com_choose: "rd_com (Choose c1 c2) = rd_com c1 \ rd_com c2"
and rd_com_loop: "rd_com (Loop c) = rd_com c"
and rd_com_skip: "rd_com (Skip) = {}"
and rd_com_seq: "rd_com (Seq c1 c2) = rd_com c1 \ rd_com c2"
text {* Program variables written by a command. *}
axiomatization
wr_com :: "command \ string set"
where wr_com_choose: "wr_com (Choose c1 c2) = wr_com c1 \ wr_com c2"
and wr_com_loop: "wr_com (Loop c) = wr_com c"
and wr_com_skip: "wr_com (Skip) = {}"
and wr_com_seq: "wr_com (Seq c1 c2) = wr_com c1 \ wr_com c2"
text {* Separation logic rules for proving Hoare triples. *}
inductive
prov_com :: "assertion \ command \ assertion \ bool"
where
exists:
"prov_com (p, c, q)
\ prov_com (Exists x p, c, Exists x q)"
| choose:
"\prov_com (p, c1, q);
prov_com (p, c2, q)\
\ prov_com (p, Choose c1 c2, q)"
| loop:
"prov_com (p, c, p)
\ prov_com (p, Loop c, p)"
| frame:
"\prov_com (p, c, q); wr_com(c) \ rd_ass(r) = {}\
\ prov_com (Star p r, c, Star q r)"
| skip:
"prov_com(p, Skip, p)"
| seq:
"\prov_com (p, c1, q); prov_com (q, c2, r)\
\ prov_com (p, Seq c1 c2, r)"
subsection {* Syntax and semantics of interfaces *}
text {* An interface is obtained by extracting a single row from a diagram. We are particularly interested in the interfaces at the top and bottom of a diagram, as it is through these interfaces that diagrams are vertically composed. *}
datatype interface =
Ribbon "assertion"
| HComp_int "interface" "interface"
| Emp_int
| Exists_int "string" "interface"
text {* Since HComp_int is associative, with Emp_int as its unit, we can canonicalise an interface as a list of faces. *}
datatype face =
Ribbon_fl "assertion"
| Exists_fl "string" "face list"
fun
int_to_fl :: "interface \ face list"
where
"int_to_fl (Ribbon p) = [Ribbon_fl p]"
| "int_to_fl (HComp_int P Q) = int_to_fl P @ int_to_fl Q"
| "int_to_fl (Emp_int) = []"
| "int_to_fl (Exists_int x P) = [Exists_fl x (int_to_fl P)]"
text {* Interfaces are equivalent if their canonicalisations are the same. *}
definition
equiv_int :: "interface \ interface \ bool"
where
"equiv_int P Q \ int_to_fl P = int_to_fl Q"
fun
ass_fl :: "face list \ assertion"
and
ass_face :: "face \ assertion"
where
"ass_face (Ribbon_fl p) = p"
| "ass_face (Exists_fl x F) = Exists x (ass_fl F)"
| "ass_fl F = foldr Star (map ass_face F) Emp"
text {* The semantics of an interface is an assertion. *}
primrec
ass :: "interface \ assertion"
where
"ass (Ribbon p) = p"
| "ass (HComp_int P Q) = Star(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 P
have "ass P = ass_fl (int_to_fl P)"
proof -
{ fix F F'
have "ass_fl (F @ F') = Star (ass_fl F) (ass_fl F')"
by (induct F, auto simp add: emp_star star_assoc)
}
thus ?thesis by (induct P, auto simp add: star_emp)
qed
}
thus ?thesis unfolding equiv_int_def by 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 (HComp_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 *}
datatype diagram =
Blank "interface"
| Basic "interface" "command" "interface"
| HComp_dia "diagram" "diagram"
| VComp_dia "diagram" "diagram"
| Exists_dia "string" "diagram"
| Choose_dia "interface" "diagram" "diagram" "interface"
| Loop_dia "interface" "diagram" "interface"
text {* Interface presented at the top of a diagram. *}
primrec
top :: "diagram \ interface"
where
"top (Blank P) = P"
| "top (Basic P c Q) = P"
| "top (HComp_dia A B) = HComp_int (top A) (top B)"
| "top (VComp_dia A B) = top A"
| "top (Exists_dia x A) = Exists_int x (top A)"
| "top (Choose_dia P A B Q) = P"
| "top (Loop_dia P A Q) = P"
text {* Interface presented at the bottom of a diagram. *}
primrec
bot :: "diagram \ interface"
where
"bot (Blank P) = P"
| "bot (Basic P c Q) = Q"
| "bot (HComp_dia A B) = HComp_int (bot A) (bot B)"
| "bot (VComp_dia A B) = bot B"
| "bot (Exists_dia x A) = Exists_int x (bot A)"
| "bot (Choose_dia P A B Q) = Q"
| "bot (Loop_dia P A Q) = Q"
text {* Program variables read by a diagram (either by being mentioned in an assertion or accessed by a command in the diagram). *}
primrec
rd_dia :: "diagram \ string set"
where
"rd_dia (Blank P) = rd_int P"
| "rd_dia (Basic P c Q) = rd_int P \ rd_com c \ rd_int Q"
| "rd_dia (HComp_dia A B) = rd_dia A \ rd_dia B"
| "rd_dia (VComp_dia A B) = rd_dia A \ rd_dia B"
| "rd_dia (Exists_dia x A) = rd_dia A"
| "rd_dia (Choose_dia P A B Q) = rd_int P \ rd_dia A \ rd_dia B \ rd_int Q"
| "rd_dia (Loop_dia P A Q) = rd_int P \ rd_dia A \ rd_int Q"
text {* Program variables written by a diagram (that is, written by a command in the diagram). *}
primrec
wr_dia :: "diagram \ string set"
where
"wr_dia (Blank P) = {}"
| "wr_dia (Basic P c Q) = wr_com c"
| "wr_dia (HComp_dia A B) = wr_dia A \ wr_dia B"
| "wr_dia (VComp_dia A B) = wr_dia A \ wr_dia B"
| "wr_dia (Exists_dia x A) = wr_dia A"
| "wr_dia (Choose_dia P A B Q) = wr_dia A \ wr_dia B"
| "wr_dia (Loop_dia P A Q) = wr_dia A"
text {* The set of commands that can be extracted from a diagram. The @{text \} operator returns the set of all interleavings of a given pair of lists. *}
fun
coms :: "diagram \ command set"
and
coms_list :: "diagram \ command list set"
where
"coms A = image (\C. foldr Seq C Skip) (coms_list A)"
| "coms_list (Blank P) = {[]}"
| "coms_list (Basic P c Q) = {[c]}"
| "coms_list (HComp_dia A B)
= \ {C1\C2 | C1 C2. C1 \ coms_list A \ C2 \ coms_list B}"
| "coms_list (VComp_dia A B)
= {C1@C2 | C1 C2. C1 \ coms_list A \ C2 \ coms_list B}"
| "coms_list (Exists_dia x A) = coms_list A"
| "coms_list (Choose_dia P A B Q)
= image (\(c1,c2). [Choose c1 c2]) (coms A \ coms B)"
| "coms_list (Loop_dia P A Q)
= image (\c. [Loop c]) (coms A)"
text {* Two diagrams are 'disjoint' if neither writes a program variable that is read by the other. *}
definition disj_dia :: "diagram \ diagram \ bool"
where
"disj_dia A B \ rd_dia A \ wr_dia B = {} \ rd_dia B \ wr_dia A = {}"
text {* Provability of a diagram. Note that this relation could be defined recursively rather than inductively, as the rules given here are syntax-directed. However, we shall stick with the traditional presentation of a provability relation. *}
inductive
prov_dia :: "diagram \ bool"
where
Blank:
"prov_dia (Blank P)"
| Basic:
"prov_com (ass P, c, ass Q) \ prov_dia (Basic P c Q)"
| Exists:
"prov_dia A \ prov_dia (Exists_dia x A)"
| HComp:
"\prov_dia A; prov_dia B; disj_dia A B\
\ prov_dia (HComp_dia A B)"
| VComp:
"\prov_dia A; prov_dia B; equiv_int (bot A) (top B)\ \ prov_dia (VComp_dia A B)"
| Choose:
"\prov_dia A; prov_dia B; equiv_int (top A) P;
equiv_int (top B) P; equiv_int (bot A) Q; equiv_int (bot B) Q\
\ prov_dia (Choose_dia P A B Q)"
| Loop:
"\prov_dia A; equiv_int (top A) P;
equiv_int (bot A) P; equiv_int Q P\
\ prov_dia (Loop_dia P A Q)"
inductive_cases prov_dia_hcomp_inv: "prov_dia (HComp_dia A B)"
inductive_cases prov_dia_vcomp_inv: "prov_dia (VComp_dia A B)"
inductive_cases prov_dia_exists_inv: "prov_dia (Exists_dia x A)"
inductive_cases prov_dia_choose_inv: "prov_dia (Choose_dia P A B Q)"
inductive_cases prov_dia_loop_inv: "prov_dia (Loop_dia P A Q)"
text {* The semantics of a diagram is a set of Hoare triples. *}
definition
sem_dia :: "diagram \ (assertion * command * assertion) set"
where
"sem_dia A \ {(p,c,q) | p c q. p = ass(top A) \ c \ coms A \ q = ass(bot A)}"
subsection {* Proof chains *}
text {* To enable the proof of soundness, we introduce proof chains. A proof chain is a sequence of alternating assertions and commands, beginning and ending with an assertion. *}
datatype chain =
cNil "assertion"
| cCons "assertion" "command" "chain"
text {* An induction principle for pairs of chains. Think of it as induction over pairs of natural numbers: if @{text \} holds on all pairs (x,0) and (0,y), and whenever it holds of (x,y+1) and (x+1,y) then it holds of (x+1,y+1), then it must hold of all (x,y). *}
lemma chainpair_induction [case_names NC CN CC]:
assumes "\p1 G2. \ (cNil p1) G2"
assumes "\p2 G1. \ G1 (cNil p2)"
assumes "\p1 p2 c1 c2 G1 G2.
\\ G1 (cCons p2 c2 G2); \ (cCons p1 c1 G1) G2\
\ \ (cCons p1 c1 G1) (cCons p2 c2 G2)"
shows "\ G1 G2"
using assms
by induction_schema (pat_completeness, lexicographic_order)
text {* Project first assertion. *}
fun
pre :: "chain \ assertion"
where
"pre(cNil p) = p"
| "pre(cCons p c G) = p"
text {* Project final assertion. *}
fun
post :: "chain \ assertion"
where
"post(cNil p) = p"
| "post(cCons p c G) = post G"
text {* Project list of commands. *}
fun
comlist :: "chain \ command list"
where
"comlist(cNil p) = []"
| "comlist(cCons p c G) = c # (comlist G)"
text {* Project a single command from a chain by flattening the list of commands. *}
definition
com :: "chain \ command"
where
"com G = foldr Seq (comlist G) Skip"
text {* Program variables read by a chain (either mentioned in an assertion, or accessed by a command). *}
fun
rd_chain :: "chain \ string set"
where
"rd_chain (cNil p) = rd_ass p"
| "rd_chain (cCons p c G) = rd_ass p \ rd_com c \ rd_chain G"
text {* Program variables written by a chain (that is, written by a command). *}
fun
wr_chain :: "chain \ string set"
where
"wr_chain (cNil _) = {}"
| "wr_chain (cCons _ c G) = wr_com c \ wr_chain G"
text {* Two chains are disjoint if neither writes a program variable that is read by the other. *}
definition disj_chain :: "chain \ chain \ bool"
where
"disj_chain G1 G2 \
rd_chain G1 \ wr_chain G2 = {}
\ rd_chain G2 \ wr_chain G1 = {}"
text {* The program variables read by a chain include those read by the commands in the chain (plus those mentioned in the assertions). *}
lemma rd_comlist_subseteq_rd_chain:
"rd_com (com G) \ rd_chain G"
by (induct G, auto simp add: rd_com_choose rd_com_loop rd_com_seq rd_com_skip com_def)
text {* The program variables written by a chain are those written by the commands in the chain. *}
lemma wr_comlist_is_wr_chain:
"wr_com (com G) = wr_chain G"
by (induct G, auto simp add: wr_com_choose wr_com_loop wr_com_skip wr_com_seq com_def)
subsubsection {* The ass_map functional, and its properties. *}
text {* Apply a transformation to each assertion in a chain. *}
fun
ass_map :: "(assertion \ assertion) \ chain \ chain"
where
"ass_map f (cNil p) = cNil (f p)"
| "ass_map f (cCons p c G) = cCons (f p) c (ass_map f G)"
text {* The ass_map transformation does not affect the command list. *}
lemma comlist_distrib_map:
fixes G f
shows "comlist G = comlist (ass_map f G)"
by (induct G, auto)
text {* The first assertion of a chain transformed by f is the first assertion of the chain, transformed by f. *}
lemma distrib_pre_assmap:
fixes G f
shows "pre (ass_map f G) = f (pre G)"
by (induct G, auto)
text {* The final assertion of a chain transformed by f is the final assertion of the chain, transformed by f. *}
lemma distrib_post_assmap:
fixes G f
shows "post (ass_map f G) = f (post G)"
by (induct G, auto)
text {* The program variables read by a transformed chain are those read by the untransformed chain, providing the transformation does not affect the read set. *}
lemma distrib_rd_assmap:
fixes G f
assumes "\p. rd_ass (f p) = rd_ass p"
shows "rd_chain (ass_map f G) = rd_chain G"
using assms by (induct G, auto)
text {* The program variables written by a transformed chain are those written by the untransformed chain. *}
lemma distrib_wr_assmap:
fixes G x
shows "wr_chain (ass_map f G) = wr_chain G"
by (induct G, auto)
subsubsection {* An interleaving operator on chains, and its properties. *}
text {* An interleaving operator on chains. Example: the interleavings of {p1}c1{q1} and {p2}c2{q2} are {p1*p2}c1{q1*p2}c2{q1*q2} and {p1*p2}c2{p1*q2}c1{q1*q2}. Note that this function is non-sequential: whenever both of the first two clauses apply, either can be used (the result is identical). *}
function
interleave_chains :: "(chain \ chain) \ chain set"
where
"interleave_chains (cNil p, G) = {ass_map (\q. Star p q) G}"
| "interleave_chains (G, cNil p) = {ass_map (\q. Star q p) G}"
| "interleave_chains (cCons p1 c1 G1, cCons p2 c2 G2)
= image (cCons (Star p1 p2) c1) (interleave_chains(G1, cCons p2 c2 G2))
\ image (cCons (Star p1 p2) c2) (interleave_chains(cCons p1 c1 G1, G2))"
by pat_completeness auto
termination by lexicographic_order
text {* The first assertion of an interleaved chain is the separating conjunction of the first assertions of the component chains. *}
lemma distrib_pre_interleave:
fixes G1 G2
shows "\G. G \ interleave_chains (G1, G2)
\ pre G = Star (pre G1) (pre G2)"
proof (induct G1)
case (cNil p1)
assume "G \ interleave_chains(cNil p1, G2)"
hence "G = ass_map (\q. Star p1 q) G2" by auto
thus ?case by (induct G2, auto)
next
case cCons
thus ?case by (induct G2, auto)
qed
text {* The final assertion of an interleaved chain is the separating conjunction of the final assertions of the component chains. *}
lemma distrib_post_interleave:
fixes G1 G2
shows "\G. G \ interleave_chains (G1, G2)
\ post G = Star (post G1) (post G2)"
proof (induct rule: chainpair_induction)
case (NC p1 G2 G)
moreover have "post(ass_map (\q. Star p1 q) G2) = Star p1 (post G2)"
by (induct G2, auto)
ultimately show ?case by auto
next
case (CN p2 G1 G)
moreover have "post(ass_map (\q. Star q p2) G1) = Star (post G1) p2"
by (induct G1, auto)
ultimately show ?case by auto
next
case (CC p1 p2 c1 c2 G1 G2)
thus ?case by auto
qed
text {* The program variables read by an interleaved chain are those read by either of the component chains. *}
lemma distrib_rd_interleave:
fixes G1 G2
shows "\G. G \ interleave_chains(G1, G2)
\ rd_chain G = rd_chain G1 \ rd_chain G2"
proof (induct rule: chainpair_induction)
case (NC p1 G2 G)
have "rd_chain (ass_map (\q. Star p1 q) G2)
= rd_chain (cNil p1) \ rd_chain G2"
by (induct G2, auto simp add: rd_star)
with NC show ?case by auto
next
case (CN p2 G1 G)
have "rd_chain (ass_map (\q. Star q p2) G1)
= rd_chain G1 \ rd_chain (cNil p2)"
by (induct G1, auto simp add: rd_star)
with CN show ?case by auto
next
case (CC p1 p2 c1 c2 G1 G2 G)
moreover
{
assume "G \ {cCons (Star p1 p2) c1 G' | G'.
G' \ interleave_chains(G1, cCons p2 c2 G2)}"
hence ?case using CC.hyps(1) by (auto simp add: rd_star)
}
moreover
{
assume "G \ {cCons (Star p1 p2) c2 G' | G'.
G' \ interleave_chains(cCons p1 c1 G1, G2)}"
hence ?case using CC.hyps(2) by (auto simp add: rd_star)
}
ultimately show ?case by auto
qed
text {* The program variables written by an interleaved chain are those written by either of the component chains. *}
lemma distrib_wr_interleave:
fixes G1 G2
shows "\G. G \ interleave_chains(G1, G2)
\ wr_chain G = wr_chain G1 \ wr_chain G2"
proof (induct rule: chainpair_induction)
case (NC p1 G2 G)
have "wr_chain (ass_map (\q. Star p1 q) G2)
= wr_chain (cNil p1) \ wr_chain G2" by (induct G2, auto)
with NC show ?case by auto
next
case (CN p2 G1 G)
have "wr_chain (ass_map (\q. Star q p2) G1)
= wr_chain G1 \ wr_chain (cNil p2)" by (induct G1, auto)
with CN show ?case by auto
next
case (CC p1 p2 c1 c2 G1 G2 G)
moreover
{
assume "G \ {cCons (Star p1 p2) c1 G' | G'.
G' \ interleave_chains(G1, cCons p2 c2 G2)}"
hence ?case using CC.hyps(1) by auto
}
moreover
{
assume "G \ {cCons (Star p1 p2) c2 G' | G'.
G' \ interleave_chains(cCons p1 c1 G1, G2)}"
hence ?case using CC.hyps(2) by auto
}
ultimately show ?case by auto
qed
subsubsection {* An operator for appending two chains, and its properties *}
text {* Appending two chains, ignoring the final assertion of the first chain. This function is only called when the final assertion of the first chain is equivalent to the first assertion of the second chain. *}
fun
chain_append :: "chain \ chain \ chain"
where
"chain_append (cNil _, G') = G'"
| "chain_append (cCons p c G, G') = cCons p c (chain_append (G, G'))"
text {* The command list of the chain G1@G2 is the concatenation of the command lists of G1 and G2. *}
lemma distrib_comlist_seq:
fixes G1
shows "\G2. comlist (chain_append(G1,G2)) = comlist G1 @ comlist G2"
by (induct G1, auto)
text {* The first assertion of the chain G1@G2 is the first assertion of G1, providing the final assertion of G1 matches the first assertion of G2. *}
lemma distrib_pre_seq:
fixes G1 G2
shows "post G1 = pre G2 \ pre(chain_append(G1,G2)) = pre G1"
by (induct G1, auto)
text {* The final assertion of the chain G1@G2 is the final assertion of G2. *}
lemma distrib_post_seq:
fixes G1 G2
shows "post(chain_append(G1,G2)) = post G2"
by (induct G1, auto)
text {* The program variables read by the chain G1@G2 are those read by either G1 or G2. *}
lemma distrib_rd_seq:
fixes G1 G2
shows "post G1 = pre G2 \
rd_chain (chain_append (G1, G2)) = rd_chain G1 \ rd_chain G2"
proof (induct G1)
case cNil
thus ?case by (induct G2, auto)
qed (auto)
text {* The program variables written by the chain G1@G2 are those written by either G1 or G2. *}
lemma distrib_wr_seq:
fixes G1 G2
shows "post G1 = pre G2 \
wr_chain (chain_append (G1, G2)) = wr_chain G1 \ wr_chain G2"
proof (induct G1)
case cNil
thus ?case by (induct G2, auto)
qed (auto)
subsubsection {* Further properties of chains *}
text {* The program variables read by the chain {p} Choose c1 c2 {q} are those read by p, c1, c2 or q. *}
lemma distrib_rd_choose:
fixes G1 G2
shows "rd_chain (cCons (ass P) (Choose (com G1) (com G2)) (cNil (ass Q)))
\ rd_int P \ rd_chain G1 \ rd_chain G2 \ rd_int Q"
using rd_int_is_rd_ass rd_comlist_subseteq_rd_chain rd_com_choose
by auto
text {* The program variables written by the chain {p} Choose c1 c2 {q} are those written by c1 or c2. *}
lemma distrib_wr_choose:
fixes G1 G2
shows "wr_chain (cCons (ass P) (Choose (com G1) (com G2)) (cNil (ass Q)))
= wr_chain G1 \ wr_chain G2"
using wr_comlist_is_wr_chain wr_com_choose by auto
text {* The program variables read by the chain {p} Loop c {q} are those read by p, c or q. *}
lemma distrib_rd_loop:
fixes G
shows "rd_chain (cCons (ass P) (Loop (com G)) (cNil (ass Q)))
\ rd_int P \ rd_chain G \ rd_int Q"
using rd_int_is_rd_ass rd_comlist_subseteq_rd_chain rd_com_loop
by auto
text {* The program variables written by the chain {p} Loop c {q} are those written by c. *}
lemma distrib_wr_loop:
fixes G
shows "wr_chain (cCons (ass P) (Loop (com G)) (cNil (ass Q)))
= wr_chain G"
using wr_comlist_is_wr_chain wr_com_loop by auto
subsubsection {* Provability of chains *}
text {* A chain is provable when each step of the chain is provable. *}
inductive
prov_chain :: "chain \ bool"
where
skip: "prov_chain(cNil p)"
| seq: "\prov_com(p, c, pre G); prov_chain G\
\ prov_chain(cCons p c G)"
inductive_cases prov_chain_skip_inv: "prov_chain(cNil p)"
inductive_cases prov_chain_seq_inv: "prov_chain(cCons p c G)"
text {* If a chain is provable, then the intermediate assertions can be elided. *}
lemma prov_chain_to_prov_com:
fixes G
shows "prov_chain G \ prov_com(pre G, com G, post G)"
proof (induct G)
case cNil
thus ?case using prov_com.skip com_def by auto
next
case (cCons p c G)
hence "prov_com (p, c, pre G)" and "prov_chain G"
using prov_chain_seq_inv by auto
with cCons.hyps
show ?case using prov_com.seq com_def by auto
qed
text {* Analogy of the Exists rule for chains *}
lemma prov_chain_exists:
fixes G x
shows "prov_chain G \ prov_chain (ass_map (Exists x) G)"
proof (induct G)
case (cNil p)
show ?case using prov_chain.skip by auto
next
case (cCons p c G')
hence "prov_com(p, c, pre G')" and "prov_chain G'"
using prov_chain_seq_inv by auto
from prov_com.exists[OF this(1)] and cCons.hyps[OF this(2)]
have "prov_com(Exists x p, c, Exists x (pre G'))"
and oqfyt: "prov_chain(ass_map (Exists x) G')" by auto
from this(1)
have "prov_com(Exists x p, c, pre (ass_map (Exists x) G'))"
by (cases G', auto)
from prov_chain.seq[OF this oqfyt]
show ?case by auto
qed
text {* Analogy of the Frame rule for chains *}
lemma prov_chain_frame:
fixes G r
shows "\prov_chain G; rd_ass r \ wr_chain G = {}\
\ prov_chain (ass_map (\q. Star q r) G)"
proof (induct G)
case (cNil P)
thus ?case using prov_chain.skip by auto
next
case (cCons p c G')
hence wcbaz: "prov_com(p, c, pre G')"
and almll: "prov_chain G'"
using prov_chain_seq_inv by auto
from cCons.prems(2) have "wr_com c \ rd_ass r = {}"
and "rd_ass r \ wr_chain G' = {}" by auto
from prov_com.frame[OF wcbaz this(1)] and cCons.hyps[OF almll this(2)]
have "prov_com(Star p r, c, Star (pre G') r)"
and ipbpk: "prov_chain(ass_map (\q. Star q r) G')" by auto
from this(1)
have "prov_com(Star p r, c, pre (ass_map (\q. Star q r) G'))"
by (cases G', auto)
from prov_chain.seq[OF this ipbpk]
show ?case by auto
qed
text {* Analogy of the Sequencing rule for chains *}
lemma prov_chain_seq:
fixes G1 G2
shows "\prov_chain G1; prov_chain G2;
post G1 = pre G2\ \ prov_chain(chain_append(G1,G2))"
proof (induct G1 arbitrary: G2)
case (cCons p1 c1 G1')
from prov_chain_seq_inv[OF cCons.prems(1)]
have "prov_com(p1, c1, pre G1')" and "prov_chain G1'" by auto
with cCons.hyps[OF _ cCons.prems(2)]
and cCons.prems(3)
have "prov_chain(chain_append (G1',G2))"
and "prov_com(p1,c1, pre(chain_append(G1',G2)))" by (induct G1', auto)
thus ?case using prov_chain.seq by auto
qed(auto)
text {* Analogy of the Par rule for chains *}
lemma prov_chain_par:
fixes G1 G2
shows "\prov_chain G1; prov_chain G2; disj_chain G1 G2\
\ (\G. G \ interleave_chains(G1,G2) \ prov_chain G)"
unfolding disj_chain_def
proof (induct rule: chainpair_induction)
case NC
thus ?case using prov_chain_frame and star_comm by auto
next
case CN
thus ?case using prov_chain_frame by auto
next
case (CC p1 p2 c1 c2 G1 G2 G)
from CC.prems(1)
have komyu: "prov_chain G1" and abcrd: "prov_com (p1, c1, pre G1)"
using prov_chain_seq_inv by auto
from CC.prems(2)
have lkwds: "prov_chain G2" and yikpu: "prov_com (p2, c2, pre G2)"
using prov_chain_seq_inv by auto
from CC.prems(3)
have wasic: "rd_chain G1 \ wr_chain (cCons p2 c2 G2) = {}
\ rd_chain (cCons p2 c2 G2) \ wr_chain G1 = {}"
and thqte: "rd_chain (cCons p1 c1 G1) \ wr_chain G2 = {}
\ rd_chain G2 \ wr_chain (cCons p1 c1 G1) = {}"
and jzcvn: "wr_com c2 \ rd_ass p1 = {}"
and nqmnc: "wr_com c1 \ rd_ass p2 = {}" by auto
from CC.prems(4)
have "G \ interleave_chains (cCons p1 c1 G1, cCons p2 c2 G2)" by auto
hence "G \ {cCons (Star p1 p2) c1 G' | G'.
G' \ interleave_chains(G1, cCons p2 c2 G2)}
\ G \ {cCons (Star p1 p2) c2 G' | G'.
G' \ interleave_chains(cCons p1 c1 G1, G2)}" (is "?lhs \ ?rhs")
by auto
moreover
{
assume ?lhs
then obtain G' where cyrow: "G = cCons (Star p1 p2) c1 G'"
and rwawt: "G' \ interleave_chains(G1, cCons p2 c2 G2)" by auto
from CC.hyps(1)[OF komyu CC.prems(2) wasic rwawt]
have "prov_chain G'" by auto
moreover
from prov_com.frame[OF abcrd nqmnc]
have "prov_com(Star p1 p2, c1, Star (pre G1) p2)" by auto
with distrib_pre_interleave[OF rwawt]
have "prov_com(Star p1 p2, c1, pre G')"
by auto
ultimately
have ?case using cyrow and prov_chain.seq by auto
}
moreover
{
assume ?rhs
then obtain G' where cyrow: "G = cCons (Star p1 p2) c2 G'"
and rwawt: "G' \ interleave_chains(cCons p1 c1 G1, G2)" by auto
from CC.hyps(2)[OF CC.prems(1) lkwds thqte rwawt]
have "prov_chain G'" by auto
moreover
from prov_com.frame[OF yikpu jzcvn]
have "prov_com(Star p1 p2, c2, Star p1 (pre G2))"
using star_comm by auto
with distrib_pre_interleave[OF rwawt]
have "prov_com(Star p1 p2, c2, pre G')"
by auto
ultimately
have ?case using cyrow and prov_chain.seq by auto
}
ultimately show ?case by auto
qed
text {* Analogy of the Choose rule for chains *}
lemma prov_chain_choose:
fixes G1 G2 p q
assumes "prov_chain G1"
assumes "prov_chain G2"
assumes "pre G1 = p"
assumes "pre G2 = p"
assumes "post G1 = q"
assumes "post G2 = q"
shows "prov_chain (cCons p (Choose (com G1) (com G2)) (cNil q))"
proof -
from prov_chain_to_prov_com[OF assms(1)] and assms(3) and assms(5)
have "prov_com (p, com G1, q)" by auto
moreover
from prov_chain_to_prov_com[OF assms(2)] and assms(4) and assms(6)
have "prov_com (p, com G2, q)" by auto
ultimately
have "prov_com (p, Choose (com G1) (com G2), q)"
using prov_com.choose by auto
thus ?thesis using prov_chain.seq[OF _ prov_chain.skip] by auto
qed
text {* Analogy of the Loop rule for chains *}
lemma prov_chain_loop:
fixes G p q
assumes "prov_chain G"
assumes "pre G = p"
assumes "post G = p"
assumes "q = p"
shows "prov_chain (cCons p (Loop (com G)) (cNil q))"
proof -
from prov_chain_to_prov_com[OF assms(1)] and assms(2) and assms(3)
have "prov_com (p, com G, p)" by auto
hence "prov_com (p, Loop (com G), q)"
using prov_com.loop and assms(4) by auto
thus ?thesis using prov_chain.seq[OF _ prov_chain.skip] by auto
qed
subsubsection {* Extracting chains from a diagram *}
text {* The following function extracts a set of proof chains from a given diagram. *}
primrec
chains :: "diagram \ chain set"
where
"chains (Blank P) = {cNil (ass P)}"
| "chains (Basic P c Q) = {cCons (ass P) c (cNil (ass Q))}"
| "chains (HComp_dia A B) = \ {interleave_chains (G1, G2)
| G1 G2. G1 \ chains A \ G2 \ chains B \ disj_chain G1 G2}"
| "chains (VComp_dia A B) = {chain_append (G1, G2)
| G1 G2. G1 \ chains A \ G2 \ chains B \ post G1 = pre G2}"
| "chains (Exists_dia x A) = {ass_map (Exists x) G
| G. G \ chains A}"
| "chains (Choose_dia P A B Q)
= {cCons (ass P) (Choose (com G1) (com G2)) (cNil (ass Q))
| G1 G2. G1 \ chains A \ G2 \ chains B
\ pre G1 = ass P \ pre G2 = ass P
\ post G1 = ass Q \ post G2 = ass Q }"
| "chains (Loop_dia P A Q)
= { cCons (ass P) (Loop (com G)) (cNil (ass Q))
| G. G \ chains A \ post G = ass P
\ pre G = ass P \ ass Q = ass P }"
text {* The first assertion of any chain extracted from a diagram matches the top interface of the diagram. *}
lemma pre_is_top:
fixes A
shows "\G. G \ chains A \ pre G = ass (top A)"
proof (induct A)
case HComp_dia
thus ?case using distrib_pre_interleave by auto
next
case VComp_dia
thus ?case using distrib_pre_seq by auto
next
case (Exists_dia x A)
thus ?case using distrib_pre_assmap by auto
qed (auto)
text {* The final assertion of any chain extracted from a diagram matches the bottom interface of the diagram. *}
lemma post_is_bot:
fixes A
shows "\G. G \ chains A \