# Theory Example

```section ‹Example›

text ‹We provide an example in order to prove that our locale is non-vacuous.
This example corresponds to the computation and associated snapshot described
in Section 4 of~\<^cite>‹"chandy"›.›

theory Example
imports
Snapshot

begin

datatype PType = P | Q
datatype MType = M | M'
datatype SType = S_Wait | S_Send | T_Wait | T_Send

fun trans :: "PType ⇒ SType ⇒ SType ⇒ bool" where
"trans p s s' = False"

fun send :: "channel_id ⇒ PType ⇒ PType ⇒ SType
⇒ SType ⇒ MType ⇒ bool" where
"send c p q s s' m = ((c = 0 ∧ p = P ∧ q = Q
∧ s = S_Send ∧ s' = S_Wait ∧ m = M)
∨ (c = 1 ∧ p = Q ∧ q = P
∧ s = T_Send ∧ s' = T_Wait ∧ m = M'))"

fun recv :: "channel_id ⇒ PType ⇒ PType ⇒ SType
⇒ SType ⇒ MType ⇒ bool" where
"recv c p q s s' m = ((c = 1 ∧ p = P ∧ q = Q
∧ s = S_Wait ∧ s' = S_Send ∧ m = M')
∨ (c = 0 ∧ p = Q ∧ q = P
∧ s = T_Wait ∧ s' = T_Send ∧ m = M))"

fun chan :: "nat ⇒ (PType * PType) option" where
"chan n = (if n = 0 then Some (P, Q)
else if n = 1 then Some (Q, P)
else None)"

abbreviation init :: "(PType, SType, MType) configuration" where
"init ≡ ⦇
states = (%p. if p = P then S_Send else T_Send),
msgs = (%d. []),
process_snapshot = (%p. None),
channel_snapshot = (%d. ([], NotStarted))
⦈"

abbreviation t0 where "t0 ≡ Snapshot P"

abbreviation s1 :: "(PType, SType, MType) configuration" where
"s1 ≡ ⦇
states = (%p. if p = P then S_Send else T_Send),
msgs = (%d. if d = 0 then [Marker] else []),
process_snapshot = (%p. if p = P then Some S_Send else None),
channel_snapshot = (%d. if d = 1 then ([], Recording) else ([], NotStarted))
⦈"

abbreviation t1 where "t1 ≡ Send 0 P Q S_Send S_Wait M"

abbreviation s2 :: "(PType, SType, MType) configuration" where
"s2 ≡ ⦇
states = (%p. if p = P then S_Wait else T_Send),
msgs = (%d. if d = 0 then [Marker, Msg M] else []),
process_snapshot = (%p. if p = P then Some S_Send else None),
channel_snapshot = (%d. if d = 1 then ([], Recording) else ([], NotStarted))
⦈"

abbreviation t2 where "t2 ≡ Send 1 Q P T_Send T_Wait M'"

abbreviation s3 :: "(PType, SType, MType) configuration" where
"s3 ≡ ⦇
states = (%p. if p = P then S_Wait else T_Wait),
msgs = (%d. if d = 0 then [Marker, Msg M] else if d = 1 then [Msg M'] else []),
process_snapshot = (%p. if p = P then Some S_Send else None),
channel_snapshot = (%d. if d = 1 then ([], Recording) else ([], NotStarted))
⦈"

abbreviation t3 where "t3 ≡ Snapshot Q"

abbreviation s4 :: "(PType, SType, MType) configuration" where
"s4 ≡ ⦇
states = (%p. if p = P then S_Wait else T_Wait),
msgs = (%d. if d = 0 then [Marker, Msg M] else if d = 1 then [Msg M', Marker] else []),
process_snapshot = (%p. if p = P then Some S_Send else Some T_Wait),
channel_snapshot = (%d. if d = 1 then ([], Recording) else if d = 0 then ([], Recording) else ([], NotStarted))
⦈"

abbreviation t4 where "t4 ≡ RecvMarker 0 Q P"

abbreviation s5 :: "(PType, SType, MType) configuration" where
"s5 ≡ ⦇
states = (%p. if p = P then S_Wait else T_Wait),
msgs = (%d. if d = 0 then [Msg M] else if d = 1 then [Msg M', Marker] else []),
process_snapshot = (%p. if p = P then Some S_Send else Some T_Wait),
channel_snapshot = (%d. if d = 0 then ([], Done) else if d = 1 then ([], Recording) else ([], NotStarted))
⦈"

abbreviation t5 where "t5 ≡ Recv 1 P Q S_Wait S_Send M'"

abbreviation s6 :: "(PType, SType, MType) configuration" where
"s6 ≡ ⦇
states = (%p. if p = P then S_Send else T_Wait),
msgs = (%d. if d = 0 then [Msg M] else if d = 1 then [Marker] else []),
process_snapshot = (%p. if p = P then Some S_Send else Some T_Wait),
channel_snapshot = (%d. if d = 0 then ([], Done) else if d = 1 then ([M'], Recording) else ([], NotStarted))
⦈"

abbreviation t6 where "t6 ≡ RecvMarker 1 P Q"

abbreviation s7 :: "(PType, SType, MType) configuration" where
"s7 ≡ ⦇
states = (%p. if p = P then S_Send else T_Wait),
msgs = (%d. if d = 0 then [Msg M] else if d = 1 then [] else []),
process_snapshot = (%p. if p = P then Some S_Send else Some T_Wait),
channel_snapshot = (%d. if d = 0 then ([], Done) else if d = 1 then ([M'], Done) else ([], NotStarted))
⦈"

lemma s7_no_marker:
shows
"∀cid. Marker ∉ set (msgs s7 cid)"
by simp

interpretation computation chan trans send recv init s7
proof
have "distributed_system chan"
proof
show "∀i. ∄p. chan i = Some (p, p)" by simp
qed
show "∀p q. p ≠ q ⟶ (λp q. ∃i. chan i = Some (p, q))⇧+⇧+ p q"
proof ((rule allI)+, rule impI)
fix p q :: PType assume "p ≠ q"
then have "(p = P ∧ q = Q) ∨ (p = Q ∧ q = P)"
using PType.exhaust by auto
then have "∃i. chan i = Some (p, q)" by (elim disjE) auto
then show "(λp q. ∃i. chan i = Some (p, q))⇧+⇧+ p q" by blast
qed
show "finite {i. ∃p q. chan i = Some (p, q)}"
proof -
have "{i. ∃p q. chan i = Some (p, q)} = {0,1}" by auto
then show ?thesis by simp
qed
show "1 < card (UNIV :: PType set)"
proof -
have "(UNIV :: PType set) = {P, Q}"
using PType.exhaust by blast
then have "card (UNIV :: PType set) = 2"
by (metis One_nat_def PType.distinct(1) Suc_1 card.insert card.empty finite.emptyI finite.insertI insert_absorb insert_not_empty singletonD)
then show ?thesis by auto
qed
show "finite (UNIV :: PType set)"
proof -
have "(UNIV :: PType set) = {P, Q}"
using PType.exhaust by blast
then show ?thesis
by (metis finite.emptyI finite.insertI)
qed
show "∀i. ∄p. chan i = Some (p, p)" by simp
show "∀i. (∃p q. chan i = Some (p, q)) ⟶ Marker ∉ set (msgs init i)" by auto
show "∀i. chan i = None ⟶ msgs init i = []" by auto
show "∀p. ¬ ps init p ≠ None" by auto
show "∀i. cs init i = ([], NotStarted)" by auto
show "∃t. distributed_system.trace chan Example.trans send recv init t s7"
proof -
let ?t = "[t0, t1, t2, t3, t4, t5, t6]"
have "distributed_system.next chan trans send recv init t0 s1"
proof -
have "distributed_system.can_occur chan trans send recv t0 init"
using ‹distributed_system chan› distributed_system.can_occur_def by fastforce
then show ?thesis
by (simp add: ‹distributed_system chan› distributed_system.next_snapshot)
qed
moreover have "distributed_system.next chan trans send recv s1 t1 s2"
proof -
have "distributed_system.can_occur chan trans send recv t1 s1"
using ‹distributed_system chan› distributed_system.can_occur_def by fastforce
then show ?thesis
by (simp add: ‹distributed_system chan› distributed_system.next_send)
qed
moreover have "distributed_system.next chan trans send recv s2 t2 s3"
proof -
have "distributed_system.can_occur chan trans send recv t2 s2"
using ‹distributed_system chan› distributed_system.can_occur_def by fastforce
moreover have "∀r. r ≠ P ⟶ r = Q" using PType.exhaust by auto
ultimately show ?thesis by (simp add: ‹distributed_system chan› distributed_system.next_send)
qed
moreover have "distributed_system.next chan trans send recv s3 t3 s4"
proof -
have "distributed_system.can_occur chan trans send recv t3 s3"
using ‹distributed_system chan› distributed_system.can_occur_def by fastforce
moreover have "∀p'. p' ≠ P ⟶ p' = Q" using PType.exhaust by auto
ultimately show ?thesis by (simp add: ‹distributed_system chan› distributed_system.next_snapshot)
qed
moreover have "distributed_system.next chan trans send recv s4 t4 s5"
proof -
have "distributed_system.can_occur chan trans send recv t4 s4"
using ‹distributed_system chan› distributed_system.can_occur_def by fastforce
then show ?thesis
by (simp add: ‹distributed_system chan› distributed_system.next_def)
qed
moreover have "distributed_system.next chan trans send recv s5 t5 s6"
proof -
have "distributed_system.can_occur chan trans send recv t5 s5"
using ‹distributed_system chan› distributed_system.can_occur_def by fastforce
then show ?thesis
by (simp add: ‹distributed_system chan› distributed_system.next_def)
qed
moreover have "distributed_system.next chan trans send recv s6 t6 s7"
proof -
have "distributed_system.can_occur chan trans send recv t6 s6"
using ‹distributed_system chan› distributed_system.can_occur_def by fastforce
then show ?thesis
by (simp add: ‹distributed_system chan› distributed_system.next_def)
qed
ultimately have "distributed_system.trace chan trans send recv init ?t s7"
by (meson ‹distributed_system chan› distributed_system.trace.simps)
then show ?thesis by blast
qed
show "∀t i cid. distributed_system.trace chan Example.trans send recv init t s7 ∧
Marker ∈ set (msgs (distributed_system.s chan Example.trans send recv init t i) cid) ⟶
(∃j≥i. Marker ∉ set (msgs (distributed_system.s chan Example.trans send recv init t j) cid))"
proof ((rule allI)+, (rule impI)+)
fix t i cid
assume asm: "distributed_system.trace chan Example.trans send recv init t s7 ∧
Marker ∈ set (msgs (distributed_system.s chan Example.trans send recv init t i) cid)"
have tr_exists: "distributed_system.trace chan Example.trans send recv init t s7" using asm by blast
have marker_in_channel: "Marker ∈ set (msgs (distributed_system.s chan Example.trans send recv init t i) cid)" using asm by simp
have s7_is_fin: "s7 = (distributed_system.s chan Example.trans send recv init t (length t))"
by (metis (no_types, lifting) ‹distributed_system chan› ‹distributed_system.trace chan Example.trans send recv init t s7› distributed_system.exists_trace_for_any_i distributed_system.trace_and_start_determines_end order_refl take_all)
have "i < length t"
proof (rule ccontr)
assume "~ i < length t"
then have "distributed_system.trace chan Example.trans send recv
(distributed_system.s chan Example.trans send recv init t (length t))
[]
(distributed_system.s chan Example.trans send recv init t i)"
by (metis (no_types, lifting) ‹distributed_system chan› distributed_system.exists_trace_for_any_i distributed_system.trace.simps distributed_system.trace_and_start_determines_end not_less s7_is_fin take_all tr_exists)
then have "Marker ∉ set (msgs (distributed_system.s chan Example.trans send recv init t i) cid)"
proof -
have "distributed_system.s chan Example.trans send recv init t i = s7"
using ‹distributed_system chan› ‹distributed_system.trace chan Example.trans send recv (distributed_system.s chan Example.trans send recv init t (length t)) [] (distributed_system.s chan Example.trans send recv init t i)› distributed_system.trace.simps s7_is_fin by fastforce
then show ?thesis using s7_no_marker by simp
qed
then show False using marker_in_channel by simp
qed
then show "(∃j≥i. Marker ∉ set (msgs (distributed_system.s chan Example.trans send recv init t j) cid))"
proof -
have "distributed_system.trace chan Example.trans send recv
(distributed_system.s chan Example.trans send recv init t i)
(take ((length t) - i) (drop i t))
(distributed_system.s chan Example.trans send recv init t (length t))"
using ‹distributed_system chan› ‹i < length t› distributed_system.exists_trace_for_any_i_j less_imp_le_nat tr_exists by blast
then have "Marker ∉ set (msgs (distributed_system.s chan Example.trans send recv init t (length t)) cid)"
proof -
have "distributed_system.s chan Example.trans send recv init t (length t) = s7"
then show ?thesis using s7_no_marker by simp
qed
then show ?thesis
using ‹i < length t› less_imp_le_nat by blast
qed
qed
show "∀t p. distributed_system.trace chan Example.trans send recv init t s7 ⟶
(∃i. ps (distributed_system.s chan Example.trans send recv init t i) p ≠ None ∧ i ≤ length t)"
proof ((rule allI)+, rule impI)
fix t p
assume "distributed_system.trace chan Example.trans send recv init t s7"
have s7_is_fin: "s7 = (distributed_system.s chan Example.trans send recv init t (length t))"
by (metis (no_types, lifting) ‹distributed_system chan› ‹distributed_system.trace chan Example.trans send recv init t s7› distributed_system.exists_trace_for_any_i distributed_system.trace_and_start_determines_end order_refl take_all)
moreover have "has_snapshotted s7 p" by simp
ultimately show "(∃i. ps (distributed_system.s chan Example.trans send recv init t i) p ≠ None ∧ i ≤ length t)"
by auto
qed
qed

end
```