Commands, assertions and separation logic rules
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
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
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
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
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
Separation logic rules for proving Hoare triples.
inductive
prov_com :: assertion × command × assertion ⇒ bool
where
prov_com (p, c, q)
prov_com (Exists x p, c, Exists x q)
prov_com (p, c1, q);
prov_com (p, c2, q)
prov_com (p, Choose c1 c2, q)
prov_com (p, c, p)
prov_com (p, Loop c, p)
prov_com (p, c, q); wr_com(c) ∩ rd_ass(r) = {}
prov_com (Star p r, c, Star q r)
prov_com(p, Skip, p)
prov_com (p, c1, q); prov_com (q, c2, r)
prov_com (p, Seq c1 c2, r)
Syntax and semantics of interfaces
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
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)]
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
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)
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
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
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
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
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
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
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
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
The set of commands that can be extracted from a diagram. The ⊗ 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)
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 = {}
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
prov_dia (Blank P)
prov_com (ass P, c, ass Q)
prov_dia (Basic P c Q)
prov_dia A
prov_dia (Exists_dia x A)
prov_dia A; prov_dia B; disj_dia A B
prov_dia (HComp_dia A B)
prov_dia A; prov_dia B; equiv_int (bot A) (top B)
prov_dia (VComp_dia A B)
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)
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)
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)}
Proof chains
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
An induction principle for pairs of chains. Think of it as induction over pairs of natural numbers: if Φ 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)
Project first assertion.
fun
pre :: chain ⇒ assertion
where
pre(cNil p) = p
| pre(cCons p c G) = p
Project final assertion.
fun
post :: chain ⇒ assertion
where
post(cNil p) = p
| post(cCons p c G) = post G
Project list of commands.
fun
comlist :: chain ⇒ command list
where
comlist(cNil p) = []
| comlist(cCons p c G) = c # (comlist G)
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
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
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
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 = {}
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)
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)
The ass_map functional, and its properties.
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)
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)
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)
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)
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)
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)
An interleaving operator on chains, and its properties.
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
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
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
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
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
An operator for appending two chains, and its properties
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'))
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)
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)
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)
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)
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)
Further properties of chains
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
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
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
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
Provability of chains
A chain is provable when each step of the chain is provable.
inductive
prov_chain :: chain ⇒ bool
where
prov_chain(cNil p)
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)
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
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
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
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)
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
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
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
Extracting chains from a diagram
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 }
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)
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 ⟹ post G = ass (bot A)
proof (induct A)
case (HComp_dia A1 A2)
thus ?case using distrib_post_interleave by auto
next
case (VComp_dia A1 A2)
thus ?case using distrib_post_seq by auto
next
case (Exists_dia x A)
thus ?case using distrib_post_assmap by auto
qed (auto)
The program variables read by any chain extracted from a diagram include those read by the diagram. Note: chains collapse if and while statements to single commands, so any intermediate assertions used to prove their bodies do not feature in a chain.
lemma rd_chain_subseteq_rd_dia: fixes A
shows ⋀G. G ∈ chains A ⟹ rd_chain G ⊆ rd_dia A
proof (induct A)
case (Blank P)
thus ?case using rd_int_is_rd_ass by auto
next
case (Basic P c Q)
thus ?case using rd_int_is_rd_ass by auto
next
case (HComp_dia A1 A2)
then obtain G1 G2 where npvhi: G ∈ interleave_chains(G1,G2)
and G1 ∈ chains A1 and G2 ∈ chains A2 by auto
with HComp_dia.hyps
have fbdto: rd_chain G1 ⊆ rd_dia A1 and ofvoh: rd_chain G2 ⊆ rd_dia A2
by auto
from npvhi have rd_chain G = rd_chain G1 ∪ rd_chain G2
using distrib_rd_interleave by auto
thus ?case using fbdto ofvoh by auto
next
case (VComp_dia A1 A2)
then obtain G1 G2 where npvhi: G = chain_append (G1,G2)
and G1 ∈ chains A1 and G2 ∈ chains A2 and wmmam: post G1 = pre G2 by auto
with VComp_dia.hyps
have fbdto: rd_chain G1 ⊆ rd_dia A1 and ofvoh: rd_chain G2 ⊆ rd_dia A2
by auto
from npvhi have rd_chain G = rd_chain G1 ∪ rd_chain G2
using distrib_rd_seq[OF wmmam] by auto
thus ?case using fbdto ofvoh by auto
next
case (Exists_dia x A')
then obtain G' where npvhi: G = ass_map (Exists x) G'
and G' ∈ chains A' by auto
with Exists_dia.hyps
have fbdto: rd_chain G' ⊆ rd_dia A'
by auto
from npvhi have rd_chain G = rd_chain G'
using distrib_rd_assmap[OF rd_exists] by auto
thus ?case using fbdto by auto
next
case (Choose_dia P A1 A2 Q)
then obtain G1 G2
where npvhi: G = cCons (ass P) (Choose (com G1) (com G2)) (cNil (ass Q))
and G1 ∈ chains A1 and G2 ∈ chains A2 by auto
with Choose_dia.hyps
have fbdto: rd_chain G1 ⊆ rd_dia A1 and ofvoh: rd_chain G2 ⊆ rd_dia A2
by auto
from npvhi have rd_chain G ⊆ rd_int P ∪ rd_chain G1 ∪ rd_chain G2 ∪ rd_int Q
using distrib_rd_choose by auto
thus ?case using fbdto ofvoh by auto
next
case (Loop_dia P A Q)
then obtain G'
where npvhi: G = cCons (ass P) (Loop (com G')) (cNil (ass Q))
and G' ∈ chains A by auto
with Loop_dia.hyps
have fbdto: rd_chain G' ⊆ rd_dia A by auto
from npvhi have rd_chain G ⊆ rd_int P ∪ rd_chain G' ∪ rd_int Q
using distrib_rd_loop by auto
thus ?case using fbdto by auto
qed
The program variables written by any chain extracted from a diagram are those written by the diagram.
lemma wr_chain_eq_wr_dia: fixes A
shows ⋀G. G ∈ chains A ⟹ wr_dia A = wr_chain G
proof (induct A)
case (HComp_dia A1 A2)
thus ?case using distrib_wr_interleave by auto
next
case (VComp_dia A1 A2)
thus ?case using distrib_wr_seq by auto
next
case (Exists_dia x A1)
thus ?case using distrib_wr_assmap by auto
next
case (Choose_dia P A1 A2 Q)
thus ?case using distrib_wr_choose by auto
next
case (Loop_dia P A1 Q)
thus ?case using distrib_wr_loop by auto
qed (auto)
If a diagram is provable, then every chain that can be extracted from it is provable.
lemma soundness_part_one: fixes A::diagram
shows prov_dia A ⟹ (∀G ∈ chains A. prov_chain G)
proof(induct rule: prov_dia.induct)
case (Blank P)
show ?case using prov_chain.skip by auto
next
case Basic
thus ?case using prov_chain.seq[OF _ prov_chain.skip] by auto
next
case (Exists A x)
thus ?case using prov_chain_exists by auto
next
case (HComp A B)
show ?case
proof(intro ballI)
fix G
assume srmjd: G ∈ chains (HComp_dia A B)
then obtain G1 G2 where
grirj: G ∈ interleave_chains (G1, G2)
and G1 ∈ chains A and G2 ∈ chains B
and yecnl: disj_chain G1 G2 by auto
with HComp.hyps
have prov_chain G1 and prov_chain G2 by auto
from prov_chain_par[OF this yecnl grirj]
show prov_chain G by auto
qed
next
case (VComp A B)
show ?case
proof(intro ballI)
fix G
assume G ∈ chains (VComp_dia A B)
then obtain G1 G2 where
grirj: G = chain_append(G1,G2)
and G1 ∈ chains A and G2 ∈ chains B
and hhwel: post G1 = pre G2 by auto
with VComp.hyps(2) and VComp.hyps(4)
have prov_chain G1 and prov_chain G2 by auto
from prov_chain_seq[OF this hhwel] grirj
show prov_chain G by auto
qed
next
case (Choose A B P Q)
show ?case
proof(intro ballI)
fix G
assume G ∈ chains (Choose_dia P A B Q)
then obtain G1 G2 where
grirj: G = cCons (ass P) (Choose (com G1) (com G2)) (cNil (ass Q))
and G1 ∈ chains A and G2 ∈ chains B
and clugz: pre G1 = ass P
and kcgsh: pre G2 = ass P
and ivawk: post G1 = ass Q and gryoo: post G2 = ass Q by auto
with Choose.hyps(2) and Choose.hyps(4)
have prov_chain G1 and prov_chain G2 by auto
from prov_chain_choose[OF this clugz kcgsh ivawk gryoo] and grirj
show prov_chain G by auto
qed
next
case (Loop A P Q)
show ?case
proof(intro ballI)
fix G
assume G ∈ chains (Loop_dia P A Q)
then obtain G' where
grirj: G = cCons (ass P) (Loop (com G')) (cNil (ass Q))
and G' ∈ chains A
and clugz: pre G' = ass P
and kcgsh: post G' = ass P
and ivawk: ass Q = ass P by auto
with Loop.hyps(2)
have prov_chain G' by auto
from prov_chain_loop[OF this clugz kcgsh ivawk] and grirj
show prov_chain G by auto
qed
qed
For each interleaving C of the command lists of two chains G1 and G2, we can obtain an interleaving of G1 and G2 whose command list is C.
lemma obtain_interleave_chains_from_interleave_coms: fixes G1 G2
shows ⋀C. C ∈ comlist G1 ⊗ comlist G2 ⟹ (∃G ∈ interleave_chains(G1,G2). C = comlist G)
proof(induct rule: chainpair_induction)
case (NC p1 G2 C)
moreover have comlist G2 = comlist (ass_map (λq. Star p1 q) G2)
by (induct G2, auto)
ultimately show ?case by (induct G2, auto)
next
case (CN p2 G1 C)
moreover have comlist G1 = comlist (ass_map (λq. Star q p2) G1)
by (induct G1, auto)
ultimately show ?case by (induct G1, auto)
next
case (CC p1 p2 c1 c2 G1 G2)
hence C ∈ comlist (cCons p1 c1 G1) ⊗ comlist (cCons p2 c2 G2)
by auto
hence C ∈ (c1 # comlist G1) ⊗ (c2 # comlist G2)
by auto
hence C ∈ {c1#C' | C'. C' ∈ comlist G1 ⊗ (c2 # comlist G2)}
∨ C ∈ {c2#C' | C'. C' ∈ (c1 # comlist G1) ⊗ comlist G2}
(is ?lhs ∨ ?rhs) by auto
moreover
{
assume ?lhs
then obtain C' where pupdr: C = c1#C'
and C' ∈ comlist G1 ⊗ comlist (cCons p2 c2 G2) by auto
from CC.hyps(1)[OF this(2)]
obtain G' where veksv: G' ∈ interleave_chains (G1, cCons p2 c2 G2)
and yseva: C' = comlist G' by auto
let ?G = cCons (Star p1 p2) c1 G'
from pupdr and yseva have C = comlist ?G by auto
hence ?case using bexI[of _ ?G] veksv by auto
}
moreover
{
assume ?rhs
then obtain C' where pupdr: C = c2#C'
and C' ∈ comlist (cCons p1 c1 G1) ⊗ comlist G2 by auto
from CC.hyps(2)[OF this(2)]
obtain G' where veksv: G' ∈ interleave_chains (cCons p1 c1 G1, G2)
and yseva: C' = comlist G' by auto
let ?G = cCons (Star p1 p2) c2 G'
from pupdr and yseva have C = comlist ?G by auto
hence ?case using bexI[of _ ?G] veksv by auto
}
ultimately show ?case by auto
qed
From disjoint diagrams can be extracted only disjoint chains.
lemma disj_dia_implies_disj_chain: fixes A1 A2 G1 G2
assumes G1 ∈ chains A1
assumes G2 ∈ chains A2
shows disj_dia A1 A2 ⟹ disj_chain G1 G2
unfolding disj_dia_def disj_chain_def
proof(elim conjE)
assume rd_dia A1 ∩ wr_dia A2 = {}
and rd_dia A2 ∩ wr_dia A1 = {}
with rd_chain_subseteq_rd_dia[OF assms(1)]
and rd_chain_subseteq_rd_dia[OF assms(2)]
and wr_chain_eq_wr_dia[OF assms(1)]
and wr_chain_eq_wr_dia[OF assms(2)]
show rd_chain G1 ∩ wr_chain G2 = {}
∧ rd_chain G2 ∩ wr_chain G1 = {} by auto
qed
For each command list C extracted from a provable diagram, we can find a chain of that diagram whose command list is C.
lemma obtain_chain_from_comlist: fixes A
shows ⋀C. ⟦prov_dia A; C ∈ coms_list A⟧ ⟹ (∃G. G ∈ chains A ∧ C = comlist G)
proof (induct A)
case (HComp_dia A B)
from HComp_dia.prems(1)
have rilex: prov_dia A and ldiqm: prov_dia B and nyxis: disj_dia A B
using prov_dia_hcomp_inv by auto
from HComp_dia.prems(2) obtain C1 C2 where nsnoa: C ∈ C1 ⊗ C2
and ouwyw: C1 ∈ coms_list A and rfcto: C2 ∈ coms_list B by auto
from HComp_dia.hyps(1)[OF rilex ouwyw]
obtain G1 where ppvuk: G1 ∈ chains A and ykfjd: C1 = comlist G1 by auto
from HComp_dia.hyps(2)[OF ldiqm rfcto]
obtain G2 where vqfqu: G2 ∈ chains B and ayxqc: C2 = comlist G2 by auto
from nsnoa ykfjd ayxqc have C ∈ comlist G1 ⊗ comlist G2 by auto
from obtain_interleave_chains_from_interleave_coms[OF this]
obtain G where G ∈ interleave_chains(G1,G2) and C = comlist G by auto
moreover from disj_dia_implies_disj_chain[OF ppvuk vqfqu nyxis]
have disj_chain G1 G2 by auto
ultimately show ?case using ppvuk vqfqu by auto
next
case (VComp_dia A B)
from VComp_dia.prems(1)
have rilex: prov_dia A and ldiqm: prov_dia B
and nyxis: equiv_int (bot A) (top B)
using prov_dia_vcomp_inv by auto
from VComp_dia.prems(2) obtain C1 C2 where nsnoa: C = C1 @ C2
and ouwyw: C1 ∈ coms_list A and rfcto: C2 ∈ coms_list B by auto
from VComp_dia.hyps(1)[OF rilex ouwyw]
obtain G1 where ppvuk: G1 ∈ chains A and ykfjd: C1 = comlist G1 by auto
from VComp_dia.hyps(2)[OF ldiqm rfcto]
obtain G2 where vqfqu: G2 ∈ chains B and ayxqc: C2 = comlist G2 by auto
from nyxis have iybvs: post G1 = pre G2
using pre_is_top[OF vqfqu] and post_is_bot[OF ppvuk] and equiv_int_sound by auto
let ?G = chain_append(G1,G2)
have ?G ∈ chains(VComp_dia A B) using ppvuk vqfqu iybvs by auto
moreover have C = comlist ?G using nsnoa ykfjd ayxqc distrib_comlist_seq by auto
ultimately show ?case by auto
next
case (Exists_dia x A)
from Exists_dia.prems(1)
have rilex: prov_dia A
using prov_dia_exists_inv by auto
from Exists_dia.prems(2)
have ouwyw: C ∈ coms_list A by auto
from Exists_dia.hyps[OF rilex ouwyw]
obtain G' where lbpxt: G' ∈ chains A and bsvav: C = comlist G' by auto
let ?G = ass_map (Exists x) G'
have ?G ∈ chains (Exists_dia x A) and C = comlist ?G
using lbpxt bsvav comlist_distrib_map by auto
thus ?case by auto
next
case (Choose_dia P A B Q)
from prov_dia_choose_inv[OF Choose_dia.prems(1)]
have rilex: prov_dia A and ldiqm: prov_dia B
and jjobf: equiv_int (top A) P
and pxese: equiv_int (top B) P
and xbhsu: equiv_int (bot A) Q and bjxcs: equiv_int (bot B) Q by auto
from Choose_dia.prems(2) obtain c1 c2 where nsnoa: C = [Choose c1 c2]
and c1 ∈ coms A and c2 ∈ coms B by auto
then obtain C1 C2
where rswrj: c1 = foldr Seq C1 Skip and ouwyw: C1 ∈ coms_list A
and psjzb: c2 = foldr Seq C2 Skip and rfcto: C2 ∈ coms_list B by auto
from Choose_dia.hyps(1)[OF rilex ouwyw]
obtain G1 where ppvuk: G1 ∈ chains A and ykfjd: C1 = comlist G1 by auto
from Choose_dia.hyps(2)[OF ldiqm rfcto]
obtain G2 where vqfqu: G2 ∈ chains B and ayxqc: C2 = comlist G2 by auto
from jjobf have jgelm: pre G1 = ass P
using pre_is_top[OF ppvuk] equiv_int_sound by auto
from pxese have zckeo: pre G2 = ass P
using pre_is_top[OF vqfqu] equiv_int_sound by auto
from xbhsu have rdajb: post G1 = ass Q
using post_is_bot[OF ppvuk] equiv_int_sound by auto
from bjxcs have pxmqn: post G2 = ass Q
using post_is_bot[OF vqfqu] equiv_int_sound by auto
let ?G = cCons (ass P) (Choose (com G1) (com G2)) (cNil (ass Q))
have ?G ∈ chains(Choose_dia P A B Q) and C = comlist ?G
using ppvuk vqfqu jgelm zckeo rdajb pxmqn nsnoa ykfjd ayxqc rswrj psjzb com_def by auto
thus ?case using exI[of _ ?G] by auto
next
case (Loop_dia P A Q)
from prov_dia_loop_inv[OF Loop_dia.prems(1)]
have rilex: prov_dia A
and jjobf: equiv_int (top A) P
and pxese: equiv_int (bot A) P
and xbhsu: equiv_int Q P by auto
from Loop_dia.prems(2) obtain c' where nsnoa: C = [Loop c']
and c' ∈ coms A by auto
then obtain C' where reema: c' = foldr Seq C' Skip
and ouwyw: C' ∈ coms_list A by auto
from Loop_dia.hyps(1)[OF rilex ouwyw]
obtain G' where ppvuk: G' ∈ chains A and ykfjd: C' = comlist G' by auto
from jjobf have jgelm: pre G' = ass P
using pre_is_top[OF ppvuk] equiv_int_sound by auto
from pxese have zckeo: post G' = ass P
using post_is_bot[OF ppvuk] equiv_int_sound by auto
from xbhsu have rdajb: ass Q = ass P
using equiv_int_sound by auto
let ?G = cCons (ass P) (Loop (com G')) (cNil (ass Q))
have ?G ∈ chains(Loop_dia P A Q) and C = comlist ?G
using ppvuk jgelm zckeo rdajb nsnoa ykfjd reema com_def by auto
thus ?case by auto
qed (auto)
For each command c extracted from a provable diagram, we can extract a chain from that diagram whose command is c.
lemma obtain_chain_from_com: fixes A
shows ⋀c. ⟦prov_dia A; c ∈ coms A⟧ ⟹ (∃G. G ∈ chains A ∧ c = com G)
proof -
fix c
assume rxynj: prov_dia A
assume c ∈ coms A
then obtain C where gpygs: c = foldr Seq C Skip
and qttqd: C ∈ coms_list A by auto
from obtain_chain_from_comlist[OF rxynj qttqd]
obtain G where hmkod: G ∈ chains A and C = comlist G by auto
from this(2) and gpygs have c = com G using com_def by auto
with hmkod show ∃G. G ∈ chains A ∧ c = com G by auto
qed
If every chain extracted from a provable diagram is provable, then every Hoare triple in the semantics of that diagram is provable in separation logic.
lemma soundness_part_two: fixes A::diagram
assumes prov_dia A and ∀G ∈ chains A. prov_chain G
shows ∀p c q. (p,c,q) ∈ sem_dia A ⟶ prov_com(p,c,q)
proof(intro allI impI)
fix p c q
assume (p,c,q) ∈ sem_dia A
hence cslfl: p = ass (top A) and lrenu: q = ass (bot A) and c ∈ coms A
using sem_dia_def by auto
with obtain_chain_from_com[OF assms(1)]
obtain G where ojjhx: G ∈ chains A and cicpm: c = com G
by auto
from ojjhx have prov_chain G using assms by auto
hence prov_com(pre G, com G, post G)
using prov_chain_to_prov_com by auto
with ojjhx cicpm cslfl lrenu show prov_com(p, c, q)
using pre_is_top and post_is_bot by auto
qed
If there exist a provable diagram whose semantics contains a Hoare triple {p}c{q}, then {p}c{q} is provable in separation logic.
theorem soundness:
(∃A. prov_dia A ∧ (p,c,q) ∈ sem_dia A)
prov_com (p, c, q)
using soundness_part_one soundness_part_two by auto
For every Hoare triple {p}c{q} that is provable in separation logic, we can construct a provable diagram whose semantics contains {p}c{q}.
theorem relative_completeness:
prov_com (p,c,q)
(∃A. prov_dia A ∧ (p,c,q) ∈ sem_dia A)
proof -
fix p c q
assume bujaa: prov_com (p,c,q)
let ?A = Basic (Ribbon p) c (Ribbon q)
have prov_dia ?A using bujaa prov_dia.Basic by auto
moreover
have (p,c,q) ∈ sem_dia ?A using seq_skip unfolding sem_dia_def by auto
ultimately show ∃A. prov_dia A ∧ (p,c,q) ∈ sem_dia A by auto
qed
Visual congruence
Define diagram contexts, which are diagrams containing a hole.
datatype diagram_ctx =
Hole
| HComp_ctx1 diagram_ctx diagram
| HComp_ctx2 diagram diagram_ctx
| VComp_ctx1 diagram_ctx diagram
| VComp_ctx2 diagram diagram_ctx
| Exists_ctx string diagram_ctx
| Choose_ctx1 interface diagram_ctx diagram interface
| Choose_ctx2 interface diagram diagram_ctx interface
| Loop_ctx interface diagram_ctx interface
Inserting a diagram into a context's hole.
fun
apply_ctx :: diagram_ctx ⇒ diagram ⇒ diagram
where
apply_ctx Hole A = A
| apply_ctx (HComp_ctx1 C A) B = HComp_dia (apply_ctx C B) A
| apply_ctx (HComp_ctx2 A C) B = HComp_dia A (apply_ctx C B)
| apply_ctx (VComp_ctx1 C A) B = VComp_dia (apply_ctx C B) A
| apply_ctx (VComp_ctx2 A C) B = VComp_dia A (apply_ctx C B)
| apply_ctx (Exists_ctx x C) B = Exists_dia x (apply_ctx C B)
| apply_ctx (Choose_ctx1 P C A Q) B
= Choose_dia P (apply_ctx C B) A Q
| apply_ctx (Choose_ctx2 P A C Q) B
= Choose_dia P A (apply_ctx C B) Q
| apply_ctx (Loop_ctx P C Q) B = Loop_dia P (apply_ctx C B) Q
The 'visual congruence' relation. The first four rules make this a congruence relation. The final six equate diagrams that appear the same on the printed page.
inductive
sim :: diagram ⇒ diagram ⇒ bool
where
sim A A
sim A B
sim B A
sim A B; sim B C
sim A C
sim A B
sim (apply_ctx C A) (apply_ctx C B)
sim (HComp_dia A (HComp_dia B C)) (HComp_dia (HComp_dia A B) C)
sim (VComp_dia A (VComp_dia B C)) (VComp_dia (VComp_dia A B) C)
sim (HComp_dia (Blank Emp_int) A) A
sim (HComp_dia A (Blank Emp_int)) A
sim (VComp_dia (Blank (top A)) A) A
sim (VComp_dia A (Blank (bot A))) A
Visually congruent diagrams are equiprovable and semantically equivalent.
theorem sim_sound: fixes A B
assumes sim A B
shows prov_dia A = prov_dia B ∧ sem_dia A = sem_dia B
proof -
{
fix A B
have sim A B ⟹ prov_dia A = prov_dia B
∧ rd_dia A = rd_dia B ∧ wr_dia A = wr_dia B
∧ equiv_int (top A) (top B) ∧ equiv_int (bot A) (bot B) ∧ coms_list A = coms_list B
proof (induct rule:sim.induct)
case refl
thus ?case unfolding equiv_int_def by auto
next
case sym
thus ?case unfolding equiv_int_def by auto
next
case trans
thus ?case unfolding equiv_int_def by auto
next
case (cong A B C)
show ?case
proof (induct C)
case Hole
thus ?case using cong by auto
next
case (HComp_ctx1 C A')
{
assume prov_dia (HComp_dia (apply_ctx C A) A')
hence prov_dia (apply_ctx C A) and prov_dia A'
and disj_dia (apply_ctx C A) A'
using prov_dia_hcomp_inv by auto
hence prov_dia (apply_ctx C B) and prov_dia A'
and disj_dia (apply_ctx C B) A'
unfolding disj_dia_def using HComp_ctx1.hyps by auto
hence prov_dia (HComp_dia (apply_ctx C B) A')
using prov_dia.HComp by auto
}
moreover
{
assume prov_dia (HComp_dia (apply_ctx C B) A')
hence prov_dia (apply_ctx C B) and prov_dia A'
and disj_dia (apply_ctx C B) A'
using prov_dia_hcomp_inv by auto
hence prov_dia (apply_ctx C A) and prov_dia A'
and disj_dia (apply_ctx C A) A'
unfolding disj_dia_def using HComp_ctx1.hyps by auto
hence prov_dia (HComp_dia (apply_ctx C A) A')
using prov_dia.HComp by auto
}
ultimately show ?case using HComp_ctx1.hyps
unfolding equiv_int_def by auto
next
case (HComp_ctx2 A' C)
{
assume prov_dia (HComp_dia A' (apply_ctx C A))
hence prov_dia (apply_ctx C A) and prov_dia A'
and disj_dia A' (apply_ctx C A)
using prov_dia_hcomp_inv by auto
hence prov_dia (apply_ctx C B) and prov_dia A'
and disj_dia A' (apply_ctx C B)
unfolding disj_dia_def using HComp_ctx2.hyps by auto
hence prov_dia (HComp_dia A' (apply_ctx C B))
using prov_dia.HComp by auto
}
moreover
{
assume prov_dia (HComp_dia A' (apply_ctx C B))
hence prov_dia (apply_ctx C B) and prov_dia A'
and disj_dia A' (apply_ctx C B)
using prov_dia_hcomp_inv by auto
hence prov_dia (apply_ctx C A) and prov_dia A'
and disj_dia A' (apply_ctx C A)
unfolding disj_dia_def using HComp_ctx2.hyps by auto
hence prov_dia (HComp_dia A' (apply_ctx C A))
using prov_dia.HComp by auto
}
ultimately show ?case
using HComp_ctx2.hyps unfolding equiv_int_def by auto
next
case (VComp_ctx1 C A')
{
assume prov_dia (VComp_dia (apply_ctx C A) A')
hence prov_dia (apply_ctx C A) and prov_dia A'
and equiv_int (bot (apply_ctx C A)) (top A')
using prov_dia_vcomp_inv by auto
hence prov_dia (apply_ctx C B) and prov_dia A'
and equiv_int (bot (apply_ctx C B)) (top A')
using VComp_ctx1.hyps unfolding equiv_int_def by auto
hence prov_dia (VComp_dia (apply_ctx C B) A')
using prov_dia.VComp by auto
}
moreover
{
assume prov_dia (VComp_dia (apply_ctx C B) A')
hence prov_dia (apply_ctx C B) and prov_dia A'
and equiv_int (bot (apply_ctx C B)) (top A')
using prov_dia_vcomp_inv by auto
hence prov_dia (apply_ctx C A) and prov_dia A'
and equiv_int (bot (apply_ctx C A)) (top A')
using VComp_ctx1.hyps unfolding equiv_int_def by auto
hence prov_dia (VComp_dia (apply_ctx C A) A')
using prov_dia.VComp by auto
}
ultimately show ?case using VComp_ctx1.hyps
unfolding equiv_int_def by auto
next
case (VComp_ctx2 A' C)
{
assume prov_dia (VComp_dia A' (apply_ctx C A))
hence prov_dia (apply_ctx C A) and prov_dia A'
and equiv_int (bot A') (top (apply_ctx C A))
using prov_dia_vcomp_inv by auto
hence prov_dia (apply_ctx C B) and prov_dia A'
and equiv_int (bot A') (top (apply_ctx C B))
using VComp_ctx2.hyps unfolding equiv_int_def by auto
hence prov_dia (VComp_dia A' (apply_ctx C B))
using prov_dia.VComp by auto
}
moreover
{
assume prov_dia (VComp_dia A' (apply_ctx C B))
hence prov_dia (apply_ctx C B) and prov_dia A'
and equiv_int (bot A') (top (apply_ctx C B))
using prov_dia_vcomp_inv by auto
hence prov_dia (apply_ctx C A) and prov_dia A'
and equiv_int (bot A') (top (apply_ctx C A))
using VComp_ctx2.hyps unfolding equiv_int_def by auto
hence prov_dia (VComp_dia A' (apply_ctx C A))
using prov_dia.VComp by auto
}
ultimately show ?case using VComp_ctx2.hyps
unfolding equiv_int_def by auto
next
case (Exists_ctx x C)
{
assume prov_dia (Exists_dia x (apply_ctx C A))
hence prov_dia (apply_ctx C A)
using prov_dia_exists_inv by auto
hence prov_dia (apply_ctx C B)
using Exists_ctx.hyps by auto
hence prov_dia (Exists_dia x (apply_ctx C B))
using prov_dia.Exists by auto
}
moreover
{
assume prov_dia (Exists_dia x (apply_ctx C B))
hence prov_dia (apply_ctx C B)
using prov_dia_exists_inv by auto
hence prov_dia (apply_ctx C A)
using Exists_ctx.hyps by auto
hence prov_dia (Exists_dia x (apply_ctx C A))
using prov_dia.Exists by auto
}
ultimately show ?case using Exists_ctx.hyps
unfolding equiv_int_def by auto
next
case (Choose_ctx1 P C A' Q)
{
assume prov_dia (Choose_dia P (apply_ctx C A) A' Q)
from prov_dia_choose_inv[OF this]
have prov_dia (apply_ctx C A) and prov_dia A'
and equiv_int (top (apply_ctx C A)) P
and equiv_int (top A') P
and equiv_int (bot (apply_ctx C A)) Q
and equiv_int (bot A') Q
by auto
hence prov_dia (apply_ctx C B) and prov_dia A'
and equiv_int (top (apply_ctx C B)) P
and equiv_int (top A') P
and equiv_int (bot (apply_ctx C B)) Q
and equiv_int (bot A') Q
using Choose_ctx1.hyps unfolding equiv_int_def by auto
hence prov_dia (Choose_dia P (apply_ctx C B) A' Q)
using prov_dia.Choose by auto
}
moreover
{
assume prov_dia (Choose_dia P (apply_ctx C B) A' Q)
from prov_dia_choose_inv[OF this]
have prov_dia (apply_ctx C B) and prov_dia A'
and equiv_int (top (apply_ctx C B)) P
and equiv_int (top A') P
and equiv_int (bot (apply_ctx C B)) Q
and equiv_int (bot A') Q
by auto
hence prov_dia (apply_ctx C A) and prov_dia A'
and equiv_int (top (apply_ctx C A)) P
and equiv_int (top A') P
and equiv_int (bot (apply_ctx C A)) Q
and equiv_int (bot A') Q
using Choose_ctx1.hyps unfolding equiv_int_def by auto
hence prov_dia (Choose_dia P (apply_ctx C A) A' Q)
using prov_dia.Choose by auto
}
ultimately show ?case using Choose_ctx1.hyps
unfolding equiv_int_def by auto
next
case (Choose_ctx2 P A' C Q)
{
assume prov_dia (Choose_dia P A' (apply_ctx C A) Q)
from prov_dia_choose_inv[OF this]
have prov_dia (apply_ctx C A) and prov_dia A'
and equiv_int (top A') P
and equiv_int (top (apply_ctx C A)) P
and equiv_int (bot A') Q
and equiv_int (bot (apply_ctx C A)) Q
by auto
hence prov_dia (apply_ctx C B) and prov_dia A'
and equiv_int (top A') P
and equiv_int (top (apply_ctx C B)) P
and equiv_int (bot A') Q
and equiv_int (bot (apply_ctx C B)) Q
using Choose_ctx2.hyps unfolding equiv_int_def by auto
hence prov_dia (Choose_dia P A' (apply_ctx C B) Q)
using prov_dia.Choose by auto
}
moreover
{
assume prov_dia (Choose_dia P A' (apply_ctx C B) Q)
from prov_dia_choose_inv[OF this]
have prov_dia (apply_ctx C B) and prov_dia A'
and equiv_int (top A') P
and equiv_int (top (apply_ctx C B)) P
and equiv_int (bot A') Q
and equiv_int (bot (apply_ctx C B)) Q
by auto
hence prov_dia (apply_ctx C A) and prov_dia A'
and equiv_int (top A') P
and equiv_int (top (apply_ctx C A)) P
and equiv_int (bot A') Q
and equiv_int (bot (apply_ctx C A)) Q
using Choose_ctx2.hyps unfolding equiv_int_def by auto
hence prov_dia (Choose_dia P A' (apply_ctx C A) Q)
using prov_dia.Choose by auto
}
ultimately show ?case using Choose_ctx2.hyps
unfolding equiv_int_def by auto
next
case (Loop_ctx P C Q)
{
assume prov_dia (Loop_dia P (apply_ctx C A) Q)
from prov_dia_loop_inv[OF this]
have prov_dia (apply_ctx C A)
and equiv_int (top (apply_ctx C A)) P
and equiv_int (bot (apply_ctx C A)) P
and equiv_int Q P by auto
hence prov_dia (apply_ctx C B)
and equiv_int (top (apply_ctx C B)) P
and equiv_int (bot (apply_ctx C B)) P
and equiv_int Q P
using Loop_ctx.hyps unfolding equiv_int_def by auto
hence prov_dia (Loop_dia P (apply_ctx C B) Q)
using prov_dia.Loop by auto
}
moreover
{
assume prov_dia (Loop_dia P (apply_ctx C B) Q)
from prov_dia_loop_inv[OF this]
have prov_dia (apply_ctx C B)
and equiv_int (top (apply_ctx C B)) P
and equiv_int (bot (apply_ctx C B)) P
and equiv_int Q P by auto
hence prov_dia (apply_ctx C A)
and equiv_int (top (apply_ctx C A)) P
and equiv_int (bot (apply_ctx C A)) P
and equiv_int Q P
using Loop_ctx.hyps unfolding equiv_int_def by auto
hence prov_dia (Loop_dia P (apply_ctx C A) Q)
using prov_dia.Loop by auto
}
ultimately show ?case using Loop_ctx.hyps
unfolding equiv_int_def by auto
qed
next
case (hcomp_assoc A B C)
have prov_dia (HComp_dia A (HComp_dia B C))
= prov_dia (HComp_dia (HComp_dia A B) C)
proof(intro iffI)
assume prov_dia(HComp_dia A (HComp_dia B C))
hence prov_dia A and prov_dia (HComp_dia B C)
and disj_dia A (HComp_dia B C)
using prov_dia_hcomp_inv by auto
hence prov_dia A and prov_dia B and prov_dia C
and disj_dia (HComp_dia A B) C and disj_dia A B
using prov_dia_hcomp_inv unfolding disj_dia_def by auto
thus prov_dia(HComp_dia (HComp_dia A B) C)
using prov_dia.HComp by auto
next
assume prov_dia(HComp_dia (HComp_dia A B) C)
hence prov_dia (HComp_dia A B) and prov_dia C
and disj_dia (HComp_dia A B) C
using prov_dia_hcomp_inv by auto
hence prov_dia A and prov_dia B and prov_dia C
and disj_dia A (HComp_dia B C) and disj_dia B C
using prov_dia_hcomp_inv unfolding disj_dia_def by auto
thus prov_dia(HComp_dia A (HComp_dia B C))
using prov_dia.HComp by auto
qed
moreover have rd_dia (HComp_dia A (HComp_dia B C))
= rd_dia (HComp_dia (HComp_dia A B) C) by auto
moreover have wr_dia (HComp_dia A (HComp_dia B C))
= wr_dia (HComp_dia (HComp_dia A B) C) by auto
moreover have equiv_int (top (HComp_dia A (HComp_dia B C)))
(top (HComp_dia (HComp_dia A B) C)) unfolding equiv_int_def by auto
moreover have equiv_int (bot (HComp_dia A (HComp_dia B C)))
(bot (HComp_dia (HComp_dia A B) C)) unfolding equiv_int_def by auto
moreover have coms_list (HComp_dia A (HComp_dia B C))
= coms_list (HComp_dia (HComp_dia A B) C)
proof (intro set_eqI iffI)
fix C_ABC
assume C_ABC ∈ coms_list (HComp_dia A (HComp_dia B C))
hence ∃C_A C_BC. C_ABC ∈ C_A ⊗ C_BC ∧ C_A ∈ coms_list A
∧ C_BC ∈ (⋃ {C_B ⊗ C_C | C_B C_C . C_B ∈ coms_list B ∧ C_C ∈ coms_list C})
by (auto, blast)
hence ∃C_A C_B C_C C_AB. C_AB ∈ C_A ⊗ C_B ∧ C_ABC ∈ C_AB ⊗ C_C
∧ C_A ∈ coms_list A ∧ C_B ∈ coms_list B ∧ C_C ∈ coms_list C
using interleave_s_assoc by blast
thus C_ABC ∈ coms_list (HComp_dia (HComp_dia A B) C)
by (auto, blast)
next
fix C_ABC
assume C_ABC ∈ coms_list (HComp_dia (HComp_dia A B) C)
hence ∃C_AB C_C. C_ABC ∈ C_AB ⊗ C_C ∧
C_AB ∈ (⋃ {C_A ⊗ C_B | C_A C_B . C_A ∈ coms_list A ∧ C_B ∈ coms_list B})
∧ C_C ∈ coms_list C
by (auto, blast)
hence ∃C_A C_B C_C C_BC. C_BC ∈ C_B ⊗ C_C ∧ C_ABC ∈ C_A ⊗ C_BC
∧ C_A ∈ coms_list A ∧ C_B ∈ coms_list B ∧ C_C ∈ coms_list C
using interleave_s_assoc by blast
thus C_ABC ∈ coms_list (HComp_dia A (HComp_dia B C))
by (auto, blast)
qed
ultimately show ?case by auto
next
case (vcomp_assoc A B C)
have prov_dia(VComp_dia A (VComp_dia B C))
= prov_dia(VComp_dia (VComp_dia A B) C)
proof (intro iffI)
assume prov_dia(VComp_dia A (VComp_dia B C))
from prov_dia_vcomp_inv[OF this]
have prov_dia A and prov_dia (VComp_dia B C)
and equiv_int (bot A) (top (VComp_dia B C))
by auto
with prov_dia_vcomp_inv[OF this(2)]
have prov_dia A and prov_dia B and prov_dia C
and equiv_int (bot A) (top B)
and equiv_int (bot (VComp_dia A B)) (top C) by auto
thus prov_dia(VComp_dia (VComp_dia A B) C)
using prov_dia.VComp by auto
next
assume prov_dia(VComp_dia (VComp_dia A B) C)
from prov_dia_vcomp_inv[OF this]
have prov_dia (VComp_dia A B) and prov_dia C
and equiv_int (bot (VComp_dia A B)) (top C)
by auto
with prov_dia_vcomp_inv[OF this(1)]
have prov_dia A and prov_dia B and prov_dia C
and equiv_int (bot A) (top (VComp_dia B C))
and equiv_int (bot B) (top C) by auto
thus prov_dia(VComp_dia A (VComp_dia B C))
using prov_dia.VComp by auto
qed
moreover have rd_dia (VComp_dia A (VComp_dia B C))
= rd_dia (VComp_dia (VComp_dia A B) C) by auto
moreover have wr_dia (VComp_dia A (VComp_dia B C))
= wr_dia (VComp_dia (VComp_dia A B) C) by auto
moreover have equiv_int (top (VComp_dia A (VComp_dia B C)))
(top (VComp_dia (VComp_dia A B) C)) unfolding equiv_int_def by auto
moreover have equiv_int (bot (VComp_dia A (VComp_dia B C)))
(bot (VComp_dia (VComp_dia A B) C)) unfolding equiv_int_def by auto
moreover have coms_list (VComp_dia A (VComp_dia B C))
= coms_list (VComp_dia (VComp_dia A B) C)
proof(intro set_eqI)
fix C_ABC
have (∃C_A C_B C_C. C_ABC = (C_A @ C_B) @ C_C
∧ C_A ∈ coms_list A ∧ C_B ∈ coms_list B ∧ C_C ∈ coms_list C)
= (∃C_AB C_C. C_ABC = C_AB @ C_C ∧ (∃C_A C_B . C_AB = C_A @ C_B
∧ C_A ∈ coms_list A ∧ C_B ∈ coms_list B) ∧ C_C ∈ coms_list C)
by blast
thus (C_ABC ∈ coms_list (VComp_dia A (VComp_dia B C)))
= (C_ABC ∈ coms_list (VComp_dia (VComp_dia A B) C)) by auto
qed
ultimately show ?case by auto
next
case (hcomp_unit1 A)
have prov_dia (HComp_dia (Blank Emp_int) A) = prov_dia A
proof(intro iffI)
assume prov_dia (HComp_dia (Blank Emp_int) A)
thus prov_dia A using prov_dia_hcomp_inv by auto
next
assume prov_dia A
moreover have prov_dia (Blank Emp_int)
using prov_dia.Blank by auto
moreover have disj_dia (Blank Emp_int) A
unfolding disj_dia_def by auto
ultimately show prov_dia (HComp_dia (Blank Emp_int) A)
using prov_dia.HComp by auto
qed
moreover have rd_dia (HComp_dia (Blank Emp_int) A)
= rd_dia A by auto
moreover have wr_dia (HComp_dia (Blank Emp_int) A)
= wr_dia A by auto
moreover have equiv_int (top (HComp_dia (Blank Emp_int) A))
(top A) unfolding equiv_int_def by auto
moreover have equiv_int (bot (HComp_dia (Blank Emp_int) A))
(bot A) unfolding equiv_int_def by auto
moreover have coms_list (HComp_dia (Blank Emp_int) A)
= coms_list A by auto
ultimately show ?case by auto
next
case (hcomp_unit2 A)
have prov_dia (HComp_dia A (Blank Emp_int)) = prov_dia A
proof(intro iffI)
assume prov_dia (HComp_dia A (Blank Emp_int))
thus prov_dia A using prov_dia_hcomp_inv by auto
next
assume prov_dia A
moreover have prov_dia (Blank Emp_int)
using prov_dia.Blank by auto
moreover have disj_dia A (Blank Emp_int)
unfolding disj_dia_def by auto
ultimately show prov_dia (HComp_dia A (Blank Emp_int))
using prov_dia.HComp by auto
qed
moreover have rd_dia (HComp_dia A (Blank Emp_int))
= rd_dia A by auto
moreover have wr_dia (HComp_dia A (Blank Emp_int))
= wr_dia A by auto
moreover have equiv_int (top (HComp_dia A (Blank Emp_int)))
(top A) unfolding equiv_int_def by auto
moreover have equiv_int (bot (HComp_dia A (Blank Emp_int)))
(bot A) unfolding equiv_int_def by auto
moreover have coms_list (HComp_dia A (Blank Emp_int))
= coms_list A by auto
ultimately show ?case by auto
next
case (vcomp_unit1 A)
have prov_dia (VComp_dia (Blank (top A)) A) = prov_dia A
proof (intro iffI)
assume prov_dia (VComp_dia (Blank (top A)) A)
thus prov_dia A using prov_dia_vcomp_inv by auto
next
assume prov_dia A
moreover have prov_dia (Blank (top A))
using prov_dia.Blank by auto
moreover have equiv_int (bot (Blank (top A))) (top A)
unfolding equiv_int_def by auto
ultimately show prov_dia (VComp_dia (Blank (top A)) A)
using prov_dia.VComp by auto
qed
moreover have rd_dia (VComp_dia (Blank (top A)) A)
= rd_dia A by (induct A, auto)
moreover have wr_dia (VComp_dia (Blank (top A)) A)
= wr_dia A by auto
moreover have equiv_int (top (VComp_dia (Blank (top A)) A))
(top A) unfolding equiv_int_def by auto
moreover have equiv_int (bot (VComp_dia (Blank (top A)) A))
(bot A) unfolding equiv_int_def by auto
moreover have coms_list (VComp_dia (Blank (top A)) A)
= coms_list A by auto
ultimately show ?case by auto
next
case (vcomp_unit2 A)
have prov_dia (VComp_dia A (Blank (bot A))) = prov_dia A
proof (intro iffI)
assume prov_dia (VComp_dia A (Blank (bot A)))
thus prov_dia A using prov_dia_vcomp_inv by auto
next
assume prov_dia A
moreover have prov_dia (Blank (bot A))
using prov_dia.Blank by auto
moreover have equiv_int (bot A) (top (Blank (bot A)))
unfolding equiv_int_def by auto
ultimately show prov_dia (VComp_dia A (Blank (bot A)))
using prov_dia.VComp by auto
qed
moreover have rd_dia (VComp_dia A (Blank (bot A)))
= rd_dia A by (induct A, auto)
moreover have wr_dia (VComp_dia A (Blank (bot A)))
= wr_dia A by auto
moreover have equiv_int (top (VComp_dia A (Blank (bot A))))
(top A) unfolding equiv_int_def by auto
moreover have equiv_int (bot (VComp_dia A (Blank (bot A))))
(bot A) unfolding equiv_int_def by auto
moreover have coms_list (VComp_dia A (Blank (bot A)))
= coms_list A by auto
ultimately show ?case by auto
qed
}
from this[OF assms] and equiv_int_sound
have prov_dia A = prov_dia B and ass (top A) = ass (top B)
and ass (bot A) = ass (bot B) and coms A = coms B by auto
thus prov_dia A = prov_dia B ∧ sem_dia A = sem_dia B
unfolding sem_dia_def by auto
qed
The exchange law holds for equiprovability (but not semantic equivalence)
theorem exchange: fixes A B C D
assumes disj_dia A D and disj_dia B C
and equiv_int (bot A) (top C)
shows prov_dia (VComp_dia (HComp_dia A B) (HComp_dia C D))
= prov_dia (HComp_dia (VComp_dia A C) (VComp_dia B D))
proof(intro iffI)
assume prov_dia(VComp_dia (HComp_dia A B) (HComp_dia C D))
from prov_dia_vcomp_inv[OF this(1)]
have prov_dia(HComp_dia A B) and prov_dia(HComp_dia C D)
and equiv_int (bot (HComp_dia A B)) (top (HComp_dia C D)) by auto
hence prov_dia A and prov_dia B and disj_dia A B
and prov_dia C and prov_dia D and disj_dia C D
and equiv_int (bot A) (top C) and equiv_int (bot B) (top D)
using prov_dia_hcomp_inv assms(3) unfolding equiv_int_def by auto
hence prov_dia (VComp_dia A C) and prov_dia (VComp_dia B D)
and disj_dia (VComp_dia A C) (VComp_dia B D)
using prov_dia.VComp assms(1) assms(2)
unfolding disj_dia_def by auto
thus prov_dia (HComp_dia (VComp_dia A C) (VComp_dia B D))
using prov_dia.HComp by auto
next
assume prov_dia (HComp_dia (VComp_dia A C) (VComp_dia B D))
from prov_dia_hcomp_inv[OF this]
have prov_dia (VComp_dia A C) and prov_dia (VComp_dia B D)
and disj_dia (VComp_dia A C) (VComp_dia B D) by auto
with prov_dia_vcomp_inv
have prov_dia A and prov_dia C and prov_dia B
and prov_dia D and equiv_int (bot A) (top C)
and equiv_int (bot B) (top D)
and disj_dia A B and disj_dia C D
unfolding disj_dia_def by auto
thus prov_dia (VComp_dia (HComp_dia A B) (HComp_dia C D))
using prov_dia.VComp and prov_dia.HComp
unfolding equiv_int_def by auto
qed
end
