Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Safety, liveness and refinement of simple TLA+ clock specifications in Isabelle/HOL
theory Clock
imports "HOL-TLA.TLA"
begin
lemma imp_imp_leadsto:
fixes F G :: stpred
fixes S :: temporal
assumes "⊢ F ⟶ G"
shows "⊢ S ⟶ (F ↝ G)"
apply (auto simp add: Valid_def)
using ImplLeadsto_simple assms by blast
lemma imp_leadsto_transitive[trans]:
fixes F G H :: stpred
fixes S :: temporal
assumes "⊢ S ⟶ (F ↝ G)"
assumes "⊢ S ⟶ (G ↝ H)"
shows "⊢ S ⟶ (F ↝ H)"
using assms
apply (auto simp add: Valid_def)
using LatticeTransitivity by fastforce
lemma temp_impI:
assumes "sigma ⊨ P ⟹ sigma ⊨ Q"
shows "sigma ⊨ P ⟶ Q"
using assms by auto
lemma temp_conjI:
assumes "sigma ⊨ P" "sigma ⊨ Q"
shows "sigma ⊨ P ∧ Q"
using assms by auto
lemma temp_conjE:
assumes "sigma ⊨ F ∧ G"
assumes "⟦ sigma ⊨ F; sigma ⊨ G ⟧ ⟹ P"
shows "P"
using assms by auto
lemma temp_imp_conjI:
assumes "⊢ S ⟶ P" "⊢ S ⟶ Q"
shows "⊢ S ⟶ P ∧ Q"
using assms unfolding Valid_def
by auto
lemma temp_box_conjE:
assumes "sigma ⊨ □(F ∧ G)"
assumes "⟦ sigma ⊨ □F; sigma ⊨ □G ⟧ ⟹ P"
shows "P"
using assms STL5 unfolding Valid_def
by (simp add: split_box_conj)
lemma temp_imp_trans [trans]:
assumes "⊢ F ⟶ G"
assumes "⊢ G ⟶ H"
shows "⊢ F ⟶ H"
using assms unfolding Valid_def by auto
lemma imp_leadsto_invariant:
fixes S :: temporal
fixes P I :: stpred
assumes "⊢ S ⟶ □I"
shows "⊢ S ⟶ (P ↝ I)"
proof (intro tempI temp_impI)
fix sigma
assume S: "sigma ⊨ S"
with assms have "sigma ⊨ □I" by auto
thus "sigma ⊨ P ↝ I"
unfolding leadsto_def
by (metis InitDmd STL4E boxInit_stp dmdInit_stp intI temp_impI)
qed
lemma imp_forall_leadsto:
fixes S :: temporal
fixes P :: "'a ⇒ bool"
fixes Q :: "'a ⇒ stpred"
fixes R :: stpred
assumes "⋀x. P x ⟹ ⊢ S ⟶ (Q x ↝ R)"
shows "⊢ S ⟶ (∀ x. (#(P x) ∧ Q x) ↝ R)"
using assms
unfolding Valid_def leadsto_def
apply auto
by (metis (full_types) ImplLeadsto_simple TrueW int_simps(11) int_simps(17) int_simps(19) inteq_reflection leadsto_def tempD)
lemma temp_dmd_box_imp:
assumes "sigma ⊨ ◇□ P"
assumes "⊢ P ⟶ Q"
shows "sigma ⊨ ◇□ Q"
using assms DmdImplE STL4 by blast
lemma temp_box_dmd_imp:
assumes "sigma ⊨ □◇ P"
assumes "⊢ P ⟶ Q"
shows "sigma ⊨ □◇ Q"
using assms DmdImpl STL4E by blast
lemma not_stuck_forever:
fixes Stuck :: stpred
fixes Progress :: action
assumes "⊢ Progress ⟶ $Stuck ⟶ ¬ Stuck$"
shows "⊢ □◇Progress ⟶ ¬ ◇□Stuck"
using assms
by (unfold dmd_def, simp, intro STL4, simp, intro TLA2, auto)
lemma stable_dmd_stuck:
assumes "⊢ S ⟶ stable P"
assumes "⊢ S ⟶ ◇P"
shows "⊢ S ⟶ ◇□P"
using assms DmdStable by (meson temp_imp_conjI temp_imp_trans)
lemma enabled_before_conj[simp]:
"PRED Enabled ($P ∧ Q) = (PRED (P ∧ Enabled Q))"
unfolding enabled_def by (intro ext, auto)
definition next_hour :: "nat ⇒ nat" where "⋀n. next_hour n ≡ if n = 12 then 1 else n+1"
lemma next_hour_induct [case_names base step, consumes 1]:
fixes m :: nat
assumes type: "m ∈ {1..12}"
assumes base: "P 1"
assumes step: "⋀n. 1 ≤ n ⟹ n < 12 ⟹ P n ⟹ P (next_hour n)"
shows "P m"
using type
proof (induct m)
case 0 thus ?case by simp
next
case (Suc m)
from `Suc m ∈ {1..12}` have "m = 0 ∨ (m ∈ {1..12} ∧ 1 ≤ m ∧ m < 12)" by auto
thus ?case
proof (elim disjE conjE)
assume "m = 0" with base show ?case by simp
next
assume "m ∈ {1..12}" with Suc have "P m" "1 ≤ m" "m < 12" by simp_all
hence "P (next_hour m)" by (intro step, auto)
with `m < 12` show ?case by (simp add: next_hour_def)
qed
qed
locale HourClock =
fixes hr :: "nat stfun"
assumes hr_basevar: "basevars hr"
fixes HCini HCnxt HC
defines "HCini ≡ PRED hr ∈ #{1..12}"
defines "HCnxt ≡ ACT hr$ = next_hour<$hr>"
defines "HC ≡ TEMP Init HCini ∧ □[HCnxt]_hr ∧ WF(HCnxt)_hr"
context HourClock
begin
lemma HCnxt_angle[simp]: "ACT <HCnxt>_hr = ACT HCnxt"
unfolding HCnxt_def angle_def next_hour_def by auto
lemma HCnxt_enabled[simp]: "PRED (Enabled HCnxt) = PRED #True"
using basevars [OF hr_basevar] unfolding enabled_def HCnxt_def by auto
lemma HC_safety: "⊢ HC ⟶ □ HCini"
unfolding HC_def HCini_def HCnxt_def next_hour_def by (auto_invariant, auto)
lemma HC_liveness_step:
assumes n: "n ∈ {1..12}"
shows "⊢ HC ⟶ (hr = #n ↝ hr = #(next_hour n))"
proof -
from basevars [OF hr_basevar]
have "⊢ □[HCnxt]_hr ∧ WF(HCnxt)_hr ⟶ (hr = #n ↝ hr = #(next_hour n))"
apply (intro WF1, auto simp add: HCnxt_def square_def next_hour_def angle_def enabled_def, auto)
apply fastforce
by fastforce
thus ?thesis
by (auto simp add: HC_def)
qed
lemma HC_liveness_progress_forwards:
assumes m: "m ∈ {1..12}"
assumes n: "n ∈ {1..12}"
assumes mn: "m ≤ n"
shows "⊢ HC ⟶ (hr = #m ↝ hr = #n)"
using n mn
proof (induct n rule: next_hour_induct)
case base with m show ?case apply auto using LatticeReflexivity by blast
next
case (step n)
hence "m ≤ n ∨ m = next_hour n" by (auto simp add: next_hour_def)
thus ?case
proof (elim disjE)
assume "m = next_hour n" thus ?case apply auto using LatticeReflexivity by blast
next
assume "m ≤ n"
with step have "⊢ HC ⟶ (hr = #m ↝ hr = #n)" by blast
also from step have "⊢ HC ⟶ (hr = #n ↝ hr = #(next_hour n))"
by (intro HC_liveness_step, auto)
finally show ?thesis .
qed
qed
lemma HC_liveness_progress:
assumes m: "m ∈ {1..12}"
assumes n: "n ∈ {1..12}"
shows "⊢ HC ⟶ (hr = #m ↝ hr = #n)"
proof -
from m have "⊢ HC ⟶ (hr = #m ↝ hr = #12)" by (intro HC_liveness_progress_forwards, auto)
also from HC_liveness_step [where n = 12]
have "⊢ HC ⟶ (hr = #12 ↝ hr = #1)" by (simp add: next_hour_def)
also from n have "⊢ HC ⟶ (hr = #1 ↝ hr = #n)" by (intro HC_liveness_progress_forwards, auto)
finally show ?thesis .
qed
lemma HC_liveness:
assumes n: "n ∈ {1..12}"
shows "⊢ HC ⟶ □◇ hr = #n"
proof -
from HC_safety have "⊢ HC ⟶ ((#True :: stpred) ↝ HCini)"
by (intro imp_leadsto_invariant, simp)
also have "⊢ HC ⟶ (HCini ↝ (∃ h0. #(h0 ∈ {1..12}) ∧ hr = #h0))"
by (intro imp_imp_leadsto, auto simp add: HCini_def)
also have "⊢ HC ⟶ ((∃ h0. #(h0 ∈ {1..12}) ∧ hr = #h0) ↝ hr = #n)"
unfolding inteq_reflection [OF leadsto_exists]
proof (intro imp_forall_leadsto)
fix h0
from n show "h0 ∈ {1..12} ⟹ ⊢ HC ⟶ (hr = #h0 ↝ hr = #n)" by (intro HC_liveness_progress)
qed
finally have "⊢ HC ⟶ ((#True :: stpred) ↝ hr = #n)" .
thus ?thesis unfolding leadsto_def by auto
qed
end
locale HourMinuteClock = HourClock +
fixes mn :: "nat stfun"
assumes hr_mn_basevars: "basevars (hr,mn)"
fixes HMCini Mn Hr HMCnxt HMC
defines "HMCini ≡ PRED HCini ∧ mn ∈ #{0..59}"
defines "Mn ≡ ACT mn$ = (if $mn = #59 then #0 else $mn + #1)"
defines "Hr ≡ ACT ($mn = #59 ∧ HCnxt) ∨ ($mn < #59 ∧ unchanged hr)"
defines "HMCnxt ≡ ACT (Mn ∧ Hr)"
defines "HMC ≡ TEMP Init HMCini ∧ □[HMCnxt]_(hr, mn) ∧ WF(HMCnxt)_(hr, mn)"
context HourMinuteClock
begin
lemma HMCnxt_eq:
"HMCnxt = ACT ($mn < #59 ∧ mn$ = $mn + #1 ∧ hr$ = $hr)
∨ ($mn = #59 ∧ mn$ = #0 ∧ $hr = #12 ∧ hr$ = #1)
∨ ($mn = #59 ∧ mn$ = #0 ∧ $hr ≠ #12 ∧ hr$ = $hr + #1)"
by (intro ext, auto simp add: HMCnxt_def Mn_def Hr_def next_hour_def HCnxt_def)
lemma HMCnxt_angle[simp]: "ACT <HMCnxt>_(hr, mn) = ACT HMCnxt"
by (intro ext, auto simp add: angle_def HMCnxt_eq)
lemma HMCnxt_enabled[simp]: "PRED Enabled HMCnxt = PRED mn ≤ #59"
using basevars [OF hr_mn_basevars]
apply (intro ext, auto simp add: enabled_def HMCnxt_eq next_hour_def)
by (meson nat_less_le)
lemma HMC_safety: "⊢ HMC ⟶ □ (hr ∈ #{1..12} ∧ mn ∈ #{0..59})"
unfolding HMC_def HMCini_def HCini_def HMCnxt_eq next_hour_def
by (invariant, auto simp add: square_def Init_def)
definition timeIs :: "nat × nat ⇒ stpred" where "timeIs t ≡ PRED (hr, mn) = #t"
lemma timeIs[simp]: "PRED (timeIs (h,m)) = PRED (hr = #h ∧ mn = #m)"
by (auto simp add: timeIs_def)
lemma HMC_liveness_step:
assumes "m ≤ 59"
shows "⊢ HMC ⟶ (timeIs (h, m) ↝ (timeIs (if m = 59 then (if h = 12 then (1, 0) else (h+1, 0)) else (h, m+1))))"
(is "⊢ HMC ⟶ ?P")
proof -
from assms
have "⊢ □[HMCnxt]_(hr, mn) ∧ WF(HMCnxt)_(hr,mn) ⟶ ?P"
by (intro WF1 actionI temp_impI, auto simp add: square_def, auto simp add: HMCnxt_eq)
thus ?thesis by (auto simp add: HMC_def)
qed
lemma HMC_liveness_step_minute:
assumes "m < 59"
shows "⊢ HMC ⟶ (timeIs (h,m) ↝ timeIs (h, Suc m))"
using HMC_liveness_step [of m h] assms by auto
lemma HMC_liveness_step_hour:
shows "⊢ HMC ⟶ (timeIs (h,59) ↝ timeIs (next_hour h, 0))"
using HMC_liveness_step [of 59 h] unfolding next_hour_def by auto
lemma HMC_liveness_progress_forwards_minute:
assumes m12: "m1 ≤ m2" and m2: "m2 ≤ 59"
shows "⊢ HMC ⟶ (timeIs (h,m1) ↝ timeIs (h,m2))"
using assms
proof (induct m2)
case 0 thus ?case apply auto using LatticeReflexivity by blast
next
case (Suc m)
hence m59: "m ≤ 59" by simp
from Suc have "m1 ≤ m ∨ m1 = Suc m" by auto
thus ?case
proof (elim disjE)
assume "m1 = Suc m" thus ?thesis apply auto using LatticeReflexivity by blast
next
assume "m1 ≤ m"
with Suc.hyps m59
have "⊢ HMC ⟶ (timeIs (h,m1) ↝ timeIs (h,m))" by metis
also from Suc have "⊢ HMC ⟶ (timeIs (h,m) ↝ timeIs (h, Suc m))"
by (intro HMC_liveness_step_minute, auto)
finally show ?thesis .
qed
qed
lemma HMC_liveness_progress_forwards_hour:
assumes h1: "h1 ∈ {1..12}"
assumes h2: "h2 ∈ {1..12}"
assumes h1h2: "h1 ≤ h2"
shows "⊢ HMC ⟶ (timeIs (h1,59) ↝ timeIs (h2,59))"
using h2 h1h2
proof (induct h2 rule: next_hour_induct)
case base with h1 show ?case apply auto using LatticeReflexivity by blast
next
case (step h)
hence "h1 ≤ h ∨ h1 = next_hour h" unfolding next_hour_def by auto
thus ?case
proof (elim disjE)
assume "h1 = next_hour h" thus ?thesis apply auto using LatticeReflexivity by blast
next
assume "h1 ≤ h"
with step have "⊢ HMC ⟶ (timeIs (h1, 59) ↝ timeIs (h, 59))" by metis
also have "⊢ HMC ⟶ (timeIs (h, 59) ↝ timeIs (next_hour h, 0))" by (intro HMC_liveness_step_hour)
also have "⊢ HMC ⟶ (timeIs (next_hour h, 0) ↝ timeIs (next_hour h, 59))"
by (intro HMC_liveness_progress_forwards_minute, simp_all)
finally show ?thesis.
qed
qed
lemma HMC_liveness_progress:
assumes h1: "h1 ∈ {1..12}"
assumes h2: "h2 ∈ {1..12}"
assumes m1: "m1 ≤ 59"
assumes m2: "m2 ≤ 59"
shows "⊢ HMC ⟶ (timeIs (h1,m1) ↝ timeIs (h2,m2))"
proof -
from m1 have "⊢ HMC ⟶ (timeIs (h1,m1) ↝ timeIs (h1,59))"
by (intro HMC_liveness_progress_forwards_minute, simp_all)
also from h1 have "⊢ HMC ⟶ (timeIs (h1,59) ↝ timeIs (12,59))"
by (intro HMC_liveness_progress_forwards_hour, simp_all)
also from HMC_liveness_step_hour [of 12]
have "⊢ HMC ⟶ (timeIs (12,59) ↝ timeIs (1,0))"
by (simp add: next_hour_def)
also have "⊢ HMC ⟶ (timeIs (1,0) ↝ timeIs (h2,0))"
proof (cases "h2 = 1")
case True thus ?thesis apply auto using LatticeReflexivity by blast
next
case False
have "⊢ HMC ⟶ (timeIs (1, 0) ↝ timeIs (1, 59))"
by (intro HMC_liveness_progress_forwards_minute, simp_all)
also from False h2
have "⊢ HMC ⟶ (timeIs (1, 59) ↝ timeIs (h2 - 1, 59))"
by (intro HMC_liveness_progress_forwards_hour, auto)
also from False h2 have "next_hour (h2 - 1) = h2"
by (auto simp add: next_hour_def)
with HMC_liveness_step_hour [of "h2 - 1"]
have "⊢ HMC ⟶ (timeIs (h2 - 1, 59) ↝ timeIs (h2, 0))" by auto
finally show ?thesis .
qed
also from m2 have "⊢ HMC ⟶ (timeIs (h2, 0) ↝ timeIs (h2, m2))"
by (intro HMC_liveness_progress_forwards_minute, simp_all)
finally show ?thesis .
qed
lemma HMC_liveness:
assumes h: "h ∈ {1..12}"
assumes m: "m ≤ 59"
shows "⊢ HMC ⟶ □◇ timeIs (h,m)"
proof -
from HMC_safety
have "⊢ HMC ⟶ ((#True :: stpred) ↝ (hr ∈ #{1..12} ∧ mn ∈ #{0..59}))"
by (intro imp_leadsto_invariant, simp)
also have "⊢ HMC ⟶ ((hr ∈ #{1..12} ∧ mn ∈ #{0..59}) ↝ (∃t. #(fst t ∈ {1..12} ∧ snd t ≤ 59) ∧ timeIs t))"
by (intro imp_imp_leadsto, auto)
also have "⊢ HMC ⟶ ((∃t. #(fst t ∈ {1..12} ∧ snd t ≤ 59) ∧ timeIs t) ↝ timeIs (h,m))"
unfolding inteq_reflection [OF leadsto_exists]
proof (intro imp_forall_leadsto)
fix t :: "nat × nat"
obtain h' m' where t: "t = (h', m')" by fastforce
show "fst t ∈ {1..12} ∧ snd t ≤ 59 ⟹ ⊢ HMC ⟶ (timeIs t ↝ timeIs (h, m))"
unfolding t using h m
by (intro HMC_liveness_progress, auto)
qed
finally show ?thesis
by (auto simp add: leadsto_def)
qed
lemma HMC_refines_HC: "⊢ HMC ⟶ HC"
unfolding HC_def
proof (intro temp_imp_conjI)
show "⊢ HMC ⟶ Init HCini" by (auto simp add: HMC_def HMCini_def Init_def)
have "⊢ HMC ⟶ □[HMCnxt]_(hr, mn)" by auto (simp add: HMC_def)
moreover have "⊢ [HMCnxt]_(hr, mn) ⟶ [HCnxt]_hr"
proof (intro intI temp_impI, clarify)
fix before after
assume "(before, after) ⊨ [HMCnxt]_(hr, mn)"
thus "(before, after) ⊨ [HCnxt]_hr"
by (cases "mn before = 59", auto simp add: square_def HMCnxt_eq HCnxt_def next_hour_def)
qed
ultimately show "⊢ HMC ⟶ □[HCnxt]_hr" by (metis STL4 temp_imp_trans)
define P :: stpred where "P ≡ timeIs (1,59)"
define B :: action where "B ≡ ACT $P"
define F :: temporal where "F ≡ TEMP ◇P"
define N :: action where "N ≡ ACT [HMCnxt]_(hr,mn)"
define A :: action where "A ≡ HMCnxt"
have "⊢ <$P ∧ HMCnxt>_(hr, mn) = ($P ∧ HMCnxt)" by (auto simp add: angle_def HMCnxt_eq)
note eqs = inteq_reflection [OF this]
have "⊢ HMC ⟶ □N ∧ WF(A)_(hr,mn) ∧ □F"
proof (intro temp_imp_conjI)
show "⊢ HMC ⟶ □N" by (auto simp add: N_def HMC_def)
from HMC_liveness show "⊢ HMC ⟶ □F" unfolding F_def P_def by auto
show "⊢ HMC ⟶ WF(A)_(hr, mn)"
unfolding HMC_def WF_def eqs A_def by auto
qed
also have "⊢ □N ∧ WF(A)_(hr,mn) ∧ □F ⟶ WF(HCnxt)_hr"
proof (intro WF2 stable_dmd_stuck)
show "⊢ N ∧ <B>_(hr, mn) ⟶ <HCnxt>_hr"
by (auto simp add: N_def square_def angle_def P_def B_def HMCnxt_eq HCnxt_def next_hour_def)
show "⊢ $P ∧ P$ ∧ <N ∧ A>_(hr, mn) ⟶ B"
by (auto simp add: angle_def P_def)
show "⊢ P ∧ Enabled (<HCnxt>_hr) ⟶ Enabled (<A>_(hr, mn))"
unfolding eqs A_def by (auto simp add: P_def)
let ?PREM = "TEMP □(N ∧ [¬ B]_(hr, mn)) ∧ WF(A)_(hr, mn) ∧ □F ∧ ◇□Enabled (<HCnxt>_hr)"
show "⊢ ?PREM ⟶ stable P"
apply (intro tempI temp_impI Stable [where A = "ACT N ∧ [¬ $P]_(hr, mn)"])
by (auto simp add: square_def P_def N_def B_def)
have "⊢ ?PREM ⟶ □◇P" unfolding F_def by auto
also have "⊢ □◇P ⟶ ◇P" by (intro STL2)
finally show "⊢ ?PREM ⟶ ◇ P" .
qed
finally show "⊢ HMC ⟶ WF(HCnxt)_hr" .
qed
end
end
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment