section ‹The Rely-guarantee Proof System of PiCore and its Soundness›
theory PiCore_Hoare
imports PiCore_Validity List_Lemmata
begin
subsection ‹Proof System for Programs›
definition stable :: "'a set ⇒ ('a × 'a) set ⇒ bool" where
"stable P R ≡ ∀s s'. s ∈ P ⟶ (s, s') ∈ R ⟶ s' ∈ P"
subsection ‹Rely-guarantee Condition›
locale event_hoare = event_validity ptran fin_com prog_validity
for ptran :: "'Env ⇒ (('prog × 's) × 'prog × 's) set"
and fin_com :: "'prog"
and prog_validity :: "'Env ⇒ 'prog ⇒ 's set ⇒ ('s × 's) set ⇒ ('s × 's) set ⇒ 's set ⇒ bool"
("_ ⊨ _ sat⇩p [_, _, _, _]" [60,60,0,0,0,0] 45)
+
fixes rghoare_p :: "'Env ⇒ ['prog, 's set, ('s × 's) set, ('s × 's) set, 's set] ⇒ bool"
("_ ⊢ _ sat⇩p [_, _, _, _]" [60,60,0,0,0,0] 45)
assumes rgsound_p: "Γ ⊢ P sat⇩p [pre, rely, guar, post] ⟹ Γ ⊨ P sat⇩p [pre, rely, guar, post]"
begin
lemma stable_lift:
‹stable P R ⟹ stable (lift_state_set P) (lift_state_pair_set R)›
by (simp add: lift_state_set_def lift_state_pair_set_def stable_def)
subsection ‹Proof System for Events›
lemma estran_anon_inv:
assumes ‹((EAnon p,s,x), (EAnon q,t,y))∈estran Γ›
shows ‹((p,s), (q,t))∈ptran Γ›
using assms apply-
apply(simp add: estran_def)
apply(erule exE)
apply(erule estran_p.cases, auto)
done
lemma unlift_cpt:
assumes ‹cpt ∈ cpts_from (estran Γ) (EAnon p0, s0, x0)›
shows ‹unlift_cpt cpt ∈ cpts_from (ptran Γ) (p0, s0)›
using assms
proof(auto)
assume a1: ‹cpt ∈ cpts (estran Γ)›
assume a2: ‹hd cpt = (EAnon p0, s0, x0)›
show ‹map (λ(p, s, _). (unlift_prog p, s)) cpt ∈ cpts (ptran Γ)›
using a1 a2
proof(induct arbitrary:p0 s0 x0)
case (CptsOne P s)
then show ?case by auto
next
case (CptsEnv P T cs S)
obtain t y where T: ‹T=(t,y)› by fastforce
from CptsEnv(3) T have ‹hd ((P,T)#cs) = (EAnon p0, t, y)› by simp
from CptsEnv(2)[OF this] have ‹map (λa. case a of (p, s, _) ⇒ (unlift_prog p, s)) ((P, T) # cs) ∈ cpts (ptran Γ)› .
then show ?case by (auto simp add: case_prod_unfold)
next
case (CptsComp P S Q T cs)
from CptsComp(4) have P: ‹P = EAnon p0› by simp
obtain q where ptran: ‹((p0,fst S),(q,fst T))∈ptran Γ› and Q: ‹Q = EAnon q›
proof-
assume a: ‹⋀q. ((p0, fst S), q, fst T) ∈ ptran Γ ⟹ Q = EAnon q ⟹ thesis›
show thesis
using CptsComp(1) apply(simp add: P estran_def)
apply(erule exE)
apply(erule estran_p.cases, auto)
apply(rule a) apply simp+
by (simp add: a)
qed
obtain t y where T: ‹T=(t,y)› by fastforce
have ‹hd ((Q, T) # cs) = (EAnon q, t, y)› by (simp add: Q T)
from CptsComp(3)[OF this] have *: ‹map (λa. case a of (p, s, uu_) ⇒ (unlift_prog p, s)) ((Q, T) # cs) ∈ cpts (ptran Γ)› .
show ?case
apply(simp add: case_prod_unfold)
apply(rule cpts.CptsComp)
using ptran Q apply(simp add: P)
using * by (simp add: case_prod_unfold)
qed
next
assume a1: ‹cpt ∈ cpts (estran Γ)›
assume a2: ‹hd cpt = (EAnon p0, s0, x0)›
show ‹hd (map (λ(p, s, _). (unlift_prog p, s)) cpt) = (p0, s0)›
by (simp add: hd_map[OF cpts_nonnil[OF a1]] case_prod_unfold a2)
qed
theorem Anon_sound:
assumes h: ‹Γ ⊢ p sat⇩p [pre, rely, guar, post]›
shows ‹Γ ⊨ EAnon p sat⇩e [pre, rely, guar, post]›
proof-
from h have "Γ ⊨ p sat⇩p [pre, rely, guar, post]" using rgsound_p by blast
then have ‹validity (ptran Γ) {fin_com} p pre rely guar post› using prog_validity_def by simp
then have p_valid[rule_format]: ‹∀S0. cpts_from (ptran Γ) (p,S0) ∩ assume pre rely ⊆ commit (ptran Γ) {fin_com} guar post› using validity_def by fast
let ?pre = ‹lift_state_set pre›
let ?rely = ‹lift_state_pair_set rely›
let ?guar = ‹lift_state_pair_set guar›
let ?post = ‹lift_state_set post›
have ‹∀S0. cpts_from (estran Γ) (EAnon p, S0) ∩ assume ?pre ?rely ⊆ commit (estran Γ) {EAnon fin_com} ?guar ?post›
proof
fix S0
show ‹cpts_from (estran Γ) (EAnon p, S0) ∩ assume ?pre ?rely ⊆ commit (estran Γ) {EAnon fin_com} ?guar ?post›
proof
fix cpt
assume h1: ‹cpt ∈ cpts_from (estran Γ) (EAnon p, S0) ∩ assume ?pre ?rely›
from h1 have cpt: ‹cpt ∈ cpts_from (estran Γ) (EAnon p, S0)› by blast
then have ‹cpt ∈ cpts (estran Γ)› by simp
from h1 have cpt_assume: ‹cpt ∈ assume ?pre ?rely› by blast
have cpt_unlift: ‹unlift_cpt cpt ∈ cpts_from (ptran Γ) (p, fst S0) ∩ assume pre rely›
proof
show ‹unlift_cpt cpt ∈ cpts_from (ptran Γ) (p, fst S0)›
using unlift_cpt cpt surjective_pairing by metis
next
from cpt_assume have ‹snd (hd (map (λ(p, s, _). (unlift_prog p, s)) cpt)) ∈ pre›
by (auto simp add: assume_def hd_map[OF cpts_nonnil[OF ‹cpt ∈ cpts (estran Γ)›]] case_prod_unfold lift_state_set_def)
then show ‹unlift_cpt cpt ∈ assume pre rely›
using h1
apply(auto simp add: assume_def case_prod_unfold)
apply(erule_tac x=i in allE)
apply(simp add: lift_state_pair_set_def case_prod_unfold)
by (metis (mono_tags, lifting) Suc_lessD cpt cpts_from_anon' fst_conv unlift_prog.simps)
qed
with p_valid have unlift_commit: ‹unlift_cpt cpt ∈ commit (ptran Γ) {fin_com} guar post› by blast
show "cpt ∈ commit (estran Γ) {EAnon fin_com} ?guar ?post"
proof(auto simp add: commit_def)
fix i
assume a1: ‹Suc i < length cpt›
assume estran: ‹(cpt ! i, cpt ! Suc i) ∈ estran Γ›
from cpts_from_anon'[OF cpt, rule_format, OF a1[THEN Suc_lessD]]
obtain p1 s1 x1 where 1: ‹cpt!i = (EAnon p1,s1,x1)› by blast
from cpts_from_anon'[OF cpt, rule_format, OF a1]
obtain p2 s2 x2 where 2: ‹cpt!Suc i = (EAnon p2,s2,x2)› by blast
from estran have ‹((p1,s1), (p2,s2)) ∈ ptran Γ›
using 1 2 estran_anon_inv by fastforce
then have ‹(unlift_conf (cpt!i), unlift_conf (cpt!Suc i)) ∈ ptran Γ›
by (simp add: 1 2)
then have ‹(fst (snd (cpt!i)), fst (snd (cpt!Suc i))) ∈ guar› using unlift_commit
apply(simp add: commit_def case_prod_unfold)
apply clarify
apply(erule allE[where x=i])
using a1 by blast
then show ‹(snd (cpt ! i), snd (cpt ! Suc i)) ∈ lift_state_pair_set guar›
by (simp add: lift_state_pair_set_def case_prod_unfold)
next
assume a1: ‹fst (last cpt) = fin›
from cpt cpts_nonnil have ‹cpt≠[]› by auto
have ‹fst (last (map (λp. (unlift_prog (fst p), fst (snd p))) cpt)) = fin_com›
by (simp add: last_map[OF ‹cpt≠[]›] a1)
then have ‹snd (last (map (λp. (unlift_prog (fst p), fst (snd p))) cpt)) ∈ post› using unlift_commit
by (simp add: commit_def case_prod_unfold)
then show ‹snd (last cpt) ∈ lift_state_set post›
by (simp add: last_map[OF ‹cpt≠[]›] lift_state_set_def case_prod_unfold)
qed
qed
qed
then have ‹validity (estran Γ) {EAnon fin_com} (EAnon p) ?pre ?rely ?guar ?post›
by (subst validity_def, assumption)
then show ?thesis
by (subst es_validity_def, assumption)
qed
type_synonym 'a tran = ‹'a × 'a›
inductive_cases estran_from_basic: ‹Γ ⊢ (EBasic ev, s) ─es[a]→ (es, t)›
lemma assume_tl_comp:
‹(P, s) # (P, t) # cs ∈ assume pre rely ⟹
stable pre rely ⟹
(P, t) # cs ∈ assume pre rely›
apply (simp add: assume_def)
apply clarify
apply(rule conjI)
apply(erule_tac x=0 in allE)
apply(simp add: stable_def)
apply auto
done
lemma assume_tl_env:
assumes ‹(P,s)#(Q,s)#cs ∈ assume pre rely›
shows ‹(Q,s)#cs ∈ assume pre rely›
using assms
apply(clarsimp simp add: assume_def)
apply(erule_tac x=‹Suc i› in allE)
by auto
lemma Basic_sound:
assumes h: ‹Γ ⊢ body (ev::('l,'s,'prog)event) sat⇩p [pre ∩ guard ev, rely, guar, post]›
and stable: ‹stable pre rely›
and guar_refl: ‹∀s. (s, s) ∈ guar›
shows ‹Γ ⊨ EBasic ev sat⇩e [pre, rely, guar, post]›
proof-
let ?pre = ‹lift_state_set pre›
let ?rely = ‹lift_state_pair_set rely›
let ?guar = ‹lift_state_pair_set guar›
let ?post = ‹lift_state_set post›
from stable have stable': ‹stable ?pre ?rely›
by (simp add: lift_state_set_def lift_state_pair_set_def stable_def)
from h Anon_sound have
‹Γ ⊨ EAnon (body ev) sat⇩e [pre ∩ guard ev, rely, guar, post]› by blast
then have es_valid:
‹∀S0. cpts_from (estran Γ) (EAnon (body ev), S0) ∩ assume (lift_state_set (pre ∩ guard ev)) ?rely ⊆ commit (estran Γ) {fin} ?guar ?post›
using es_validity_def by (simp)
have ‹∀S0. cpts_from (estran Γ) (EBasic ev, S0) ∩ assume ?pre ?rely ⊆ commit (estran Γ) {fin} ?guar ?post›
proof
fix S0
show ‹cpts_from (estran Γ) (EBasic ev, S0) ∩ assume ?pre ?rely ⊆ commit (estran Γ) {fin} ?guar ?post›
proof
fix cpt
assume cpt: ‹cpt ∈ cpts_from (estran Γ) (EBasic ev, S0) ∩ assume ?pre ?rely›
then have cpt_nonnil: ‹cpt ≠ []› using cpts_nonnil by auto
then have cpt_Cons: "cpt = hd cpt # tl cpt" using hd_Cons_tl by simp
let ?c0 = "hd cpt"
from cpt have fst_c0: "fst (hd cpt) = EBasic ev" by auto
from cpt have cpt1: ‹cpt ∈ cpts_from (estran Γ) (EBasic ev, S0)› by blast
then have cpt1_1: ‹cpt ∈ cpts (estran Γ)› using cpts_from_def by blast
from cpt have cpt_assume: ‹cpt ∈ assume ?pre ?rely› by blast
show ‹cpt ∈ commit (estran Γ) {fin} ?guar ?post›
using cpt1_1 cpt
proof(induct arbitrary:S0)
case (CptsOne P S)
then have ‹(P,S) = (EBasic ev, S0)› by simp
then show ?case by (simp add: commit_def)
next
case (CptsEnv P T cs S)
from CptsEnv(3) have P_s:
‹(P,S) = (EBasic ev, S0)› by simp
from CptsEnv(3) have
‹(P, S) # (P, T) # cs ∈ assume ?pre ?rely› by blast
with assume_tl_comp stable' have assume':
‹(P,T)#cs ∈ assume ?pre ?rely› by fast
have ‹(P, T) # cs ∈ cpts_from (estran Γ) (EBasic ev, T)› using CptsEnv(1) P_s by simp
with assume' have ‹(P, T) # cs ∈ cpts_from (estran Γ) (EBasic ev, T) ∩ assume ?pre ?rely› by blast
with CptsEnv(2) have ‹(P, T) # cs ∈ commit (estran Γ) {fin} ?guar ?post› by blast
then show ?case using commit_Cons_env_es by blast
next
case (CptsComp P S Q T cs)
obtain s0 x0 where S0: ‹S0=(s0,x0)› by fastforce
obtain s x where S: ‹S=(s,x)› by fastforce
obtain t y where T: ‹T=(t,y)› by fastforce
from CptsComp(4) have P_s:
‹(P,S) = (EBasic ev, S0)› by simp
from CptsComp(4) have
‹(P, S) # (Q, T) # cs ∈ assume ?pre ?rely› by blast
then have pre:
‹snd (hd ((P,S)#(Q,T)#cs)) ∈ ?pre›
and rely:
‹∀i. Suc i < length ((P,S)#(Q,T)#cs) ⟶
(((P,S)#(Q,T)#cs)!i ─e→ ((P,S)#(Q,T)#cs)!(Suc i)) ⟶
(snd (((P,S)#(Q,T)#cs)!i), snd (((P,S)#(Q,T)#cs)!Suc i)) ∈ ?rely›
using assume_def by blast+
from pre have ‹S ∈ ?pre› by simp
then have ‹s∈pre› by (simp add: lift_state_set_def S)
from CptsComp(1) have ‹∃a k. Γ ⊢ (P,S) ─es[a♯k]→ (Q,T)›
apply(simp add: estran_def)
apply(erule exE) apply(rule_tac x=‹Act a› in exI) apply(rule_tac x=‹K a› in exI)
apply(subst(asm) actk_destruct) by assumption
then obtain a k where ‹Γ ⊢ (P,S) ─es[a♯k]→ (Q,T)› by blast
with P_s have tran: ‹Γ ⊢ (EBasic ev, S0) ─es[a♯k]→ (Q,T)› by simp
then have a: ‹a = EvtEnt ev› apply- apply(erule estran_from_basic) apply simp done
from tran have guard: ‹s0 ∈ guard ev› apply- apply(erule estran_from_basic) apply (simp add: S0) done
from tran have "s0=t" apply- apply(erule estran_from_basic) using a guard apply (simp add: T S0) done
with P_s S S0 have "s=t" by simp
with guar_refl have guar: ‹(s, t) ∈ guar› by simp
have ‹(Q,T)#cs ∈ cpts_from (estran Γ) (EAnon (body ev), T)›
proof-
have "(Q,T)#cs ∈ cpts (estran Γ)" by (rule CptsComp(2))
moreover have "Q = EAnon (body ev)" using estran_from_basic using tran by blast
ultimately show ?thesis by auto
qed
moreover have ‹(Q,T)#cs ∈ assume (lift_state_set (pre ∩ guard ev)) ?rely›
proof-
have ‹fst (snd (hd ((Q,T)#cs))) ∈ (pre ∩ guard ev)›
proof
show ‹fst (snd (hd ((Q, T) # cs))) ∈ pre› using ‹s=t› ‹s∈pre› T by simp
next
show ‹fst (snd (hd ((Q, T) # cs))) ∈ guard ev› using ‹s0=t› guard T by fastforce
qed
then have ‹snd (hd ((Q,T)#cs)) ∈ lift_state_set (pre ∩ guard ev)› using lift_state_set_def by fastforce
moreover have
‹∀i. Suc i < length ((Q,T)#cs) ⟶ (((Q,T)#cs)!i ─e→ ((Q,T)#cs)!(Suc i)) ⟶ (snd (((Q,T)#cs)!i), snd (((Q,T)#cs)!Suc i)) ∈ ?rely›
using rely by auto
ultimately show ?thesis using assume_def by blast
qed
ultimately have ‹(Q,T)#cs ∈ cpts_from (estran Γ) (EAnon (body ev), T) ∩ assume (lift_state_set (pre ∩ guard ev)) ?rely› by blast
then have ‹(Q,T)#cs ∈ commit (estran Γ) {fin} ?guar ?post› using es_valid by blast
then show ?case using commit_Cons_comp CptsComp(1) guar S T lift_state_set_def lift_state_pair_set_def by fast
qed
qed
qed
then show ?thesis by simp
qed
inductive_cases estran_from_atom: ‹Γ ⊢ (EAtom ev, s) ─es[a]→ (Q, t)›
lemma estran_from_atom':
assumes h: ‹Γ ⊢ (EAtom ev, s,x) ─es[a♯k]→ (Q, t,y)›
shows ‹a = AtomEvt ev ∧ s ∈ guard ev ∧ Γ ⊢ (body ev, s) ─c*→ (fin_com, t) ∧ Q = EAnon fin_com›
using h estran_from_atom by blast
lemma last_sat_post:
assumes t: ‹t ∈ post›
and cpt: "cpt = (Q,t)#cs"
and etran: ‹∀i. Suc i < length cpt ⟶ cpt!i ─e→ cpt!Suc i›
and stable: ‹stable post rely›
and rely: ‹∀i. Suc i < length cpt ⟶ (cpt!i ─e→ cpt!Suc i) ⟶ (snd (cpt!i), snd (cpt!Suc i)) ∈ rely›
shows ‹snd (last cpt) ∈ post›
proof-
from etran rely have rely':
‹∀i. Suc i < length cpt ⟶ (snd (cpt!i), snd (cpt!Suc i)) ∈ rely› by auto
show ?thesis using cpt rely'
proof(induct cs arbitrary:cpt rule:rev_induct)
case Nil
then show ?case using t by simp
next
case (snoc x xs)
have
‹∀i. Suc i < length ((Q,t)#xs) ⟶ (snd (((Q,t)#xs) ! i), snd (((Q,t)#xs) ! Suc i)) ∈ rely›
proof
fix i
show ‹Suc i < length ((Q,t)#xs) ⟶ (snd (((Q,t)#xs) ! i), snd (((Q,t)#xs) ! Suc i)) ∈ rely›
proof
assume Suc_i_lt: ‹Suc i < length ((Q,t)#xs)›
then have eq1:
"((Q,t)#xs)!i = cpt!i" using snoc(2)
by (metis Suc_lessD butlast.simps(2) nth_butlast snoc_eq_iff_butlast)
from Suc_i_lt snoc(2) have eq2:
"((Q,t)#xs)!Suc i = cpt!Suc i"
by (simp add: nth_append)
have ‹(snd (cpt ! i), snd (cpt ! Suc i)) ∈ rely›
using Suc_i_lt snoc.prems(1) snoc.prems(2) by auto
then show ‹(snd (((Q,t)#xs) ! i), snd (((Q,t)#xs) ! Suc i)) ∈ rely› using eq1 eq2 by simp
qed
qed
then have last_post: ‹snd (last ((Q, t) # xs)) ∈ post›
using snoc.hyps by blast
have ‹(snd (last ((Q,t)#xs)), snd x) ∈ rely› using snoc(2,3)
by (metis List.nth_tl append_butlast_last_id append_is_Nil_conv butlast.simps(2) butlast_snoc length_Cons length_append_singleton lessI list.distinct(1) list.sel(3) nth_append_length nth_butlast)
with last_post stable
have "snd x ∈ post" by (simp add: stable_def)
then show ?case using snoc(2) by simp
qed
qed
lemma Atom_sound:
assumes h: ‹∀V. Γ ⊢ body (ev::('l,'s,'prog)event) sat⇩p [pre ∩ guard ev ∩ {V}, Id, UNIV, {s. (V,s)∈guar} ∩ post]›
and stable_pre: ‹stable pre rely›
and stable_post: ‹stable post rely›
shows ‹Γ ⊨ EAtom ev sat⇩e [pre, rely, guar, post]›
proof-
let ?pre = ‹lift_state_set pre›
let ?rely = ‹lift_state_pair_set rely›
let ?guar = ‹lift_state_pair_set guar›
let ?post = ‹lift_state_set post›
from stable_pre have stable_pre': ‹stable ?pre ?rely›
by (simp add: lift_state_set_def lift_state_pair_set_def stable_def)
from stable_post have stable_post': ‹stable ?post ?rely›
by (simp add: lift_state_set_def lift_state_pair_set_def stable_def)
from h rgsound_p have
‹∀V. Γ ⊨ (body ev) sat⇩p [pre ∩ guard ev ∩ {V}, Id, UNIV, {s. (V,s)∈guar} ∩ post]› by blast
then have body_valid:
‹∀V s0. cpts_from (ptran Γ) ((body ev), s0) ∩ assume (pre ∩ guard ev ∩ {V}) Id ⊆ commit (ptran Γ) {fin_com} UNIV ({s. (V,s)∈guar} ∩ post)›
using prog_validity_def by (meson validity_def)
have ‹∀s0. cpts_from (estran Γ) (EAtom ev, s0) ∩ assume ?pre ?rely ⊆ commit (estran Γ) {fin} ?guar ?post›
proof
fix S0
show ‹cpts_from (estran Γ) (EAtom ev, S0) ∩ assume ?pre ?rely ⊆ commit (estran Γ) {fin} ?guar ?post›
proof
fix cpt
assume cpt: ‹cpt ∈ cpts_from (estran Γ) (EAtom ev, S0) ∩ assume ?pre ?rely›
then have cpt1: ‹cpt ∈ cpts_from (estran Γ) (EAtom ev, S0)› by blast
then have cpt1_1: ‹cpt ∈ cpts (estran Γ)› by simp
from cpt1 have "hd cpt = (EAtom ev, S0)" by fastforce
show ‹cpt ∈ commit (estran Γ) {fin} ?guar ?post›
using cpt1_1 cpt
proof(induct arbitrary:S0)
case (CptsOne P S)
then show ?case by (simp add: commit_def)
next
case (CptsEnv P T cs S)
have ‹(P, T) # cs ∈ cpts_from (estran Γ) (EAtom ev, T) ∩ assume ?pre ?rely›
proof
from CptsEnv(3) have ‹(P, S) # (P, T) # cs ∈ cpts_from (estran Γ) (EAtom ev, S0)› by blast
then show ‹(P, T) # cs ∈ cpts_from (estran Γ) (EAtom ev, T)›
using CptsEnv.hyps(1) by auto
next
from CptsEnv(3) have ‹(P, S) # (P, T) # cs ∈ assume ?pre ?rely› by blast
with assume_tl_comp stable_pre' show ‹(P, T) # cs ∈ assume ?pre ?rely› by fast
qed
then have ‹(P, T) # cs ∈ commit (estran Γ) {fin} ?guar ?post› using CptsEnv(2) by blast
then show ?case using commit_Cons_env_es by blast
next
case (CptsComp P S Q T cs)
obtain s0 x0 where S0: ‹S0=(s0,x0)› by fastforce
obtain s x where S: ‹S=(s,x)› by fastforce
obtain t y where T: ‹T=(t,y)› by fastforce
from CptsComp(1) have ‹∃a k. Γ ⊢ (P,S) ─es[a♯k]→ (Q,T)›
apply- apply(simp add: estran_def) apply(erule exE) apply(rule_tac x=‹Act a› in exI) apply(rule_tac x=‹K a› in exI)
apply(subst (asm) actk_destruct) by assumption
then obtain a k where "Γ ⊢ (P,S) ─es[a♯k]→ (Q,T)" by blast
moreover from CptsComp(4) have P_s: "(P,S) = (EAtom ev, S0)" by force
ultimately have tran: ‹Γ ⊢ (EAtom ev, S0) ─es[a♯k]→ (Q,T)› by simp
then have tran_inv:
"a = AtomEvt ev ∧ s0 ∈ guard ev ∧ Γ ⊢ (body ev, s0) ─c*→ (fin_com, t) ∧ Q = EAnon fin_com"
using estran_from_atom' S0 T by fastforce
from tran_inv have Q: ‹Q = EAnon fin_com› by blast
from CptsComp(4) have "assume": ‹(P, S) # (Q, T) # cs ∈ assume ?pre ?rely› by blast
from "assume" have assume1: ‹snd (hd ((P,S)#(Q,T)#cs)) ∈ ?pre› using assume_def by blast
then have ‹S ∈ ?pre› by simp
then have ‹s∈pre› by (simp add: lift_state_set_def S)
then have ‹s0 ∈ pre› using P_s S0 S by simp
have ‹s0 ∈ guard ev› using tran_inv by blast
have ‹S0 ∈ {S0}› by simp
from "assume" have assume2:
‹∀i. Suc i < length ((P,S)#(Q,T)#cs) ⟶ (((P,S)#(Q,T)#cs)!i ─e→ ((P,S)#(Q,T)#cs)!(Suc i)) ⟶ (snd (((P,S)#(Q,T)#cs)!i), snd (((P,S)#(Q,T)#cs)!Suc i)) ∈ ?rely›
using assume_def by blast
then have assume2_tl:
‹∀i. Suc i < length ((Q,T)#cs) ⟶ (((Q,T)#cs)!i ─e→ ((Q,T)#cs)!(Suc i)) ⟶ (snd (((Q,T)#cs)!i), snd (((Q,T)#cs)!Suc i)) ∈ ?rely›
by fastforce
from tran_inv have ‹Γ ⊢ (body ev, s0) ─c*→ (fin_com, t)› by blast
with cpt_from_ptran_star obtain pcpt where pcpt:
‹pcpt ∈ cpts_from (ptran Γ) (body ev, s0) ∩ assume {s0} {} ∧ last pcpt = (fin_com, t)› by blast
from pcpt have
‹pcpt ∈ assume {s0} {}› by blast
with ‹s0∈pre› ‹s0∈guard ev› have ‹pcpt ∈ assume (pre ∩ guard ev ∩ {s0}) Id›
by (simp add: assume_def)
with pcpt body_valid have pcpt_commit:
‹pcpt ∈ commit (ptran Γ) {fin_com} UNIV ({s. (s0, s) ∈ guar} ∩ post)›
by blast
then have ‹t ∈ ({s. (s0, s) ∈ guar} ∩ post)›
by (simp add: pcpt commit_def)
with P_s S0 S T have ‹(s,t)∈guar› by simp
from pcpt_commit have
‹fst (last pcpt) = fin_com ⟶ snd (last pcpt) ∈ ({s. (s0, s) ∈ guar} ∩ post)›
by (simp add: commit_def)
with pcpt have t:
‹t ∈ ({s. (s0, s) ∈ guar} ∩ post)› by force
have rest_etran:
‹∀i. Suc i < length ((Q,T)#cs) ⟶ ((Q,T)#cs)!i ─e→ ((Q,T)#cs)!Suc i› using all_etran_from_fin
using CptsComp.hyps(2) Q by blast
from rest_etran assume2_tl have rely:
‹∀i. Suc i < length ((Q,T)#cs) ⟶ (snd (((Q, T) # cs) ! i), snd (((Q, T) # cs) ! Suc i)) ∈ ?rely›
by blast
have commit1:
‹∀i. Suc i < length ((P,S)#(Q,T)#cs) ⟶ (((P,S)#(Q,T)#cs)!i, ((P,S)#(Q,T)#cs)!(Suc i)) ∈ (estran Γ) ⟶ (snd (((P,S)#(Q,T)#cs)!i), snd (((P,S)#(Q,T)#cs)!(Suc i))) ∈ ?guar›
proof
fix i
show ‹Suc i < length ((P,S)#(Q,T)#cs) ⟶ (((P,S)#(Q,T)#cs)!i, ((P,S)#(Q,T)#cs)!(Suc i)) ∈ (estran Γ) ⟶ (snd (((P,S)#(Q,T)#cs)!i), snd (((P,S)#(Q,T)#cs)!(Suc i))) ∈ ?guar›
proof
assume ‹Suc i < length ((P, S) # (Q, T) # cs)›
show ‹(((P, S) # (Q, T) # cs) ! i, ((P, S) # (Q, T) # cs) ! Suc i) ∈ (estran Γ) ⟶
(snd (((P, S) # (Q, T) # cs) ! i), snd (((P, S) # (Q, T) # cs) ! Suc i)) ∈ ?guar›
proof(cases i)
case 0
then show ?thesis apply simp using ‹(s,t)∈guar› lift_state_pair_set_def S T by blast
next
case (Suc i')
then show ?thesis apply simp apply(subst Q)
using no_ctran_from_fin
using CptsComp.hyps(2) Q ‹Suc i < length ((P, S) # (Q, T) # cs)›
by (metis Suc_less_eq length_Cons nth_Cons_Suc)
qed
qed
qed
have commit2_aux:
‹fst (last ((Q,T)#cs)) = fin ⟶ snd (last ((Q,T)#cs)) ∈ ?post›
proof
assume ‹fst (last ((Q, T) # cs)) = fin›
from t have 1: ‹T∈?post› using T by (simp add: lift_state_set_def)
from last_sat_post[OF 1 refl rest_etran stable_post'] rely
show ‹snd (last ((Q, T) # cs)) ∈ ?post› by blast
qed
then have commit2:
‹fst (last ((P,S)#(Q,T)#cs)) = fin ⟶ snd (last ((P,S)#(Q,T)#cs)) ∈ ?post› by simp
show ?case using commit1 commit2
by (simp add: commit_def)
qed
qed
qed
then show ?thesis
by (simp)
qed
theorem conseq_sound:
assumes h: ‹Γ ⊨ es sat⇩e [pre', rely', guar', post']›
and pre: "pre ⊆ pre'"
and rely: "rely ⊆ rely'"
and guar: "guar' ⊆ guar"
and post: "post' ⊆ post"
shows ‹Γ ⊨ es sat⇩e [pre, rely, guar, post]›
proof-
let ?pre = ‹lift_state_set pre›
let ?rely = ‹lift_state_pair_set rely›
let ?guar = ‹lift_state_pair_set guar›
let ?post = ‹lift_state_set post›
let ?pre' = ‹lift_state_set pre'›
let ?rely' = ‹lift_state_pair_set rely'›
let ?guar' = ‹lift_state_pair_set guar'›
let ?post' = ‹lift_state_set post'›
from h have
valid: ‹∀S0. cpts_from (estran Γ) (es, S0) ∩ assume ?pre' ?rely' ⊆ commit (estran Γ) {fin} ?guar' ?post'›
by auto
have ‹∀S0. cpts_from (estran Γ) (es, S0) ∩ assume ?pre ?rely ⊆ commit (estran Γ) {fin} ?guar ?post›
proof
fix S0
show ‹cpts_from (estran Γ) (es, S0) ∩ assume ?pre ?rely ⊆ commit (estran Γ) {fin} ?guar ?post›
proof
fix cpt
assume cpt: ‹cpt ∈ cpts_from (estran Γ) (es, S0) ∩ assume ?pre ?rely›
then have cpt1: ‹cpt ∈ cpts_from (estran Γ) (es, S0)› by blast
from cpt have "assume": ‹cpt ∈ assume ?pre ?rely› by blast
then have assume': ‹cpt ∈ assume ?pre' ?rely'›
apply(simp add: assume_def lift_state_set_def lift_state_pair_set_def case_prod_unfold)
using pre rely by auto
from cpt1 assume' have ‹cpt ∈ cpts_from (estran Γ) (es, S0) ∩ assume ?pre' ?rely'› by blast
with valid have commit: "cpt ∈ commit (estran Γ) {fin} ?guar' ?post'" by blast
then show ‹cpt ∈ commit (estran Γ) {fin} ?guar ?post›
apply(simp add: commit_def lift_state_set_def lift_state_pair_set_def case_prod_unfold)
using guar post by auto
qed
qed
then have ‹validity (estran Γ) {fin} es ?pre ?rely ?guar ?post› using validity_def by metis
then show ?thesis using es_validity_def by simp
qed
primrec (nonexhaustive) unlift_seq where
‹unlift_seq (ESeq P Q) = P›
primrec unlift_seq_esconf where
‹unlift_seq_esconf (P,s) = (unlift_seq P, s)›
abbreviation ‹unlift_seq_cpt ≡ map unlift_seq_esconf›
lemma split_seq:
assumes cpt: ‹cpt ∈ cpts_from (estran Γ) (ESeq es1 es2, S0)›
and not_all_seq: ‹¬ all_seq es2 cpt›
shows
"∃i S'. cpt!Suc i = (es2, S') ∧
Suc i < length cpt ∧
all_seq es2 (take (Suc i) cpt) ∧
unlift_seq_cpt (take (Suc i) cpt) @ [(fin,S')] ∈ cpts_from (estran Γ) (es1, S0) ∧
(cpt!i, cpt!Suc i)∈estran Γ ∧
(unlift_seq_esconf (cpt!i), (fin,S'))∈estran Γ"
proof-
from cpt have hd_cpt: ‹hd cpt = (ESeq es1 es2, S0)› by simp
from cpt have ‹cpt ∈ cpts (estran Γ)› by simp
then have ‹cpt ∈ cpts_es_mod Γ› using cpts_es_mod_equiv by blast
then show ?thesis using hd_cpt not_all_seq
proof(induct arbitrary:S0 es1)
case (CptsModOne)
then show ?case
by (simp add: all_seq_def)
next
case (CptsModEnv P t y cs s x)
from CptsModEnv(3) have 1: ‹hd ((P,t,y)#cs) = (es1 NEXT es2, t,y)› by simp
from CptsModEnv(4) have 2: ‹¬ all_seq es2 ((P,t,y)#cs)› by (simp add: all_seq_def)
from CptsModEnv(2)[OF 1 2] obtain i S' where
‹((P, t, y) # cs) ! Suc i = (es2, S') ∧
Suc i < length ((P, t, y) # cs) ∧
all_seq es2 (take (Suc i) ((P, t, y) # cs)) ∧
map unlift_seq_esconf (take (Suc i) ((P, t, y) # cs)) @ [(fin, S')] ∈ cpts_from (estran Γ) (es1, t, y) ∧ (((P, t, y) # cs) ! i, ((P, t, y) # cs) ! Suc i) ∈ estran Γ ∧ (unlift_seq_esconf (((P, t, y) # cs) ! i), fin, S') ∈ estran Γ›
by blast
then show ?case apply-
apply(rule exI[where x="Suc i"])
apply (simp add: all_seq_def)
apply(rule conjI)
apply(rule CptsEnv)
apply fastforce
apply(rule conjI)
using CptsModEnv(3) apply simp
by argo
next
case (CptsModAnon)
then show ?case by simp
next
case (CptsModAnon_fin)
then show ?case by simp
next
case (CptsModBasic)
then show ?case by simp
next
case (CptsModAtom)
then show ?case by simp
next
case (CptsModSeq P s x a Q t y R cs)
from CptsModSeq(5) have ‹(s,x) = S0› and ‹R=es2› and ‹P=es1› by simp+
from CptsModSeq(5) have 1: ‹hd ((Q NEXT R, t,y) # cs) = (Q NEXT es2, t,y)› by simp
from CptsModSeq(6) have 2: ‹¬ all_seq es2 ((Q NEXT R, t,y) # cs)› by (simp add: all_seq_def)
from CptsModSeq(4)[OF 1 2] obtain i S' where
‹((Q NEXT R, t, y) # cs) ! Suc i = (es2, S') ∧
Suc i < length ((Q NEXT R, t, y) # cs) ∧
all_seq es2 (take (Suc i) ((Q NEXT R, t, y) # cs)) ∧
map unlift_seq_esconf (take (Suc i) ((Q NEXT R, t, y) # cs)) @ [(fin, S')] ∈ cpts_from (estran Γ) (Q, t, y) ∧
(((Q NEXT R, t, y) # cs) ! i, ((Q NEXT R, t, y) # cs) ! Suc i) ∈ estran Γ ∧
(unlift_seq_esconf (((Q NEXT R, t, y) # cs) ! i), fin, S') ∈ estran Γ›
by blast
then show ?case apply-
apply(rule exI[where x="Suc i"])
apply(simp add: all_seq_def)
apply(rule conjI)
apply(rule CptsComp)
apply(simp add: estran_def; rule exI)
apply(rule CptsModSeq(1))
apply fast
apply(rule conjI)
apply(rule ‹P=es1›)
apply(rule conjI)
apply(rule ‹(s,x) = S0›)
by argo
next
case (CptsModSeq_fin Q s x a t y cs cs')
then show ?case
apply-
apply(rule exI[where x=0])
apply (simp add: all_seq_def)
apply(rule conjI)
apply(rule CptsComp)
apply(simp add: estran_def; rule exI; assumption)
apply(rule CptsOne)
apply(rule conjI)
apply(simp add: estran_def; rule exI)
using ESeq_fin apply blast
apply(simp add: estran_def)
apply(rule exI)
by assumption
next
case (CptsModChc1)
then show ?case by simp
next
case (CptsModChc2)
then show ?case by simp
next
case (CptsModJoin1)
then show ?case by simp
next
case (CptsModJoin2)
then show ?case by simp
next
case (CptsModJoin_fin)
then show ?case by simp
next
case (CptsModWhileTOnePartial)
then show ?case by simp
next
case (CptsModWhileTOneFull)
then show ?case by simp
next
case (CptsModWhileTMore)
then show ?case by simp
next
case (CptsModWhileF)
then show ?case by simp
qed
qed
lemma all_seq_unlift:
assumes all_seq: "all_seq Q cpt"
and h: ‹cpt ∈ cpts_from (estran Γ) (ESeq P Q, S0) ∩ assume pre rely›
shows ‹unlift_seq_cpt cpt ∈ cpts_from (estran Γ) (P, S0) ∩ assume pre rely›
proof
from h have h1:
‹cpt ∈ cpts_from (estran Γ) (ESeq P Q, S0)› by blast
then have cpt: ‹cpt ∈ cpts (estran Γ)› by simp
with cpts_es_mod_equiv have cpt_mod: "cpt ∈ cpts_es_mod Γ" by auto
from h1 have hd_cpt: ‹hd cpt = (ESeq P Q, S0)› by simp
show ‹map unlift_seq_esconf cpt ∈ cpts_from (estran Γ) (P, S0)› using cpt_mod hd_cpt all_seq
proof(induct arbitrary:P S0)
case (CptsModOne P s)
then show ?case apply simp apply(rule CptsOne) done
next
case (CptsModEnv P1 t y cs s x)
from CptsModEnv(3) have ‹hd ((P1, t,y) # cs) = (P NEXT Q, t,y)› by simp
moreover from CptsModEnv(4) have ‹all_seq Q ((P1, t,y) # cs)›
apply- apply(unfold all_seq_def) apply auto done
ultimately have ‹map unlift_seq_esconf ((P1, t,y) # cs) ∈ cpts_from (estran Γ) (P, t,y)›
using CptsModEnv(2) by blast
moreover have "(s,x)=S0" using CptsModEnv(3) by simp
ultimately show ?case apply clarsimp apply(erule CptsEnv) done
next
case (CptsModAnon)
then show ?case by simp
next
case (CptsModAnon_fin)
then show ?case by simp
next
case (CptsModBasic)
then show ?case by simp
next
case (CptsModAtom)
then show ?case by simp
next
case (CptsModSeq P1 s x a Q1 t y R cs)
from CptsModSeq(5) have ‹hd ((Q1 NEXT R, t,y) # cs) = (Q1 NEXT Q, t,y)› by simp
moreover from CptsModSeq(6) have ‹all_seq Q ((Q1 NEXT R, t,y) # cs)›
apply(unfold all_seq_def) by auto
ultimately have ‹map unlift_seq_esconf ((Q1 NEXT R, t,y) # cs) ∈ cpts_from (estran Γ) (Q1, t,y)›
using CptsModSeq(4) by blast
moreover from CptsModSeq(5) have "(s,x)=S0" and "P1=P" by simp_all
ultimately show ?case apply (simp add: estran_def)
apply(rule CptsComp) using CptsModSeq(1) by auto
next
case (CptsModSeq_fin)
from CptsModSeq_fin(5) have False
apply(auto simp add: all_seq_def)
using seq_neq2 by metis
then show ?case by blast
next
case (CptsModChc1)
then show ?case by simp
next
case (CptsModChc2)
then show ?case by simp
next
case (CptsModJoin1)
then show ?case by simp
next
case (CptsModJoin2)
then show ?case by simp
next
case (CptsModJoin_fin)
then show ?case by simp
next
case CptsModWhileTOnePartial
then show ?case by simp
next
case CptsModWhileTOneFull
then show ?case by simp
next
case CptsModWhileTMore
then show ?case by simp
next
case CptsModWhileF
then show ?case by simp
qed
next
from h have h2: "cpt ∈ assume pre rely" by blast
then have a1: ‹snd (hd cpt) ∈ pre› by (simp add: assume_def)
from h2 have a2:
‹∀i. Suc i < length cpt ⟶
fst ( (cpt ! i)) = fst ( (cpt ! Suc i)) ⟶
(snd ( (cpt ! i)), snd ( (cpt ! Suc i))) ∈ rely› by (simp add: assume_def)
from h have ‹cpt ∈ cpts (estran Γ)› by fastforce
with cpts_nonnil have cpt_nonnil: "cpt ≠ []" by blast
show ‹map unlift_seq_esconf cpt ∈ assume pre rely›
apply (simp add: assume_def)
proof
show ‹snd (hd (map unlift_seq_esconf cpt)) ∈ pre› using a1 cpt_nonnil
by (metis eq_snd_iff hd_map unlift_seq_esconf.simps)
next
show ‹∀i. Suc i < length cpt ⟶
fst (unlift_seq_esconf (cpt ! i)) = fst (unlift_seq_esconf (cpt ! Suc i)) ⟶
(snd (unlift_seq_esconf (cpt ! i)), snd (unlift_seq_esconf (cpt ! Suc i))) ∈ rely›
using a2 by (metis Suc_lessD all_seq all_seq_def fst_conv nth_mem prod.collapse snd_conv unlift_seq.simps unlift_seq_esconf.simps)
qed
qed
lemma cpts_from_assume_snoc_fin:
assumes cpt: ‹cpt ∈ cpts_from (estran Γ) (P, S0) ∩ assume pre rely›
and tran: ‹(last cpt, (fin, S1)) ∈ (estran Γ)›
shows ‹cpt @ [(fin, S1)] ∈ cpts_from (estran Γ) (P, S0) ∩ assume pre rely›
proof
from cpt have cpt_from:
‹cpt ∈ cpts_from (estran Γ) (P,S0)› by blast
with cpts_snoc_comp tran cpts_from_def show ‹cpt @ [(fin, S1)] ∈ cpts_from (estran Γ) (P, S0)›
using cpts_nonnil by fastforce
next
from cpt have cpt_assume:
‹cpt ∈ assume pre rely› by blast
from cpt have cpt_nonnil:
‹cpt ≠ []› using cpts_nonnil by fastforce
from tran ctran_imp_not_etran have not_etran:
‹¬ last cpt ─e→ (fin, S1)› by fast
show ‹cpt @ [(fin, S1)] ∈ assume pre rely›
using assume_snoc cpt_assume cpt_nonnil not_etran by blast
qed
lemma unlift_seq_estran:
assumes all_seq: ‹all_seq Q cpt›
and cpt: ‹cpt ∈ cpts (estran Γ)›
and i: ‹Suc i < length cpt›
and tran: ‹(cpt!i, cpt!Suc i) ∈ (estran Γ)›
shows ‹(unlift_seq_cpt cpt ! i, unlift_seq_cpt cpt ! Suc i) ∈ (estran Γ)›
proof-
let ?part = ‹drop i cpt›
from i have i': ‹i < length cpt› by simp
from cpts_drop cpt i' have ‹?part ∈ cpts (estran Γ)› by blast
with cpts_es_mod_equiv have part_cpt: ‹?part ∈ cpts_es_mod Γ› by blast
show ?thesis using part_cpt
proof(cases)
case (CptsModOne P s)
then show ?thesis using i
by (metis Cons_nth_drop_Suc i' list.discI list.sel(3))
next
case (CptsModEnv P t y cs s x)
with tran have ‹((P,s,x),(P,t,y)) ∈ (estran Γ)›
using Cons_nth_drop_Suc i' nth_via_drop by fastforce
then have False apply (simp add: estran_def)
using no_estran_to_self by fast
then show ?thesis by blast
next
case (CptsModAnon)
from CptsModAnon(1) all_seq all_seq_def show ?thesis
using i' nth_mem nth_via_drop by fastforce
next
case (CptsModAnon_fin)
from CptsModAnon_fin(1) all_seq all_seq_def show ?thesis
using i' nth_mem nth_via_drop by fastforce
next
case (CptsModBasic)
from CptsModBasic(1) all_seq all_seq_def show ?thesis
using i' nth_mem nth_via_drop by fastforce
next
case (CptsModAtom)
from CptsModAtom(1) all_seq all_seq_def show ?thesis
using i' nth_mem nth_via_drop by fastforce
next
case (CptsModSeq P1 s x a Q1 t y R cs)
then have eq1:
‹map unlift_seq_esconf cpt ! i = (P1,s,x)›
by (simp add: i' nth_via_drop)
from CptsModSeq have eq2:
‹map unlift_seq_esconf cpt ! Suc i = (Q1,t,y)›
by (metis Cons_nth_drop_Suc i i' list.sel(1) list.sel(3) nth_map unlift_seq.simps unlift_seq_esconf.simps)
from CptsModSeq(2) eq1 eq2 show ?thesis
apply(unfold estran_def) by auto
next
case (CptsModSeq_fin)
from CptsModSeq_fin(1) all_seq all_seq_def obtain P2 where ‹Q = P2 NEXT Q›
by (metis (no_types, lifting) Cons_nth_drop_Suc esys.inject(4) fst_conv i i' list.inject nth_mem)
then show ?thesis using seq_neq2 by metis
next
case (CptsModChc1)
from CptsModChc1(1) all_seq all_seq_def show ?thesis
using i' nth_mem nth_via_drop by fastforce
next
case (CptsModChc2)
from CptsModChc2(1) all_seq all_seq_def show ?thesis
using i' nth_mem nth_via_drop by fastforce
next
case (CptsModJoin1)
from CptsModJoin1(1) all_seq all_seq_def show ?thesis
using i' nth_mem nth_via_drop by fastforce
next
case (CptsModJoin2)
from CptsModJoin2(1) all_seq all_seq_def show ?thesis
using i' nth_mem nth_via_drop by fastforce
next
case CptsModJoin_fin
from CptsModJoin_fin(1) all_seq all_seq_def show ?thesis
using i' nth_mem nth_via_drop by fastforce
next
case CptsModWhileTOnePartial
with all_seq all_seq_def show ?thesis
using i' nth_mem nth_via_drop by fastforce
next
case CptsModWhileTOneFull
with all_seq all_seq_def show ?thesis
using i' nth_mem nth_via_drop by fastforce
next
case CptsModWhileTMore
with all_seq all_seq_def show ?thesis
using i' nth_mem nth_via_drop by fastforce
next
case CptsModWhileF
with all_seq all_seq_def show ?thesis
using i' nth_mem nth_via_drop by fastforce
qed
qed
lemma fin_imp_not_all_seq:
assumes ‹fst (last cpt) = fin›
and ‹cpt ≠ []›
shows ‹¬ all_seq Q cpt›
apply(unfold all_seq_def)
proof
assume ‹∀c∈set cpt. ∃P. fst c = P NEXT Q›
then obtain P where ‹fst (last cpt) = P NEXT Q›
using assms(2) last_in_set by blast
with assms(1) show False by simp
qed
lemma all_seq_guar:
assumes all_seq: ‹all_seq es2 cpt›
and h1': ‹∀s0. cpts_from (estran Γ) (es1, s0) ∩ assume pre rely ⊆ commit (estran Γ) {fin} guar post›
and cpt: ‹cpt ∈ cpts_from (estran Γ) (ESeq es1 es2, s0) ∩ assume pre rely›
shows ‹∀i. Suc i < length cpt ⟶ (cpt ! i, cpt ! Suc i) ∈ (estran Γ) ⟶ (snd (cpt ! i), snd (cpt ! Suc i)) ∈ guar›
proof-
let ?cpt' = ‹unlift_seq_cpt cpt›
from all_seq_unlift[of es2 cpt Γ es1 s0 pre rely] all_seq cpt have cpt':
‹?cpt' ∈ cpts_from (estran Γ) (es1, s0) ∩ assume pre rely› by blast
with h1' have ‹?cpt' ∈ commit (estran Γ) {fin} guar post› by blast
then have guar:
‹∀i. Suc i < length ?cpt' ⟶ (?cpt'!i, ?cpt'!Suc i) ∈ (estran Γ) ⟶ (snd (?cpt'!i), snd (?cpt'!Suc i)) ∈ guar›
by (simp add: commit_def)
show ?thesis
proof
fix i
from guar have guar_i: ‹Suc i < length ?cpt' ⟶ (?cpt'!i, ?cpt'!Suc i) ∈ (estran Γ) ⟶ (snd (?cpt'!i), snd (?cpt'!Suc i)) ∈ guar› by blast
show ‹Suc i < length cpt ⟶ (cpt ! i, cpt ! Suc i) ∈ (estran Γ) ⟶ (snd (cpt ! i), snd (cpt ! Suc i)) ∈ guar› apply clarify
proof-
assume i: ‹Suc i < length cpt›
assume tran: ‹(cpt ! i, cpt ! Suc i) ∈ (estran Γ)›
from cpt have ‹cpt ∈ cpts (estran Γ)› by force
with unlift_seq_estran[of es2 cpt Γ i] all_seq i tran have tran':
‹(?cpt'!i, ?cpt'!Suc i) ∈ (estran Γ)› by blast
with guar_i i show ‹(snd (cpt ! i), snd (cpt ! Suc i)) ∈ guar›
by (metis (no_types, lifting) Suc_lessD length_map nth_map prod.collapse sndI unlift_seq_esconf.simps)
qed
qed
qed
lemma part1_cpt_assume:
assumes split:
‹cpt!Suc i = (es2, S) ∧
Suc i < length cpt ∧
all_seq es2 (take (Suc i) cpt) ∧
unlift_seq_cpt (take (Suc i) cpt) @ [(fin,S)] ∈ cpts_from (estran Γ) (es1, S0) ∧
(unlift_seq_esconf (cpt!i), (fin,S))∈estran Γ›
and h1':
‹∀S0. cpts_from (estran Γ) (es1, S0) ∩ assume pre rely ⊆ commit (estran Γ) {fin} guar mid›
and cpt:
‹cpt ∈ cpts_from (estran Γ) (ESeq es1 es2, S0) ∩ assume pre rely›
shows ‹unlift_seq_cpt (take (Suc i) cpt)@[(fin,S)] ∈ cpts_from (estran Γ) (es1, S0) ∩ assume pre rely›
proof-
let ?part1 = ‹take (Suc i) cpt›
let ?part2 = ‹drop (Suc i) cpt›
let ?part1' = ‹unlift_seq_cpt ?part1›
let ?part1'' = ‹?part1'@[(fin,S)]›
show ‹?part1'' ∈ cpts_from (estran Γ) (es1, S0) ∩ assume pre rely›
proof
show ‹map unlift_seq_esconf (take (Suc i) cpt) @ [(fin, S)] ∈ cpts_from (estran Γ) (es1, S0)›
using split by blast
next
from cpt cpts_nonnil have ‹cpt≠[]› by auto
then have ‹take (Suc i) cpt ≠ []› by simp
have 1: ‹snd (hd (map unlift_seq_esconf (take (Suc i) cpt))) ∈ pre›
apply(simp add: hd_map[OF ‹take(Suc i)cpt≠[]›])
using cpt by (auto simp add: assume_def)
show ‹map unlift_seq_esconf (take (Suc i) cpt) @ [(fin, S)] ∈ assume pre rely›
apply(auto simp add: assume_def)
using 1 ‹cpt≠[]› apply fastforce
subgoal for j
proof(cases "j=i")
case True
assume contra: ‹fst ((map unlift_seq_esconf (take (Suc i) cpt) @ [(fin, S)]) ! j) = fst ((map unlift_seq_esconf (take (Suc i) cpt) @ [(fin, S)]) ! Suc j)›
from split have ‹Suc i < length cpt› by argo
have 1: ‹fst ((map unlift_seq_esconf (take (Suc i) cpt) @ [(fin, S)]) ! i) ≠ fin›
proof-
from split have tran: ‹(unlift_seq_esconf (cpt!i), (fin,S))∈estran Γ› by argo
have *: ‹i < length (take(Suc i)cpt)›
by (simp add: ‹Suc i < length cpt›[THEN Suc_lessD])
have ‹fst ((map unlift_seq_esconf (take (Suc i) cpt)) ! i) ≠ fin›
apply(simp add: nth_map[OF *])
using no_estran_from_fin'[OF tran] .
then show ?thesis by (simp add: ‹Suc i < length cpt›[THEN Suc_lessD] nth_append)
qed
have 2: ‹fst ((map unlift_seq_esconf (take (Suc i) cpt) @ [(fin, S)]) ! Suc i) = fin›
using ‹cpt≠[]› ‹Suc i < length cpt›
by (metis (no_types, lifting) Suc_leI Suc_lessD length_map length_take min.absorb2 nth_append_length prod.collapse prod.inject)
from contra have False using True 1 2 by argo
then show ?thesis by blast
next
case False
assume a2: ‹j<Suc i›
with False have ‹j<i› by simp
from split have ‹Suc i < length cpt› by argo
from split have all_seq: ‹all_seq es2 (take (Suc i) cpt)› by argo
have *: ‹Suc j < length (take (Suc i) cpt)›
using ‹Suc i < length cpt› ‹j<i› by auto
assume a3:
‹fst ((map unlift_seq_esconf (take (Suc i) cpt) @ [(fin, S)]) ! j) =
fst ((map unlift_seq_esconf (take (Suc i) cpt) @ [(fin, S)]) ! Suc j)›
then have
‹fst ((map unlift_seq_esconf (take (Suc i) cpt)) ! j) =
fst ((map unlift_seq_esconf (take (Suc i) cpt)) ! Suc j)›
using ‹j<i› ‹Suc i < length cpt›
by (smt Suc_lessD Suc_mono length_map length_take less_trans_Suc min_less_iff_conj nth_append)
then have ‹fst (unlift_seq_esconf (take (Suc i) cpt ! j)) = fst (unlift_seq_esconf (take (Suc i) cpt ! Suc j))›
by (simp add: nth_map[OF *] nth_map[OF *[THEN Suc_lessD]])
then have ‹fst (cpt!j) = fst (cpt!Suc j)›
proof-
assume a: ‹fst (unlift_seq_esconf (take (Suc i) cpt ! j)) = fst (unlift_seq_esconf (take (Suc i) cpt ! Suc j))›
have 1: ‹take (Suc i) cpt ! j = cpt ! j›
by (simp add: a2)
have 2: ‹take (Suc i) cpt ! Suc j = cpt ! Suc j›
by (simp add: ‹j<i›)
obtain P1 S1 where 3: ‹cpt!j = (P1 NEXT es2, S1)›
using all_seq apply(simp add: all_seq_def)
by (metis "*" "1" Suc_lessD nth_mem prod.collapse)
obtain P2 S2 where 4: ‹cpt!Suc j = (P2 NEXT es2, S2)›
using all_seq apply(simp add: all_seq_def)
by (metis "*" "2" nth_mem prod.collapse)
from a have ‹fst (unlift_seq_esconf (cpt ! j)) = fst (unlift_seq_esconf (cpt ! Suc j))›
by (simp add: 1 2)
then show ?thesis by (simp add: 3 4)
qed
from cpt have ‹cpt ∈ assume pre rely› by blast
then have ‹fst (cpt!j) = fst (cpt!Suc j) ⟹ (snd (cpt!j), snd (cpt!Suc j))∈rely›
apply(auto simp add: assume_def)
apply(erule allE[where x=j])
using ‹Suc i < length cpt› ‹j<i› by fastforce
from this[OF ‹fst (cpt!j) = fst (cpt!Suc j)›]
have ‹(snd ((map unlift_seq_esconf (take (Suc i) cpt)) ! j), snd ((map unlift_seq_esconf (take (Suc i) cpt)) ! Suc j)) ∈ rely›
apply(simp add: nth_map[OF *] nth_map[OF *[THEN Suc_lessD]])
using ‹j<i› all_seq
by (metis (no_types, lifting) Suc_mono a2 nth_take prod.collapse prod.inject unlift_seq_esconf.simps)
then show ?thesis
by (metis (no_types, lifting) "*" Suc_lessD length_map nth_append)
qed
done
qed
qed
lemma part2_assume:
assumes split:
‹cpt!Suc i = (es2, S) ∧
Suc i < length cpt ∧
all_seq es2 (take (Suc i) cpt) ∧
unlift_seq_cpt (take (Suc i) cpt) @ [(fin,S)] ∈ cpts_from (estran Γ) (es1, S0) ∧
(unlift_seq_esconf (cpt!i), (fin,S))∈estran Γ›
and h1':
‹∀S0. cpts_from (estran Γ) (es1, S0) ∩ assume pre rely ⊆ commit (estran Γ) {fin} guar mid›
and cpt:
‹cpt ∈ cpts_from (estran Γ) (ESeq es1 es2, S0) ∩ assume pre rely›
shows ‹drop (Suc i) cpt ∈ assume mid rely›
apply(unfold assume_def)
apply(subst mem_Collect_eq)
proof
let ?part1 = ‹take (Suc i) cpt›
let ?part2 = ‹drop (Suc i) cpt›
let ?part1' = ‹unlift_seq_cpt ?part1›
let ?part1'' = ‹?part1'@[(fin,S)]›
have ‹?part1'' ∈ cpts_from (estran Γ) (es1, S0) ∩ assume pre rely›
using part1_cpt_assume[OF split h1' cpt] .
with h1' have ‹?part1'' ∈ commit (estran Γ) {fin} guar mid› by blast
then have ‹S∈mid›
by (auto simp add: commit_def)
then show ‹snd (hd ?part2) ∈ mid›
by (simp add: split hd_drop_conv_nth)
next
let ?part2 = ‹drop (Suc i) cpt›
from cpt have ‹cpt ∈ assume pre rely› by blast
then have ‹∀j. Suc j < length cpt ⟶ cpt!j ─e→ cpt!Suc j ⟶ (snd (cpt!j), snd (cpt!Suc j)) ∈ rely› by (simp add: assume_def)
then show ‹∀j. Suc j < length ?part2 ⟶ ?part2!j ─e→ ?part2!Suc j ⟶ (snd (?part2!j), snd (?part2!Suc j)) ∈ rely› by simp
qed
theorem Seq_sound:
assumes h1:
‹Γ ⊨ es1 sat⇩e [pre, rely, guar, mid]›
assumes h2:
‹Γ ⊨ es2 sat⇩e [mid, rely, guar, post]›
shows
‹Γ ⊨ ESeq es1 es2 sat⇩e [pre, rely, guar, post]›
proof-
let ?pre = ‹lift_state_set pre›
let ?rely = ‹lift_state_pair_set rely›
let ?guar = ‹lift_state_pair_set guar›
let ?post = ‹lift_state_set post›
let ?mid = ‹lift_state_set mid›
from h1 have h1':
‹∀S0. cpts_from (estran Γ) (es1, S0) ∩ assume ?pre ?rely ⊆ commit (estran Γ) {fin} ?guar ?mid›
by (simp)
from h2 have h2':
‹∀S0. cpts_from (estran Γ) (es2, S0) ∩ assume ?mid ?rely ⊆ commit (estran Γ) {fin} ?guar ?post›
by (simp)
have ‹∀S0. cpts_from (estran Γ) (ESeq es1 es2, S0) ∩ assume ?pre ?rely ⊆ commit (estran Γ) {fin} ?guar ?post›
proof
fix S0
show ‹cpts_from (estran Γ) (ESeq es1 es2, S0) ∩ assume ?pre ?rely ⊆ commit (estran Γ) {fin} ?guar ?post›
proof
fix cpt
assume cpt: ‹cpt ∈ cpts_from (estran Γ) (ESeq es1 es2, S0) ∩ assume ?pre ?rely›
from cpt have cpt1: ‹cpt ∈ cpts_from (estran Γ) (ESeq es1 es2, S0)› by blast
then have cpt_cpts: ‹cpt ∈ cpts (estran Γ)› by simp
then have ‹cpt ≠ []› using cpts_nonnil by auto
from cpt have hd_cpt: ‹hd cpt = (ESeq es1 es2, S0)› by simp
from cpt have cpt_assume: ‹cpt ∈ assume ?pre ?rely› by blast
show ‹cpt ∈ commit (estran Γ) {fin} ?guar ?post›
apply (simp add: commit_def)
proof
show ‹∀i. Suc i < length cpt ⟶ (cpt ! i, cpt ! Suc i) ∈ estran Γ ⟶ (snd (cpt ! i), snd (cpt ! Suc i)) ∈ ?guar›
proof(cases ‹all_seq es2 cpt›)
case True
with all_seq_guar h1' cpt show ?thesis by blast
next
case False
with split_seq[OF cpt1] obtain i S where split:
‹cpt ! Suc i = (es2, S) ∧
Suc i < length cpt ∧
all_seq es2 (take (Suc i) cpt) ∧ map unlift_seq_esconf (take (Suc i) cpt) @ [(fin, S)] ∈ cpts_from (estran Γ) (es1, S0) ∧ (cpt ! i, cpt ! Suc i) ∈ estran Γ ∧ (unlift_seq_esconf (cpt ! i), fin, S) ∈ estran Γ› by blast
let ?part1 = ‹take (Suc i) cpt›
let ?part1' = ‹unlift_seq_cpt ?part1›
let ?part1'' = ‹?part1' @ [(fin,S)]›
let ?part2 = ‹drop (Suc i) cpt›
from split have
Suc_i_lt: ‹Suc i < length cpt› and
all_seq_part1: ‹all_seq es2 ?part1› by argo+
have part1_cpt:
‹?part1 ∈ cpts_from (estran Γ) (es1 NEXT es2, S0) ∩ assume ?pre ?rely›
using cpts_from_assume_take[OF cpt, of ‹Suc i›] by simp
have guar_part1:
"∀j. Suc j < length ?part1 ⟶ (?part1!j, ?part1!Suc j)∈(estran Γ) ⟶ (snd (?part1!j), snd (?part1!Suc j))∈?guar"
using all_seq_guar all_seq_part1 h1' part1_cpt by blast
have guar_part2:
‹∀j. Suc j < length ?part2 ⟶ (?part2!j, ?part2!Suc j)∈(estran Γ) ⟶ (snd (?part2!j), snd (?part2!Suc j))∈?guar›
proof-
from part2_assume[OF _ h1' cpt] split have ‹?part2 ∈ assume ?mid ?rely› by blast
moreover from cpts_drop cpt cpts_from_def split have "?part2 ∈ cpts (estran Γ)" by blast
moreover from split have ‹hd ?part2 = (es2, S)› by (simp add: hd_conv_nth)
ultimately have ‹?part2 ∈ cpts_from (estran Γ) (es2,S) ∩ assume ?mid ?rely› by fastforce
with h2' have ‹?part2 ∈ commit (estran Γ) {fin} ?guar ?post› by blast
then show ?thesis by (simp add: commit_def)
qed
have guar_tran:
‹(snd (last ?part1), snd (hd ?part2))∈?guar›
proof-
have ‹(snd (?part1''!i), snd (?part1''!Suc i))∈?guar›
proof-
have part1''_cpt_asm: ‹?part1'' ∈ cpts_from (estran Γ) (es1, S0) ∩ assume ?pre ?rely›
using part1_cpt_assume[of cpt i es2 S Γ es1 S0, OF _ h1' cpt] split by blast
from split have tran: ‹(unlift_seq_esconf (cpt ! i), fin, S) ∈ estran Γ› by argo
have ‹(map unlift_seq_esconf (take (Suc i) cpt) @ [(fin, S)]) ! i = (map unlift_seq_esconf (take (Suc i) cpt)) ! i›
using ‹Suc i < length cpt› by (simp add: nth_append)
moreover have ‹(map unlift_seq_esconf (take (Suc i) cpt)) ! i = unlift_seq_esconf (cpt ! i)›
proof-
have *: ‹i < length (take (Suc i) cpt)› using ‹Suc i < length cpt› by simp
show ?thesis by (simp add: nth_map[OF *])
qed
ultimately have 1: ‹(map unlift_seq_esconf (take (Suc i) cpt) @ [(fin, S)]) ! i = (unlift_seq_esconf (cpt!i))› by simp
have 2: ‹(map unlift_seq_esconf (take (Suc i) cpt) @ [(fin, S)]) ! Suc i = (fin, S)›
using ‹Suc i < length cpt›
by (metis (no_types, lifting) length_map length_take min.absorb2 nat_less_le nth_append_length)
from tran have tran': ‹((map unlift_seq_esconf (take (Suc i) cpt) @ [(fin, S)]) ! i, (map unlift_seq_esconf (take (Suc i) cpt) @ [(fin, S)]) ! Suc i) ∈ estran Γ›
by (simp add: 1 2)
from h1' part1''_cpt_asm have ‹?part1'' ∈ commit (estran Γ) {fin} (lift_state_pair_set guar) (lift_state_set mid)›
by blast
then show ?thesis
apply(auto simp add: commit_def)
apply(erule allE[where x=i])
using ‹Suc i < length cpt› tran' by linarith
qed
moreover have ‹snd (?part1''!i) = snd (last ?part1)›
proof-
have 1: ‹snd (last (take (Suc i) cpt)) = snd (cpt!i)› using Suc_i_lt
by (simp add: last_take_Suc)
have 2: ‹snd ((map unlift_seq_esconf (take (Suc i) cpt) @ [(fin, S)]) ! i) = snd ((map unlift_seq_esconf (take (Suc i) cpt)) ! i)›
using Suc_i_lt
by (simp add: nth_append)
have 3: ‹i < length (take (Suc i) cpt)› using Suc_i_lt by simp
show ?thesis
apply (simp add: 1 2 nth_map[OF 3])
apply(subst surjective_pairing[of ‹cpt!i›])
apply(subst unlift_seq_esconf.simps)
by simp
qed
moreover have ‹snd (?part1''!Suc i) = snd (hd ?part2)›
proof-
have ‹snd (?part1''!Suc i) = S›
proof-
have ‹length (map unlift_seq_esconf (take (Suc i) cpt)) = Suc i› using Suc_i_lt by simp
then show ?thesis by (simp add: nth_via_drop)
qed
moreover have ‹snd (hd ?part2) = S› using split by (simp add: hd_conv_nth)
ultimately show ?thesis by simp
qed
ultimately show ?thesis by simp
qed
show ?thesis
proof
fix j
show ‹Suc j < length cpt ⟶ (cpt ! j, cpt ! Suc j) ∈ estran Γ ⟶ (snd (cpt ! j), snd (cpt ! Suc j)) ∈ ?guar›
proof(cases ‹j<i›)
case True
then show ?thesis using guar_part1 by simp
next
case False
then show ?thesis
proof(cases ‹j=i›)
case True
then show ?thesis using guar_tran
by (metis Suc_lessD hd_drop_conv_nth last_take_Suc)
next
case False
with ‹¬j<i› have ‹j>i› by simp
then obtain d where ‹Suc i + d = j›
using Suc_leI le_Suc_ex by blast
then show ?thesis using guar_part2[THEN spec, of d] by simp
qed
qed
qed
qed
next
show ‹fst (last cpt) = fin ⟶ snd (last cpt) ∈ ?post›
proof
assume fin: ‹fst (last cpt) = fin›
then have
‹¬ all_seq es2 cpt›
using fin_imp_not_all_seq ‹cpt≠[]› by blast
with split_seq[OF cpt1] obtain i S where split:
‹cpt ! Suc i = (es2, S) ∧
Suc i < length cpt ∧
all_seq es2 (take (Suc i) cpt) ∧ map unlift_seq_esconf (take (Suc i) cpt) @ [(fin, S)] ∈ cpts_from (estran Γ) (es1, S0) ∧ (cpt ! i, cpt ! Suc i) ∈ estran Γ ∧ (unlift_seq_esconf (cpt ! i), fin, S) ∈ estran Γ› by blast
then have
cpt_Suc_i: ‹cpt!(Suc i) = (es2, S)› and
Suc_i_lt: ‹Suc i < length cpt› and
all_seq: ‹all_seq es2 (take (Suc i) cpt)› by argo+
let ?part2 = ‹drop (Suc i) cpt›
from cpt_Suc_i have hd_part2:
‹hd ?part2 = (es2, S)›
by (simp add: Suc_i_lt hd_drop_conv_nth)
have ‹?part2 ∈ cpts (estran Γ)› using cpts_drop Suc_i_lt cpt1 by fastforce
with cpt_Suc_i have ‹?part2 ∈ cpts_from (estran Γ) (es2, S)›
using hd_drop_conv_nth Suc_i_lt by fastforce
moreover have ‹?part2 ∈ assume ?mid ?rely›
using part2_assume split h1' cpt by blast
ultimately have ‹?part2 ∈ commit (estran Γ) {fin} ?guar ?post› using h2' by blast
then have "fst (last ?part2) ∈ {fin} ⟶ snd (last ?part2) ∈ ?post"
by (simp add: commit_def)
moreover from fin have "fst (last ?part2) = fin" using Suc_i_lt by fastforce
ultimately have ‹snd (last ?part2) ∈ ?post› by blast
then show ‹snd (last cpt) ∈ ?post› using Suc_i_lt by force
qed
qed
qed
qed
then show ?thesis using es_validity_def validity_def
by metis
qed
lemma assume_choice1:
‹(P OR R, S) # (Q, T) # cs ∈ assume pre rely ⟹
Γ ⊢ (P,S) ─es[a]→ (Q,T) ⟹
(P,S)#(Q,T)#cs ∈ assume pre rely›
apply(simp add: assume_def)
apply clarify
apply(case_tac i)
prefer 2
apply fastforce
apply simp
using no_estran_to_self surjective_pairing by metis
lemma assume_choice2:
‹(P OR R, S) # (Q, T) # cs ∈ assume pre rely ⟹
Γ ⊢ (R,S) ─es[a]→ (Q,T) ⟹
(R,S)#(Q,T)#cs ∈ assume pre rely›
apply(simp add: assume_def)
apply clarify
apply(case_tac i)
prefer 2
apply fastforce
apply simp
using no_estran_to_self surjective_pairing by metis
lemma exists_least:
‹P (n::nat) ⟹ ∃m. P m ∧ (∀i<m. ¬ P i)›
using exists_least_iff by auto
lemma choice_sound_aux1:
‹cpt' = map (λ(_, s). (P, s)) (take (Suc m) cpt) @ drop (Suc m) cpt ⟹
Suc m < length cpt ⟹
∀j<Suc m. fst (cpt' ! j) = P›
proof
fix j
assume cpt': ‹cpt' = map (λ(_, s). (P, s)) (take (Suc m) cpt) @ drop (Suc m) cpt›
assume Suc_m_lt: ‹Suc m < length cpt›
show ‹j<Suc m ⟶ fst(cpt'!j) = P›
proof
assume ‹j<Suc m›
with cpt' have ‹cpt'!j = map (λ(_, s). (P, s)) (take (Suc m) cpt) ! j›
by (metis (mono_tags, lifting) Suc_m_lt length_map length_take less_trans min_less_iff_conj nth_append)
then have ‹fst (cpt'!j) = fst (map (λ(_, s). (P, s)) (take (Suc m) cpt) ! j)› by simp
moreover have ‹fst (map (λ(_, s). (P, s)) (take (Suc m) cpt) ! j) = P› using ‹j<Suc m›
by (simp add: Suc_leI Suc_lessD Suc_m_lt case_prod_unfold min.absorb2)
ultimately show ‹fst(cpt'!j) = P› by simp
qed
qed
theorem Choice_sound:
assumes h1:
‹Γ ⊨ P sat⇩e [pre, rely, guar, post]›
assumes h2:
‹Γ ⊨ Q sat⇩e [pre, rely, guar, post]›
shows
‹Γ ⊨ EChc P Q sat⇩e [pre, rely, guar, post]›
proof-
let ?pre = ‹lift_state_set pre›
let ?rely = ‹lift_state_pair_set rely›
let ?guar = ‹lift_state_pair_set guar›
let ?post = ‹lift_state_set post›
from h1 have h1':
‹∀S0. cpts_from (estran Γ) (P, S0) ∩ assume ?pre ?rely ⊆ commit (estran Γ) {fin} ?guar ?post›
by (simp)
from h2 have h2':
‹∀S0. cpts_from (estran Γ) (Q, S0) ∩ assume ?pre ?rely ⊆ commit (estran Γ) {fin} ?guar ?post›
by (simp)
have ‹∀S0. cpts_from (estran Γ) (EChc P Q, S0) ∩ assume ?pre ?rely ⊆ commit (estran Γ) {fin} ?guar ?post›
proof
fix S0
show ‹cpts_from (estran Γ) (EChc P Q, S0) ∩ assume ?pre ?rely ⊆ commit (estran Γ) {fin} ?guar ?post›
proof
fix cpt
assume cpt_from_assume: ‹cpt ∈ cpts_from (estran Γ) (EChc P Q, S0) ∩ assume ?pre ?rely›
then have cpt: ‹cpt ∈ cpts (estran Γ)›
and hd_cpt: ‹hd cpt = (P OR Q, S0)›
and fst_hd_cpt: "fst (hd cpt) = P OR Q"
and cpt_assume: ‹cpt ∈ assume ?pre ?rely› by auto
from cpt cpts_nonnil have ‹cpt≠[]› by auto
show ‹cpt ∈ commit (estran Γ) {fin} ?guar ?post›
proof(cases ‹∀i. Suc i < length cpt ⟶ cpt!i ─e→ cpt!Suc i›)
case True
then show ?thesis
apply(simp add: commit_def)
proof
assume ‹∀i. Suc i < length cpt ⟶ fst (cpt ! i) = fst (cpt ! Suc i)›
then show
‹∀i. Suc i < length cpt ⟶ (cpt ! i, cpt ! Suc i) ∈ estran Γ ⟶
(snd (cpt ! i), snd (cpt ! Suc i)) ∈ ?guar›
using no_estran_to_self'' by blast
next
assume ‹∀i. Suc i < length cpt ⟶ fst (cpt ! i) = fst (cpt ! Suc i)›
show ‹fst (last cpt) = fin ⟶ snd (last cpt) ∈ ?post›
proof-
have ‹∀i<length cpt. fst (cpt ! i) = P OR Q›
by (rule all_etran_same_prog[OF True fst_hd_cpt ‹cpt≠[]›])
then have ‹fst (last cpt) = P OR Q› using last_conv_nth ‹cpt≠[]› by force
then show ?thesis by simp
qed
qed
next
case False
then obtain i where 1: ‹Suc i < length cpt ∧ ¬ cpt ! i ─e→ cpt ! Suc i› (is "?P i") by blast
with exists_least[of ?P, OF 1] obtain m where 2: ‹?P m ∧ (∀i<m. ¬?P i)› by blast
from 2 have Suc_m_lt: ‹Suc m < length cpt› and all_etran: ‹∀i<m. cpt!i ─e→ cpt!Suc i› by simp_all
from 2 have ‹¬ cpt!m ─e→ cpt!Suc m› by blast
then have ctran: ‹(cpt!m, cpt!Suc m) ∈ (estran Γ)› using ctran_or_etran[OF cpt Suc_m_lt] by simp
have fst_cpt_m: ‹fst (cpt!m) = P OR Q›
proof-
let ?cpt = ‹take (Suc m) cpt›
from Suc_m_lt all_etran have 1: ‹∀i. Suc i < length ?cpt ⟶ ?cpt!i ─e→ ?cpt!Suc i› by simp
from fst_hd_cpt have 2: ‹fst (hd ?cpt) = P OR Q› by simp
from ‹cpt≠[]› have ‹?cpt ≠ []› by simp
have ‹∀i<length (take (Suc m) cpt). fst (take (Suc m) cpt ! i) = P OR Q›
by (rule all_etran_same_prog[OF 1 2 ‹?cpt≠[]›])
then show ?thesis
by (simp add: Suc_lessD Suc_m_lt)
qed
with ctran show ?thesis
apply(subst (asm) estran_def)
apply(subst (asm) mem_Collect_eq)
apply(subst (asm) case_prod_unfold)
apply(erule exE)
apply(erule estran_p.cases, auto)
proof-
fix s a P' t
assume cpt_m: ‹cpt!m = (P OR Q, s)›
assume cpt_Suc_m: ‹cpt!Suc m = (P', t)›
assume ctran_from_P: ‹Γ ⊢ (P, s) ─es[a]→ (P', t)›
obtain cpt' where cpt': ‹cpt' = map (λ(_,s). (P, s)) (take (Suc m) cpt) @ drop (Suc m) cpt› by simp
then have cpt'_m: ‹cpt'!m = (P, s)› using Suc_m_lt
by (simp add: Suc_lessD cpt_m nth_append)
have len_eq: ‹length cpt' = length cpt› using cpt' by simp
have same_state: ‹∀i<length cpt. snd (cpt'!i) = snd (cpt!i)› using cpt' Suc_m_lt
by (metis (mono_tags, lifting) append_take_drop_id length_map nth_append nth_map prod.collapse prod.simps(2) snd_conv)
have ‹cpt' ∈ cpts_from (estran Γ) (P,S0) ∩ assume ?pre ?rely›
proof
show ‹cpt' ∈ cpts_from (estran Γ) (P,S0)›
apply(subst cpts_from_def')
proof
show ‹cpt' ∈ cpts (estran Γ)›
apply(subst cpts_def')
proof
show ‹cpt'≠[]› using cpt' ‹cpt≠[]› by simp
next
show ‹∀i. Suc i < length cpt' ⟶ (cpt' ! i, cpt' ! Suc i) ∈ estran Γ ∨ cpt' ! i ─e→ cpt' ! Suc i›
proof
fix i
show ‹Suc i < length cpt' ⟶ (cpt' ! i, cpt' ! Suc i) ∈ estran Γ ∨ cpt' ! i ─e→ cpt' ! Suc i›
proof
assume Suc_i_lt: ‹Suc i < length cpt'›
show ‹(cpt' ! i, cpt' ! Suc i) ∈ estran Γ ∨ cpt' ! i ─e→ cpt' ! Suc i›
proof(cases ‹i<m›)
case True
have ‹∀j < Suc m. fst(cpt'!j) = P› by (rule choice_sound_aux1[OF cpt' Suc_m_lt])
then have all_etran': ‹∀j<m. cpt'!j ─e→ cpt'!Suc j› by simp
have ‹cpt'!i ─e→ cpt'!Suc i› by (rule all_etran'[THEN spec[where x=i], rule_format, OF True])
then show ?thesis by blast
next
case False
have eq_Suc_i: ‹cpt'!Suc i = cpt!Suc i› using cpt' False Suc_m_lt
by (metis (no_types, lifting) Suc_less_SucD append_take_drop_id length_map length_take min_less_iff_conj nth_append)
show ?thesis
proof(cases ‹i=m›)
case True
then show ?thesis
apply simp
apply(rule disjI1)
using cpt'_m eq_Suc_i cpt_Suc_m apply (simp add: estran_def)
using ctran_from_P by blast
next
case False
with ‹¬ i < m› have ‹m<i› by simp
then have eq_i: ‹cpt'!i = cpt!i› using cpt' Suc_m_lt
by (metis (no_types, lifting) ‹¬ i < m› append_take_drop_id length_map length_take less_SucE min_less_iff_conj nth_append)
from cpt have ‹∀i. Suc i < length cpt ⟶ (cpt!i, cpt!Suc i)∈estran Γ ∨ (cpt!i ─e→ cpt!Suc i)› using cpts_def' by metis
then show ?thesis using eq_i eq_Suc_i Suc_i_lt len_eq by simp
qed
qed
qed
qed
qed
next
show ‹hd cpt' = (P, S0)› using cpt' hd_cpt
by (simp add: ‹cpt ≠ []› hd_map)
qed
next
show ‹cpt' ∈ assume ?pre ?rely›
apply(simp add: assume_def)
proof
from cpt' have ‹snd (hd cpt') = snd (hd cpt)›
by (simp add: ‹cpt ≠ []› hd_cpt hd_map)
then show ‹snd (hd cpt') ∈ ?pre›
using cpt_assume by (simp add: assume_def)
next
show ‹∀i. Suc i < length cpt' ⟶ fst (cpt' ! i) = fst (cpt' ! Suc i) ⟶ (snd (cpt' ! i), snd (cpt' ! Suc i)) ∈ ?rely›
proof
fix i
show ‹Suc i < length cpt' ⟶ fst (cpt' ! i) = fst (cpt' ! Suc i) ⟶ (snd (cpt' ! i), snd (cpt' ! Suc i)) ∈ ?rely›
proof
assume ‹Suc i < length cpt'›
with len_eq have ‹Suc i < length cpt› by simp
show ‹fst (cpt' ! i) = fst (cpt' ! Suc i) ⟶ (snd (cpt' ! i), snd (cpt' ! Suc i)) ∈ ?rely›
proof(cases ‹i<m›)
case True
from same_state ‹Suc i < length cpt'› len_eq have
‹snd (cpt'!i) = snd (cpt!i)› and ‹snd (cpt'!Suc i) = snd (cpt!Suc i)› by simp_all
then show ?thesis
using cpt_assume ‹Suc i < length cpt› all_etran True by (auto simp add: assume_def)
next
case False
have eq_Suc_i: ‹cpt'!Suc i = cpt!Suc i› using cpt' False Suc_m_lt
by (metis (no_types, lifting) Suc_less_SucD append_take_drop_id length_map length_take min_less_iff_conj nth_append)
show ?thesis
proof(cases ‹i=m›)
case True
have ‹fst (cpt'!i) ≠ fst (cpt'!Suc i)› using True eq_Suc_i cpt'_m cpt_Suc_m ctran_from_P no_estran_to_self surjective_pairing by metis
then show ?thesis by blast
next
case False
with ‹¬ i < m› have ‹m<i› by simp
then have eq_i: ‹cpt'!i = cpt!i› using cpt' Suc_m_lt
by (metis (no_types, lifting) ‹¬ i < m› append_take_drop_id length_map length_take less_SucE min_less_iff_conj nth_append)
from eq_i eq_Suc_i cpt_assume ‹Suc i < length cpt›
show ?thesis by (auto simp add: assume_def)
qed
qed
qed
qed
qed
qed
with h1' have cpt'_commit: ‹cpt' ∈ commit (estran Γ) {fin} ?guar ?post› by blast
show ‹cpt ∈ commit (estran Γ) {fin} ?guar ?post›
apply(simp add: commit_def)
proof
show ‹∀i. Suc i < length cpt ⟶ (cpt ! i, cpt ! Suc i) ∈ estran Γ ⟶ (snd (cpt ! i), snd (cpt ! Suc i)) ∈ ?guar›
(is ‹∀i. ?P i›)
proof
fix i
show ‹?P i›
proof(cases "i<m")
case True
then show ?thesis
apply clarify
apply(insert all_etran[THEN spec[where x=i]])
apply auto
using no_estran_to_self'' apply blast
done
next
case False
have eq_Suc_i: ‹cpt'!Suc i = cpt!Suc i› using cpt' False Suc_m_lt
by (metis (no_types, lifting) Suc_less_SucD append_take_drop_id length_map length_take min_less_iff_conj nth_append)
show ?thesis
proof(cases "i=m")
case True
with eq_Suc_i have eq_Suc_m: ‹cpt'!Suc m = cpt!Suc m› by simp
have snd_cpt_m_eq: ‹snd (cpt!m) = s› using cpt_m by simp
from True show ?thesis using cpt'_commit
apply(simp add: commit_def)
apply clarify
apply(erule allE[where x=i])
apply (simp add: cpt'_m eq_Suc_m cpt_Suc_m estran_def snd_cpt_m_eq len_eq)
using ctran_from_P by blast
next
case False
with ‹¬ i < m› have ‹m<i› by simp
then have eq_i: ‹cpt'!i = cpt!i› using cpt' Suc_m_lt
by (metis (no_types, lifting) ‹¬ i < m› append_take_drop_id length_map length_take less_SucE min_less_iff_conj nth_append)
from False show ?thesis using cpt'_commit
apply(simp add: commit_def)
apply clarify
apply(erule allE[where x=i])
apply(simp add: eq_i eq_Suc_i len_eq)
done
qed
qed
qed
next
have eq_last: ‹last cpt = last cpt'› using cpt' Suc_m_lt by simp
show ‹fst (last cpt) = fin ⟶ snd (last cpt) ∈ ?post›
using cpt'_commit
by (simp add: commit_def eq_last)
qed
next
fix s a Q' t
assume cpt_m: ‹cpt!m = (P OR Q, s)›
assume cpt_Suc_m: ‹cpt!Suc m = (Q', t)›
assume ctran_from_Q: ‹Γ ⊢ (Q, s) ─es[a]→ (Q', t)›
obtain cpt' where cpt': ‹cpt' = map (λ(_,s). (Q, s)) (take (Suc m) cpt) @ drop (Suc m) cpt› by simp
then have cpt'_m: ‹cpt'!m = (Q, s)› using Suc_m_lt
by (simp add: Suc_lessD cpt_m nth_append)
have len_eq: ‹length cpt' = length cpt› using cpt' by simp
have same_state: ‹∀i<length cpt. snd (cpt'!i) = snd (cpt!i)› using cpt' Suc_m_lt
by (metis (mono_tags, lifting) append_take_drop_id length_map nth_append nth_map prod.collapse prod.simps(2) snd_conv)
have ‹cpt' ∈ cpts_from (estran Γ) (Q,S0) ∩ assume ?pre ?rely›
proof
show ‹cpt' ∈ cpts_from (estran Γ) (Q,S0)›
apply(subst cpts_from_def')
proof
show ‹cpt' ∈ cpts (estran Γ)›
apply(subst cpts_def')
proof
show ‹cpt'≠[]› using cpt' ‹cpt≠[]› by simp
next
show ‹∀i. Suc i < length cpt' ⟶ (cpt' ! i, cpt' ! Suc i) ∈ estran Γ ∨ cpt' ! i ─e→ cpt' ! Suc i›
proof
fix i
show ‹Suc i < length cpt' ⟶ (cpt' ! i, cpt' ! Suc i) ∈ estran Γ ∨ cpt' ! i ─e→ cpt' ! Suc i›
proof
assume Suc_i_lt: ‹Suc i < length cpt'›
show ‹(cpt' ! i, cpt' ! Suc i) ∈ estran Γ ∨ cpt' ! i ─e→ cpt' ! Suc i›
proof(cases ‹i<m›)
case True
have ‹∀j < Suc m. fst(cpt'!j) = Q› by (rule choice_sound_aux1[OF cpt' Suc_m_lt])
then have all_etran': ‹∀j<m. cpt'!j ─e→ cpt'!Suc j› by simp
have ‹cpt'!i ─e→ cpt'!Suc i› by (rule all_etran'[THEN spec[where x=i], rule_format, OF True])
then show ?thesis by blast
next
case False
have eq_Suc_i: ‹cpt'!Suc i = cpt!Suc i› using cpt' False Suc_m_lt
by (metis (no_types, lifting) Suc_less_SucD append_take_drop_id length_map length_take min_less_iff_conj nth_append)
show ?thesis
proof(cases ‹i=m›)
case True
then show ?thesis
apply simp
apply(rule disjI1)
using cpt'_m eq_Suc_i cpt_Suc_m apply (simp add: estran_def)
using ctran_from_Q by blast
next
case False
with ‹¬ i < m› have ‹m<i› by simp
then have eq_i: ‹cpt'!i = cpt!i› using cpt' Suc_m_lt
by (metis (no_types, lifting) ‹¬ i < m› append_take_drop_id length_map length_take less_SucE min_less_iff_conj nth_append)
from cpt have ‹∀i. Suc i < length cpt ⟶ (cpt!i, cpt!Suc i)∈estran Γ ∨ (cpt!i ─e→ cpt!Suc i)› using cpts_def' by metis
then show ?thesis using eq_i eq_Suc_i Suc_i_lt len_eq by simp
qed
qed
qed
qed
qed
next
show ‹hd cpt' = (Q, S0)› using cpt' hd_cpt
by (simp add: ‹cpt ≠ []› hd_map)
qed
next
show ‹cpt' ∈ assume ?pre ?rely›
apply(simp add: assume_def)
proof
from cpt' have ‹snd (hd cpt') = snd (hd cpt)›
by (simp add: ‹cpt ≠ []› hd_cpt hd_map)
then show ‹snd (hd cpt') ∈ ?pre›
using cpt_assume by (simp add: assume_def)
next
show ‹∀i. Suc i < length cpt' ⟶ fst (cpt' ! i) = fst (cpt' ! Suc i) ⟶ (snd (cpt' ! i), snd (cpt' ! Suc i)) ∈ ?rely›
proof
fix i
show ‹Suc i < length cpt' ⟶ fst (cpt' ! i) = fst (cpt' ! Suc i) ⟶ (snd (cpt' ! i), snd (cpt' ! Suc i)) ∈ ?rely›
proof
assume ‹Suc i < length cpt'›
with len_eq have ‹Suc i < length cpt› by simp
show ‹fst (cpt' ! i) = fst (cpt' ! Suc i) ⟶ (snd (cpt' ! i), snd (cpt' ! Suc i)) ∈ ?rely›
proof(cases ‹i<m›)
case True
from same_state ‹Suc i < length cpt'› len_eq have
‹snd (cpt'!i) = snd (cpt!i)› and ‹snd (cpt'!Suc i) = snd (cpt!Suc i)› by simp_all
then show ?thesis
using cpt_assume ‹Suc i < length cpt› all_etran True by (auto simp add: assume_def)
next
case False
have eq_Suc_i: ‹cpt'!Suc i = cpt!Suc i› using cpt' False Suc_m_lt
by (metis (no_types, lifting) Suc_less_SucD append_take_drop_id length_map length_take min_less_iff_conj nth_append)
show ?thesis
proof(cases ‹i=m›)
case True
have ‹fst (cpt'!i) ≠ fst (cpt'!Suc i)› using True eq_Suc_i cpt'_m cpt_Suc_m ctran_from_Q no_estran_to_self surjective_pairing by metis
then show ?thesis by blast
next
case False
with ‹¬ i < m› have ‹m<i› by simp
then have eq_i: ‹cpt'!i = cpt!i› using cpt' Suc_m_lt
by (metis (no_types, lifting) ‹¬ i < m› append_take_drop_id length_map length_take less_SucE min_less_iff_conj nth_append)
from eq_i eq_Suc_i cpt_assume ‹Suc i < length cpt›
show ?thesis by (auto simp add: assume_def)
qed
qed
qed
qed
qed
qed
with h2' have cpt'_commit: ‹cpt' ∈ commit (estran Γ) {fin} ?guar ?post› by blast
show ‹cpt ∈ commit (estran Γ) {fin} ?guar ?post›
apply(simp add: commit_def)
proof
show ‹∀i. Suc i < length cpt ⟶ (cpt ! i, cpt ! Suc i) ∈ estran Γ ⟶ (snd (cpt ! i), snd (cpt ! Suc i)) ∈ ?guar›
(is ‹∀i. ?P i›)
proof
fix i
show ‹?P i›
proof(cases "i<m")
case True
then show ?thesis
apply clarify
apply(insert all_etran[THEN spec[where x=i]])
apply auto
using no_estran_to_self'' apply blast
done
next
case False
have eq_Suc_i: ‹cpt'!Suc i = cpt!Suc i› using cpt' False Suc_m_lt
by (metis (no_types, lifting) Suc_less_SucD append_take_drop_id length_map length_take min_less_iff_conj nth_append)
show ?thesis
proof(cases "i=m")
case True
with eq_Suc_i have eq_Suc_m: ‹cpt'!Suc m = cpt!Suc m› by simp
have snd_cpt_m_eq: ‹snd (cpt!m) = s› using cpt_m by simp
from True show ?thesis using cpt'_commit
apply(simp add: commit_def)
apply clarify
apply(erule allE[where x=i])
apply (simp add: cpt'_m eq_Suc_m cpt_Suc_m estran_def snd_cpt_m_eq len_eq)
using ctran_from_Q by blast
next
case False
with ‹¬ i < m› have ‹m<i› by simp
then have eq_i: ‹cpt'!i = cpt!i› using cpt' Suc_m_lt
by (metis (no_types, lifting) ‹¬ i < m› append_take_drop_id length_map length_take less_SucE min_less_iff_conj nth_append)
from False show ?thesis using cpt'_commit
apply(simp add: commit_def)
apply clarify
apply(erule allE[where x=i])
apply(simp add: eq_i eq_Suc_i len_eq)
done
qed
qed
qed
next
have eq_last: ‹last cpt = last cpt'› using cpt' Suc_m_lt by simp
show ‹fst (last cpt) = fin ⟶ snd (last cpt) ∈ ?post›
using cpt'_commit
by (simp add: commit_def eq_last)
qed
qed
qed
qed
qed
then show ?thesis by simp
qed
lemma join_sound_aux2:
assumes cpt_from_assume: ‹cpt ∈ cpts_from (estran Γ) (P ⋈ Q, s0) ∩ assume pre rely›
and valid1: ‹∀s0. cpts_from (estran Γ) (P, s0) ∩ assume pre1 rely1 ⊆ commit (estran Γ) {fin} guar1 post1›
and valid2: ‹∀s0. cpts_from (estran Γ) (Q, s0) ∩ assume pre2 rely2 ⊆ commit (estran Γ) {fin} guar2 post2›
and pre: ‹pre ⊆ pre1 ∩ pre2›
and rely1: ‹rely ∪ guar2 ⊆ rely1›
and rely2: ‹rely ∪ guar1 ⊆ rely2›
shows
‹∀i. Suc i < length (fst (split cpt)) ∧ Suc i < length (snd (split cpt)) ⟶
((fst (split cpt)!i, fst (split cpt)!Suc i) ∈ estran Γ ⟶ (snd (fst (split cpt)!i), snd (fst (split cpt)!Suc i)) ∈ guar1) ∧
((snd (split cpt)!i, snd (split cpt)!Suc i) ∈ estran Γ ⟶ (snd (snd (split cpt)!i), snd (snd (split cpt)!Suc i)) ∈ guar2)›
proof-
let ?cpt1 = ‹fst (split cpt)›
let ?cpt2 = ‹snd (split cpt)›
have cpt1_from: ‹?cpt1 ∈ cpts_from (estran Γ) (P,s0)›
using cpt_from_assume split_cpt by blast
have cpt2_from: ‹?cpt2 ∈ cpts_from (estran Γ) (Q,s0)›
using cpt_from_assume split_cpt by blast
from cpt_from_assume have cpt_from: ‹cpt ∈ cpts_from (estran Γ) (P ⋈ Q, s0)›
and cpt_assume: "cpt ∈ assume pre rely" by auto
from cpt_from have cpt: ‹cpt ∈ cpts (estran Γ)› and fst_hd_cpt: ‹fst (hd cpt) = P ⋈ Q› by auto
from cpts_nonnil[OF cpt] have ‹cpt≠[]› .
show ?thesis
proof(rule ccontr, simp, erule exE)
fix k
assume
‹Suc k < length ?cpt1 ∧ Suc k < length ?cpt2 ∧
((?cpt1 ! k, ?cpt1 ! Suc k) ∈ estran Γ ∧ (snd (?cpt1 ! k), snd (?cpt1 ! Suc k)) ∉ guar1 ∨
(?cpt2 ! k, ?cpt2 ! Suc k) ∈ estran Γ ∧ (snd (?cpt2 ! k), snd (?cpt2 ! Suc k)) ∉ guar2)›
(is "?P k")
from exists_least[of ?P k, OF this] obtain m where ‹?P m ∧ (∀i<m. ¬?P i)› by blast
then show False
proof(auto)
assume Suc_m_lt1: ‹Suc m < length ?cpt1›
assume Suc_m_lt2: ‹Suc m < length ?cpt2›
from Suc_m_lt1 split_length_le1[of cpt] have Suc_m_lt: ‹Suc m < length cpt› by simp
assume h:
‹∀i<m. ((?cpt1 ! i, ?cpt1 ! Suc i) ∈ estran Γ ⟶ (snd (?cpt1 ! i), snd (?cpt1 ! Suc i)) ∈ guar1) ∧
((?cpt2 ! i, ?cpt2 ! Suc i) ∈ estran Γ ⟶ (snd (?cpt2 ! i), snd (?cpt2 ! Suc i)) ∈ guar2)›
assume ctran: ‹(?cpt1 ! m, ?cpt1 ! Suc m) ∈ estran Γ›
assume not_guar: ‹(snd (?cpt1 ! m), snd (?cpt1 ! Suc m)) ∉ guar1›
let ?cpt1' = ‹take (Suc (Suc m)) ?cpt1›
from cpt1_from have cpt1'_from: ‹?cpt1' ∈ cpts_from (estran Γ) (P,s0)›
by (metis Zero_not_Suc cpts_from_take)
then have cpt1': ‹?cpt1' ∈ cpts (estran Γ)› by simp
from ctran have ctran': ‹(?cpt1'!m, ?cpt1'!Suc m) ∈ estran Γ› by auto
from split_ctran1_aux[OF Suc_m_lt1]
have Suc_m_not_fin: ‹fst (cpt ! Suc m) ≠ fin› .
have ‹∀i. Suc i < length ?cpt1' ⟶ ?cpt1'!i ─e→ ?cpt1'!Suc i ⟶ (snd (?cpt1'!i), snd (?cpt1'!Suc i)) ∈ rely ∪ guar2›
proof
fix i
show ‹Suc i < length ?cpt1' ⟶ ?cpt1'!i ─e→ ?cpt1'!Suc i ⟶ (snd (?cpt1'!i), snd (?cpt1'!Suc i)) ∈ rely ∪ guar2›
proof(rule impI, rule impI)
assume Suc_i_lt': ‹Suc i < length ?cpt1'›
with Suc_m_lt1 have ‹i≤m› by simp
from Suc_i_lt' have Suc_i_lt1: ‹Suc i < length ?cpt1› by simp
with split_same_length[of cpt] have Suc_i_lt2: ‹Suc i < length ?cpt2› by simp
from no_fin_before_non_fin[OF cpt Suc_m_lt Suc_m_not_fin] ‹i≤m›
have Suc_i_not_fin: ‹fst (cpt!Suc i) ≠ fin› by fast
from Suc_i_lt' split_length_le1[of cpt] have Suc_i_lt: ‹Suc i < length cpt› by simp
assume etran': ‹?cpt1'!i ─e→ ?cpt1'!Suc i›
then have etran: ‹?cpt1!i ─e→ ?cpt1!Suc i› using Suc_m_lt Suc_i_lt' by (simp add: split_def)
show ‹(snd (?cpt1'!i), snd (?cpt1'!Suc i)) ∈ rely ∪ guar2›
proof-
from split_etran1[OF cpt fst_hd_cpt Suc_i_lt Suc_i_not_fin etran]
have ‹cpt ! i ─e→ cpt ! Suc i ∨ (?cpt2 ! i, ?cpt2 ! Suc i) ∈ estran Γ› .
then show ?thesis
proof
assume etran: ‹cpt!i ─e→ cpt!Suc i›
with cpt_assume Suc_i_lt have ‹(snd (cpt!i), snd (cpt!Suc i)) ∈ rely›
by (simp add: assume_def)
then have ‹(snd (?cpt1!i), snd (?cpt1!Suc i)) ∈ rely›
using split_same_state1[OF Suc_i_lt1] split_same_state1[OF Suc_i_lt1[THEN Suc_lessD]] by argo
then have ‹(snd (?cpt1'!i), snd (?cpt1'!Suc i)) ∈ rely› using ‹i≤m› by simp
then show ‹(snd (?cpt1'!i), snd (?cpt1'!Suc i)) ∈ rely ∪ guar2› by simp
next
assume ctran2: ‹(?cpt2!i, ?cpt2!Suc i) ∈ estran Γ›
have ‹(snd (?cpt2!i), snd (?cpt2!Suc i)) ∈ guar2›
proof(cases ‹i=m›)
case True
with ctran etran ctran_imp_not_etran show ?thesis by blast
next
case False
with ‹i≤m› have ‹i<m› by linarith
show ?thesis using ctran2 h[THEN spec[where x=i], rule_format, OF ‹i<m›] by blast
qed
thm split_same_state2
then have ‹(snd (cpt!i), snd(cpt!Suc i)) ∈ guar2›
using Suc_i_lt2 by (simp add: split_same_state2)
then have ‹(snd (?cpt1!i), snd (?cpt1!Suc i)) ∈ guar2›
using split_same_state1[OF Suc_i_lt1] split_same_state1[OF Suc_i_lt1[THEN Suc_lessD]] by argo
then have ‹(snd (?cpt1'!i), snd (?cpt1'!Suc i)) ∈ guar2› using ‹i≤m› by simp
then show ‹(snd (?cpt1'!i), snd (?cpt1'!Suc i)) ∈ rely ∪ guar2› by simp
qed
qed
qed
qed
moreover have ‹snd (hd ?cpt1') ∈ pre›
proof-
have ‹snd (hd cpt) ∈ pre› using cpt_assume by (simp add: assume_def)
then have ‹snd (hd ?cpt1) ∈ pre› using split_same_state1
by (metis ‹cpt ≠ []› cpt1' cpts_def' hd_conv_nth length_greater_0_conv take_eq_Nil)
then show ?thesis by simp
qed
ultimately have ‹?cpt1' ∈ assume pre1 rely1› using rely1 pre
by (auto simp add: assume_def)
with cpt1'_from pre have ‹?cpt1' ∈ cpts_from (estran Γ) (P,s0) ∩ assume pre1 rely1› by blast
with valid1 have ‹?cpt1' ∈ commit (estran Γ) {fin} guar1 post1› by blast
then have ‹(snd (?cpt1' ! m), snd (?cpt1' ! Suc m)) ∈ guar1›
apply(simp add: commit_def)
apply clarify
apply(erule allE[where x=m])
using Suc_m_lt1 ctran' by simp
with not_guar Suc_m_lt show False by (simp add: Suc_m_lt Suc_lessD)
next
assume Suc_m_lt1: ‹Suc m < length ?cpt1›
assume Suc_m_lt2: ‹Suc m < length ?cpt2›
from Suc_m_lt1 split_length_le1[of cpt] have Suc_m_lt: ‹Suc m < length cpt› by simp
assume h:
‹∀i<m. ((?cpt1 ! i, ?cpt1 ! Suc i) ∈ estran Γ ⟶ (snd (?cpt1 ! i), snd (?cpt1 ! Suc i)) ∈ guar1) ∧
((?cpt2 ! i, ?cpt2 ! Suc i) ∈ estran Γ ⟶ (snd (?cpt2 ! i), snd (?cpt2 ! Suc i)) ∈ guar2)›
assume ctran: ‹(?cpt2 ! m, ?cpt2 ! Suc m) ∈ estran Γ›
assume not_guar: ‹(snd (?cpt2 ! m), snd (?cpt2 ! Suc m)) ∉ guar2›
let ?cpt2' = ‹take (Suc (Suc m)) ?cpt2›
from cpt2_from have cpt2'_from: ‹?cpt2' ∈ cpts_from (estran Γ) (Q,s0)›
by (metis Zero_not_Suc cpts_from_take)
then have cpt2': ‹?cpt2' ∈ cpts (estran Γ)› by simp
from ctran have ctran': ‹(?cpt2'!m, ?cpt2'!Suc m) ∈ estran Γ› by fastforce
from split_ctran2_aux[OF Suc_m_lt2]
have Suc_m_not_fin: ‹fst (cpt ! Suc m) ≠ fin› .
have ‹∀i. Suc i < length ?cpt2' ⟶ ?cpt2'!i ─e→ ?cpt2'!Suc i ⟶ (snd (?cpt2'!i), snd (?cpt2'!Suc i)) ∈ rely ∪ guar1›
proof
fix i
show ‹Suc i < length ?cpt2' ⟶ ?cpt2'!i ─e→ ?cpt2'!Suc i ⟶ (snd (?cpt2'!i), snd (?cpt2'!Suc i)) ∈ rely ∪ guar1›
proof(rule impI, rule impI)
assume Suc_i_lt': ‹Suc i < length ?cpt2'›
with Suc_m_lt have ‹i≤m› by simp
from Suc_i_lt' have Suc_i_lt2: ‹Suc i < length ?cpt2› by simp
with split_same_length[of cpt] have Suc_i_lt1: ‹Suc i < length ?cpt1› by simp
from no_fin_before_non_fin[OF cpt Suc_m_lt Suc_m_not_fin] ‹i≤m›have
Suc_i_not_fin: ‹fst (cpt!Suc i) ≠ fin› by fast
from Suc_i_lt' split_length_le2[of cpt] have Suc_i_lt: ‹Suc i < length cpt› by simp
assume etran': ‹?cpt2'!i ─e→ ?cpt2'!Suc i›
then have etran: ‹?cpt2!i ─e→ ?cpt2!Suc i› using Suc_m_lt Suc_i_lt' by (simp add: split_def)
show ‹(snd (?cpt2'!i), snd (?cpt2'!Suc i)) ∈ rely ∪ guar1›
proof-
have ‹cpt ! i ─e→ cpt ! Suc i ∨ (?cpt1 ! i, ?cpt1 ! Suc i) ∈ estran Γ›
by (rule split_etran2[OF cpt fst_hd_cpt Suc_i_lt Suc_i_not_fin etran])
then show ?thesis
proof
assume etran: ‹cpt!i ─e→ cpt!Suc i›
with cpt_assume Suc_i_lt have ‹(snd (cpt!i), snd (cpt!Suc i)) ∈ rely›
by (simp add: assume_def)
then have ‹(snd (?cpt2!i), snd (?cpt2!Suc i)) ∈ rely›
using split_same_state2[OF Suc_i_lt2] split_same_state2[OF Suc_i_lt2[THEN Suc_lessD]] by argo
then have ‹(snd (?cpt2'!i), snd (?cpt2'!Suc i)) ∈ rely› using ‹i≤m› by simp
then show ‹(snd (?cpt2'!i), snd (?cpt2'!Suc i)) ∈ rely ∪ guar1› by simp
next
assume ctran1: ‹(?cpt1!i, ?cpt1!Suc i) ∈ estran Γ›
then have ‹(snd (?cpt1!i), snd (?cpt1!Suc i)) ∈ guar1›
proof(cases ‹i=m›)
case True
with ctran etran ctran_imp_not_etran show ?thesis by blast
next
case False
with ‹i≤m› have ‹i<m› by simp
show ?thesis using ctran1 h[THEN spec[where x=i], rule_format, OF ‹i<m›] by blast
qed
then have ‹(snd (cpt!i), snd(cpt!Suc i)) ∈ guar1›
using Suc_i_lt1 by (simp add: split_same_state1)
then have ‹(snd (?cpt2!i), snd (?cpt2!Suc i)) ∈ guar1›
using split_same_state2[OF Suc_i_lt2] split_same_state2[OF Suc_i_lt2[THEN Suc_lessD]] by argo
then have ‹(snd (?cpt2'!i), snd (?cpt2'!Suc i)) ∈ guar1› using ‹i≤m› by simp
then show ‹(snd (?cpt2'!i), snd (?cpt2'!Suc i)) ∈ rely ∪ guar1› by simp
qed
qed
qed
qed
moreover have ‹snd (hd ?cpt2') ∈ pre›
proof-
have ‹snd (hd cpt) ∈ pre› using cpt_assume by (simp add: assume_def)
then have ‹snd (hd ?cpt2) ∈ pre› using split_same_state2
by (metis ‹cpt ≠ []› cpt2' cpts_def' hd_conv_nth length_greater_0_conv take_eq_Nil)
then show ?thesis by simp
qed
ultimately have ‹?cpt2' ∈ assume pre2 rely2› using rely2 pre
by (auto simp add: assume_def)
with cpt2'_from have ‹?cpt2' ∈ cpts_from (estran Γ) (Q,s0) ∩ assume pre2 rely2› by blast
with valid2 have ‹?cpt2' ∈ commit (estran Γ) {fin} guar2 post2› by blast
then have ‹(snd (?cpt2' ! m), snd (?cpt2' ! Suc m)) ∈ guar2›
apply(simp add: commit_def)
apply clarify
apply(erule allE[where x=m])
using Suc_m_lt2 ctran' by simp
with not_guar Suc_m_lt show False by (simp add: Suc_m_lt Suc_lessD)
qed
qed
qed
lemma join_sound_aux3a:
‹(c1, c2) ∈ estran Γ ⟹ ∃P' Q'. fst c1 = P' ⋈ Q' ⟹ fst c2 = fin ⟹ ∀s. (s,s)∈guar ⟹ (snd c1, snd c2) ∈ guar›
apply(subst (asm) surjective_pairing[of c1])
apply(subst (asm) surjective_pairing[of c2])
apply(erule exE, erule exE)
apply(simp add: estran_def)
apply(erule exE)
apply(erule estran_p.cases, auto)
done
lemma split_assume_pre:
assumes cpt: "cpt ∈ cpts (estran Γ)"
assumes fst_hd_cpt: "fst (hd cpt) = P ⋈ Q"
assumes cpt_assume: "cpt ∈ assume pre rely"
shows
"snd (hd (fst (split cpt))) ∈ pre ∧
snd (hd (snd (split cpt))) ∈ pre"
proof-
from cpt_assume have pre: ‹snd (hd cpt) ∈ pre› using assume_def by blast
from cpt cpts_nonnil have "cpt≠[]" by blast
from pre hd_conv_nth[OF ‹cpt≠[]›] have ‹snd (cpt!0) ∈ pre› by simp
obtain s where hd_cpt_conv: ‹hd cpt = (P ⋈ Q, s)› using fst_hd_cpt surjective_pairing by metis
from ‹cpt≠[]› have 1:
‹snd (fst (split cpt)!0) ∈ pre›
apply-
apply(subst hd_Cons_tl[symmetric, of cpt]) apply assumption
using pre hd_cpt_conv by auto
from ‹cpt≠[]› have 2:
‹snd (snd (split cpt)!0) ∈ pre›
apply-
apply(subst hd_Cons_tl[symmetric, of cpt]) apply assumption
using pre hd_cpt_conv by auto
from cpt fst_hd_cpt have ‹cpt ∈ cpts_from (estran Γ) (P ⋈ Q, snd (hd cpt))›
using cpts_from_def' by (metis surjective_pairing)
from split_cpt[OF this] have cpt1:
"fst (split cpt) ∈ cpts (estran Γ)"
and cpt2:
"snd (split cpt) ∈ cpts (estran Γ)" by auto
from cpt1 cpts_nonnil have cpt1_nonnil: ‹fst(split cpt)≠[]› by blast
from cpt2 cpts_nonnil have cpt2_nonnil: ‹snd(split cpt)≠[]› by blast
from 1 2 hd_conv_nth[OF cpt1_nonnil] hd_conv_nth[OF cpt2_nonnil] show ?thesis by simp
qed
lemma join_sound_aux3_1:
‹cpt ∈ cpts_from (estran Γ) (P ⋈ Q, s0) ∩ assume pre rely ⟹
∀s0. cpts_from (estran Γ) (P, s0) ∩ assume pre1 rely1 ⊆ commit (estran Γ) {fin} guar1 post1 ⟹
∀s0. cpts_from (estran Γ) (Q, s0) ∩ assume pre2 rely2 ⊆ commit (estran Γ) {fin} guar2 post2 ⟹
pre ⊆ pre1 ∩ pre2 ⟹
rely ∪ guar2 ⊆ rely1 ⟹
rely ∪ guar1 ⊆ rely2 ⟹
Suc i < length (fst (split cpt)) ⟹
fst (split cpt)!i ─e→ fst (split cpt)!Suc i ⟹
(snd (fst (split cpt)!i), snd (fst (split cpt)!Suc i)) ∈ rely ∪ guar2›
proof-
assume cpt_from_assume: ‹cpt ∈ cpts_from (estran Γ) (P ⋈ Q, s0) ∩ assume pre rely›
then have cpt_from: ‹cpt ∈ cpts_from (estran Γ) (P ⋈ Q, s0)›
and cpt_assume: ‹cpt ∈ assume pre rely›
and ‹cpt≠[]› apply auto using cpts_nonnil by blast
from cpt_from have cpt: ‹cpt ∈ cpts (estran Γ)› and hd_cpt: ‹hd cpt = (P ⋈ Q, s0)› by auto
from hd_cpt have fst_hd_cpt: ‹fst (hd cpt) = P ⋈ Q› by simp
assume valid1: ‹∀s0. cpts_from (estran Γ) (P, s0) ∩ assume pre1 rely1 ⊆ commit (estran Γ) {fin} guar1 post1›
assume valid2: ‹∀s0. cpts_from (estran Γ) (Q, s0) ∩ assume pre2 rely2 ⊆ commit (estran Γ) {fin} guar2 post2›
assume pre: ‹pre ⊆ pre1 ∩ pre2›
assume rely1: ‹rely ∪ guar2 ⊆ rely1›
assume rely2: ‹rely ∪ guar1 ⊆ rely2›
let ?cpt1 = ‹fst (split cpt)›
let ?cpt2 = ‹snd (split cpt)›
assume Suc_i_lt1: ‹Suc i < length ?cpt1›
from Suc_i_lt1 split_same_length have Suc_i_lt2: ‹Suc i < length ?cpt2› by metis
from Suc_i_lt1 split_length_le1[of cpt] have Suc_i_lt: ‹Suc i < length cpt› by simp
assume etran1: ‹?cpt1!i ─e→ ?cpt1!Suc i›
from split_cpt[OF cpt_from, THEN conjunct1] have cpt1_from: ‹?cpt1 ∈ cpts_from (estran Γ) (P, s0)› .
from split_cpt[OF cpt_from, THEN conjunct2] have cpt2_from: ‹?cpt2 ∈ cpts_from (estran Γ) (Q, s0)› .
from cpt1_from have cpt1: ‹?cpt1 ∈ cpts (estran Γ)› by auto
from cpt2_from have cpt2: ‹?cpt2 ∈ cpts (estran Γ)› by auto
from cpts_nonnil[OF cpt1] have ‹?cpt1≠[]› .
from cpts_nonnil[OF cpt2] have ‹?cpt2≠[]› .
from ctran_or_etran[OF cpt Suc_i_lt]
show ‹(snd (?cpt1!i), snd(?cpt1!Suc i)) ∈ rely ∪ guar2›
proof
assume ctran_no_etran: ‹(cpt ! i, cpt ! Suc i) ∈ estran Γ ∧ ¬ cpt ! i ─e→ cpt ! Suc i›
from split_ctran1_aux[OF Suc_i_lt1] have Suc_i_not_fin: ‹fst (cpt ! Suc i) ≠ fin› .
from split_ctran[OF cpt fst_hd_cpt Suc_i_not_fin Suc_i_lt ctran_no_etran[THEN conjunct1]] show ?thesis
proof
assume ‹(fst (split cpt) ! i, fst (split cpt) ! Suc i) ∈ estran Γ ∧ snd (split cpt) ! i ─e→ snd (split cpt) ! Suc i›
with ctran_or_etran[OF cpt1 Suc_i_lt1] etran1 have False by blast
then show ?thesis by blast
next
assume ‹(snd (split cpt) ! i, snd (split cpt) ! Suc i) ∈ estran Γ ∧ fst (split cpt) ! i ─e→ fst (split cpt) ! Suc i›
from join_sound_aux2[OF cpt_from_assume valid1 valid2 pre rely1 rely2, rule_format, OF conjI[OF Suc_i_lt1 Suc_i_lt2], THEN conjunct2, rule_format, OF this[THEN conjunct1]]
have ‹(snd (snd (split cpt) ! i), snd (snd (split cpt) ! Suc i)) ∈ guar2› .
with split_same_state1[OF Suc_i_lt1] split_same_state1[OF Suc_i_lt1[THEN Suc_lessD]] split_same_state2[OF Suc_i_lt2] split_same_state2[OF Suc_i_lt2[THEN Suc_lessD]]
have ‹(snd (fst (split cpt) ! i), snd (fst (split cpt) ! Suc i)) ∈ guar2› by simp
then show ?thesis by blast
qed
next
assume ‹cpt ! i ─e→ cpt ! Suc i ∧ (cpt ! i, cpt ! Suc i) ∉ estran Γ›
from this[THEN conjunct1] cpt_assume have ‹(snd (cpt ! i), snd (cpt ! Suc i)) ∈ rely›
apply(auto simp add: assume_def)
apply(erule allE[where x=i])
using Suc_i_lt by blast
with split_same_state1[OF Suc_i_lt1] split_same_state1[OF Suc_i_lt1[THEN Suc_lessD]]
have ‹(snd (?cpt1!i), snd (?cpt1!Suc i)) ∈ rely› by simp
then show ?thesis by blast
qed
qed
lemma join_sound_aux3_2:
‹cpt ∈ cpts_from (estran Γ) (P ⋈ Q, s0) ∩ assume pre rely ⟹
∀s0. cpts_from (estran Γ) (P, s0) ∩ assume pre1 rely1 ⊆ commit (estran Γ) {fin} guar1 post1 ⟹
∀s0. cpts_from (estran Γ) (Q, s0) ∩ assume pre2 rely2 ⊆ commit (estran Γ) {fin} guar2 post2 ⟹
pre ⊆ pre1 ∩ pre2 ⟹
rely ∪ guar2 ⊆ rely1 ⟹
rely ∪ guar1 ⊆ rely2 ⟹
Suc i < length (snd (split cpt)) ⟹
snd (split cpt)!i ─e→ snd (split cpt)!Suc i ⟹
(snd (snd (split cpt)!i), snd (snd (split cpt)!Suc i)) ∈ rely ∪ guar1›
proof-
assume cpt_from_assume: ‹cpt ∈ cpts_from (estran Γ) (P ⋈ Q, s0) ∩ assume pre rely›
then have cpt_from: ‹cpt ∈ cpts_from (estran Γ) (P ⋈ Q, s0)›
and cpt_assume: ‹cpt ∈ assume pre rely›
and ‹cpt≠[]› apply auto using cpts_nonnil by blast
from cpt_from have cpt: ‹cpt ∈ cpts (estran Γ)› and hd_cpt: ‹hd cpt = (P ⋈ Q, s0)› by auto
from hd_cpt have fst_hd_cpt: ‹fst (hd cpt) = P ⋈ Q› by simp
assume valid1: ‹∀s0. cpts_from (estran Γ) (P, s0) ∩ assume pre1 rely1 ⊆ commit (estran Γ) {fin} guar1 post1›
assume valid2: ‹∀s0. cpts_from (estran Γ) (Q, s0) ∩ assume pre2 rely2 ⊆ commit (estran Γ) {fin} guar2 post2›
assume pre: ‹pre ⊆ pre1 ∩ pre2›
assume rely1: ‹rely ∪ guar2 ⊆ rely1›
assume rely2: ‹rely ∪ guar1 ⊆ rely2›
let ?cpt1 = ‹fst (split cpt)›
let ?cpt2 = ‹snd (split cpt)›
assume Suc_i_lt2: ‹Suc i < length ?cpt2›
from Suc_i_lt2 split_same_length have Suc_i_lt1: ‹Suc i < length ?cpt1› by metis
from Suc_i_lt2 split_length_le2[of cpt] have Suc_i_lt: ‹Suc i < length cpt› by simp
assume etran2: ‹?cpt2!i ─e→ ?cpt2!Suc i›
from split_cpt[OF cpt_from, THEN conjunct1] have cpt1_from: ‹?cpt1 ∈ cpts_from (estran Γ) (P, s0)› .
from split_cpt[OF cpt_from, THEN conjunct2] have cpt2_from: ‹?cpt2 ∈ cpts_from (estran Γ) (Q, s0)› .
from cpt1_from have cpt1: ‹?cpt1 ∈ cpts (estran Γ)› by auto
from cpt2_from have cpt2: ‹?cpt2 ∈ cpts (estran Γ)› by auto
from cpts_nonnil[OF cpt1] have ‹?cpt1≠[]› .
from cpts_nonnil[OF cpt2] have ‹?cpt2≠[]› .
from ctran_or_etran[OF cpt Suc_i_lt]
show ‹(snd (?cpt2!i), snd(?cpt2!Suc i)) ∈ rely ∪ guar1›
proof
assume ctran_no_etran: ‹(cpt ! i, cpt ! Suc i) ∈ estran Γ ∧ ¬ cpt ! i ─e→ cpt ! Suc i›
from split_ctran1_aux[OF Suc_i_lt1] have Suc_i_not_fin: ‹fst (cpt ! Suc i) ≠ fin› .
from split_ctran[OF cpt fst_hd_cpt Suc_i_not_fin Suc_i_lt ctran_no_etran[THEN conjunct1]] show ?thesis
proof
assume ‹(fst (split cpt) ! i, fst (split cpt) ! Suc i) ∈ estran Γ ∧ snd (split cpt) ! i ─e→ snd (split cpt) ! Suc i›
from join_sound_aux2[OF cpt_from_assume valid1 valid2 pre rely1 rely2, rule_format, OF conjI[OF Suc_i_lt1 Suc_i_lt2], THEN conjunct1, rule_format, OF this[THEN conjunct1]]
have ‹(snd (fst (split cpt) ! i), snd (fst (split cpt) ! Suc i)) ∈ guar1› .
with split_same_state1[OF Suc_i_lt1] split_same_state1[OF Suc_i_lt1[THEN Suc_lessD]] split_same_state2[OF Suc_i_lt2] split_same_state2[OF Suc_i_lt2[THEN Suc_lessD]]
have ‹(snd (snd (split cpt) ! i), snd (snd (split cpt) ! Suc i)) ∈ guar1› by simp
then show ?thesis by blast
next
assume ‹(snd (split cpt) ! i, snd (split cpt) ! Suc i) ∈ estran Γ ∧ fst (split cpt) ! i ─e→ fst (split cpt) ! Suc i›
with ctran_or_etran[OF cpt2 Suc_i_lt2] etran2 have False by blast
then show ?thesis by blast
qed
next
assume ‹cpt ! i ─e→ cpt ! Suc i ∧ (cpt ! i, cpt ! Suc i) ∉ estran Γ›
from this[THEN conjunct1] cpt_assume have ‹(snd (cpt ! i), snd (cpt ! Suc i)) ∈ rely›
apply(auto simp add: assume_def)
apply(erule allE[where x=i])
using Suc_i_lt by blast
with split_same_state2[OF Suc_i_lt2] split_same_state2[OF Suc_i_lt2[THEN Suc_lessD]]
have ‹(snd (?cpt2!i), snd (?cpt2!Suc i)) ∈ rely› by simp
then show ?thesis by blast
qed
qed
lemma split_cpt_nonnil:
‹cpt ≠ [] ⟹ fst (hd cpt) = P ⋈ Q ⟹ fst (split cpt) ≠ [] ∧ snd (split cpt) ≠ []›
apply(rule conjI)
apply(subst hd_Cons_tl[of cpt, symmetric]) apply assumption
apply(subst surjective_pairing[of ‹hd cpt›])
apply simp
apply(subst hd_Cons_tl[of cpt, symmetric]) apply assumption
apply(subst surjective_pairing[of ‹hd cpt›])
apply simp
done
lemma join_sound_aux5:
‹cpt ∈ cpts_from (estran Γ) (P ⋈ Q, S0) ∩ assume pre rely ⟹
∀S0. cpts_from (estran Γ) (P, S0) ∩ assume pre1 rely1 ⊆ commit (estran Γ) {fin} guar1 post1 ⟹
∀S0. cpts_from (estran Γ) (Q, S0) ∩ assume pre2 rely2 ⊆ commit (estran Γ) {fin} guar2 post2 ⟹
pre ⊆ pre1 ∩ pre2 ⟹
rely ∪ guar2 ⊆ rely1 ⟹
rely ∪ guar1 ⊆ rely2 ⟹
fst (last cpt) ∈ {fin} ⟶ snd (last cpt) ∈ post1 ∩ post2›
proof-
assume cpt_from_assume: ‹cpt ∈ cpts_from (estran Γ) (P ⋈ Q, S0) ∩ assume pre rely›
then have cpt: ‹cpt ∈ cpts (estran Γ)›
and fst_hd_cpt: ‹fst (hd cpt) = P ⋈ Q›
and cpt_assume: ‹cpt ∈ assume pre rely›
and cpt_from: ‹cpt ∈ cpts_from (estran Γ) (P ⋈ Q, S0)›
by auto
assume valid1: ‹∀S0. cpts_from (estran Γ) (P, S0) ∩ assume pre1 rely1 ⊆ commit (estran Γ) {fin} guar1 post1›
assume valid2: ‹∀S0. cpts_from (estran Γ) (Q, S0) ∩ assume pre2 rely2 ⊆ commit (estran Γ) {fin} guar2 post2›
assume pre: ‹pre ⊆ pre1 ∩ pre2›
assume rely1: ‹rely ∪ guar2 ⊆ rely1›
assume rely2: ‹rely ∪ guar1 ⊆ rely2›
let ?cpt1 = ‹fst (split cpt)›
let ?cpt2 = ‹snd (split cpt)›
from cpts_nonnil[OF cpt] have ‹cpt≠[]› .
from split_cpt_nonnil[OF ‹cpt≠[]› fst_hd_cpt, THEN conjunct1] have ‹?cpt1≠[]› .
from split_cpt_nonnil[OF ‹cpt≠[]› fst_hd_cpt, THEN conjunct2] have ‹?cpt2≠[]› .
show ?thesis
proof(cases ‹fst (last cpt) = fin›)
case True
with last_conv_nth[OF ‹cpt≠[]›] have ‹fst (cpt ! (length cpt - 1)) = fin› by simp
from exists_least[where P=‹λi. fst (cpt!i) = fin›, OF this]
obtain m where m: ‹fst (cpt ! m) = fin ∧ (∀i<m. fst (cpt ! i) ≠ fin)› by blast
note m_fin = m[THEN conjunct1]
have ‹m≠0›
apply(rule ccontr)
apply(insert m)
apply(insert ‹fst (hd cpt) = P ⋈ Q›)
apply(subst (asm) hd_conv_nth) apply(rule ‹cpt≠[]›)
apply simp
done
then obtain m' where m': ‹m = Suc m'› using not0_implies_Suc by blast
have m_lt: ‹m < length cpt›
proof(rule ccontr)
assume h: ‹¬ m < length cpt›
from m[THEN conjunct2] have ‹∀i<m. fst (cpt ! i) ≠ fin› .
then have ‹fst (cpt ! (length cpt - 1)) ≠ fin›
apply-
apply(erule allE[where x=‹length cpt - 1›])
using h by (metis ‹cpt ≠ []› diff_less length_greater_0_conv less_imp_diff_less linorder_neqE_nat zero_less_one)
with last_conv_nth[OF ‹cpt≠[]›] have ‹fst (last cpt) ≠ fin› by simp
with ‹fst (last cpt) = fin› show False by blast
qed
with m' have Suc_m'_lt: ‹Suc m' < length cpt› by simp
from m m' have m1: ‹fst (cpt ! Suc m') = fin ∧ (∀i<Suc m'. fst (cpt ! i) ≠ fin)› by simp
from m1[THEN conjunct1] obtain s where cpt_Suc_m': ‹cpt!Suc m' = (fin, s)› using surjective_pairing by metis
from m1 have m'_not_fin: ‹fst (cpt!m') ≠ fin›
apply clarify
apply(erule allE[where x=m'])
by fast
have ‹fst (cpt!m') = fin ⋈ fin›
proof-
from ctran_or_etran[OF cpt Suc_m'_lt]
have ‹(cpt ! m', cpt ! Suc m') ∈ estran Γ ∧ ¬ cpt ! m' ─e→ cpt ! Suc m' ∨ cpt ! m' ─e→ cpt ! Suc m' ∧ (cpt ! m', cpt ! Suc m') ∉ estran Γ› .
moreover have ‹¬ cpt ! m' ─e→ cpt ! Suc m'›
proof(rule ccontr, simp)
assume h: ‹fst (cpt ! m') = fst (cpt ! Suc m')›
from m1[THEN conjunct1] m'_not_fin h show False by simp
qed
ultimately have ctran: ‹(cpt ! m', cpt ! Suc m') ∈ estran Γ› by blast
with cpt_Suc_m' show ?thesis
apply(simp add: estran_def)
apply(erule exE)
apply(insert all_join[OF cpt fst_hd_cpt Suc_m'_lt[THEN Suc_lessD] m'_not_fin, rule_format, of m'])
apply(erule estran_p.cases, auto)
done
qed
have ‹length ?cpt1 = m ∧ length ?cpt2 = m›
using split_length[OF cpt fst_hd_cpt Suc_m'_lt m'_not_fin m1[THEN conjunct1]] m' by simp
then have ‹length ?cpt1 = m› and ‹length ?cpt2 = m› by auto
from ‹length ?cpt1 = m› m_lt have cpt1_shorter: ‹length ?cpt1 < length cpt› by simp
from ‹length ?cpt2 = m› m_lt have cpt2_shorter: ‹length ?cpt2 < length cpt› by simp
have ‹m' < length ?cpt1› using ‹length ?cpt1 = m› m' by simp
from split_prog1[OF this ‹fst (cpt!m') = fin ⋈ fin›]
have ‹fst (fst (split cpt) ! m') = fin› .
moreover have ‹last ?cpt1 = ?cpt1 ! m'›
apply(subst last_conv_nth[OF ‹?cpt1≠[]›])
using m' ‹length ?cpt1 = m› by simp
ultimately have ‹fst (last (fst (split cpt))) = fin› by simp
have ‹m' < length ?cpt2› using ‹length ?cpt2 = m› m' by simp
from split_prog2[OF this ‹fst (cpt!m') = fin ⋈ fin›]
have ‹fst (snd (split cpt) ! m') = fin› .
moreover have ‹last ?cpt2 = ?cpt2 ! m'›
apply(subst last_conv_nth[OF ‹?cpt2≠[]›])
using m' ‹length ?cpt2 = m› by simp
ultimately have ‹fst (last (snd (split cpt))) = fin› by simp
let ?cpt1' = ‹?cpt1 @ drop (Suc m) cpt›
let ?cpt2' = ‹?cpt2 @ drop (Suc m) cpt›
from split_cpt[OF cpt_from, THEN conjunct1, simplified, THEN conjunct2]
have ‹hd (fst (split cpt)) = (P, S0)› .
with hd_Cons_tl[OF ‹?cpt1≠[]›]
have ‹?cpt1 = (P,S0) # tl ?cpt1› by simp
from split_cpt[OF cpt_from, THEN conjunct2, simplified, THEN conjunct2]
have ‹hd (snd (split cpt)) = (Q, S0)› .
with hd_Cons_tl[OF ‹?cpt2≠[]›]
have ‹?cpt2 = (Q,S0) # tl ?cpt2› by simp
have cpt'_from: ‹?cpt1' ∈ cpts_from (estran Γ) (P,S0) ∧ ?cpt2' ∈ cpts_from (estran Γ) (Q,S0)›
proof(cases ‹Suc m < length cpt›)
case True
then have ‹m < length cpt› by simp
have ‹m < Suc m› by simp
from all_fin_after_fin''[OF cpt ‹m < length cpt› m_fin, rule_format, OF ‹m < Suc m› True]
have ‹fst (cpt ! Suc m) = fin› .
then have ‹fst (hd (drop (Suc m) cpt)) = fin› by (simp add: True hd_drop_conv_nth)
show ?thesis
apply auto
apply(rule cpts_append_env)
using split_cpt cpt_from_assume apply fastforce
apply(rule cpts_drop[OF cpt True])
apply(simp add: ‹fst (last (fst (split cpt))) = fin› ‹fst (hd (drop (Suc m) cpt)) = fin›)
apply(subst ‹?cpt1 = (P,S0) # tl (fst (split cpt))›)
apply simp
apply(rule cpts_append_env)
using split_cpt cpt_from_assume apply fastforce
apply(rule cpts_drop[OF cpt True])
apply(simp add: ‹fst (last (snd (split cpt))) = fin› ‹fst (hd (drop (Suc m) cpt)) = fin›)
apply(subst ‹?cpt2 = (Q,S0) # tl ?cpt2›)
apply simp
done
next
case False
then have ‹length cpt ≤ Suc m› by simp
from drop_all[OF this]
show ?thesis
apply auto
using split_cpt cpt_from_assume apply fastforce
apply(rule ‹hd (fst (split cpt)) = (P, S0)›)
using split_cpt cpt_from_assume apply fastforce
apply(rule ‹hd (snd (split cpt)) = (Q, S0)›)
done
qed
from cpt_from[simplified, THEN conjunct2] have ‹hd cpt = (P ⋈ Q, S0)› .
have ‹S0 ∈ pre›
using cpt_assume apply(simp add: assume_def)
apply(drule conjunct1)
by (simp add: ‹hd cpt = (P ⋈ Q, S0)›)
have cpt'_assume: ‹?cpt1' ∈ assume pre1 rely1 ∧ ?cpt2' ∈ assume pre2 rely2›
proof(auto simp add: assume_def)
show ‹snd (hd (fst (split cpt) @ drop (Suc m) cpt)) ∈ pre1›
apply(subst ‹?cpt1 = (P,S0) # tl ?cpt1›)
apply simp
using ‹S0∈pre› pre by blast
next
fix i
assume ‹Suc i < length ?cpt1 + (length cpt - Suc m)›
with ‹length ?cpt1 = m› Suc_leI[OF m_lt] have ‹Suc (Suc i) < length cpt› by linarith
then have ‹Suc i < length cpt› by simp
assume ‹fst (?cpt1'!i) = fst (?cpt1'!Suc i)›
show ‹(snd (?cpt1'!i), snd (?cpt1'!Suc i)) ∈ rely1›
proof(cases ‹Suc i < length ?cpt1›)
case True
from True have ‹?cpt1'!i = ?cpt1!i›
by (simp add: Suc_lessD nth_append)
from True have ‹?cpt1'!Suc i = ?cpt1!Suc i›
by (simp add: nth_append)
from ‹fst (?cpt1'!i) = fst (?cpt1'!Suc i)› ‹?cpt1'!i = ?cpt1!i› ‹?cpt1'!Suc i = ?cpt1!Suc i›
have ‹?cpt1!i ─e→ ?cpt1!Suc i› by simp
have ‹(snd (fst (split cpt) ! i), snd (fst (split cpt) ! Suc i)) ∈ rely1›
using join_sound_aux3_1[OF cpt_from_assume valid1 valid2 pre rely1 rely2 True ‹?cpt1!i ─e→ ?cpt1!Suc i›] rely1 by blast
then show ?thesis
by (simp add: ‹?cpt1'!i = ?cpt1!i› ‹?cpt1'!Suc i = ?cpt1!Suc i›)
next
case False
then have Suc_i_ge: ‹Suc i ≥ length ?cpt1› by simp
show ?thesis
proof(cases ‹Suc i = length ?cpt1›)
case True
then have ‹i < length ?cpt1› by linarith
from cpt1_shorter True have ‹Suc i < length cpt› by simp
from True ‹length ?cpt1 = m› have ‹Suc i = m› by simp
with m' have ‹i = m'› by simp
with ‹fst (cpt!m') = fin ⋈ fin› have ‹fst (cpt!i) = fin ⋈ fin› by simp
from ‹Suc i < length ?cpt1 + (length cpt - Suc m)› ‹Suc i = m› ‹length ?cpt1 = m›
have ‹Suc m < length cpt› by simp
from ‹Suc i = m› m_fin have ‹fst (cpt!Suc i) = fin› by simp
have conv1: ‹snd (?cpt1' ! i) = snd (cpt ! Suc i)›
proof-
have ‹snd (?cpt1'!i) = snd (?cpt1!i)› using True by (simp add: nth_append)
moreover have ‹snd (?cpt1!i) = snd (cpt!i)›
using split_same_state1[OF ‹i < length ?cpt1›] .
moreover have ‹snd (cpt!i) = snd (cpt!Suc i)›
proof-
from ctran_or_etran[OF cpt ‹Suc i < length cpt›] ‹fst (cpt!i) = fin ⋈ fin› ‹fst (cpt!Suc i) = fin›
have ‹(cpt ! i, cpt ! Suc i) ∈ estran Γ› by fastforce
then show ?thesis
apply(subst (asm) surjective_pairing[of ‹cpt!i›])
apply(subst (asm) surjective_pairing[of ‹cpt!Suc i›])
apply(simp add: ‹fst (cpt!i) = fin ⋈ fin› ‹fst (cpt!Suc i) = fin› estran_def)
apply(erule exE)
apply(erule estran_p.cases, auto)
done
qed
ultimately show ?thesis by simp
qed
have conv2: ‹snd (?cpt1' ! Suc i) = snd (cpt ! Suc (Suc i))›
apply(simp add: nth_append True)
apply(subst nth_drop) apply(rule Suc_leI[OF m_lt])
apply(simp add: ‹length ?cpt1 = m›)
done
have ‹(snd (cpt ! Suc i), snd (cpt ! Suc (Suc i))) ∈ rely›
proof-
have ‹m<Suc m› by simp
from all_fin_after_fin''[OF cpt m_lt m_fin, rule_format, OF this ‹Suc m < length cpt›]
have Suc_m_fin: ‹fst (cpt ! Suc m) = fin› .
from cpt_assume show ?thesis
apply(simp add: assume_def)
apply(drule conjunct2)
apply(erule allE[where x=m])
using ‹Suc m < length cpt› m_fin Suc_m_fin ‹Suc i = m› by argo
qed
then show ?thesis
apply(simp add: conv1 conv2) using rely1 by blast
next
case False
with Suc_i_ge have Suc_i_gt: ‹Suc i > length ?cpt1› by linarith
with ‹length ?cpt1 = m› have ‹¬ i < m› by simp
then have ‹m < Suc i› by simp
then have ‹m < Suc (Suc i)› by simp
have conv1: ‹?cpt1'!i = cpt!Suc i›
apply(simp add: nth_append Suc_i_gt ‹length ?cpt1 = m› ‹¬ i < m›)
apply(subst nth_drop) apply(rule Suc_leI[OF m_lt])
using ‹¬i<m› by simp
have conv2: ‹?cpt1'!Suc i = cpt!Suc(Suc i)›
using Suc_i_gt apply(simp add: nth_append)
apply(subst nth_drop) apply(rule Suc_leI[OF m_lt])
by (simp add: ‹length ?cpt1 = m›)
from all_fin_after_fin''[OF cpt m_lt m_fin, rule_format, OF ‹m < Suc i› ‹Suc i < length cpt›]
have ‹fst (cpt ! Suc i) = fin› .
from all_fin_after_fin''[OF cpt m_lt m_fin, rule_format, OF ‹m < Suc (Suc i)› ‹Suc (Suc i) < length cpt›]
have ‹fst (cpt ! Suc (Suc i)) = fin› .
from cpt_assume show ?thesis
apply(simp add: assume_def conv1 conv2)
apply(drule conjunct2)
apply(erule allE[where x=‹Suc i›])
using ‹Suc (Suc i) < length cpt› ‹fst (cpt ! Suc i) = fin› ‹fst (cpt ! Suc (Suc i)) = fin› rely1 by auto
qed
qed
next
show ‹snd (hd (snd (split cpt) @ drop (Suc m) cpt)) ∈ pre2›
apply(subst ‹?cpt2 = (Q,S0) # tl ?cpt2›)
apply simp
using ‹S0∈pre› pre by blast
next
fix i
assume ‹Suc i < length ?cpt2 + (length cpt - Suc m)›
with ‹length ?cpt2 = m› Suc_leI[OF m_lt] have ‹Suc (Suc i) < length cpt› by linarith
then have ‹Suc i < length cpt› by simp
assume ‹fst (?cpt2'!i) = fst (?cpt2'!Suc i)›
show ‹(snd (?cpt2'!i), snd (?cpt2'!Suc i)) ∈ rely2›
proof(cases ‹Suc i < length ?cpt2›)
case True
from True have conv1: ‹?cpt2'!i = ?cpt2!i›
by (simp add: Suc_lessD nth_append)
from True have conv2: ‹?cpt2'!Suc i = ?cpt2!Suc i›
by (simp add: nth_append)
from ‹fst (?cpt2'!i) = fst (?cpt2'!Suc i)› conv1 conv2
have ‹?cpt2!i ─e→ ?cpt2!Suc i› by simp
have ‹(snd (snd (split cpt) ! i), snd (snd (split cpt) ! Suc i)) ∈ rely2›
using join_sound_aux3_2[OF cpt_from_assume valid1 valid2 pre rely1 rely2 True ‹?cpt2!i ─e→ ?cpt2!Suc i›] rely2 by blast
then show ?thesis
by (simp add: conv1 conv2)
next
case False
then have Suc_i_ge: ‹Suc i ≥ length ?cpt2› by simp
show ?thesis
proof(cases ‹Suc i = length ?cpt2›)
case True
then have ‹i < length ?cpt2› by linarith
from cpt2_shorter True have ‹Suc i < length cpt› by simp
from True ‹length ?cpt2 = m› have ‹Suc i = m› by simp
with m' have ‹i = m'› by simp
with ‹fst (cpt!m') = fin ⋈ fin› have ‹fst (cpt!i) = fin ⋈ fin› by simp
from ‹Suc i < length ?cpt2 + (length cpt - Suc m)› ‹Suc i = m› ‹length ?cpt2 = m›
have ‹Suc m < length cpt› by simp
from ‹Suc i = m› m_fin have ‹fst (cpt!Suc i) = fin› by simp
have conv1: ‹snd (?cpt2' ! i) = snd (cpt ! Suc i)›
proof-
have ‹snd (?cpt2'!i) = snd (?cpt2!i)› using True by (simp add: nth_append)
moreover have ‹snd (?cpt2!i) = snd (cpt!i)›
using split_same_state2[OF ‹i < length ?cpt2›] .
moreover have ‹snd (cpt!i) = snd (cpt!Suc i)›
proof-
from ctran_or_etran[OF cpt ‹Suc i < length cpt›] ‹fst (cpt!i) = fin ⋈ fin› ‹fst (cpt!Suc i) = fin›
have ‹(cpt ! i, cpt ! Suc i) ∈ estran Γ› by fastforce
then show ?thesis
apply(subst (asm) surjective_pairing[of ‹cpt!i›])
apply(subst (asm) surjective_pairing[of ‹cpt!Suc i›])
apply(simp add: ‹fst (cpt!i) = fin ⋈ fin› ‹fst (cpt!Suc i) = fin› estran_def)
apply(erule exE)
apply(erule estran_p.cases, auto)
done
qed
ultimately show ?thesis by simp
qed
have conv2: ‹snd (?cpt2' ! Suc i) = snd (cpt ! Suc (Suc i))›
apply(simp add: nth_append True)
apply(subst nth_drop) apply(rule Suc_leI[OF m_lt])
apply(simp add: ‹length ?cpt2 = m›)
done
have ‹(snd (cpt ! Suc i), snd (cpt ! Suc (Suc i))) ∈ rely›
proof-
have ‹m<Suc m› by simp
from all_fin_after_fin''[OF cpt m_lt m_fin, rule_format, OF this ‹Suc m < length cpt›]
have Suc_m_fin: ‹fst (cpt ! Suc m) = fin› .
from cpt_assume show ?thesis
apply(simp add: assume_def)
apply(drule conjunct2)
apply(erule allE[where x=m])
using ‹Suc m < length cpt› m_fin Suc_m_fin ‹Suc i = m› by argo
qed
then show ?thesis
apply(simp add: conv1 conv2) using rely2 by blast
next
case False
with Suc_i_ge have Suc_i_gt: ‹Suc i > length ?cpt2› by linarith
with ‹length ?cpt2 = m› have ‹¬ i < m› by simp
then have ‹m < Suc i› by simp
then have ‹m < Suc (Suc i)› by simp
have conv1: ‹?cpt2'!i = cpt!Suc i›
apply(simp add: nth_append Suc_i_gt ‹length ?cpt2 = m› ‹¬ i < m›)
apply(subst nth_drop) apply(rule Suc_leI[OF m_lt])
using ‹¬i<m› by simp
have conv2: ‹?cpt2'!Suc i = cpt!Suc(Suc i)›
using Suc_i_gt apply(simp add: nth_append)
apply(subst nth_drop) apply(rule Suc_leI[OF m_lt])
by (simp add: ‹length ?cpt2 = m›)
from all_fin_after_fin''[OF cpt m_lt m_fin, rule_format, OF ‹m < Suc i› ‹Suc i < length cpt›]
have ‹fst (cpt ! Suc i) = fin› .
from all_fin_after_fin''[OF cpt m_lt m_fin, rule_format, OF ‹m < Suc (Suc i)› ‹Suc (Suc i) < length cpt›]
have ‹fst (cpt ! Suc (Suc i)) = fin› .
from cpt_assume show ?thesis
apply(simp add: assume_def conv1 conv2)
apply(drule conjunct2)
apply(erule allE[where x=‹Suc i›])
using ‹Suc (Suc i) < length cpt› ‹fst (cpt ! Suc i) = fin› ‹fst (cpt ! Suc (Suc i)) = fin› rely2 by auto
qed
qed
qed
from cpt'_from cpt'_assume valid1 valid2
have
commit1: ‹?cpt1' ∈ commit (estran Γ) {fin} guar1 post1› and
commit2: ‹?cpt2' ∈ commit (estran Γ) {fin} guar2 post2› by blast+
from ctran_or_etran[OF cpt Suc_m'_lt] ‹fst (cpt!m') = fin ⋈ fin› ‹fst (cpt!Suc m') = fin›
have ‹(cpt ! m', cpt ! Suc m') ∈ estran Γ› by fastforce
then have ‹snd (cpt!m') = snd (cpt!m)›
apply(subst ‹m = Suc m'›)
apply(simp add: estran_def)
apply(erule exE)
apply(insert ‹fst (cpt!m') = fin ⋈ fin›)
apply(insert ‹fst (cpt!Suc m') = fin›)
apply(erule estran_p.cases, auto)
done
have last_conv1: ‹last ?cpt1' = last cpt›
proof(cases ‹Suc m = length cpt›)
case True
then have ‹m = length cpt - 1› by linarith
have ‹snd (last ?cpt1) = snd (cpt ! m')›
apply(simp add: ‹last ?cpt1 = ?cpt1 ! m'›)
by (rule split_same_state1[OF ‹m' < length ?cpt1›])
moreover have ‹cpt!m = last cpt›
apply(subst last_conv_nth[OF ‹cpt≠[]›])
using ‹m = length cpt - 1› by simp
ultimately have ‹snd (last ?cpt1) = snd (last cpt)› using ‹snd (cpt!m') = snd (cpt!m)› by argo
with ‹fst (last ?cpt1) = fin› ‹fst (last cpt) = fin› show ?thesis
apply(simp add: True)
using surjective_pairing by metis
next
case False
with ‹m < length cpt› have ‹Suc m < length cpt› by linarith
then show ?thesis by simp
qed
have last_conv2: ‹last ?cpt2' = last cpt›
proof(cases ‹Suc m = length cpt›)
case True
then have ‹m = length cpt - 1› by linarith
have ‹snd (last ?cpt2) = snd (cpt ! m')›
apply(simp add: ‹last ?cpt2 = ?cpt2 ! m'›)
by (rule split_same_state2[OF ‹m' < length ?cpt2›])
moreover have ‹cpt!m = last cpt›
apply(subst last_conv_nth[OF ‹cpt≠[]›])
using ‹m = length cpt - 1› by simp
ultimately have ‹snd (last ?cpt2) = snd (last cpt)› using ‹snd (cpt!m') = snd (cpt!m)› by argo
with ‹fst (last ?cpt2) = fin› ‹fst (last cpt) = fin› show ?thesis
apply(simp add: True)
using surjective_pairing by metis
next
case False
with ‹m < length cpt› have ‹Suc m < length cpt› by linarith
then show ?thesis by simp
qed
from commit1 commit2
show ?thesis apply(simp add: commit_def)
apply(drule conjunct2)
apply(drule conjunct2)
using last_conv1 last_conv2 by argo
next
case False
have ‹?cpt1 ∈ cpts_from (estran Γ) (P,S0)› using cpt_from_assume split_cpt by blast
moreover have ‹?cpt1 ∈ assume pre1 rely1›
proof(auto simp add: assume_def)
from split_assume_pre[OF cpt fst_hd_cpt cpt_assume, THEN conjunct1] pre
show ‹snd (hd (fst (split cpt))) ∈ pre1› by blast
next
fix i
assume etran: ‹fst (fst (split cpt) ! i) = fst (fst (split cpt) ! Suc i)›
assume Suc_i_lt1: ‹Suc i < length (fst (split cpt))›
from join_sound_aux3_1[OF cpt_from_assume valid1 valid2 pre rely1 rely2 Suc_i_lt1] etran
have ‹(snd (fst (split cpt) ! i), snd (fst (split cpt) ! Suc i)) ∈ rely ∪ guar2› by force
then show ‹(snd (fst (split cpt) ! i), snd (fst (split cpt) ! Suc i)) ∈ rely1› using rely1 by blast
qed
ultimately have cpt1_commit: ‹?cpt1 ∈ commit (estran Γ) {fin} guar1 post1› using valid1 by blast
have ‹?cpt2 ∈ cpts_from (estran Γ) (Q,S0)› using cpt_from_assume split_cpt by blast
moreover have ‹?cpt2 ∈ assume pre2 rely2›
proof(auto simp add: assume_def)
show ‹snd (hd (snd (split cpt))) ∈ pre2›
using split_assume_pre[OF cpt fst_hd_cpt cpt_assume] pre by blast
next
fix i
assume etran: ‹fst (?cpt2!i) = fst (?cpt2!Suc i)›
assume Suc_i_lt2: ‹Suc i < length ?cpt2›
from join_sound_aux3_2[OF cpt_from_assume valid1 valid2 pre rely1 rely2 Suc_i_lt2] etran
have ‹(snd (snd (split cpt) ! i), snd (snd (split cpt) ! Suc i)) ∈ rely ∪ guar1› by force
then show ‹(snd (?cpt2!i), snd (?cpt2!Suc i)) ∈ rely2› using rely2 by blast
qed
ultimately have cpt2_commit: ‹?cpt2 ∈ commit (estran Γ) {fin} guar2 post2› using valid2 by blast
from cpt1_commit commit_def have
‹fst (last ?cpt1) ∈ {fin} ⟶ snd (last ?cpt1) ∈ post1› by fastforce
moreover from cpt2_commit commit_def have
‹fst (last ?cpt2) ∈ {fin} ⟶ snd (last ?cpt2) ∈ post2› by fastforce
ultimately show ‹fst (last cpt) ∈ {fin} ⟶ snd (last cpt) ∈ post1 ∩ post2›
using False by blast
qed
qed
lemma split_length_gt:
assumes cpt: ‹cpt ∈ cpts (estran Γ)›
and fst_hd_cpt: ‹fst (hd cpt) = P ⋈ Q›
and i_lt: ‹i < length cpt›
and not_fin: ‹fst (cpt!i) ≠ fin›
shows ‹length (fst (split cpt)) > i ∧ length (snd (split cpt)) > i›
proof-
from all_join[OF cpt fst_hd_cpt i_lt not_fin]
have 1: ‹∀ia≤i. ∃P' Q'. fst (cpt ! ia) = P' ⋈ Q'› .
from cpt fst_hd_cpt i_lt not_fin 1
show ?thesis
proof(induct cpt arbitrary:P Q i rule:split.induct; simp; case_tac ia; simp)
fix s Pa Qa ia nat
fix rest
assume IH:
‹⋀P Q i.
rest ∈ cpts (estran Γ) ⟹
fst (hd rest) = P ⋈ Q ⟹
i < length rest ⟹
fst (rest ! i) ≠ fin ⟹
∀ia≤i. ∃P' Q'. fst (rest ! ia) = P' ⋈ Q' ⟹
i < length (fst (split rest)) ∧ i < length (snd (split rest))›
assume a1: ‹(Pa ⋈ Qa, s) # rest ∈ cpts (estran Γ)›
assume a2: ‹nat < length rest›
assume a3: ‹fst (rest ! nat) ≠ fin›
assume a4: ‹∀ia≤Suc nat. ∃P' Q'. fst (((Pa ⋈ Qa, s) # rest) ! ia) = P' ⋈ Q'›
from a2 have "rest≠[]" by fastforce
from cpts_tl[OF a1, simplified, OF ‹rest≠[]›] have 1: ‹rest ∈ cpts (estran Γ)› .
from a4 have 5: ‹∀ia≤nat. ∃P' Q'. fst (rest ! ia) = P' ⋈ Q'› by auto
from a4[THEN spec[where x=1]] have ‹∃P' Q'. fst (((Pa ⋈ Qa, s) # rest) ! 1) = P' ⋈ Q'› by force
then have ‹∃P' Q'. fst (hd rest) = P' ⋈ Q'›
apply simp
apply(subst hd_conv_nth) apply(rule ‹rest≠[]›) apply assumption done
then obtain P' Q' where 2: ‹fst (hd rest) = P' ⋈ Q'› by blast
from IH[OF 1 2 a2 a3 5]
show ‹nat < length (fst (split rest)) ∧ nat < length (snd (split rest))› .
qed
qed
lemma Join_sound_aux:
assumes h1:
‹Γ ⊨ P sat⇩e [pre1, rely1, guar1, post1]›
assumes h2:
‹Γ ⊨ Q sat⇩e [pre2, rely2, guar2, post2]›
and rely1: ‹rely ∪ guar2 ⊆ rely1›
and rely2: ‹rely ∪ guar1 ⊆ rely2›
and guar_refl: ‹∀s. (s,s)∈guar›
and guar: ‹guar1 ∪ guar2 ⊆ guar›
shows
‹Γ ⊨ EJoin P Q sat⇩e [pre1 ∩ pre2, rely, guar, post1 ∩ post2]›
using h1 h2
proof(unfold es_validity_def validity_def)
let ?pre1 = ‹lift_state_set pre1›
let ?pre2 = ‹lift_state_set pre2›
let ?rely = ‹lift_state_pair_set rely›
let ?rely1 = ‹lift_state_pair_set rely1›
let ?rely2 = ‹lift_state_pair_set rely2›
let ?guar = ‹lift_state_pair_set guar›
let ?guar1 = ‹lift_state_pair_set guar1›
let ?guar2 = ‹lift_state_pair_set guar2›
let ?post1 = ‹lift_state_set post1›
let ?post2 = ‹lift_state_set post2›
let ?inter_pre = ‹lift_state_set (pre1∩pre2)›
let ?inter_post = ‹lift_state_set (post1∩post2)›
have rely1': ‹?rely ∪ ?guar2 ⊆ ?rely1›
apply standard
apply(simp add: lift_state_pair_set_def case_prod_unfold)
using rely1 by blast
have rely2': ‹?rely ∪ ?guar1 ⊆ ?rely2›
apply standard
apply(simp add: lift_state_pair_set_def case_prod_unfold)
using rely2 by blast
have guar_refl': ‹∀S. (S,S)∈?guar› using guar_refl lift_state_pair_set_def by blast
have guar': ‹?guar1 ∪ ?guar2 ⊆ ?guar›
apply standard
apply(simp add: lift_state_pair_set_def case_prod_unfold)
using guar by blast
assume h1': ‹∀s0. cpts_from (estran Γ) (P, s0) ∩ assume ?pre1 ?rely1 ⊆ commit (estran Γ) {fin} ?guar1 ?post1›
assume h2': ‹∀s0. cpts_from (estran Γ) (Q, s0) ∩ assume ?pre2 ?rely2 ⊆ commit (estran Γ) {fin} ?guar2 ?post2›
show ‹∀s0. cpts_from (estran Γ) (P ⋈ Q, s0) ∩ assume ?inter_pre ?rely ⊆ commit (estran Γ) {fin} ?guar ?inter_post›
proof
fix s0
show ‹cpts_from (estran Γ) (P ⋈ Q, s0) ∩ assume ?inter_pre ?rely ⊆ commit (estran Γ) {fin} ?guar ?inter_post›
proof
fix cpt
assume cpt_from_assume: ‹cpt ∈ cpts_from (estran Γ) (P ⋈ Q, s0) ∩ assume ?inter_pre ?rely›
then have
cpt_from: ‹cpt ∈ cpts_from (estran Γ) (P ⋈ Q, s0)› and
cpt: ‹cpt ∈ cpts (estran Γ)› and
fst_hd_cpt: ‹fst (hd cpt) = P ⋈ Q› and
cpt_assume: ‹cpt ∈ assume ?inter_pre ?rely› by auto
show ‹cpt ∈ commit (estran Γ) {fin} ?guar ?inter_post›
proof-
let ?cpt1 = ‹fst (split cpt)›
let ?cpt2 = ‹snd (split cpt)›
from split_cpt[OF cpt_from, THEN conjunct1] have "?cpt1 ∈ cpts_from (estran Γ) (P, s0)" .
then have ‹?cpt1≠[]› using cpts_nonnil by auto
from split_cpt[OF cpt_from, THEN conjunct2] have "?cpt2 ∈ cpts_from (estran Γ) (Q, s0)" .
then have ‹?cpt2≠[]› using cpts_nonnil by auto
from cpts_nonnil[OF cpt] have ‹cpt≠[]› .
from join_sound_aux2[OF cpt_from_assume h1' h2' _ rely1' rely2']
have 2:
‹∀i. Suc i < length ?cpt1 ∧ Suc i < length ?cpt2 ⟶
((?cpt1 ! i, ?cpt1 ! Suc i) ∈ estran Γ ⟶
(snd (?cpt1 ! i), snd (?cpt1 ! Suc i)) ∈ ?guar1) ∧
((?cpt2 ! i, ?cpt2 ! Suc i) ∈ estran Γ ⟶
(snd (?cpt2 ! i), snd (?cpt2 ! Suc i)) ∈ ?guar2)› unfolding lift_state_set_def by blast
show ?thesis using cpt_from_assume
proof(auto simp add: assume_def commit_def)
fix i
assume Suc_i_lt: ‹Suc i < length cpt›
assume ctran: ‹(cpt ! i, cpt ! Suc i) ∈ estran Γ›
show ‹(snd (cpt ! i), snd (cpt ! Suc i)) ∈ ?guar›
proof(cases ‹fst (cpt!Suc i) = fin›)
case True
have ‹fst (cpt ! i) ≠ fin› by (rule no_estran_from_fin'[OF ctran])
from all_join[OF cpt fst_hd_cpt Suc_i_lt[THEN Suc_lessD] this, THEN spec[where x=i]] have
‹∃P' Q'. fst (cpt ! i) = P' ⋈ Q'› by simp
from join_sound_aux3a[OF ctran this True guar_refl'] show ?thesis .
next
case False
from split_length_gt[OF cpt fst_hd_cpt Suc_i_lt False]
have
Suc_i_lt1: ‹Suc i < length ?cpt1› and
Suc_i_lt2: ‹Suc i < length ?cpt2› by auto
from split_ctran[OF cpt fst_hd_cpt False Suc_i_lt ctran] have
"(?cpt1!i, ?cpt1!Suc i) ∈ estran Γ ∨
(?cpt2!i, ?cpt2!Suc i) ∈ estran Γ" by fast
then show ?thesis
proof
assume ‹(?cpt1 ! i, ?cpt1 ! Suc i) ∈ estran Γ›
with 2 Suc_i_lt1 Suc_i_lt2 have ‹(snd (?cpt1!i), snd (?cpt1!Suc i)) ∈ ?guar1› by blast
with split_same_state1[OF Suc_i_lt1[THEN Suc_lessD]] split_same_state1[OF Suc_i_lt1]
have ‹(snd (cpt!i), snd (cpt!Suc i)) ∈ ?guar1› by argo
with guar' show ‹(snd (cpt ! i), snd (cpt ! Suc i)) ∈ ?guar› by blast
next
assume ‹(?cpt2 ! i, ?cpt2 ! Suc i) ∈ estran Γ›
with 2 Suc_i_lt1 Suc_i_lt2 have ‹(snd (?cpt2!i), snd (?cpt2!Suc i)) ∈ ?guar2› by blast
with split_same_state2[OF Suc_i_lt2[THEN Suc_lessD]] split_same_state2[OF Suc_i_lt2]
have ‹(snd (cpt!i), snd (cpt!Suc i)) ∈ ?guar2› by argo
with guar' show ‹(snd (cpt ! i), snd (cpt ! Suc i)) ∈ ?guar› by blast
qed
qed
next
have 1: ‹fst (last cpt) = fin ⟹ snd (last cpt) ∈ ?post1›
using join_sound_aux5[OF cpt_from_assume h1' h2' _ rely1' rely2'] unfolding lift_state_set_def by fastforce
have 2: ‹fst (last cpt) = fin ⟹ snd (last cpt) ∈ ?post2›
using join_sound_aux5[OF cpt_from_assume h1' h2' _ rely1' rely2'] unfolding lift_state_set_def by fastforce
from 1 2
show ‹fst (last cpt) = fin ⟹ snd (last cpt) ∈ lift_state_set (post1 ∩ post2)›
by (simp add: lift_state_set_def case_prod_unfold)
qed
qed
qed
qed
qed
lemma post_after_fin:
‹(fin, s) # cs ∈ cpts (estran Γ) ⟹
(fin, s) # cs ∈ assume pre rely ⟹
s ∈ post ⟹
stable post rely ⟹
snd (last ((fin, s) # cs)) ∈ post›
proof-
assume 1: ‹(fin, s) # cs ∈ cpts (estran Γ)›
assume asm: ‹(fin, s) # cs ∈ assume pre rely›
assume ‹s ∈ post›
assume stable: ‹stable post rely›
obtain cpt where cpt: ‹cpt = (fin, s) # cs› by simp
with asm have ‹cpt ∈ assume pre rely› by simp
have all_etran: ‹∀i. Suc i < length cpt ⟶ cpt!i ─e→ cpt!Suc i›
apply(rule allI)
apply(case_tac i; simp)
using cpt all_fin_after_fin[OF 1] by simp+
from asm have all_rely: ‹∀i. Suc i < length cpt ⟶ (snd (cpt!i), snd (cpt!Suc i))∈rely›
apply (auto simp add: assume_def)
using all_etran by (simp add: cpt)
from cpt have fst_hd_cpt: ‹fst (hd cpt) = fin› by simp
have aux: ‹∀i. i < length cpt ⟶ snd (cpt!i) ∈ post›
apply(rule allI)
apply(induct_tac i)
using cpt apply simp apply (rule ‹s∈post›)
apply clarify
proof-
fix n
assume h: ‹n < length cpt ⟶ snd (cpt ! n) ∈ post›
assume lt: ‹Suc n < length cpt›
with h have ‹snd (cpt!n) ∈ post› by fastforce
moreover have ‹(snd (cpt!n), snd(cpt!Suc n))∈rely› using all_rely lt by simp
ultimately show ‹snd (cpt!Suc n) ∈ post› using stable stable_def by fast
qed
then have ‹snd (last cpt) ∈ post›
apply(subst last_conv_nth)
using cpt apply simp
using aux[THEN spec[where x=‹length cpt-1›]] cpt by force
then show ?thesis using cpt by simp
qed
lemma unlift_seq_assume:
‹map (lift_seq_esconf Q) ((P, s) # cs) ∈ assume pre rely ⟹ (P,s)#cs ∈ assume pre rely›
apply(auto simp add: assume_def lift_seq_esconf_def case_prod_unfold)
apply(erule_tac x=i in allE)
apply auto
apply (metis (no_types, lifting) Suc_diff_1 Suc_lessD fst_conv linorder_neqE_nat nth_Cons' nth_map zero_order(3))
by (metis (no_types, lifting) Suc_diff_1 Suc_lessD linorder_neqE_nat nth_Cons' nth_map snd_conv zero_order(3))
lemma lift_seq_commit_aux:
‹((P NEXT Q, S), fst c NEXT Q, snd c) ∈ estran Γ ⟹ ((P, S), c) ∈ estran Γ›
apply(simp add: estran_def, erule exE)
apply(erule estran_p.cases, auto)
using surjective_pairing apply metis
using seq_neq2 by fast
lemma nth_length_last:
‹((P, s) # cs @ cs') ! length cs = last ((P, s) # cs)›
by (induct cs) auto
lemma while_sound_aux1:
‹(Q,t)#cs' ∈ commit (estran Γ) {fin} guar post ⟹
(P,s)#cs ∈ commit (estran Γ) {f} guar p ⟹
(last ((P,s)#cs), (Q,t)) ∈ estran Γ ⟹
snd (last ((P,s)#cs)) = t ⟹
∀s. (s,s)∈guar ⟹
(P,s) # cs @ (Q,t) # cs' ∈ commit (estran Γ) {fin} guar post›
proof-
assume commit2: ‹(Q,t)#cs' ∈ commit (estran Γ) {fin} guar post›
assume commit1: ‹(P,s)#cs ∈ commit (estran Γ) {f} guar p›
assume tran: ‹(last ((P,s)#cs), (Q,t)) ∈ estran Γ›
assume last_state1: ‹snd (last ((P,s)#cs)) = t›
assume guar_refl: ‹∀s. (s,s)∈guar›
show ‹(P,s) # cs @ (Q,t) # cs' ∈ commit (estran Γ) {fin} guar post›
apply(auto simp add: commit_def)
apply(case_tac ‹i<length cs›)
apply simp
using commit1 apply(simp add: commit_def)
apply clarify
apply(erule_tac x=i in allE)
apply (smt append_is_Nil_conv butlast.simps(2) butlast_snoc length_Cons less_SucI nth_butlast)
apply(subgoal_tac ‹i = length cs›)
prefer 2
apply linarith
apply(thin_tac ‹i < Suc (length cs)›)
apply(thin_tac ‹¬ i < length cs›)
apply simp
apply(thin_tac ‹i = length cs›)
apply(unfold nth_length_last)
using tran last_state1 guar_refl apply simp using guar_refl apply blast
using commit2 apply(simp add: commit_def)
apply(case_tac ‹i<length cs›)
apply simp
using commit1 apply(simp add: commit_def)
apply clarify
apply(erule_tac x=i in allE)
apply (metis (no_types, lifting) Suc_diff_1 Suc_lessD linorder_neqE_nat nth_Cons' nth_append zero_order(3))
apply(case_tac ‹i = length cs›)
apply simp
apply(unfold nth_length_last)
using tran last_state1 guar_refl apply simp using guar_refl apply blast
apply(subgoal_tac ‹i > length cs›)
prefer 2
apply linarith
apply(thin_tac ‹¬ i < length cs›)
apply(thin_tac ‹i ≠ length cs›)
apply(case_tac i; simp)
apply(rename_tac i')
using commit2 apply(simp add: commit_def)
apply(subgoal_tac ‹∃j. i' = length cs + j›)
prefer 2
using le_Suc_ex apply simp
apply(erule exE)
apply simp
apply clarify
apply(erule_tac x=j in allE)
apply (metis (no_types, hide_lams) add_Suc_right nth_Cons_Suc nth_append_length_plus)
using commit2 apply(simp add: commit_def)
done
qed
lemma while_sound_aux2:
assumes ‹stable post rely›
and ‹s ∈ post›
and ‹∀i. Suc i < length ((P,s)#cs) ⟶ ((P,s)#cs)!i ─e→ ((P,s)#cs)!Suc i›
and ‹∀i. Suc i < length ((P,s)#cs) ⟶ ((P,s)#cs)!i ─e→ ((P,s)#cs)!Suc i ⟶ (snd(((P,s)#cs)!i), snd(((P,s)#cs)!Suc i))∈rely›
shows ‹snd (last ((P,s)#cs)) ∈ post›
using assms(2-4)
proof(induct cs arbitrary:P s)
case Nil
then show ?case by simp
next
case (Cons c cs)
obtain P' s' where c: ‹c=(P',s')› by fastforce
have 1: ‹s'∈post›
proof-
have rely: ‹(s,s')∈rely›
using Cons(3)[THEN spec[where x=0]] Cons(4)[THEN spec[where x=0]] c
by (simp add: assume_def)
show ?thesis using assms(1) ‹s∈post› rely
by (simp add: stable_def)
qed
from Cons(3) c
have 2: ‹∀i. Suc i < length ((P', s') # cs) ⟶ ((P', s') # cs) ! i ─e→ ((P', s') # cs) ! Suc i› by fastforce
from Cons(4) c
have 3: ‹∀i. Suc i < length ((P', s') # cs) ⟶ ((P', s') # cs) ! i ─e→ ((P', s') # cs) ! Suc i ⟶ (snd (((P', s') # cs) ! i), snd (((P',s') # cs) ! Suc i)) ∈ rely› by fastforce
show ?case using Cons(1)[OF 1 2 3] c by fastforce
qed
lemma seq_tran_inv:
assumes ‹((P NEXT Q,S), (P' NEXT Q,T))∈estran Γ›
shows ‹((P,S), (P',T))∈estran Γ›
using assms
apply (simp add: estran_def)
apply(erule exE) apply(rule exI) apply(erule estran_p.cases, auto)
using seq_neq2 by blast
lemma seq_tran_inv_fin:
assumes ‹((P NEXT Q,S), (Q,T))∈estran Γ›
shows ‹((P,S), (fin,T))∈estran Γ›
using assms
apply (simp add: estran_def)
apply(erule exE) apply(rule exI) apply(erule estran_p.cases, auto)
using seq_neq2[symmetric] by blast
lemma lift_seq_commit:
assumes ‹cpt ∈ commit (estran Γ) {fin} guar post›
and ‹cpt≠[]›
shows ‹map (lift_seq_esconf Q) cpt ∈ commit (estran Γ) {fin} guar post›
using assms(1)
apply(simp add: commit_def lift_seq_esconf_def case_prod_unfold)
apply(rule conjI)
apply(rule allI)
apply clarify
apply(erule_tac x=i in allE)
apply(drule seq_tran_inv)
apply force
apply clarify
by (simp add: last_map[OF ‹cpt≠[]›])
lemma while_sound_aux3:
assumes ‹cs ∈ commit (estran Γ) {fin} guar post›
and ‹cs≠[]›
shows ‹map (lift_seq_esconf Q) cs ∈ commit (estran Γ) {fin} guar post'›
using assms
apply(auto simp add: commit_def lift_seq_esconf_def case_prod_unfold)
subgoal for i
proof-
assume a: ‹∀i. Suc i < length cs ⟶ (cs ! i, cs ! Suc i) ∈ estran Γ ⟶ (snd (cs ! i), snd (cs ! Suc i)) ∈ guar›
assume 1: ‹Suc i < length cs›
assume ‹((fst (cs ! i) NEXT Q, snd (cs ! i)), fst (cs ! Suc i) NEXT Q, snd (cs ! Suc i)) ∈ estran Γ›
then have 2: ‹(cs ! i, cs ! Suc i) ∈ estran Γ› using seq_tran_inv surjective_pairing by metis
from a[rule_format, OF 1 2] show ?thesis .
qed
subgoal
proof-
assume 1: ‹fst (last cs) ≠ fin›
assume 2: ‹fst (last (map (λuu. (fst uu NEXT Q, snd uu)) cs)) = fin›
from 1 2 have False
by (metis (no_types, lifting) esys.distinct(5) fst_conv last_map list.simps(8))
then show ?thesis by blast
qed
subgoal for i
proof-
assume a: ‹∀i. Suc i < length cs ⟶ (cs ! i, cs ! Suc i) ∈ estran Γ ⟶ (snd (cs ! i), snd (cs ! Suc i)) ∈ guar›
assume 1: ‹Suc i < length cs›
assume ‹((fst (cs ! i) NEXT Q, snd (cs ! i)), fst (cs ! Suc i) NEXT Q, snd (cs ! Suc i)) ∈ estran Γ›
then have 2: ‹(cs ! i, cs ! Suc i) ∈ estran Γ› using seq_tran_inv surjective_pairing by metis
from a[rule_format, OF 1 2] show ?thesis .
qed
subgoal
proof-
assume ‹fst (last (map (λuu. (fst uu NEXT Q, snd uu)) cs)) = fin›
with ‹cs≠[]› have False by (simp add: last_conv_nth)
then show ?thesis by blast
qed
.
lemma no_fin_in_unfinished:
assumes ‹cpt ∈ cpts (estran Γ)›
and ‹Γ ⊢ last cpt ─es[a]→ c›
shows ‹∀i. i<length cpt ⟶ fst (cpt!i) ≠ fin›
proof(rule allI, rule impI)
fix i
assume ‹i<length cpt›
show ‹fst (cpt!i) ≠ fin›
proof
assume fin: ‹fst (cpt!i) = fin›
let ?cpt = ‹drop i cpt›
have drop_cpt: ‹?cpt ∈ cpts (estran Γ)› using cpts_drop[OF assms(1) ‹i<length cpt›] .
obtain S where ‹cpt!i = (fin,S)› using surjective_pairing fin by metis
have drop_cpt_dest: ‹drop i cpt = (fin,S) # tl (drop i cpt)›
using ‹i<length cpt› ‹cpt!i = (fin,S)›
by (metis cpts_def' drop_cpt hd_Cons_tl hd_drop_conv_nth)
have ‹(fin,S) # tl (drop i cpt) ∈ cpts (estran Γ)› using drop_cpt drop_cpt_dest by argo
from all_fin_after_fin[OF this] have ‹fst (last cpt) = fin›
by (metis (no_types, lifting) ‹cpt ! i = (fin, S)› ‹i < length cpt› drop_cpt_dest fin last_ConsL last_ConsR last_drop last_in_set)
with assms(2) no_estran_from_fin show False
by (metis prod.collapse)
qed
qed
lemma while_sound_aux:
assumes ‹cpt ∈ cpts_es_mod Γ›
and ‹preL = lift_state_set pre›
and ‹relyL = lift_state_pair_set rely›
and ‹guarL = lift_state_pair_set guar›
and ‹postL = lift_state_set post›
and ‹pre ∩ - b ⊆ post›
and ‹∀S0. cpts_from (estran Γ) (P,S0) ∩ assume (lift_state_set (pre∩b)) relyL ⊆ commit (estran Γ) {fin} guarL preL›
and ‹∀s. (s, s) ∈ guar›
and ‹stable pre rely›
and ‹stable post rely›
shows ‹∀S cs. cpt = (EWhile b P, S)#cs ⟶ cpt ∈ assume preL relyL ⟶ cpt ∈ commit (estran Γ) {fin} guarL postL›
using assms
proof(induct)
case (CptsModOne P s x)
then show ?case by (simp add: commit_def)
next
case (CptsModEnv P t y cs s x)
have 1: ‹∀P s t. ((P, s), P, t) ∉ estran Γ› using no_estran_to_self' by blast
have 2: ‹stable preL relyL› using stable_lift[OF ‹stable pre rely›] CptsModEnv(3,4) by simp
show ?case
apply clarify
apply(rule commit_Cons_env)
apply(rule 1)
apply(insert CptsModEnv(2)[OF CptsModEnv(3-11)])
apply clarify
apply(erule allE[where x=‹(t,y)›])
apply(erule allE[where x=cs])
apply(drule assume_tl_comp[OF _ 2])
by blast
next
case (CptsModAnon P s Q t x cs)
then show ?case by simp
next
case (CptsModAnon_fin P s Q t x cs)
then show ?case by simp
next
case (CptsModBasic P e s y x k cs)
then show ?case by simp
next
case (CptsModAtom P e s t x cs)
then show ?case by simp
next
case (CptsModSeq P s x a Q t y R cs)
then show ?case by simp
next
case (CptsModSeq_fin P s x a t y Q cs)
then show ?case by simp
next
case (CptsModChc1 P s x a Q t y cs R)
then show ?case by simp
next
case (CptsModChc2 P s x a Q t y cs R)
then show ?case by simp
next
case (CptsModJoin1 P s x a Q t y R cs)
then show ?case by simp
next
case (CptsModJoin2 P s x a Q t y R cs)
then show ?case by simp
next
case (CptsModJoin_fin t y cs)
then show ?case by simp
next
case (CptsModWhileTMore s b1 P1 x cs a t y cs')
show ?case
proof(rule allI, rule allI, clarify)
assume ‹P1=P› ‹b1=b›
assume a: ‹(EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) ((P, s, x) # cs) @ (EWhile b P, t, y) # cs' ∈ assume preL relyL›
let ?part1 = ‹(EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) ((P, s, x) # cs)›
have part2_assume: ‹(EWhile b P, t, y) # cs' ∈ assume preL relyL›
proof(simp add: assume_def, rule conjI)
let ?c = ‹(P1, s, x) # cs @ [(fin, t, y)]›
have ‹?c ∈ cpts_from (estran Γ) (P1,s,x) ∩ assume (lift_state_set (pre∩b)) relyL›
proof
show ‹(P1, s, x) # cs @ [(fin, t, y)] ∈ cpts_from (estran Γ) (P1, s, x)›
proof(simp)
from CptsModWhileTMore(3) have tran: ‹(last ((P1, s, x) # cs), (fin, t, y)) ∈ estran Γ›
apply(simp only: estran_def) by blast
from cpts_snoc_comp[OF CptsModWhileTMore(2) tran]
show ‹?c ∈ cpts (estran Γ)› by simp
qed
next
from a
show ‹(P1, s, x) # cs @ [(fin, t, y)] ∈ assume (lift_state_set (pre ∩ b)) relyL›
proof(auto simp add: assume_def)
assume ‹(s, x) ∈ preL›
then show ‹(s, x) ∈ lift_state_set (pre ∩ b)›
using ‹preL = lift_state_set pre› ‹s∈b1›
by (simp add: lift_state_set_def ‹b1=b›)
next
fix i
assume a2[rule_format]: ‹∀i<Suc (Suc (length cs + length cs')).
fst (((EWhile b P, s, x) # (P NEXT EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # cs') ! i) =
fst (((P NEXT EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # cs') ! i) ⟶
(snd (((EWhile b P, s, x) # (P NEXT EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # cs') ! i),
snd (((P NEXT EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # cs') ! i)) ∈ relyL›
let ?j = ‹Suc i›
assume i_lt: ‹i < Suc (length cs)›
assume etran: ‹fst (((P1, s, x) # cs @ [(fin, t, y)]) ! i) = fst ((cs @ [(fin, t, y)]) ! i)›
show ‹(snd (((P1, s, x) # cs @ [(fin, t, y)]) ! i), snd ((cs @ [(fin, t, y)]) ! i)) ∈ relyL›
proof(cases ‹i=length cs›)
case True
from CptsModWhileTMore(3) have ctran: ‹(last ((P1, s, x) # cs), (fin, t, y)) ∈ estran Γ›
apply(simp only: estran_def) by blast
have 1: ‹((P1, s, x) # cs @ [(fin, t, y)]) ! i = last ((P1,s,x)#cs)› using True by (simp add: nth_length_last)
have 2: ‹(cs @ [(fin, t, y)]) ! i = (fin, t, y)› using True by (simp add: nth_append)
from ctran_imp_not_etran[OF ctran] etran 1 2 have False by force
then show ?thesis by blast
next
case False
with i_lt have ‹i<length cs› by simp
have
‹fst (map (lift_seq_esconf (EWhile b P)) ((P,s,x)#cs) ! i) =
fst (map (lift_seq_esconf (EWhile b P)) cs ! i)›
proof-
have *: ‹i < length ((P1,s,x)#cs)› using ‹i<length cs› by simp
have **: ‹i < length ((P,s,x)#cs)› using ‹i<length cs› by simp
have ‹(((P1, s, x) # cs) @ [(fin, t, y)]) ! i = ((P1,s,x)#cs) ! i›
using * apply(simp only: nth_append) by simp
then have eq1: ‹((P1, s, x) # cs @ [(fin, t, y)]) ! i = ((P1,s,x)#cs) ! i› by simp
have eq2: ‹(cs @ [(fin, t, y)]) ! i = cs!i›
using ‹i<length cs› by (simp add: nth_append)
show ?thesis
apply(simp only: nth_map[OF **] nth_map[OF ‹i<length cs›])
using etran apply(simp add: eq1 eq2 lift_seq_esconf_def case_prod_unfold)
using ‹P1=P› by simp
qed
then have
‹fst ((map (lift_seq_esconf (EWhile b P)) ((P,s,x)#cs) @ (EWhile b P, t, y) # cs') ! i) =
fst ((map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # cs') ! i)›
by (metis (no_types, lifting) One_nat_def ‹i < length cs› add.commute i_lt length_map list.size(4) nth_append plus_1_eq_Suc)
then have 2:
‹fst (((EWhile b P, s, x) # (P NEXT EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # cs') ! ?j) =
fst (((P NEXT EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # cs') ! ?j)›
by simp
have 1: ‹?j < Suc (Suc (length cs + length cs'))› using ‹i<length cs› by simp
from a2[OF 1 2] have rely:
‹(snd (((EWhile b P, s, x) # (P NEXT EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # cs') ! Suc i),
snd (((P NEXT EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # cs') ! Suc i))
∈ relyL› .
have eq1: ‹snd (((EWhile b P, s, x) # (P NEXT EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # cs') ! Suc i) =
snd (((P1, s, x) # cs @ [(fin, t, y)]) ! i)›
proof-
have **: ‹i < length ((P,s,x)#cs)› using ‹i<length cs› by simp
have ‹snd ((map (lift_seq_esconf (EWhile b P)) ((P,s,x)#cs)) ! i) = snd (((P1, s, x) # cs) ! i)›
apply(subst nth_map[OF **])
by (simp add: lift_seq_esconf_def case_prod_unfold ‹P1=P›)
then have ‹snd ((map (lift_seq_esconf (EWhile b P)) ((P,s,x)#cs) @ ((EWhile b P, t, y) # cs')) ! i) = snd ((((P1, s, x) # cs)@[(fin,t,y)]) ! i)›
apply-
apply(subst nth_append) apply(subst nth_append)
using ‹i<length cs› by simp
then show ?thesis by simp
qed
have eq2: ‹snd (((P NEXT EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # cs') ! Suc i) =
snd ((cs @ [(fin, t, y)]) ! i)›
proof-
have ‹snd ((map (lift_seq_esconf (EWhile b P)) cs) ! i) = snd (cs ! i)›
apply(subst nth_map[OF ‹i<length cs›])
by (simp add: lift_seq_esconf_def case_prod_unfold ‹P1=P›)
then have ‹snd ((map (lift_seq_esconf (EWhile b P)) cs @ ((EWhile b P, t, y) # cs')) ! i) = snd ((cs@[(fin,t,y)]) ! i)›
apply-
apply(subst nth_append) apply(subst nth_append)
using ‹i<length cs› by simp
then show ?thesis by simp
qed
from rely show ?thesis by (simp only: eq1 eq2)
qed
qed
qed
with CptsModWhileTMore(11) ‹P1=P› have ‹?c ∈ commit (estran Γ) {fin} guarL preL› by blast
then show ‹(t,y)∈preL› by (simp add: commit_def)
next
show ‹∀i<length cs'. fst (((EWhile b P, t, y) # cs') ! i) = fst (cs' ! i) ⟶ (snd (((EWhile b P, t, y) # cs') ! i), snd (cs' ! i)) ∈ relyL›
apply(rule allI)
using a apply(auto simp add: assume_def)
apply(erule_tac x=‹Suc(Suc(length cs)) + i› in allE)
subgoal for i
proof-
assume h[rule_format]:
‹Suc (Suc (length cs)) + i < Suc (Suc (length cs + length cs')) ⟶
fst (((EWhile b P, s, x) # (P NEXT EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # cs') ! (Suc (Suc (length cs)) + i)) =
fst (((P NEXT EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # cs') ! (Suc (Suc (length cs)) + i)) ⟶
(snd (((EWhile b P, s, x) # (P NEXT EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # cs') ! (Suc (Suc (length cs)) + i)),
snd (((P NEXT EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # cs') ! (Suc (Suc (length cs)) + i))) ∈ relyL›
assume i_lt: ‹i < length cs'›
assume etran: ‹fst (((EWhile b P, t, y) # cs') ! i) = fst (cs' ! i)›
have eq1:
‹((EWhile b P, s, x) # (P NEXT EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # cs') ! (Suc (Suc (length cs)) + i) =
((EWhile b P, t, y) # cs') ! i›
by (metis (no_types, lifting) Cons_eq_appendI One_nat_def add.commute length_map list.size(4) nth_append_length_plus plus_1_eq_Suc)
have eq2:
‹((P NEXT EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # cs') ! (Suc (Suc (length cs)) + i) =
cs'!i›
by (metis (no_types, lifting) Cons_eq_appendI One_nat_def add.commute add_Suc_shift length_map list.size(4) nth_Cons_Suc nth_append_length_plus plus_1_eq_Suc)
from i_lt have i_lt': ‹Suc (Suc (length cs)) + i < Suc (Suc (length cs + length cs'))› by simp
from etran have etran':
‹fst (((EWhile b P, s, x) # (P NEXT EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # cs') ! (Suc (Suc (length cs)) + i)) =
fst (((P NEXT EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # cs') ! (Suc (Suc (length cs)) + i))›
using eq1 eq2 by simp
from h[OF i_lt' etran'] have
‹(snd (((EWhile b P, s, x) # (P NEXT EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # cs') ! (Suc (Suc (length cs)) + i)),
snd (((P NEXT EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # cs') ! (Suc (Suc (length cs)) + i)))
∈ relyL› .
then show ?thesis
using eq1 eq2 by simp
qed
done
qed
show ‹(EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) ((P, s, x) # cs) @ (EWhile b P, t, y) # cs' ∈ commit (estran Γ) {fin} guarL postL›
proof-
from CptsModWhileTMore(5)[OF CptsModWhileTMore(6-14), rule_format, of ‹(t,y)› cs'] ‹P1=P› ‹b1=b› part2_assume
have part2_commit: ‹(EWhile b P, t, y) # cs' ∈ commit (estran Γ) {fin} guarL postL› by simp
have part1_commit: ‹(EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) ((P, s, x) # cs) ∈ commit (estran Γ) {fin} guarL preL›
proof-
have 1: ‹(P,s,x)#cs ∈ cpts_from (estran Γ) (P,s,x) ∩ assume (lift_state_set (pre ∩ b)) relyL›
proof
show ‹(P, s, x) # cs ∈ cpts_from (estran Γ) (P, s, x)›
proof(simp)
show ‹(P,s,x)#cs ∈ cpts (estran Γ)›
using CptsModWhileTMore(2) ‹P1=P› by simp
qed
next
from assume_tl_env[OF a[simplified]] assume_appendD
have ‹map (lift_seq_esconf (EWhile b P)) ((P, s, x) # cs) ∈ assume preL relyL› by simp
from unlift_seq_assume[OF this] have ‹(P, s, x) # cs ∈ assume preL relyL› .
then show ‹(P, s, x) # cs ∈ assume (lift_state_set (pre ∩ b)) relyL› using ‹s∈b1›
by (auto simp add: assume_def lift_state_set_def ‹preL = lift_state_set pre› ‹b1=b›)
qed
from ‹∀s. (s, s) ∈ guar› ‹guarL = lift_state_pair_set guar› have ‹∀S. (S,S)∈guarL›
using lift_state_pair_set_def by blast
from CptsModWhileTMore(11) 1 have ‹(P, s, x) # cs ∈ commit (estran Γ) {fin} guarL preL› by blast
from lift_seq_commit[OF this]
have 2: ‹map (lift_seq_esconf (EWhile b P)) ((P, s, x) # cs) ∈ commit (estran Γ) {fin} guarL preL› by blast
have ‹P≠fin›
proof
assume ‹P=fin›
with ‹P1=P› CptsModWhileTMore(2) have ‹(fin, s, x) # cs ∈ cpts (estran Γ)› by simp
from all_fin_after_fin[OF this] have ‹fst (last ((fin,s,x)#cs)) = fin› by simp
with CptsModWhileTMore(3) no_estran_from_fin show False
by (metis ‹P = fin› ‹P1 = P› prod.collapse)
qed
show ?thesis
apply simp
apply(rule commit_Cons_comp)
apply(rule 2[simplified])
apply(simp add: estran_def)
apply(rule exI)
apply(rule EWhileT)
using ‹s∈b1› apply(simp add: ‹b1=b›)
apply(rule ‹P≠fin›)
using ‹∀S. (S,S)∈guarL› by blast
qed
have guar: ‹(snd (last ((EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) ((P, s, x) # cs))), snd (EWhile b P, t, y)) ∈ guarL›
proof-
from CptsModWhileTMore(3)
have tran: ‹(last ((P1, s, x) # cs), (fin, t, y)) ∈ estran Γ›
apply(simp only: estran_def) by blast
thm CptsModWhileTMore
have 1: ‹(P,s,x)#cs@[(fin,t,y)] ∈ cpts_from (estran Γ) (P,s,x) ∩ assume (lift_state_set (pre ∩ b)) relyL›
proof
show ‹(P, s, x) # cs @ [(fin, t, y)] ∈ cpts_from (estran Γ) (P, s, x)›
proof(simp)
show ‹(P, s, x) # cs @ [(fin, t, y)] ∈ cpts (estran Γ)›
using CptsModWhileTMore(2) apply(auto simp add: ‹P1=P› cpts_def')
apply(erule_tac x=i in allE)
apply(case_tac ‹i=length cs›; simp)
using tran ‹P1=P› apply(simp add: nth_length_last)
by (metis (no_types, lifting) Cons_eq_appendI One_nat_def add.commute less_antisym list.size(4) nth_append plus_1_eq_Suc)
qed
next
have 1: ‹fst (((P, s, x) # cs @ [(fin, t, y)]) ! length cs) ≠ fst ((cs @ [(fin, t, y)]) ! length cs)›
apply(subst append_Cons[symmetric])
apply(subst nth_append)
apply simp
using no_fin_in_unfinished[OF CptsModWhileTMore(2,3)] ‹P1=P› by simp
from a have ‹map (lift_seq_esconf (EWhile b P)) ((P, s, x) # cs) @ (EWhile b P, t, y) # cs' ∈ assume preL relyL›
using assume_tl_env by fastforce
then have ‹map (lift_seq_esconf (EWhile b P)) ((P, s, x) # cs) ∈ assume preL relyL›
using assume_appendD by fastforce
then have ‹((P, s, x) # cs) ∈ assume preL relyL›
using unlift_seq_assume by fast
then show ‹(P, s, x) # cs @ [(fin, t, y)] ∈ assume (lift_state_set (pre ∩ b)) relyL›
apply(auto simp add: assume_def)
using ‹s∈b1› apply(simp add: lift_state_set_def ‹preL = lift_state_set pre› ‹b1=b›)
apply(case_tac ‹i=length cs›)
using 1 apply blast
apply(erule_tac x=i in allE)
apply(subst append_Cons[symmetric])
apply(subst nth_append) apply(subst nth_append)
apply simp
apply(subst(asm) append_Cons[symmetric])
apply(subst(asm) nth_append) apply(subst(asm) nth_append)
apply simp
done
qed
with CptsModWhileTMore(11) have ‹(P,s,x)#cs@[(fin,t,y)] ∈ commit (estran Γ) {fin} guarL preL› by blast
then show ?thesis
apply(auto simp add: commit_def)
using tran ‹P1=P› apply simp
apply(erule allE[where x=‹length cs›])
using tran by (simp add: nth_append last_map lift_seq_esconf_def case_prod_unfold last_conv_nth)
qed
have ‹((EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) ((P, s, x) # cs)) @ (EWhile b P, t, y) # cs' ∈ commit (estran Γ) {fin} guarL postL›
using commit_append[OF part1_commit guar part2_commit] .
then show ?thesis by simp
qed
qed
next
case (CptsModWhileTOnePartial s b1 P1 x cs)
have guar_refl': ‹∀S. (S,S)∈guarL›
using ‹∀s. (s,s)∈guar› ‹guarL = lift_state_pair_set guar› lift_state_pair_set_def by auto
show ?case
proof(rule allI, rule allI, clarify)
assume ‹P1=P› ‹b1=b›
assume a: ‹(EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) ((P, s, x) # cs) ∈ assume preL relyL›
have 1: ‹map (lift_seq_esconf (EWhile b P)) ((P, s, x) # cs) ∈ commit (estran Γ) {fin} guarL postL›
proof-
have ‹((P, s, x) # cs) ∈ commit (estran Γ) {fin} guarL preL›
proof-
have ‹((P, s, x) # cs) ∈ cpts_from (estran Γ) (P, s, x) ∩ assume (lift_state_set (pre ∩ b)) relyL›
proof
show ‹(P, s, x) # cs ∈ cpts_from (estran Γ) (P, s, x)› using ‹(P1, s, x) # cs ∈ cpts (estran Γ)› ‹P1=P› by simp
next
show ‹(P, s, x) # cs ∈ assume (lift_state_set (pre ∩ b)) relyL›
proof-
from a have ‹map (lift_seq_esconf (EWhile b P)) ((P, s, x) # cs) ∈ assume preL relyL›
by (auto simp add: assume_def)
from unlift_seq_assume[OF this] have ‹((P, s, x) # cs) ∈ assume preL relyL› .
then show ?thesis
proof(auto simp add: assume_def lift_state_set_def ‹preL = lift_state_set pre›)
show ‹s∈b› using ‹s∈b1› ‹b1=b› by simp
qed
qed
qed
with ‹ ∀S0. cpts_from (estran Γ) (P, S0) ∩ assume (lift_state_set (pre ∩ b)) relyL ⊆ commit (estran Γ) {fin} guarL preL›
show ?thesis by blast
qed
then show ?thesis using while_sound_aux3 by blast
qed
show ‹(EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) ((P, s, x) # cs) ∈ commit (estran Γ) {fin} guarL postL›
apply(auto simp add: commit_def)
using guar_refl' apply blast
apply(case_tac i; simp)
using guar_refl' apply blast
using 1 apply(simp add: commit_def)
apply(simp add: last_conv_nth lift_seq_esconf_def case_prod_unfold) .
qed
next
case (CptsModWhileTOneFull s b1 P1 x cs a t y cs')
have guar_refl': ‹∀S. (S,S)∈guarL›
using ‹∀s. (s,s)∈guar› ‹guarL = lift_state_pair_set guar› lift_state_pair_set_def by auto
show ?case
proof(rule allI, rule allI, clarify)
assume ‹P1=P› ‹b1=b›
assume a: ‹(EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) ((P, s, x) # cs) @ map (λ(_, s, x). (EWhile b P, s, x)) ((fin, t, y) # cs') ∈ assume preL relyL›
have 1: ‹map (lift_seq_esconf (EWhile b P)) ((P, s, x) # cs) @ map (λ(_, s, x). (EWhile b P, s, x)) ((fin, t, y) # cs')
∈ commit (estran Γ) {fin} guarL postL›
proof-
have 1: ‹((P, s, x) # cs) @ ((fin, t, y) # cs') ∈ commit (estran Γ) {fin} guarL preL›
proof-
let ?c = ‹((P, s, x) # cs) @ ((fin, t, y) # cs')›
have ‹?c ∈ cpts_from (estran Γ) (P,s,x) ∩ assume (lift_state_set (pre ∩ b)) relyL›
proof
show ‹((P, s, x) # cs) @ (fin, t, y) # cs' ∈ cpts_from (estran Γ) (P, s, x)›
proof(simp)
note part1 = CptsModWhileTOneFull(2)
from CptsModWhileTOneFull(4) cpts_es_mod_equiv
have part2: ‹(fin, t, y) # cs' ∈ cpts (estran Γ)› by blast
from CptsModWhileTOneFull(3)
have tran: ‹(last ((P1, s, x) # cs), (fin, t, y)) ∈ estran Γ›
apply(subst estran_def) by blast
show ‹(P, s, x) # cs @ (fin, t, y) # cs' ∈ cpts (estran Γ)›
using cpts_append_comp[OF part1 part2] tran ‹P1=P› by force
qed
next
from assume_appendD[OF assume_tl_env[OF a[simplified]]]
have ‹map (lift_seq_esconf (EWhile b P)) ((P,s,x)#cs) ∈ assume preL relyL› by simp
from unlift_seq_assume[OF this] have part1: ‹(P, s, x) # cs ∈ assume preL relyL› .
have part2: ‹∀i. Suc i < length ((fin,t,y)#cs') ⟶ (snd (((fin,t,y)#cs')!i), snd (((fin,t,y)#cs')!Suc i)) ∈ relyL›
proof-
from CptsModWhileTOneFull(4) cpts_es_mod_equiv
have part2_cpt: ‹(fin, t, y) # cs' ∈ cpts (estran Γ)› by blast
let ?c2 = ‹map (λ(_, s, x). (EWhile b P, s, x)) ((fin, t, y) # cs')›
from assume_appendD2[OF a[simplified append_Cons[symmetric]]]
have 1: ‹∀i. Suc i < length ?c2 ⟶ (snd (?c2!i), snd (?c2!Suc i))∈relyL›
apply(auto simp add: assume_def case_prod_unfold)
apply(erule_tac x=i in allE)
by (simp add: nth_Cons')
show ?thesis
proof(rule allI, rule impI)
fix i
assume a1: ‹Suc i < length ((fin, t, y) # cs')›
then have ‹i<length cs'› by simp
from 1 have ‹∀i. i < length cs' ⟶
(snd (map (λ(_, s, x). (EWhile b P, s, x)) ((fin, t, y) # cs') ! i), snd (map (λ(_, s, x). (EWhile b P, s, x)) ((fin, t, y) # cs') ! Suc i)) ∈ relyL›
by simp
from this[rule_format, OF ‹i<length cs'›]
show ‹(snd (((fin, t, y) # cs') ! i), snd (((fin, t, y) # cs') ! Suc i)) ∈ relyL›
apply(simp only: nth_map[OF ‹i<length cs'›] nth_map[OF a1[THEN Suc_lessD]] nth_map[OF a1] case_prod_unfold)
by simp
qed
qed
from CptsModWhileTOneFull(3)
have tran: ‹(last ((P1, s, x) # cs), (fin, t, y)) ∈ estran Γ›
apply(subst estran_def) by blast
from assume_append[OF part1] part2 ctran_imp_not_etran[OF tran[simplified ‹P1=P›]]
have ‹((P, s, x) # cs) @ (fin,t,y) # cs' ∈ assume preL relyL› by blast
then show ‹((P, s, x) # cs) @ (fin, t, y) # cs' ∈ assume (lift_state_set (pre ∩ b)) relyL›
using ‹s∈b1› by (simp add: assume_def lift_state_set_def ‹preL = lift_state_set pre› ‹b1=b›)
qed
with CptsModWhileTOneFull(11) show ?thesis by blast
qed
show ?thesis
apply(auto simp add: commit_def)
using 1 apply(simp add: commit_def)
apply clarify
apply(erule_tac x=i in allE)
subgoal for i
proof-
assume a: ‹i < Suc (length cs) ⟶ (((P, s, x) # cs @ [(fin, t, y)]) ! i, (cs @ [(fin, t, y)]) ! i) ∈ estran Γ ⟶ (snd (((P, s, x) # cs @ [(fin, t, y)]) ! i), snd ((cs @ [(fin, t, y)]) ! i)) ∈ guarL›
assume 1: ‹i < Suc (length cs)›
assume a3: ‹(((P NEXT EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) cs @ [(EWhile b P, t, y)]) ! i, (map (lift_seq_esconf (EWhile b P)) cs @ [(EWhile b P, t, y)]) ! i)
∈ estran Γ›
have 2: ‹(((P, s, x) # cs @ [(fin, t, y)]) ! i, (cs @ [(fin, t, y)]) ! i) ∈ estran Γ›
proof-
from a3 have a3': ‹((map (lift_seq_esconf (EWhile b P)) ((P,s,x)#cs) @ [(EWhile b P, t, y)]) ! i, (map (lift_seq_esconf (EWhile b P)) cs @ [(EWhile b P, t, y)]) ! i)
∈ estran Γ› by simp
have eq1:
‹(map (lift_seq_esconf (EWhile b P)) ((P,s,x)#cs) @ [(EWhile b P, t, y)]) ! i =
(map (lift_seq_esconf (EWhile b P)) ((P,s,x)#cs)) ! i›
using 1 by (simp add: nth_append del: list.map)
show ?thesis
proof(cases ‹i=length cs›)
case True
let ?c = ‹((P, s, x) # cs) ! length cs›
from a3' show ?thesis
apply(simp add: eq1 nth_append True del: list.map)
apply(subst append_Cons[symmetric])
apply(simp add: nth_append del: append_Cons)
apply(simp add: lift_seq_esconf_def case_prod_unfold)
apply(simp add: estran_def)
apply(erule exE)
apply(rule exI)
apply(erule estran_p.cases, auto)[]
apply(subst surjective_pairing[of ?c])
by auto
next
case False
with ‹i<Suc (length cs)› have ‹i < length cs› by simp
have eq2:
‹(map (lift_seq_esconf (EWhile b P)) cs @ [(EWhile b P, t, y)]) ! i =
(map (lift_seq_esconf (EWhile b P)) cs) ! i›
using ‹i<length cs› by (simp add: nth_append)
from a3' show ?thesis
using ‹i<length cs› apply(simp add: eq1 eq2 nth_append del: list.map)
apply(subst append_Cons[symmetric])
apply(simp add: nth_append del: append_Cons)
apply(simp add: lift_seq_esconf_def case_prod_unfold)
using seq_tran_inv by fastforce
qed
qed
from a[rule_format, OF 1 2] have
‹(snd (((P, s, x) # cs @ [(fin, t, y)]) ! i), snd ((cs @ [(fin, t, y)]) ! i)) ∈ guarL› .
then have
‹(((s,x) # map snd cs @ [(t,y)])!i, (map snd cs @ [(t,y)])!i) ∈ guarL›
using 1 nth_map[of i ‹(P, s, x) # cs @ [(fin, t, y)]› snd] nth_map[of i ‹cs @ [(fin, t, y)]› snd] by simp
then have
‹(((s,x) # map snd (map (lift_seq_esconf (EWhile b P)) cs) @ [(t,y)])!i, (map snd (map (lift_seq_esconf (EWhile b P)) cs) @ [(t,y)])!i) ∈ guarL›
proof-
assume a: ‹(((s, x) # map snd cs @ [(t, y)]) ! i, (map snd cs @ [(t, y)]) ! i) ∈ guarL›
have aux[rule_format]: ‹∀f. map (snd ∘ (λuu. (f uu, snd uu))) cs = map snd cs› by simp
from a show ?thesis by (simp add: lift_seq_esconf_def case_prod_unfold aux)
qed
then show ?thesis
using 1 nth_map[of i ‹(P NEXT EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) cs @ [(EWhile b P, t, y)]› snd]
nth_map[of i ‹map (lift_seq_esconf (EWhile b P)) cs @ [(EWhile b P, t, y)]› snd]
by simp
qed
using 1 apply(simp add: commit_def)
apply clarify
apply(erule_tac x=i in allE)
subgoal for i
proof-
assume a: ‹i < Suc (length cs + length cs') ⟶ (((P, s, x) # cs @ (fin, t, y) # cs') ! i, (cs @ (fin, t, y) # cs') ! i) ∈ estran Γ ⟶
(snd (((P, s, x) # cs @ (fin, t, y) # cs') ! i), snd ((cs @ (fin, t, y) # cs') ! i)) ∈ guarL›
assume 1: ‹i < Suc (length cs + length cs')›
assume ‹(((P NEXT EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # map (λ(_, y). (EWhile b P, y)) cs') ! i,
(map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # map (λ(_, y). (EWhile b P, y)) cs') ! i)
∈ estran Γ›
then have 2: ‹(((P, s, x) # cs @ (fin, t, y) # cs') ! i, (cs @ (fin, t, y) # cs') ! i) ∈ estran Γ›
apply(cases ‹i < length cs›; simp)
subgoal
proof-
assume a1: ‹i < length cs›
assume a2: ‹(((P NEXT EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # map (λ(_, y). (EWhile b P, y)) cs') ! i,
(map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # map (λ(_, y). (EWhile b P, y)) cs') ! i)
∈ estran Γ›
have aux[rule_format]: ‹∀x xs y ys. i < length xs ⟶ (x#xs@y#ys)!i = (x#xs)!i›
by (metis add_diff_cancel_left' less_SucI less_Suc_eq_0_disj nth_Cons' nth_append plus_1_eq_Suc)
from a1 have a1': ‹i < length (map (lift_seq_esconf (EWhile b P)) cs)› by simp
have a2': ‹(((P NEXT EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) cs)!i, (map (lift_seq_esconf (EWhile b P)) cs)!i) ∈ estran Γ›
proof-
have 1: ‹((P NEXT EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # map (λ(_, y). (EWhile b P, y)) cs') ! i =
((P NEXT EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) cs) ! i› using aux[OF a1'] .
have 2: ‹(map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # map (λ(_, y). (EWhile b P, y)) cs') ! i =
map (lift_seq_esconf (EWhile b P)) cs ! i› using a1' by (simp add: nth_append)
from a2 show ?thesis by (simp add: 1 2)
qed
thm seq_tran_inv
have ‹(((P, s, x) # cs) ! i, cs ! i) ∈ estran Γ›
proof-
from a2' have a2'': ‹((map (lift_seq_esconf (EWhile b P)) ((P,s,x)#cs)) ! i, map (lift_seq_esconf (EWhile b P)) cs ! i) ∈ estran Γ› by simp
obtain P1 S1 where 1: ‹map (lift_seq_esconf (EWhile b P)) ((P,s,x)#cs) ! i = (P1 NEXT EWhile b P, S1)›
proof-
assume a: ‹⋀P1 S1. map (lift_seq_esconf (EWhile b P)) ((P, s, x) # cs) ! i = (P1 NEXT EWhile b P, S1) ⟹ thesis›
have a1': ‹i < length ((P,s,x)#cs)› using a1 by auto
show thesis apply(rule a) apply(subst nth_map[OF a1']) by (simp add: lift_seq_esconf_def case_prod_unfold)
qed
obtain P2 S2 where 2: ‹map (lift_seq_esconf (EWhile b P)) cs ! i = (P2 NEXT EWhile b P, S2)›
proof-
assume a: ‹⋀P2 S2. map (lift_seq_esconf (EWhile b P)) cs ! i = (P2 NEXT EWhile b P, S2) ⟹ thesis›
show thesis apply(rule a) apply(subst nth_map[OF a1]) by (simp add: lift_seq_esconf_def case_prod_unfold)
qed
have tran: ‹((P1,S1),(P2,S2)) ∈ estran Γ› using seq_tran_inv a2'' 1 2 by metis
have aux[rule_format]: ‹∀Q P S cs i. map (lift_seq_esconf Q) cs ! i = (P NEXT Q,S) ⟶ i < length cs ⟶ cs!i = (P,S)›
apply(rule allI)+ apply clarify apply(simp add: lift_seq_esconf_def case_prod_unfold nth_map[OF a1])
using surjective_pairing by metis
have 3: ‹((P, s, x) # cs) ! i = (P1,S1)› using aux[OF 1] a1 by auto
have 4: ‹cs!i = (P2,S2)› using aux[OF 2 a1] .
show ?thesis using tran 3 4 by argo
qed
moreover have ‹((P, s, x) # cs) ! i = (((P, s, x) # cs) @ (fin, t, y) # cs') ! i› using a1 by (simp add: aux)
moreover have ‹(cs @ (fin, t, y) # cs') ! i = cs!i› using a1 by (simp add: nth_append)
ultimately show ?thesis by simp
qed
apply(cases ‹i = length cs›; simp)
subgoal
proof-
assume a: ‹(((P NEXT EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # map (λ(_, y). (EWhile b P, y)) cs') ! length cs,
(map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # map (λ(_, y). (EWhile b P, y)) cs') ! length cs)
∈ estran Γ›
have 1: ‹((P NEXT EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # map (λ(_, y). (EWhile b P, y)) cs') ! length cs =
((P NEXT EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) cs) ! length cs›
by (metis append_Nil2 length_map nth_length_last)
have 2: ‹(map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # map (λ(_, y). (EWhile b P, y)) cs') ! length cs =
(EWhile b P, t, y)›
by (metis (no_types, lifting) map_eq_imp_length_eq map_ident nth_append_length)
from a have a': ‹(((P NEXT EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) cs) ! length cs, (EWhile b P, t, y)) ∈ estran Γ›
by (simp add: 1 2)
obtain P1 S1 where 3: ‹(map (lift_seq_esconf (EWhile b P)) ((P,s,x)#cs)) ! length cs = (P1 NEXT EWhile b P,S1)›
proof-
assume a: ‹⋀P1 S1. (map (lift_seq_esconf (EWhile b P)) ((P,s,x)#cs)) ! length cs = (P1 NEXT EWhile b P, S1) ⟹ thesis›
have 1: ‹length cs < length ((P,s,x)#cs)› by simp
show thesis apply(rule a) apply(subst nth_map[OF 1]) by (simp add: lift_seq_esconf_def case_prod_unfold)
qed
from a' seq_tran_inv_fin 3 have ‹((P1 NEXT EWhile b P,S1),(EWhile b P,t,y))∈estran Γ› by auto
moreover have ‹((P,s,x)#cs) ! length cs = (P1,S1)›
proof-
have *: ‹length cs < length ((P,s,x)#cs)› by simp
show ?thesis using 3
apply(simp only: lift_seq_esconf_def case_prod_unfold)
apply(subst (asm) nth_map[OF *])
by auto
qed
moreover have ‹((P, s, x) # cs @ (fin, t, y) # cs') ! length cs = ((P, s, x) # cs) ! length cs›
by (metis append_Nil2 nth_length_last)
ultimately show ?thesis using seq_tran_inv_fin by metis
qed
subgoal
proof-
assume a1: ‹¬ i < length cs›
assume a2: ‹((map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # map (λ(_, y). (EWhile b P, y)) cs') ! (i - Suc 0),
(map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # map (λ(_, y). (EWhile b P, y)) cs') ! i)
∈ estran Γ›
assume a3: ‹i ≠ length cs›
from a1 a3 have ‹i>length cs› by simp
have 1: ‹((map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # map (λ(_, y). (EWhile b P, y)) cs') ! (i - Suc 0)) =
((EWhile b P, t, y) # map (λ(_, y). (EWhile b P, y)) cs') ! (i - Suc 0 - length cs)›
by (metis (no_types, lifting) Suc_pred ‹length cs < i› a1 length_map less_Suc_eq_0_disj less_antisym nth_append)
have 2: ‹((map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # map (λ(_, y). (EWhile b P, y)) cs') ! i) =
((EWhile b P, t, y) # map (λ(_, y). (EWhile b P, y)) cs') ! (i - length cs)›
by (simp add: a1 nth_append)
from a2 have a2': ‹((((EWhile b P, t, y) # map (λ(_, y). (EWhile b P, y)) cs') ! (i - Suc 0 - length cs)), (((EWhile b P, t, y) # map (λ(_, y). (EWhile b P, y)) cs') ! (i - length cs))) ∈ estran Γ›
by (simp add: 1 2)
note i_lt = ‹i < Suc (length cs + length cs')›
obtain S1 where 3: ‹((map (λ(_, y). (EWhile b P, y)) ((fin,t,y)#cs')) ! (i - Suc 0 - length cs)) = (EWhile b P, S1)›
proof-
assume a: ‹⋀S1. map (λ(_, y). (EWhile b P, y)) ((fin, t, y) # cs') ! (i - Suc 0 - length cs) = (EWhile b P, S1) ⟹ thesis›
have *: ‹i - Suc 0 - length cs < length ((fin,t,y)#cs')› using i_lt by simp
show thesis apply(rule a) apply(subst nth_map[OF *]) by (simp add: case_prod_unfold)
qed
obtain S2 where 4: ‹(map (λ(_, y). (EWhile b P, y)) ((fin,t,y)#cs')) ! (i - length cs) = (EWhile b P, S2)›
proof-
assume a: ‹⋀S2. (map (λ(_, y). (EWhile b P, y)) ((fin, t, y) # cs')) ! (i - length cs) = (EWhile b P, S2) ⟹ thesis›
have *: ‹i - length cs < length ((fin,t,y)#cs')› using i_lt by simp
show thesis apply(rule a) apply(subst nth_map[OF *]) by (simp add: case_prod_unfold)
qed
from no_estran_to_self' a2' 3 4 have False by fastforce
then show ?thesis by (rule FalseE)
qed
done
from a[rule_format, OF 1 2] have ‹(snd (((P, s, x) # cs @ (fin, t, y) # cs') ! i), snd ((cs @ (fin, t, y) # cs') ! i)) ∈ guarL› .
then have
‹(((s,x) # map snd cs @ (t,y) # map snd cs')!i, (map snd cs @ (t,y) # map snd cs')!i) ∈ guarL›
using 1 nth_map[of i ‹(P, s, x) # cs @ (fin, t, y) # cs'› snd] nth_map[of i ‹cs @ (fin, t, y) # cs'› snd] by simp
then have
‹(((s,x) # map snd (map (lift_seq_esconf (EWhile b P)) cs) @ (t,y) # map snd (map (λ(_,S). (EWhile b P, S)) cs'))!i, (map snd (map (lift_seq_esconf (EWhile b P)) cs) @ (t,y) # map snd (map (λ(_,S). (EWhile b P, S)) cs'))!i) ∈ guarL›
proof-
assume ‹(((s,x) # map snd cs @ (t,y) # map snd cs')!i, (map snd cs @ (t,y) # map snd cs')!i) ∈ guarL›
moreover have ‹map snd (map (lift_seq_esconf (EWhile b P)) cs) = map snd cs› by auto
moreover have ‹map snd (map (λ(_, S). (EWhile b P, S)) cs') = map snd cs'› by auto
ultimately show ?thesis by metis
qed
then show ?thesis
using 1 nth_map[of i ‹(P NEXT EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # map (λ(_,S). (EWhile b P, S)) cs'› snd]
nth_map[of i ‹map (lift_seq_esconf (EWhile b P)) cs @ (EWhile b P, t, y) # map (λ(_,S). (EWhile b P, S)) cs'› snd]
by simp
qed
apply(rule FalseE) by (simp add: last_conv_nth case_prod_unfold)
qed
show ‹(EWhile b P, s, x) # map (lift_seq_esconf (EWhile b P)) ((P, s, x) # cs) @ map (λ(_, s, x). (EWhile b P, s, x)) ((fin, t, y) # cs')
∈ commit (estran Γ) {fin} guarL postL›
apply(auto simp add: commit_def)
apply(case_tac i; simp)
using guar_refl' apply blast
using 1 apply(simp add: commit_def)
apply(case_tac i; simp)
using 1 apply(simp add: commit_def)
using guar_refl' apply blast
using 1 apply(simp add: commit_def)
subgoal
proof-
assume ‹cs'≠[]› ‹fst (last (map (λ(_, y). (EWhile b P, y)) cs')) = fin›
then have False by (simp add: last_conv_nth case_prod_unfold)
then show ?thesis by blast
qed.
qed
next
case (CptsModWhileF s b1 x cs P1)
have cpt: ‹((fin, s, x) # cs) ∈ cpts (estran Γ)› using ‹((fin, s, x) # cs) ∈ cpts_es_mod Γ› cpts_es_mod_equiv by blast
show ?case
proof(rule allI, rule allI, clarify)
assume ‹P1=P› ‹b1=b›
assume a: ‹(EWhile b P, s, x) # (fin, s, x) # cs ∈ assume preL relyL›
then have ‹s∈pre› by (simp add: assume_def lift_state_set_def ‹preL = lift_state_set pre›)
show ‹(EWhile b P, s, x) # (fin, s, x) # cs ∈ commit (estran Γ) {fin} guarL postL›
proof-
have 1: ‹(fin, s, x) # cs ∈ commit (estran Γ) {fin} guarL postL›
proof-
have 1: ‹(s,x)∈postL›
proof-
have ‹s∈post› using ‹s∈pre› ‹pre∩-b⊆post› ‹s∉b1› ‹b1=b› by blast
then show ?thesis using ‹postL = lift_state_set post› by (simp add: lift_state_set_def)
qed
have guar_refl': ‹∀S. (S,S)∈guarL›
using ‹∀s. (s,s)∈guar› ‹guarL = lift_state_pair_set guar› lift_state_pair_set_def by auto
have all_etran: ‹∀i. Suc i < length ((fin, s, x) # cs) ⟶ ((fin, s, x) # cs) ! i ─e→ ((fin, s, x) # cs) ! Suc i›
using all_etran_from_fin[OF cpt] by blast
show ?thesis
proof(auto simp add: commit_def 1)
fix i
assume ‹i<length cs›
assume a: ‹(((fin, s, x) # cs) ! i, cs ! i) ∈ estran Γ›
have False
proof-
from ctran_or_etran[OF cpt] ‹i<length cs› a all_etran
show False by simp
qed
then show ‹(snd (((fin, s, x) # cs) ! i), snd (cs ! i)) ∈ guarL› by blast
next
assume ‹cs≠[]›
thm while_sound_aux2
show ‹snd (last cs) ∈ postL›
proof-
have 1: ‹stable postL relyL› using ‹stable post rely› ‹postL = lift_state_set post› ‹relyL = lift_state_pair_set rely›
by (simp add: lift_state_set_def lift_state_pair_set_def stable_def)
have 2: ‹∀i. Suc i < length ((fin, s, x) # cs) ⟶
((fin, s, x) # cs) ! i ─e→ ((fin, s, x) # cs) ! Suc i ⟶ (snd (((fin, s, x) # cs) ! i), snd (((fin, s, x) # cs) ! Suc i)) ∈ relyL›
using a
apply(simp add: assume_def)
apply(rule allI)
apply(erule conjE)
apply(erule_tac x=‹Suc i› in allE)
by simp
have ‹snd (last ((fin, s, x) # cs)) ∈ postL› using while_sound_aux2[OF 1 ‹(s,x)∈postL› all_etran 2] .
then show ?thesis using ‹cs≠[]› by simp
qed
qed
qed
have 2: ‹((EWhile b P, s, x), (fin, s, x)) ∈ estran Γ›
apply(simp add: estran_def)
apply(rule exI)
apply(rule EWhileF)
using ‹s∉b1› ‹b1=b› by simp
from ‹∀s. (s, s) ∈ guar› ‹guarL = lift_state_pair_set guar› have 3: ‹∀S. (S,S)∈guarL›
using lift_state_pair_set_def by auto
from commit_Cons_comp[OF 1 2 3[rule_format]] show ?thesis .
qed
qed
qed
theorem While_sound:
‹⟦ stable pre rely; (pre ∩ -b) ⊆ post; stable post rely;
Γ ⊨ P sat⇩e [pre ∩ b, rely, guar, pre]; ∀s. (s,s)∈guar ⟧ ⟹
Γ ⊨ EWhile b P sat⇩e [pre, rely, guar, post]›
apply(unfold es_validity_def validity_def)
proof-
let ?pre = ‹lift_state_set pre›
let ?rely = ‹lift_state_pair_set rely›
let ?guar = ‹lift_state_pair_set guar›
let ?post = ‹lift_state_set post›
assume stable_pre: ‹stable pre rely›
assume pre_post: ‹pre ∩ -b ⊆ post›
assume stable_post: ‹stable post rely›
assume P_valid: ‹∀S0. cpts_from (estran Γ) (P, S0) ∩ assume (lift_state_set (pre ∩ b)) ?rely ⊆ commit (estran Γ) {fin} ?guar ?pre›
assume guar_refl: ‹∀s. (s,s)∈guar›
show ‹∀S0. cpts_from (estran Γ) (EWhile b P, S0) ∩ assume ?pre ?rely ⊆ commit (estran Γ) {fin} ?guar ?post›
proof
fix S0
show ‹cpts_from (estran Γ) (EWhile b P, S0) ∩ assume ?pre ?rely ⊆ commit (estran Γ) {fin} ?guar ?post›
proof
fix cpt
assume cpt_from_assume: ‹cpt ∈ cpts_from (estran Γ) (EWhile b P, S0) ∩ assume ?pre ?rely›
then have cpt:
‹cpt ∈ cpts (estran Γ)› and cpt_assume:
‹cpt ∈ assume ?pre ?rely› by auto
from cpt_from_assume have ‹cpt ∈ cpts_from (estran Γ) (EWhile b P, S0)› by blast
then have ‹hd cpt = (EWhile b P, S0)› by simp
moreover from cpt cpts_nonnil have ‹cpt≠[]› by blast
ultimately obtain cs where 1: ‹cpt = (EWhile b P, S0) # cs› by (metis hd_Cons_tl)
from cpt cpts_es_mod_equiv have cpt_mod:
‹cpt ∈ cpts_es_mod Γ› by blast
obtain preL :: ‹('s × ('a,'b,'s,'prog) ectx) set› where preL: ‹preL = ?pre› by simp
obtain relyL :: ‹('s × ('a,'b,'s,'prog) ectx) tran set› where relyL: ‹relyL = ?rely› by simp
obtain guarL :: ‹('s × ('a,'b,'s,'prog) ectx) tran set› where guarL: ‹guarL = ?guar› by simp
obtain postL :: ‹('s × ('a,'b,'s,'prog) ectx) set› where postL: ‹postL = ?post› by simp
show ‹cpt ∈ commit (estran Γ) {fin} ?guar ?post›
using while_sound_aux[OF cpt_mod preL relyL guarL postL pre_post _ guar_refl stable_pre stable_post, THEN spec[where x=S0], THEN spec[where x=cs], rule_format] P_valid 1 cpt_assume preL relyL guarL postL by blast
qed
qed
qed
lemma lift_seq_assume:
‹cs ≠ [] ⟹ cs ∈ assume pre rely ⟷ lift_seq_cpt P cs ∈ assume pre rely›
by (auto simp add: assume_def lift_seq_esconf_def case_prod_unfold hd_map)
inductive rghoare_es :: "'Env ⇒ [('l,'k,'s,'prog) esys, 's set, ('s × 's) set, ('s × 's) set, 's set] ⇒ bool"
("_ ⊢ _ sat⇩e [_, _, _, _]" [60,60,0,0,0,0] 45)
where
Evt_Anon: "Γ ⊢ P sat⇩p [pre, rely, guar, post] ⟹ Γ ⊢ EAnon P sat⇩e [pre, rely, guar, post]"
| Evt_Basic: "⟦ Γ ⊢ body ev sat⇩p [pre ∩ (guard ev), rely, guar, post];
stable pre rely; ∀s. (s, s)∈guar⟧ ⟹ Γ ⊢ EBasic ev sat⇩e [pre, rely, guar, post]"
| Evt_Atom:
‹⟦ ∀V. Γ ⊢ body ev sat⇩p [pre ∩ guard ev ∩ {V}, Id, UNIV, {s. (V,s)∈guar} ∩ post];
stable pre rely; stable post rely ⟧ ⟹
Γ ⊢ EAtom ev sat⇩e [pre, rely, guar, post]›
| Evt_Seq:
‹⟦ Γ ⊢ es1 sat⇩e [pre, rely, guar, mid]; Γ ⊢ es2 sat⇩e [mid, rely, guar, post] ⟧ ⟹
Γ ⊢ ESeq es1 es2 sat⇩e [pre, rely, guar, post]›
| Evt_conseq: "⟦ pre ⊆ pre'; rely ⊆ rely'; guar' ⊆ guar; post' ⊆ post;
Γ ⊢ ev sat⇩e [pre', rely', guar', post'] ⟧
⟹ Γ ⊢ ev sat⇩e [pre, rely, guar, post]"
| Evt_Choice:
‹Γ ⊢ P sat⇩e [pre, rely, guar, post] ⟹
Γ ⊢ Q sat⇩e [pre, rely, guar, post] ⟹
Γ ⊢ P OR Q sat⇩e [pre, rely, guar, post]›
| Evt_Join:
‹Γ ⊢ P sat⇩e [pre1, rely1, guar1, post1] ⟹
Γ ⊢ Q sat⇩e [pre2, rely2, guar2, post2] ⟹
pre ⊆ pre1 ∩ pre2 ⟹
rely ∪ guar2 ⊆ rely1 ⟹
rely ∪ guar1 ⊆ rely2 ⟹
∀s. (s,s)∈guar ⟹
guar1 ∪ guar2 ⊆ guar ⟹
post1 ∩ post2 ⊆ post ⟹
Γ ⊢ EJoin P Q sat⇩e [pre, rely, guar, post]›
| Evt_While:
‹⟦ stable pre rely; (pre ∩ -b) ⊆ post; stable post rely;
Γ ⊢ P sat⇩e [pre ∩ b, rely, guar, pre]; ∀s. (s,s)∈guar ⟧ ⟹
Γ ⊢ EWhile b P sat⇩e [pre, rely, guar, post]›
theorem rghoare_es_sound:
assumes h: "Γ ⊢ es sat⇩e [pre, rely, guar, post]"
shows "Γ ⊨ es sat⇩e [pre, rely, guar, post]"
using h
proof(induct)
case (Evt_Anon Γ P pre rely guar post)
then show ?case by(rule Anon_sound)
next
case (Evt_Basic Γ ev pre rely guar post)
then show ?case using Basic_sound by blast
next
case (Evt_Atom Γ ev pre guar post rely)
then show ?case using Atom_sound by blast
next
case (Evt_Seq Γ es1 pre rely guar mid es2 post)
then show ?case using Seq_sound by blast
next
case (Evt_conseq pre pre' rely rely' guar' guar post' post Γ ev)
then show ?case using conseq_sound by blast
next
case Evt_Choice
then show ?case using Choice_sound by blast
next
case (Evt_Join Γ P pre1 rely1 guar1 post1 Q pre2 rely2 guar2 post2 pre rely guar post)
then show ?case apply-
apply(rule conseq_sound[of Γ _ ‹pre1∩pre2› rely guar ‹post1∩post2›])
using Join_sound_aux apply blast
by auto
next
case Evt_While
then show ?case using While_sound by blast
qed
inductive rghoare_pes :: "['Env, 'k ⇒ (('l,'k,'s,'prog)esys,'s) rgformula, 's set, ('s × 's) set, ('s × 's) set, 's set] ⇒ bool"
("_ ⊢ _ SAT⇩e [_, _, _, _]" [60,0,0,0,0,0] 45)
where
Par:
"⟦ ∀k. Γ ⊢ Com (prgf k) sat⇩e [Pre (prgf k), Rely (prgf k), Guar (prgf k), Post (prgf k)];
∀k. pre ⊆ Pre (prgf k);
∀k. rely ⊆ Rely (prgf k);
∀k j. j≠k ⟶ Guar (prgf j) ⊆ Rely (prgf k);
∀k. Guar (prgf k) ⊆ guar;
(⋂k. (Post (prgf k))) ⊆ post ⟧ ⟹
Γ ⊢ prgf SAT⇩e [pre, rely, guar, post]"
lemma Par_conseq:
"⟦ pre ⊆ pre'; rely ⊆ rely'; guar' ⊆ guar; post' ⊆ post;
Γ ⊢ prgf SAT⇩e [pre', rely', guar', post'] ⟧ ⟹
Γ ⊢ prgf SAT⇩e [pre, rely, guar, post]"
apply(erule rghoare_pes.cases, auto)
apply(rule Par)
apply auto
by blast+
lemma par_sound_aux2:
assumes pc: ‹pc ∈ cpts_from (pestran Γ) ((λk. Com (prgf k)), S0) ∩ assume pre rely›
and valid: ‹∀k S0. cpts_from (estran Γ) (Com (prgf k), S0) ∩ assume pre (Rely (prgf k)) ⊆ commit (estran Γ) {fin} (Guar (prgf k)) (Post (prgf k))›
and rely1: ‹∀k. rely ⊆ Rely (prgf k)›
and rely2: ‹∀k k'. k' ≠ k ⟶ Guar (prgf k') ⊆ Rely (prgf k)›
and guar: ‹∀k. Guar (prgf k) ⊆ guar›
and conjoin: ‹pc ∝ cs›
shows
‹∀i k. Suc i < length pc ⟶ (cs k ! i, cs k ! Suc i) ∈ estran Γ ⟶ (snd (cs k ! i), snd (cs k ! Suc i)) ∈ Guar (prgf k)›
proof(rule ccontr, simp, erule exE)
from pc have pc_cpts_from: ‹pc ∈ cpts_from (pestran Γ) ((λk. Com (prgf k)), S0)› by blast
then have pc_cpt: ‹pc ∈ cpts (pestran Γ)› by simp
from pc have pc_assume: ‹pc ∈ assume pre rely› by blast
fix l
assume ‹Suc l < length pc ∧ (∃k. (cs k ! l, cs k ! Suc l) ∈ estran Γ ∧ (snd (cs k ! l), snd (cs k ! Suc l)) ∉ Guar (prgf k))›
(is ‹?P l›)
from exists_least[of ?P, OF this] obtain m where contra:
‹(Suc m < length pc ∧ (∃k. (cs k ! m, cs k ! Suc m) ∈ estran Γ ∧ (snd (cs k ! m), snd (cs k ! Suc m)) ∉ Guar (prgf k))) ∧
(∀i<m. ¬ (Suc i < length pc ∧ (∃k. (cs k ! i, cs k ! Suc i) ∈ estran Γ ∧ (snd (cs k ! i), snd (cs k ! Suc i)) ∉ Guar (prgf k))))›
by blast
then have Suc_m_lt: ‹Suc m < length pc› by argo
from contra obtain k where ‹(cs k ! m, cs k ! Suc m) ∈ estran Γ ∧ (snd (cs k ! m), snd (cs k ! Suc m)) ∉ Guar (prgf k)›
by blast
then have ctran: ‹(cs k ! m, cs k ! Suc m) ∈ estran Γ› and not_guar: ‹(snd (cs k ! m), snd (cs k ! Suc m)) ∉ Guar (prgf k)›
by auto
from contra have ‹∀i<m. ¬ (Suc i < length pc ∧ (∃k. (cs k ! i, cs k ! Suc i) ∈ estran Γ ∧ (snd (cs k ! i), snd (cs k ! Suc i)) ∉ Guar (prgf k)))›
by argo
then have forall_i_lt_m: ‹∀i<m. Suc i < length pc ⟶ (∀k. (cs k ! i, cs k ! Suc i) ∈ estran Γ ⟶ (snd (cs k ! i), snd (cs k ! Suc i)) ∈ Guar (prgf k))›
by simp
from Suc_m_lt have ‹Suc m < length (cs k)› using conjoin
by (simp add: conjoin_def same_length_def)
let ?c = ‹take (Suc (Suc m)) (cs k)›
have ‹cs k ∈ cpts_from (estran Γ) (Com (prgf k), S0)› using conjoin_cpt'[OF pc_cpts_from conjoin] .
then have c_from: ‹?c ∈ cpts_from (estran Γ) (Com (prgf k), S0)›
by (metis Zero_not_Suc cpts_from_take)
have ‹∀i. Suc i < length ?c ⟶ ?c!i ─e→ ?c!Suc i ⟶ (snd (?c!i), snd (?c!Suc i)) ∈ rely ∪ (⋃j∈{j. j ≠ k}. Guar (prgf j))›
proof(rule allI, rule impI, rule impI)
fix i
assume Suc_i_lt': ‹Suc i < length ?c›
then have ‹i≤m› using Suc_m_lt by simp
then have Suc_i_lt: ‹Suc i < length pc› using Suc_m_lt by simp
assume etran': ‹?c!i ─e→ ?c!Suc i›
then have etran: ‹cs k!i ─e→ cs k!Suc i› using ‹i≤m› by simp
from conjoin_etran_k[OF pc_cpt conjoin Suc_i_lt etran]
have ‹(pc!i ─e→ pc!Suc i) ∨ (∃k'. k'≠k ∧ (cs k'!i, cs k'!Suc i) ∈ estran Γ)› .
then show ‹(snd (?c!i), snd (?c!Suc i)) ∈ rely ∪ (⋃j∈{j. j ≠ k}. Guar (prgf j))›
proof
assume ‹pc!i ─e→ pc!Suc i›
then have ‹(snd (pc!i), snd (pc!Suc i)) ∈ rely› using pc_assume Suc_i_lt
by (simp add: assume_def)
then have ‹(snd (cs k!i), snd (cs k!Suc i)) ∈ rely› using conjoin Suc_i_lt
by (simp add: conjoin_def same_state_def)
then have ‹(snd (?c!i), snd (?c!Suc i)) ∈ rely› using ‹i≤m› by simp
then show ‹(snd (?c!i), snd (?c!Suc i)) ∈ rely ∪ (⋃j∈{j. j ≠ k}. Guar (prgf j))› by blast
next
assume ‹∃k'. k' ≠ k ∧ (cs k' ! i, cs k' ! Suc i) ∈ estran Γ›
then obtain k' where k': ‹k' ≠ k ∧ (cs k' ! i, cs k' ! Suc i) ∈ estran Γ› by blast
then have ctran_k': ‹(cs k' ! i, cs k' ! Suc i) ∈ estran Γ› by argo
have ‹(snd (cs k'!i), snd (cs k'!Suc i)) ∈ Guar (prgf k')›
proof(cases "i=m")
case True
with ctran etran ctran_imp_not_etran show ?thesis by blast
next
case False
with ‹i≤m› have ‹i<m› by linarith
with forall_i_lt_m Suc_i_lt ctran_k' show ?thesis by blast
qed
then have ‹(snd (cs k!i), snd (cs k!Suc i)) ∈ Guar (prgf k')› using conjoin Suc_i_lt
by (simp add: conjoin_def same_state_def)
then have ‹(snd (?c!i), snd (?c!Suc i)) ∈ Guar (prgf k')› using ‹i≤m› by fastforce
then show ‹(snd (?c!i), snd (?c!Suc i)) ∈ rely ∪ (⋃j∈{j. j ≠ k}. Guar (prgf j))›
using k' by blast
qed
qed
moreover have ‹snd (hd ?c) ∈ pre›
proof-
from pc_cpt cpts_nonnil have ‹pc≠[]› by blast
then have "length pc ≠ 0" by simp
then have ‹length (cs k) ≠ 0› using conjoin by (simp add: conjoin_def same_length_def)
then have ‹cs k ≠ []› by simp
have ‹snd (hd pc) ∈ pre› using pc_assume by (simp add: assume_def)
then have ‹snd (pc!0) ∈ pre› by (simp add: hd_conv_nth ‹pc≠[]›)
then have ‹snd (cs k ! 0) ∈ pre› using conjoin
by (simp add: conjoin_def same_state_def ‹pc ≠ []›)
then have ‹snd (hd (cs k)) ∈ pre› by (simp add: hd_conv_nth ‹cs k≠[]›)
then show ‹snd (hd ?c) ∈ pre› by simp
qed
ultimately have ‹?c ∈ assume pre (Rely (prgf k))› using rely1 rely2
apply(auto simp add: assume_def) by blast
with c_from have ‹?c ∈ cpts_from (estran Γ) (Com (prgf k), S0) ∩ assume pre (Rely (prgf k))› by blast
with valid have ‹?c ∈ commit (estran Γ) {fin} (Guar (prgf k)) (Post (prgf k))› by blast
then have ‹(snd (?c!m), snd (?c!Suc m)) ∈ Guar (prgf k)›
apply(simp add: commit_def)
apply clarify
apply(erule allE[where x=m])
using ctran ‹Suc m < length (cs k)› by blast
with not_guar ‹Suc m < length (cs k)› show False by simp
qed
lemma par_sound_aux3:
assumes pc: ‹pc ∈ cpts_from (pestran Γ) ((λk. Com (prgf k)), s0) ∩ assume pre rely›
and valid: ‹∀k s0. cpts_from (estran Γ) (Com (prgf k), s0) ∩ assume pre (Rely (prgf k)) ⊆ commit (estran Γ) {fin} (Guar (prgf k)) (Post (prgf k))›
and rely1: ‹∀k. rely ⊆ Rely (prgf k)›
and rely2: ‹∀k k'. k' ≠ k ⟶ Guar (prgf k') ⊆ Rely (prgf k)›
and guar: ‹∀k. Guar (prgf k) ⊆ guar›
and conjoin: ‹pc ∝ cs›
and Suc_i_lt: ‹Suc i < length pc›
and etran: ‹(cs k ! i ─e→ cs k ! Suc i)›
shows ‹(snd (cs k!i), snd (cs k!Suc i)) ∈ Rely (prgf k)›
proof-
from pc have pc_cpt: ‹pc ∈ cpts (pestran Γ)› by fastforce
from conjoin_etran_k[OF pc_cpt conjoin Suc_i_lt etran]
have ‹pc ! i ─e→ pc ! Suc i ∨ (∃k'. k' ≠ k ∧ (cs k' ! i, cs k' ! Suc i) ∈ estran Γ)› .
then show ?thesis
proof
assume ‹pc ! i ─e→ pc ! Suc i›
moreover from pc have ‹pc ∈ assume pre rely› by blast
ultimately have ‹(snd (pc!i), snd (pc!Suc i)) ∈ rely› using Suc_i_lt
by (simp add: assume_def)
with conjoin_same_state[OF conjoin, rule_format, OF Suc_i_lt[THEN Suc_lessD]] conjoin_same_state[OF conjoin, rule_format, OF Suc_i_lt] rely1
show ‹(snd (cs k ! i), snd (cs k ! Suc i)) ∈ Rely (prgf k)›
by auto
next
assume ‹∃k'. k' ≠ k ∧ (cs k' ! i, cs k' ! Suc i) ∈ estran Γ›
then obtain k'' where k'': ‹k'' ≠ k ∧ (cs k'' ! i, cs k'' ! Suc i) ∈ estran Γ› by blast
then have ‹(cs k'' ! i, cs k'' ! Suc i) ∈ estran Γ› by (rule conjunct2)
from par_sound_aux2[OF pc valid rely1 rely2 guar conjoin, rule_format, OF Suc_i_lt, OF this]
have 1: ‹(snd (cs k'' ! i), snd (cs k'' ! Suc i)) ∈ Guar (prgf k'')› .
show ‹(snd (cs k ! i), snd (cs k ! Suc i)) ∈ Rely (prgf k)›
proof-
from 1 conjoin_same_state[OF conjoin, rule_format, OF Suc_i_lt[THEN Suc_lessD]] conjoin_same_state[OF conjoin, rule_format, OF Suc_i_lt]
have ‹(snd (pc ! i), snd (pc ! Suc i)) ∈ Guar (prgf k'')› by simp
with conjoin_same_state[OF conjoin, rule_format, OF Suc_i_lt[THEN Suc_lessD]] conjoin_same_state[OF conjoin, rule_format, OF Suc_i_lt]
have ‹(snd (cs k ! i), snd (cs k ! Suc i)) ∈ Guar (prgf k'')› by simp
moreover from k'' have ‹k''≠k› by (rule conjunct1)
ultimately show ?thesis using rely2[rule_format, OF ‹k''≠k›] by blast
qed
qed
qed
lemma par_sound_aux5:
assumes pc: ‹pc ∈ cpts_from (pestran Γ) ((λk. Com (prgf k)), s0) ∩ assume pre rely›
and valid: ‹∀k s0. cpts_from (estran Γ) (Com (prgf k), s0) ∩ assume pre (Rely (prgf k)) ⊆ commit (estran Γ) {fin} (Guar (prgf k)) (Post (prgf k))›
and rely1: ‹∀k. rely ⊆ Rely (prgf k)›
and rely2: ‹∀k k'. k' ≠ k ⟶ Guar (prgf k') ⊆ Rely (prgf k)›
and guar: ‹∀k. Guar (prgf k) ⊆ guar›
and conjoin: ‹pc ∝ cs›
and fin: ‹fst (last pc) ∈ par_fin›
shows ‹snd (last pc) ∈ (⋂k. Post (prgf k))›
proof-
have ‹∀k. cs k ∈ cpts_from (estran Γ) (Com (prgf k), s0) ∩ assume pre (Rely (prgf k))›
proof
fix k
show ‹cs k ∈ cpts_from (estran Γ) (Com (prgf k), s0) ∩ assume pre (Rely (prgf k))›
proof
from pc have pc': ‹pc ∈ cpts_from (pestran Γ) ((λk. Com (prgf k)), s0)› by blast
show ‹cs k ∈ cpts_from (estran Γ) (Com (prgf k), s0)›
using conjoin_cpt'[OF pc' conjoin] .
next
show ‹cs k ∈ assume pre (Rely (prgf k))›
proof(auto simp add: assume_def)
from pc have pc_cpt: ‹pc ∈ cpts (pestran Γ)› by simp
from pc have pc_assume: ‹pc ∈ assume pre rely› by blast
from pc_cpt cpts_nonnil have ‹pc≠[]› by blast
then have "length pc ≠ 0" by simp
then have ‹length (cs k) ≠ 0› using conjoin by (simp add: conjoin_def same_length_def)
then have ‹cs k ≠ []› by simp
have ‹snd (hd pc) ∈ pre› using pc_assume by (simp add: assume_def)
then have ‹snd (pc!0) ∈ pre› by (simp add: hd_conv_nth ‹pc≠[]›)
then have ‹snd (cs k ! 0) ∈ pre› using conjoin
by (simp add: conjoin_def same_state_def ‹pc ≠ []›)
then show ‹snd (hd (cs k)) ∈ pre› by (simp add: hd_conv_nth ‹cs k≠[]›)
next
fix i
show ‹Suc i < length (cs k) ⟹ fst (cs k ! i) = fst (cs k ! Suc i) ⟹ (snd (cs k ! i), snd (cs k ! Suc i)) ∈ Rely (prgf k)›
proof-
assume ‹Suc i < length (cs k)›
with conjoin_same_length[OF conjoin] have ‹Suc i < length pc› by simp
assume ‹fst (cs k ! i) = fst (cs k ! Suc i)›
then have etran: ‹(cs k ! i) ─e→ (cs k ! Suc i)› by simp
show ‹(snd (cs k ! i), snd (cs k ! Suc i)) ∈ Rely (prgf k)›
using par_sound_aux3[OF pc valid rely1 rely2 guar conjoin ‹Suc i < length pc› etran] .
qed
qed
qed
qed
with valid have commit: ‹∀k. cs k ∈ commit (estran Γ) {fin} (Guar (prgf k)) (Post (prgf k))› by blast
from pc have pc_cpt: ‹pc ∈ cpts (pestran Γ)› by fastforce
with cpts_nonnil have ‹pc≠[]› by blast
have ‹∀k. fst (last (cs k)) = fin›
proof
fix k
from conjoin_cpt[OF pc_cpt conjoin] have ‹cs k ∈ cpts (estran Γ)› .
with cpts_nonnil have ‹cs k ≠ []› by blast
from fin have ‹∀k. fst (last pc) k = fin› by blast
moreover have ‹fst (last pc) k = fst (last (cs k))› using conjoin_same_spec[OF conjoin]
apply(subst last_conv_nth)
apply(rule ‹pc≠[]›)
apply(subst last_conv_nth)
apply(rule ‹cs k≠[]›)
apply(subst conjoin_same_length[OF conjoin, of k])
apply(erule allE[where x=k])
apply(erule allE[where x=‹length (cs k) - 1›])
apply(subst (asm) conjoin_same_length[OF conjoin, of k])
using ‹cs k ≠ []› by force
ultimately show ‹fst (last (cs k)) = fin› using fin conjoin_same_spec[OF conjoin] by simp
qed
then have ‹∀k. snd (last (cs k)) ∈ Post (prgf k)› using commit
by (simp add: commit_def)
moreover have ‹∀k. snd (last (cs k)) = snd (last pc)›
proof
fix k
from conjoin_cpt[OF pc_cpt conjoin] have ‹cs k ∈ cpts (estran Γ)› .
with cpts_nonnil have ‹cs k ≠ []› by blast
show ‹snd (last (cs k)) = snd (last pc)› using conjoin_same_state[OF conjoin]
apply-
apply(subst last_conv_nth)
apply(rule ‹cs k ≠ []›)
apply(subst last_conv_nth)
apply(rule ‹pc ≠ []›)
apply(subst conjoin_same_length[OF conjoin, of k])
apply(erule allE[where x=k])
apply(erule allE[where x=‹length (cs k) - 1›])
apply(subst (asm) conjoin_same_length[OF conjoin, of k])
using ‹cs k ≠ []› by force
qed
ultimately show ?thesis by fastforce
qed
definition ‹split_par pc ≡ λk. map (λ(Ps,s). (Ps k, s)) pc›
lemma split_par_conjoin:
‹pc ∈ cpts (pestran Γ) ⟹ pc ∝ split_par pc›
proof(unfold conjoin_def, auto)
show ‹same_length pc (split_par pc)›
by (simp add: same_length_def split_par_def)
next
show ‹same_state pc (split_par pc)›
by (simp add: same_state_def split_par_def case_prod_unfold)
next
show ‹same_spec pc (split_par pc)›
by (simp add: same_spec_def split_par_def case_prod_unfold)
next
assume ‹pc ∈ cpts (pestran Γ)›
then show ‹compat_tran pc (split_par pc)›
proof(auto simp add: compat_tran_def split_par_def case_prod_unfold)
fix j
assume cpt: ‹pc ∈ cpts (pestran Γ)›
assume Suc_j_lt: ‹Suc j < length pc›
assume not_etran: ‹fst (pc ! j) ≠ fst (pc ! Suc j)›
from ctran_or_etran_par[OF cpt Suc_j_lt] not_etran
have ‹(pc ! j, pc ! Suc j) ∈ pestran Γ› by fastforce
then show ‹∃t k Γ. Γ ⊢ pc ! j ─pes[t♯k]→ pc ! Suc j›
by (auto simp add: pestran_def)
next
fix j k t Γ'
assume ctran: ‹Γ' ⊢ pc ! j ─pes[t♯k]→ pc ! Suc j›
then show ‹Γ' ⊢ (fst (pc ! j) k, snd (pc ! j)) ─es[t♯k]→ (fst (pc ! Suc j) k, snd (pc ! Suc j))›
apply-
by (erule pestran_p.cases, auto)
next
fix j k t Γ' k'
assume ‹Γ' ⊢ pc ! j ─pes[t♯k]→ pc ! Suc j›
moreover assume ‹k' ≠ k›
ultimately show ‹fst (pc ! j) k' = fst (pc ! Suc j) k'›
apply-
by (erule pestran_p.cases, auto)
next
fix j k
assume cpt: ‹pc ∈ cpts (pestran Γ)›
assume Suc_j_lt: ‹Suc j < length pc›
assume ‹fst (pc ! j) k ≠ fst (pc ! Suc j) k›
then have ‹fst (pc!j) ≠ fst (pc!Suc j)› by force
with ctran_or_etran_par[OF cpt Suc_j_lt] have ‹(pc ! j, pc ! Suc j) ∈ pestran Γ› by fastforce
then show ‹∃t k Γ. Γ ⊢ pc ! j ─pes[t♯k]→ pc ! Suc j› by (auto simp add: pestran_def)
next
fix j k ka t Γ'
assume ‹Γ' ⊢ pc ! j ─pes[t♯ka]→ pc ! Suc j›
then show ‹Γ' ⊢ (fst (pc ! j) ka, snd (pc ! j)) ─es[t♯ka]→ (fst (pc ! Suc j) ka, snd (pc ! Suc j))›
apply-
by (erule pestran_p.cases, auto)
next
fix j k ka t Γ' k'
assume ‹Γ' ⊢ pc ! j ─pes[t♯ka]→ pc ! Suc j›
moreover assume ‹k' ≠ ka›
ultimately show ‹fst (pc ! j) k' = fst (pc ! Suc j) k'›
apply-
by (erule pestran_p.cases, auto)
qed
qed
theorem par_sound:
assumes h: ‹∀k. Γ ⊢ Com (prgf k) sat⇩e [Pre (prgf k), Rely (prgf k), Guar (prgf k), Post (prgf k)]›
assumes pre: ‹∀k. pre ⊆ Pre (prgf k)›
assumes rely1: ‹∀k. rely ⊆ Rely (prgf k)›
assumes rely2: ‹∀k j. j ≠ k ⟶ Guar (prgf j) ⊆ Rely (prgf k)›
assumes guar: ‹∀k. Guar (prgf k) ⊆ guar›
assumes post: ‹(⋂k. Post (prgf k)) ⊆ post›
shows
‹Γ ⊨ par_com prgf SAT⇩e [pre, rely, guar, post]›
proof(simp)
let ?pre = ‹lift_state_set pre›
let ?rely = ‹lift_state_pair_set rely›
let ?guar = ‹lift_state_pair_set guar›
let ?post = ‹lift_state_set post›
obtain prgf' :: ‹'a ⇒ (('b, 'a, 's, 'prog) esys, 's × ('a ⇒ ('b × 's set × 'prog) option)) rgformula›
where prgf'_def: ‹prgf' = (λk. ⦇ Com = Com (prgf k), Pre = lift_state_set (Pre (prgf k)), Rely = lift_state_pair_set (Rely (prgf k)),
Guar = lift_state_pair_set (Guar (prgf k)), Post = lift_state_set (Post (prgf k)) ⦈)› by simp
from rely1 have rely1': ‹∀k. lift_state_pair_set rely ⊆ lift_state_pair_set (Rely (prgf k))›
apply(simp add: lift_state_pair_set_def) by blast
from rely2 have rely2': ‹∀k k'. k' ≠ k ⟶ lift_state_pair_set (Guar (prgf k')) ⊆ lift_state_pair_set (Rely (prgf k))›
apply(simp add: lift_state_pair_set_def) by blast
from guar have guar': ‹∀k. lift_state_pair_set (Guar (prgf k)) ⊆ ?guar›
apply(simp add: lift_state_pair_set_def) by blast
from post have post': ‹⋂(lift_state_set ` (Post ` (prgf ` UNIV))) ⊆ ?post›
apply(simp add: lift_state_set_def) by fast
have valid: ‹∀k s0. cpts_from (estran Γ) (Com (prgf k), s0) ∩ assume ?pre (lift_state_pair_set (Rely (prgf k))) ⊆ commit (estran Γ) {fin} (lift_state_pair_set (Guar (prgf k))) (lift_state_set (Post (prgf k)))›
proof
fix k
from rghoare_es_sound[OF h[rule_format, of k]] pre[rule_format, of k]
show ‹∀s0. cpts_from (estran Γ) (Com (prgf k), s0) ∩ assume ?pre (lift_state_pair_set (Rely (prgf k))) ⊆ commit (estran Γ) {fin} (lift_state_pair_set (Guar (prgf k))) (lift_state_set (Post (prgf k)))›
by (auto simp add: assume_def lift_state_set_def lift_state_pair_set_def case_prod_unfold)
qed
show ‹∀s0 x0. {cpt ∈ cpts (pestran Γ). hd cpt = (par_com prgf, s0, x0)} ∩ assume ?pre ?rely ⊆ commit (pestran Γ) par_fin ?guar ?post›
proof(rule allI, rule allI)
fix s0
fix x0
show ‹{cpt ∈ cpts (pestran Γ). hd cpt = (par_com prgf, s0, x0)} ∩ assume ?pre ?rely ⊆ commit (pestran Γ) par_fin ?guar ?post›
proof(auto)
fix pc
assume hd_pc: ‹hd pc = (par_com prgf, s0, x0)›
assume pc_cpt: ‹pc ∈ cpts (pestran Γ)›
assume pc_assume: ‹pc ∈ assume ?pre ?rely›
from hd_pc pc_cpt pc_assume
have pc: ‹pc ∈ cpts_from (pestran Γ) (par_com prgf, s0, x0) ∩ assume ?pre ?rely› by simp
obtain cs where ‹cs = split_par pc› by simp
with split_par_conjoin[OF pc_cpt] have conjoin: ‹pc ∝ cs› by simp
show ‹pc ∈ commit (pestran Γ) par_fin ?guar ?post›
proof(auto simp add: commit_def)
fix i
assume Suc_i_lt: ‹Suc i < length pc›
assume ‹(pc!i, pc!Suc i) ∈ pestran Γ›
then obtain a k where ‹Γ ⊢ pc ! i ─pes[a♯k]→ pc ! Suc i› by (auto simp add: pestran_def)
then show ‹(snd (pc ! i), snd (pc ! Suc i)) ∈ ?guar› apply -
proof(erule pestran_p.cases, auto)
fix pes s x es' t y
assume eq1: ‹pc ! i = (pes, s, x)›
assume eq2: ‹pc ! Suc i = (pes(k := es'), t, y)›
have eq1s: ‹snd (cs k ! i) = (s,x)› using conjoin_same_state[OF conjoin, rule_format, OF Suc_i_lt[THEN Suc_lessD], of k] eq1
by simp
have eq2s: ‹snd (cs k ! Suc i) = (t,y)› using conjoin_same_state[OF conjoin, rule_format, OF Suc_i_lt, of k] eq2
by simp
have eq1p: ‹fst (cs k ! i) = pes k› using conjoin_same_spec[OF conjoin, rule_format, OF Suc_i_lt[THEN Suc_lessD], of k] eq1
by simp
have eq2p: ‹fst (cs k ! Suc i) = es'› using conjoin_same_spec[OF conjoin, rule_format, OF Suc_i_lt, of k] eq2
by simp
assume ‹Γ ⊢ (pes k, s, x) ─es[a♯k]→ (es', t, y)›
with eq1s eq2s eq1p eq2p
have ‹Γ ⊢ (fst (cs k ! i), snd (cs k ! i)) ─es[a♯k]→ (fst (cs k ! Suc i), snd (cs k ! Suc i))› by simp
then have estran: ‹(cs k!i, cs k!Suc i)∈estran Γ› by (auto simp add: estran_def)
from par_sound_aux2[of pc Γ prgf', simplified prgf'_def rgformula.simps, OF pc valid rely1' rely2' guar' conjoin, rule_format, of i k, OF Suc_i_lt estran]
have ‹(snd (cs k ! i), snd (cs k ! Suc i)) ∈ lift_state_pair_set (Guar (prgf k))› .
with eq1s eq2s have ‹((s,x),(t,y)) ∈ lift_state_pair_set (Guar (prgf k))› by simp
with guar' show ‹((s, x), t, y) ∈ lift_state_pair_set guar› by blast
qed
next
assume ‹∀k. fst (last pc) k = fin›
then have fin: ‹fst (last pc) ∈ par_fin› by fast
from par_sound_aux5[of pc Γ prgf', simplified prgf'_def rgformula.simps, OF pc valid rely1' rely2' guar' conjoin fin] post'
show ‹snd (last pc) ∈ lift_state_set post› by blast
qed
qed
qed
qed
theorem rghoare_pes_sound:
assumes h: ‹Γ ⊢ prgf SAT⇩e [pre, rely, guar, post]›
shows ‹Γ ⊨ par_com prgf SAT⇩e [pre, rely, guar, post]›
using h
proof(cases)
case Par
then show ?thesis using par_sound by blast
qed
definition Evt_sat_RG :: "'Env ⇒ (('l, 'k, 's, 'prog) esys, 's) rgformula ⇒ bool" ("_ ⊢ _" [60,60] 61)
where "Γ ⊢ rg ≡ Γ ⊢ Com rg sat⇩e [Pre rg, Rely rg, Guar rg, Post rg]"
end
end