section ‹Rely-guarantee Validity of PiCore Computations›
theory PiCore_Validity
imports PiCore_Computation Validity
begin
subsection ‹Definitions Correctness Formulas›
record ('p,'s) rgformula =
Com :: 'p
Pre :: "'s set"
Rely :: "('s × 's) set"
Guar :: "('s × 's) set"
Post :: "'s set"
locale event_validity = event_comp ptran fin_com
for ptran :: "'Env ⇒ (('prog × 's) × 'prog × 's) set"
and fin_com :: "'prog"
+
fixes prog_validity :: "'Env ⇒ 'prog ⇒ 's set ⇒ ('s × 's) set ⇒ ('s × 's) set ⇒ 's set ⇒ bool"
("_ ⊨ _ sat⇩p [_, _, _, _]" [60,60,0,0,0,0] 45)
assumes prog_validity_def: "Γ ⊨ P sat⇩p [pre, rely, guar, post] ⟹ validity (ptran Γ) {fin_com} P pre rely guar post"
begin
definition lift_state_set :: ‹'s set ⇒ ('s × 'a) set› where
‹lift_state_set P ≡ {(s,x).s∈P}›
definition lift_state_pair_set :: ‹('s × 's) set ⇒ (('s × 'a) × ('s × 'a))set› where
‹lift_state_pair_set P ≡ {((s,x),(t,y)). (s,t)∈P}›
definition es_validity :: "'Env ⇒ ('l,'k,'s,'prog) esys ⇒ 's set ⇒ ('s × 's) set ⇒ ('s × 's) set ⇒ 's set ⇒ bool"
("_ ⊨ _ sat⇩e [_, _, _, _]" [60,0,0,0,0,0] 45) where
"Γ ⊨ es sat⇩e [pre, rely, guar, post] ≡ validity (estran Γ) {fin} es (lift_state_set pre) (lift_state_pair_set rely) (lift_state_pair_set guar) (lift_state_set post)"
declare es_validity_def[simp]
abbreviation ‹par_fin ≡ {Ps. ∀k. Ps k = fin}›
abbreviation ‹par_com prgf ≡ λk. Com (prgf k)›
definition pes_validity :: ‹'Env ⇒ ('l,'k,'s,'prog) paresys ⇒ 's set ⇒ ('s × 's) set ⇒ ('s × 's) set ⇒ 's set ⇒ bool›
("_ ⊨ _ SAT⇩e [_, _, _, _]" [60,0,0,0,0,0] 45) where
‹Γ ⊨ Ps SAT⇩e [pre, rely, guar, post] ≡ validity (pestran Γ) par_fin Ps (lift_state_set pre) (lift_state_pair_set rely) (lift_state_pair_set guar) (lift_state_set post)›
declare pes_validity_def[simp]
lemma commit_Cons_env_p:
‹(P,t)#cpt ∈ commit (ptran Γ) {fin_com} guar post ⟹ (P,s)#(P,t)#cpt ∈ commit (ptran Γ) {fin_com} guar post›
using commit_Cons_env ptran_neq by metis
lemma commit_Cons_env_es:
‹(P,t)#cpt ∈ commit (estran Γ) {EAnon fin_com} guar post ⟹ (P,s)#(P,t)#cpt ∈ commit (estran Γ) {EAnon fin_com} guar post›
using commit_Cons_env no_estran_to_self' by metis
lemma cpt_from_ptran_star:
assumes h: ‹Γ ⊢ (P, s0) ─c*→ (fin_com, t)›
shows ‹∃cpt. cpt ∈ cpts_from (ptran Γ) (P, s0) ∩ assume {s0} {} ∧ last cpt = (fin_com, t)›
proof-
from h have ‹((P,s0),(fin_com,t)) ∈(ptran Γ)^*› by (simp add: ptrans_def)
then show ?thesis
proof(induct)
case base
show ?case
proof
show ‹[(P,s0)] ∈ cpts_from (ptran Γ) (P, s0) ∩ assume {s0} {} ∧ last [(P,s0)] = (P, s0)›
apply (simp add: assume_def)
apply(rule CptsOne)
done
qed
next
case (step c c')
from step(3) obtain cpt where cpt: ‹cpt ∈ cpts_from (ptran Γ) (P, s0) ∩ assume {s0} {} ∧ last cpt = c› by blast
with step have tran: ‹(last cpt, c') ∈ ptran Γ› by simp
then have prog_neq: ‹fst (last cpt) ≠ fst c'› using ptran_neq
by (metis prod.exhaust_sel)
from cpt have cpt1:‹cpt ∈ cpts (ptran Γ)› by simp
then have cpt_nonnil: ‹cpt ≠ []› using cpts_nonnil by blast
show ?case
proof
show ‹(cpt@[c']) ∈ cpts_from (ptran Γ) (P, s0) ∩ assume {s0} {} ∧ last (cpt@[c']) = c'›
proof
show ‹cpt @ [c'] ∈ cpts_from (ptran Γ) (P, s0) ∩ assume {s0} {}›
proof
from cpt1 tran cpts_snoc_comp have ‹cpt@[c'] ∈ cpts (ptran Γ)› by blast
moreover from cpt have ‹hd (cpt@[c']) = (P, s0)›
using cpt_nonnil by fastforce
ultimately show ‹cpt @ [c'] ∈ cpts_from (ptran Γ) (P, s0)› by fastforce
next
from cpt have "assume": ‹cpt ∈ assume {s0} {}› by blast
then have ‹snd (hd cpt) ∈ {s0}› using assume_def by blast
then have 1: ‹snd (hd (cpt@[c'])) ∈ {s0}› using cpt_nonnil
by (simp add: nth_append)
from "assume" have assume2: ‹∀i. Suc i < length cpt ⟶ (cpt!i ─e→ cpt!(Suc i)) ⟶ (snd (cpt!i), snd (cpt!Suc i)) ∈ {}›
by (simp add: assume_def)
have 2: ‹∀i. Suc i < length (cpt@[c']) ⟶ ((cpt@[c'])!i ─e→ (cpt@[c'])!(Suc i)) ⟶ (snd ((cpt@[c'])!i), snd ((cpt@[c'])!Suc i)) ∈ {}›
proof
fix i
show ‹Suc i < length (cpt @ [c']) ⟶
(cpt @ [c']) ! i ─e→ (cpt @ [c']) ! Suc i ⟶ (snd ((cpt @ [c']) ! i), snd ((cpt @ [c']) ! Suc i)) ∈ {}›
proof
assume Suc_i: ‹Suc i < length (cpt @ [c'])›
show ‹(cpt @ [c']) ! i ─e→ (cpt @ [c']) ! Suc i ⟶ (snd ((cpt @ [c']) ! i), snd ((cpt @ [c']) ! Suc i)) ∈ {}›
proof(cases ‹Suc i < length cpt›)
case True
then show ?thesis using assume2
by (simp add: Suc_lessD nth_append)
next
case False
with Suc_i have ‹Suc i = length cpt› by fastforce
then have i: "i = length cpt - 1" by fastforce
find_theorems last "length ?x - 1"
show ?thesis
proof
have eq1: ‹(cpt @ [c']) ! i = last cpt› using i cpt_nonnil
by (simp add: last_conv_nth nth_append)
have eq2: ‹(cpt @ [c']) ! Suc i = c'› using Suc_i
by (simp add: ‹Suc i = length cpt›)
assume ‹(cpt @ [c']) ! i ─e→ (cpt @ [c']) ! Suc i›
with eq1 eq2 have ‹last cpt ─e→ c'› by simp
with prog_neq have False by simp
then show ‹(snd ((cpt @ [c']) ! i), snd ((cpt @ [c']) ! Suc i)) ∈ {}› by blast
qed
qed
qed
qed
from 1 2 assume_def show ‹cpt @ [c'] ∈ assume {s0} {}› by blast
qed
next
show ‹last (cpt @ [c']) = c'› by simp
qed
qed
qed
qed
end
end