theory Ribbons_Completeness imports
Ribbons_Graphical
begin
text {* We prove that the proof rules defined in ribbons_graphical.thy are complete with respect to the rules of separation logic defined in ribbons_basic.thy. *}
theorem completeness:
fixes p c q
assumes "prov_triple (p,c,q)"
shows "\G P Q. wf_dia G \ coms_dia G c \ p = ass P \ q = ass Q \ prov_dia G P Q" (is "\G P Q. ?\ G P Q")
proof -
let ?V = "[v01,v02]"
let ?\ = "(\v. Rib Emp) (v01 := Rib p, v02 := Rib q)"
let ?E = "[([v01], Com c, [v02])]"
let ?G = "Graph ?V ?\ ?E"
let ?P = "Emp_int \ Ribbon p"
let ?Q = "Emp_int \ Ribbon q"
let ?\ = "[Inl v01, Inr ([v01], Com c, [v02]), Inl v02]"
have "coms_dia ?G c"
proof -
have "coms_dia ?G (foldr (op ;;) [Skip, c, Skip] Skip)"
proof (rule coms_main [where \ = ?\])
have yiecn: "distinct [Inl v01, Inr ([v01], Com c, [v02]), Inl v02]" by auto
show "?\ \ lins ?G"
proof (unfold lins.simps[of ?V ?\ ?E], intro CollectI conjI, simp)
show "set [Inl v01, Inr ([v01], Com c, [v02]), Inl v02] =
Inl ` set [v01, v02] \ Inr ` set [([v01], Com c, [v02])]"
by auto
next
show "\i j v e.
i < length [Inl v01, Inr ([v01], Com c, [v02]), Inl v02] \
j < length [Inl v01, Inr ([v01], Com c, [v02]), Inl v02] \
[Inl v01, Inr ([v01], Com c, [v02]), Inl v02] ! i = Inl v \
[Inl v01, Inr ([v01], Com c, [v02]), Inl v02] ! j = Inr e \
v \ set (fst3 e) \ i < j"
proof (intro allI impI, elim conjE)
fix i j v e
assume
axvgk: "i < length ?\" and
snuyc: "j < length ?\" and
bwrsk: "?\ ! i = Inl v" and
irnle: "?\ ! j = Inr e" and
lpfbk: "v \ set (fst3 e)"
from nth_in_set [OF snuyc irnle] have
lsdkf: "e = ([v01], Com c, [v02])" by auto
with lpfbk have cxtvo: "v = v01" unfolding fst3_def by auto
have "i=0"
proof (rule ccontr)
assume xiznn: "i \ 0"
have gocuj: "0 < length ?\" by auto
from distinct_conv_nth[of "?\"] yiecn have
"\i j.\ i ; j ; i \ j \ \ ?\ ! i \ ?\ ! j"
by auto
from this[OF axvgk gocuj xiznn] and bwrsk and cxtvo show
False by auto
qed
moreover have "j=1"
proof (rule ccontr)
assume xiznn: "j \ 1"
have gocuj: "1 < length ?\" by auto
from distinct_conv_nth[of "?\"] yiecn have
"\i j.\ i ; j ; i \ j \ \ ?\ ! i \ ?\ ! j"
by auto
from this[OF snuyc gocuj xiznn] and irnle and lsdkf show
False by auto
qed
ultimately show "i < j" by auto
qed
next
show "\j k w e.
j < length [Inl v01, Inr ([v01], Com c, [v02]), Inl v02] \
k < length [Inl v01, Inr ([v01], Com c, [v02]), Inl v02] \
[Inl v01, Inr ([v01], Com c, [v02]), Inl v02] ! j = Inr e \
[Inl v01, Inr ([v01], Com c, [v02]), Inl v02] ! k = Inl w \
w \ set (thd3 e) \ j < k"
proof (intro allI impI, elim conjE)
fix j k w e
assume
snuyc: "j < length ?\" and
rldms: "k < length ?\" and
irnle: "?\ ! j = Inr e" and
nthqn: "?\ ! k = Inl w" and
hfmli: "w \ set (thd3 e)"
from nth_in_set [OF snuyc irnle] have
lsdkf: "e = ([v01], Com c, [v02])" by auto
with hfmli have qtxuv: "w = v02" unfolding thd3_def by auto
have "j=1"
proof (rule ccontr)
assume xiznn: "j \ 1"
have gocuj: "1 < length ?\" by auto
from distinct_conv_nth[of "?\"] yiecn have
"\i j.\ i ; j ; i \ j \ \ ?\ ! i \ ?\ ! j"
by auto
from this[OF snuyc gocuj xiznn] and irnle and lsdkf show
False by auto
qed
moreover have "k=2"
proof (rule ccontr)
assume xiznn: "k \ 2"
have gocuj: "2 < length ?\" by auto
from distinct_conv_nth[of "?\"] yiecn have
"\i j.\ i ; j ; i \ j \ \ ?\ ! i \ ?\ ! j"
by auto
from this[OF rldms gocuj xiznn] and nthqn and qtxuv show
False by auto
qed
ultimately show "j < k" by auto
qed
qed
next
show "length [Skip, c, Skip] =
length [Inl v01, Inr ([v01], Com c, [v02]), Inl v02]"
by auto
next
fix i
assume
ukhof: "i < length ?\" and
wfzta: "\v. ?\ ! i = Inl v"
have "i = 0 \ i = 2"
proof (rule ccontr)
assume "\ (i = 0 \ i = 2)"
with ukhof have "i=1" by auto
hence "?\ ! i = Inr ([v01], Com c, [v02])" by auto
with wfzta show False by auto
qed
hence "(?\ ! i = Inl v01) \ (?\ ! i = Inl v02)"
and "[Skip, c, Skip] ! i = Skip" by auto
moreover have "coms_ass (Rib p) Skip" and
"coms_ass (Rib q) Skip" using coms_skip by auto
ultimately show
"coms_ass (?\ (Sum_Type.Projl (?\ ! i))) ([Skip, c, Skip] ! i)"
by auto
next
fix i
assume
ukhof: "i < length ?\" and
wfzta: "\e. ?\ ! i = Inr e"
have "i = 1"
proof (rule ccontr)
assume "\ (i = 1)"
with ukhof have "i=0 \ i=2" by auto
hence "?\ ! i = Inl v01 \ ?\ ! i = Inl v02" by auto
with wfzta show False by auto
qed
hence ncdef: "?\ ! i = Inr ([v01], Com c, [v02])"
and "[Skip, c, Skip] ! i = c" by auto
moreover have "coms_com (Com c) c" using coms_basic by auto
ultimately show
"coms_com (snd3 (Sum_Type.Projr (?\ ! i)))
([Skip, c, Skip] ! i)"
unfolding ncdef unfolding snd3_def by auto
qed
moreover have
"c = foldr (op ;;) [Skip, c, Skip] Skip"
using seq_skip skip_seq by auto
ultimately show "coms_dia ?G c" by auto
qed
moreover have "p = ass ?P" and "q = ass ?Q"
by (auto simp add: emp_star)
moreover have bivui: "wf_dia ?G"
proof
show "acyclicity ?E"
by (unfold acyclicity_def, auto simp add: fst3_def thd3_def, unfold acyclic_def, auto)
next
show "linearity ?E" by (unfold linearity_def, auto)
qed (auto simp add: fst3_def thd3_def)
moreover have "prov_dia ?G ?P ?Q"
proof -
have "?P = top_dia ?G" by (auto simp add: fst3_def thd3_def)
moreover have "?Q = bot_dia ?G" by (auto simp add: fst3_def thd3_def)
moreover have "prov_dia ?G (top_dia ?G) (bot_dia ?G)"
by (rule Main, auto simp add: Skip Basic emp_star assms fst3_def snd3_def thd3_def bivui)
ultimately show "prov_dia ?G ?P ?Q" by auto
qed
ultimately show "\G P Q. wf_dia G \ coms_dia G c \ p = ass P \ q = ass Q \ prov_dia G P Q"
using exI3[of "?\" "?G" "?P" "?Q"] by auto
qed
end