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