Theory a0i_agree
section ‹Injective Agreement›
theory a0i_agree imports a0n_agree
begin
text ‹This refinement adds injectiveness to the agreement property.›
subsection ‹State›
text ‹The state and observations are the same as in the previous model.›
type_synonym
'd a0i_state = "'d a0n_state"
type_synonym
'd a0i_obs = "'d a0n_obs"
subsection ‹Events›
text ‹We just refine the commit event. Everything else remains the same.›
abbreviation
a0i_init :: "'ds a0n_state set"
where
"a0i_init ≡ a0n_init"
abbreviation
a0i_running :: "[agent list, 'ds] ⇒ ('ds a0i_state × 'ds a0i_state) set"
where
"a0i_running ≡ a0n_running"
definition
a0i_commit ::
"[agent list, 'ds] ⇒ ('ds a0i_state × 'ds a0i_state) set"
where
"a0i_commit h d ≡ {(s, s').
(set h ⊆ good ⟶ d ∉ corrupted s ⟶
signals s (Commit h d) < signals s (Running h d)) ∧
s' = s⦇
signals := (signals s)(Commit h d := signals s (Commit h d) + 1)
⦈
}"
abbreviation
a0i_corrupt :: "'ds set ⇒ ('ds a0i_state × 'ds a0i_state) set"
where
"a0i_corrupt ≡ a0n_corrupt"
text ‹Transition system.›
definition
a0i_trans :: "('ds a0i_state × 'ds a0i_state) set" where
"a0i_trans ≡ (⋃ h d ds.
a0i_running h d ∪
a0i_commit h d ∪
a0i_corrupt ds ∪
Id
)"
definition
a0i :: "('ds a0i_state, 'ds a0i_obs) spec" where
"a0i ≡ ⦇
init = a0i_init,
trans = a0i_trans,
obs = id
⦈"
lemmas a0i_defs =
a0n_defs a0i_def a0i_trans_def a0i_commit_def
text ‹Any property is trivially observable.›
lemma a0i_obs [simp]: "obs a0i = id"
by (simp add: a0i_def)
lemma a0i_anyP_observable [iff]: "observable (obs a0i) P"
by (auto)
subsection ‹Invariants›
subsubsection ‹Injective agreement.›
definition
a0i_inv1_iagree :: "'ds a0i_state set"
where
"a0i_inv1_iagree ≡ {s. ∀h d.
set h ⊆ good ⟶ d ∉ corrupted s ⟶
signals s (Commit h d) ≤ signals s (Running h d)
}"
lemmas a0i_inv1_iagreeI =
a0i_inv1_iagree_def [THEN setc_def_to_intro, rule_format]
lemmas a0i_inv1_iagreeE [elim] =
a0i_inv1_iagree_def [THEN setc_def_to_elim, rule_format]
lemmas a0i_inv1_iagreeD =
a0i_inv1_iagree_def [THEN setc_def_to_dest, rule_format, rotated 1]
lemma PO_a0i_inv1_iagree_init [iff]:
"init a0i ⊆ a0i_inv1_iagree"
by (auto simp add: a0i_defs intro!: a0i_inv1_iagreeI)
lemma PO_a0i_inv1_iagree_trans [iff]:
"{a0i_inv1_iagree} trans a0i {> a0i_inv1_iagree}"
apply (auto simp add: PO_hoare_defs a0i_defs intro!: a0i_inv1_iagreeI)
apply (auto dest: a0i_inv1_iagreeD intro: le_SucI)
done
lemma PO_a0i_inv1_iagree [iff]: "reach a0i ⊆ a0i_inv1_iagree"
by (rule inv_rule_basic) (auto)
text ‹As an external invariant.›
lemma PO_a0i_obs_inv1_iagree [iff]: "oreach a0i ⊆ a0i_inv1_iagree"
apply (rule external_from_internal_invariant, fast)
apply (subst a0i_def, auto)
done
subsection ‹Refinement›
definition
med0n0i :: "'d a0i_obs ⇒ 'd a0i_obs"
where
"med0n0i ≡ id"
definition
R0n0i :: "('d a0n_state × 'd a0i_state) set"
where
"R0n0i ≡ Id"
lemma PO_a0i_running_refines_a0n_running:
"{R0n0i}
(a0n_running h d), (a0i_running h d)
{> R0n0i}"
by (unfold R0n0i_def) (rule relhoare_refl)
lemma PO_a0i_commit_refines_a0n_commit:
"{R0n0i}
(a0n_commit h d), (a0i_commit h d)
{> R0n0i}"
by (auto simp add: PO_rhoare_defs R0n0i_def a0i_defs)
lemma PO_a0i_corrupt_refines_a0n_corrupt:
"{R0n0i}
(a0n_corrupt d), (a0i_corrupt d)
{> R0n0i}"
by (unfold R0n0i_def) (rule relhoare_refl)
lemmas PO_a0i_trans_refines_a0n_trans =
PO_a0i_running_refines_a0n_running
PO_a0i_commit_refines_a0n_commit
PO_a0i_corrupt_refines_a0n_corrupt
text ‹All together now...›
lemma PO_m1_refines_init_a0n [iff]:
"init a0i ⊆ R0n0i``(init a0n)"
by (auto simp add: R0n0i_def a0i_defs)
lemma PO_m1_refines_trans_a0n [iff]:
"{R0n0i}
(trans a0n), (trans a0i)
{> R0n0i}"
by (auto simp add: a0n_def a0n_trans_def a0i_def a0i_trans_def
intro!: PO_a0i_trans_refines_a0n_trans)
lemma PO_obs_consistent [iff]:
"obs_consistent R0n0i med0n0i a0n a0i"
by (auto simp add: obs_consistent_def R0n0i_def med0n0i_def a0i_def a0n_def)
lemma PO_a0i_refines_a0n:
"refines R0n0i med0n0i a0n a0i"
by (rule Refinement_basic) (auto)
subsection ‹Derived invariants›
lemma iagree_implies_niagree [iff]: "a0i_inv1_iagree ⊆ a0n_inv1_niagree"
apply (auto intro!: a0n_inv1_niagreeI)
apply (drule_tac d=d in a0i_inv1_iagreeD, auto)
done
text ‹Non-injective agreeement as internal and external invariants.›
lemma PO_a0i_a0n_inv1_niagree [iff]: "reach a0i ⊆ a0n_inv1_niagree"
by (rule subset_trans, rule, rule)
lemma PO_a0i_obs_a0n_inv1_niagree [iff]: "oreach a0i ⊆ a0n_inv1_niagree"
by (rule subset_trans, rule, rule)
end