Skip to content

Instantly share code, notes, and snippets.

@suhr
Last active Oct 31, 2021
Embed
What would you like to do?
theory Peterson
imports "Main"
begin
datatype step =
a0 | a1 | a2 | a3a | a3b | cs | a4
record state =
flag :: "nat ⇒ bool"
turn :: nat
pc :: "nat ⇒ step"
record bar =
foo :: "nat => nat"
definition init :: "state ⇒ bool" where
"init s ⟷ (∀i ∈ {0,1}. ¬flag s i)
∧ (turn s = 0)
∧ (∀i ∈ {0,1}. pc s i = a0)"
definition n0 :: "nat ⇒ state ⇒ state ⇒ bool" where
"n0 i s s' ⟷ pc s i = a0
∧ pc s' = (pc s)(i := a1)
∧ turn s' = turn s ∧ flag s' = flag s"
definition n1 :: "nat ⇒ state ⇒ state ⇒ bool" where
"n1 i s s' ⟷ pc s i = a1
∧ pc s' = (pc s)(i := a2)
∧ flag s' = (flag s)(i := True)
∧ turn s' = turn s"
definition n2 :: "nat ⇒ state ⇒ state ⇒ bool" where
"n2 i s s' ⟷ pc s i = a2
∧ pc s' = (pc s)(i := a3a)
∧ turn s' = 1-i
∧ flag s' = flag s"
definition n3a :: "nat ⇒ state ⇒ state ⇒ bool" where
"n3a i s s' ⟷ pc s i = a3a
∧ (if flag s (1-i)
then (pc s') = (pc s)(i := a3b)
else (pc s') = (pc s)(i := cs))
∧ flag s' = flag s ∧ turn s' = turn s"
definition n3b :: "nat ⇒ state ⇒ state ⇒ bool" where
"n3b i s s' ⟷ pc s i = a3b
∧ (if turn s = 1-i
then (pc s') = (pc s)(i := a3a)
else (pc s') = (pc s)(i := cs))
∧ flag s' = flag s ∧ turn s' = turn s"
definition ncs :: "nat ⇒ state ⇒ state ⇒ bool" where
"ncs i s s' ⟷ pc s i = cs
∧ pc s' = (pc s)(i := a4)
∧ flag s' = flag s ∧ turn s' = turn s"
definition n4 :: "nat ⇒ state ⇒ state ⇒ bool" where
"n4 i s s' ⟷ pc s i = a4
∧ pc s' = (pc s)(i := a0)
∧ flag s' = (flag s)(i := False)
∧ turn s' = turn s"
definition nall :: "nat ⇒ state ⇒ state ⇒ bool" where
"nall i s s' ⟷ n0 i s s' ∨ n1 i s s' ∨ n2 i s s'
∨ n3a i s s' ∨ n3b i s s' ∨ ncs i s s' ∨ n4 i s s' "
definition nxt :: "state ⇒ state ⇒ bool" where
"nxt s s' ⟷ (∃i ∈ {0,1}. nall i s s')"
definition spec :: "(nat ⇒ state) ⇒ bool" where
"spec p ⟷ init (p 0) ∧ (∀t. p t = p (Suc t) ∨ nxt (p t) (p (Suc t)))"
lemmas ndefs = nall_def n0_def n1_def n2_def n3a_def n3b_def n4_def ncs_def
lemma ninv:
assumes sp: "spec m"
and base: "∀s. init s ⟶ P s"
and ind: "∀s s'. ∀i ∈ {0,1}. (nall i s s' ⟶ P s ⟶ P s')"
shows "P (m t)"
proof (induction t)
show "P (m 0)" using sp spec_def base by auto
fix t
assume a: "P (m t)"
have "∃i ∈ {0,1}. m t = m (Suc t) ∨ nall i (m t) (m (Suc t))" using sp spec_def nxt_def by auto
thus "P (m (Suc t))" using sp spec_def nxt_def ind a by auto
qed
lemma ninv_next:
assumes sp: "spec m"
and refl: "∀s. P s s"
and ind: "∀s s'. ∀i ∈ {0,1}. (nall i s s' ⟶ P s s')"
shows "P (m t) (m (Suc t))"
using sp refl ind spec_def nxt_def by metis
lemma flag_inv_ind:
assumes dom: "i ∈ {0,1}"
shows "∀s s'. ∀j ∈ {0,1}. nall j s s' ⟶
(pc s i ∈ {a2, a3a, a3b, cs} ⟶ flag s i) ⟶
(pc s' i ∈ {a2, a3a, a3b, cs} ⟶ flag s' i)"
using dom ndefs by simp
lemma flag_inv:
assumes sp: "spec m"
and dom: "i ∈ {0,1}"
shows "pc (m t) i ∈ {a2, a3a, a3b, cs} ⟶ flag (m t) i" (is ?thesis)
proof
let ?P = "λs. pc s i ∈ {a2, a3a, a3b, cs} ⟶ flag s i"
have base: "∀s. init s ⟶ ?P s" using dom init_def by auto
have ind: "∀s s'. ∀i ∈ {0,1}. (nall i s s' ⟶ ?P s ⟶ ?P s')"
using dom flag_inv_ind by simp
show "pc (m t) i ∈ {a2, a3a, a3b, cs} ⟹ flag (m t) i"
using sp base ind ninv[of _ ?P] by blast
qed
theorem mutex: "spec m ⟹ ∀t. ¬(pc (m t) 0 = cs ∧ pc (m t) 1 = cs)"
proof -
show ?thesis sorry
qed
end
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment