Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Isabelle model of example of dependent specs from https://www.hillelwayne.com/post/spec-composition/
theory "TLA-Utils"
imports "HOL-TLA.TLA"
begin
syntax
"_liftSubset" :: "[lift, lift] ⇒ lift" ("(_/ ⊆ _)" [50, 51] 50)
"_liftInter" :: "[lift, lift] ⇒ lift" ("(_/ ∩ _)" [50, 51] 50)
"_liftUn" :: "[lift, lift] ⇒ lift" ("(_/ ∪ _)" [50, 51] 50)
translations
"_liftSubset" == "_lift2 (⊆)"
"_liftInter" == "_lift2 (∩)"
"_liftUn" == "_lift2 (∪)"
lemma imp_imp_leadsto:
assumes "⊢ F ⟶ G"
shows "⊢ S ⟶ (F ↝ G)"
apply (auto simp add: Valid_def)
using ImplLeadsto_simple assms by blast
lemma imp_leadsto_transitive[trans]:
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 imp_eventually_tautology:
assumes "⊢ F"
shows "⊢ S ⟶ ◇F"
using assms by (smt DmdImplE Valid_def int_simps(1) temp_simps(2) unl_lift2)
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_disjE:
assumes "sigma ⊨ F ∨ G"
assumes "sigma ⊨ F ⟹ P"
assumes "sigma ⊨ G ⟹ P"
shows "P"
using assms by auto
lemma temp_exI:
assumes "sigma ⊨ F x"
shows "sigma ⊨ (∃x. F x)"
using assms by auto
lemma temp_exE:
assumes "sigma ⊨ ∃x. F x"
assumes "⋀x. sigma ⊨ F x ⟹ P"
shows "P"
using assms by auto
lemma temp_ex_impI:
assumes "⋀x. ⊢ F x ⟶ G"
shows "⊢ (∃x. F x) ⟶ G"
using assms by (auto simp add: Valid_def)
lemma action_beforeI: assumes "s ⊨ P" shows "(s,t) ⊨ $P" using assms by simp
lemma action_afterI: assumes "t ⊨ P" shows "(s,t) ⊨ P$" using assms by simp
lemma temp_imp_conjI:
assumes "⊢ S ⟶ P" "⊢ S ⟶ Q"
shows "⊢ S ⟶ P ∧ Q"
using assms unfolding Valid_def
by auto
lemma temp_imp_box_conjI:
assumes "⊢ S ⟶ □P" "⊢ S ⟶ □Q"
shows "⊢ S ⟶ □(P ∧ Q)"
using assms by (simp add: split_box_conj Valid_def)
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)
lemma imp_leadsto_reflexive: "⊢ S ⟶ (F ↝ F)" using LatticeReflexivity [where F = F] by auto
lemma imp_leadsto_diamond:
assumes "⊢ S ⟶ (A ↝ (B ∨ C))"
assumes "⊢ S ⟶ (B ↝ D)"
assumes "⊢ S ⟶ (C ↝ D)"
shows "⊢ S ⟶ (A ↝ D)"
proof (intro tempI temp_impI)
fix sigma
assume S: "sigma ⊨ S"
with assms have
ABC: "sigma ⊨ A ↝ (B ∨ C)" and
BD: "sigma ⊨ B ↝ D" and
CD: "sigma ⊨ C ↝ D"
by (auto simp add: Valid_def)
with LatticeDiamond [where A = A and B = B and C = C and D = D]
show "sigma ⊨ A ↝ D"
by (auto simp add: Valid_def)
qed
lemma imp_disj_leadstoI:
assumes "⊢ S ⟶ (A ↝ C)"
assumes "⊢ S ⟶ (B ↝ C)"
shows "⊢ S ⟶ (A ∨ B ↝ C)"
by (intro imp_leadsto_diamond [OF imp_leadsto_reflexive] assms)
lemma imp_disj_excl_leadstoI:
assumes "⊢ S ⟶ (A ↝ C)"
assumes "⊢ S ⟶ ((¬A ∧ B) ↝ C)"
shows "⊢ S ⟶ (A ∨ B ↝ C)"
proof -
have "⊢ S ⟶ (A ∨ B ↝ (A ∨ (¬A ∧ B)))"
by (intro imp_imp_leadsto, auto)
also have "⊢ S ⟶ ((A ∨ (¬A ∧ B)) ↝ C)"
using assms by (intro imp_disj_leadstoI)
finally show ?thesis .
qed
lemma temp_conj_eq_imp:
assumes "⊢ P ⟶ (Q = R)"
shows "⊢ (P ∧ Q) = (P ∧ R)"
using assms by (auto simp add: Valid_def)
textThe following lemma is particularly useful for a system that makes
some progress which either reaches the desired state directly or which leaves it in
a state that is definitely not the desired state but from which it can reach the desired state via
some further progress.
lemma imp_leadsto_triangle_excl:
assumes AB: "⊢ S ⟶ (A ↝ B)"
assumes BC: "⊢ S ⟶ ((B ∧ ¬C) ↝ C)"
shows "⊢ S ⟶ (A ↝ C)"
proof -
have "⊢ ((B ∧ ¬C) ∨ (B ∧ C)) = B" by auto
from inteq_reflection [OF this] AB have ABCBC: "⊢ S ⟶ (A ↝ ((B ∧ ¬C) ∨ (B ∧ C)))" by simp
show ?thesis
proof (intro imp_leadsto_diamond [OF ABCBC] BC)
from ImplLeadsto_simple [where F = "LIFT (B ∧ C)"]
show "⊢ S ⟶ (B ∧ C ↝ C)"
by (auto simp add: Valid_def)
qed
qed
lemma imp_leadsto_triangle_extra_assm:
assumes AB: "⊢ S ⟶ (A ∧ ¬B ↝ A ∧ B)"
shows "⊢ S ⟶ (A ↝ A ∧ B)"
proof (rule imp_leadsto_triangle_excl [OF imp_leadsto_reflexive])
have "⊢ S ⟶ (A ∧ ¬ (A ∧ B) ↝ A ∧ ¬B)"
by (intro imp_imp_leadsto, auto)
with AB show "⊢ S ⟶ (A ∧ ¬ (A ∧ B) ↝ A ∧ B)" by (metis imp_leadsto_transitive)
qed
lemma imp_forall:
assumes "⋀x. ⊢ S ⟶ P x"
shows "⊢ S ⟶ (∀x. P x)"
using assms by (auto simp add: Valid_def)
lemma imp_exists_leadstoI:
assumes "⋀x. ⊢ S ⟶ (P x ↝ Q)"
shows "⊢ S ⟶ ((∃ x. P x) ↝ Q)"
unfolding inteq_reflection [OF leadsto_exists]
by (intro imp_forall assms)
lemma imp_INV_leadsto:
"⊢ S ⟶ □I ⟹ ⊢ S ⟶ (P ∧ I ↝ Q) ⟹ ⊢ S ⟶ (P ↝ Q)"
using INV_leadsto by (auto simp add: Valid_def, blast)
lemma wf_imp_leadsto:
assumes 1: "wf r"
and 2: "⋀x. ⊢ S ⟶ (F x ↝ (G ∨ (∃y. #((y,x)∈r) ∧ F y)))"
shows "⊢ S ⟶ (F x ↝ G)"
proof (intro tempI temp_impI)
fix sigma assume sigma: "sigma ⊨ S"
with 2 have "⋀x. sigma ⊨ F x ↝ (G ∨ (∃y. #((y,x)∈r) ∧ F y))"
by (auto simp add: Valid_def)
from 1 this show "sigma ⊨ F x ↝ G" by (rule wf_leadsto)
qed
lemma wf_imp_ex_leadsto:
assumes 1: "wf r" and 2: "⋀x. ⊢ S ⟶ (F x ↝ (G ∨ (∃y. #((y,x)∈r) ∧ F y)))"
shows "⊢ S ⟶ ((∃x. F x) ↝ G)"
using 1 2
by (intro imp_exists_leadstoI wf_imp_leadsto [where G = G], auto)
lemma unstable_implies_infinitely_often:
fixes P :: stpred
assumes "⊢ S ⟶ (¬P ↝ P)"
shows "⊢ S ⟶ □◇P"
proof -
define T :: stpred where "T ≡ PRED #True"
have "⊢ S ⟶ (T ↝ P)"
proof (rule imp_leadsto_triangle_excl)
show "⊢ S ⟶ (T ↝ T)" by (intro imp_imp_leadsto, simp)
from assms show "⊢ S ⟶ (T ∧ ¬ P ↝ P)" by (simp add: T_def)
qed
thus ?thesis by (simp add: leadsto_def T_def)
qed
lemma imp_infinitely_often_implies_eventually:
assumes "⊢ S ⟶ □◇P"
shows "⊢ S ⟶ ◇P"
using assms reflT temp_imp_trans by blast
lemma imp_eventually_forever_implies_infinitely_often:
fixes P :: stpred
assumes "⊢ S ⟶ ◇□P"
shows "⊢ S ⟶ □◇P"
using assms DBImplBD temp_imp_trans by blast
lemma imp_leadsto_add_precondition:
assumes "⊢ S ⟶ □R"
assumes "⊢ S ⟶ ((P ∧ R) ↝ Q)"
shows "⊢ S ⟶ (P ↝ Q)"
using assms
by (meson INV_leadsto temp_imp_conjI temp_imp_trans)
lemma box_conj_simp[simp]: "(TEMP □(F ∧ G)) = (TEMP □F ∧ □G)"
using STL5 by fastforce
lemma box_box_conj:
shows "⊢ (□(F ∧ □P)) = (□F ∧ □P)"
by (metis STL3 STL5 inteq_reflection)
lemmas box_box_conj_simp[simp] = inteq_reflection [OF box_box_conj]
lemma box_before_conj:
shows "⊢ (□A ∧ □P) ⟶ (□(A ∧ $P))"
by (metis STL5 TLA.Init_simps(2) TrueW boxInit_act boxInit_stp int_simps(13) inteq_reflection)
lemma box_conj_box_dmd:
shows "⊢ (□P ∧ □◇Q) ⟶ □◇(P ∧ Q)"
by (metis (mono_tags, lifting) BoxDmd_simple STL3 STL4 STL5 inteq_reflection)
lemma imp_box_imp_leadsto:
assumes "⊢ S ⟶ □(P ⟶ Q)"
shows "⊢ S ⟶ (P ↝ Q)"
using assms
unfolding Valid_def
apply auto
by (metis ImplLeadsto Init.Init_simps(1) Init_simps2(3) STL4E boxInitD dmdInitD leadsto_def more_temp_simps3(2))
lemma temp_conj_assoc[simp]: "TEMP ((P ∧ Q) ∧ R) = TEMP (P ∧ Q ∧ R)" by auto
lemma enabled_exI:
assumes "s ⊨ Enabled P x"
shows "s ⊨ Enabled (∃ x. P x)"
using assms
unfolding enabled_def by auto
lemma enabled_guard_conjI:
assumes "⋀t. (s,t) ⊨ P"
assumes "s ⊨ Enabled Q"
shows "s ⊨ Enabled (P ∧ Q)"
using assms unfolding enabled_def by auto
lemma angle_ex_simp[simp]: "(ACT <∃x. P x>_vs) = (ACT ∃x. <P x>_vs)"
by (auto simp add: angle_def)
lemma leadsto_dmd_classical: "⊢ ((◇F) ∧ ((□¬G) ↝ G)) ⟶ (F ↝ G)"
unfolding leadsto_def dmd_def
by (force simp: Init_simps elim: STL4E)
lemma "⊢ WF(A)_vars ⟶ □[¬ A]_vars ⟶ □◇¬Enabled (<A>_vars)"
proof -
have 1: "⊢ [¬ A]_vars = (¬<A>_vars)" by (auto simp add: angle_def square_def)
have 2: "⊢ (□◇¬Enabled (<A>_vars)) = (¬◇□Enabled (<A>_vars))"
by (auto simp add: more_temp_simps)
show ?thesis
unfolding WF_def inteq_reflection[OF 1] inteq_reflection[OF 2]
apply auto
using more_temp_simps3(7) reflT by fastforce
qed
lemma imp_SFI:
assumes "⊢ S ⟶ (Enabled (<A>_v) ↝ <A>_v)"
shows "⊢ S ⟶ SF(A)_v"
unfolding SF_def using assms leadsto_infinite apply auto by fastforce
lemma imp_pred_leadsto_act_reflexive: "⊢ S ⟶ (A ↝ $A)"
by (metis Init_stp_act_rev imp_leadsto_reflexive leadsto_def)
lemma imp_unstable_leadsto_change:
assumes "⊢ S ⟶ (P ↝ ¬P)"
shows "⊢ S ⟶ (P ↝ ($P ∧ ¬P$))"
proof -
note assms
also have "⊢ (P ↝ ¬P) ⟶ (P ↝ ($P ∧ ¬P$))"
unfolding leadsto_def
proof (intro STL4 tempI temp_impI)
fix sigma
assume Init_P: "sigma ⊨ Init P"
assume "sigma ⊨ Init P ⟶ ◇¬ P"
with Init_P have not_always_P: "sigma ⊨ ¬□P"
by (auto simp add: more_temp_simps)
show "sigma ⊨ ◇($P ∧ ¬ P$)"
proof (rule ccontr, simp add: more_temp_simps)
assume no_transition: "sigma ⊨ □¬ ($P ∧ ¬ P$)"
have "sigma ⊨ □P"
proof (invariant, intro Init_P, intro Stable)
from no_transition show "sigma ⊨ □¬ ($P ∧ ¬ P$)".
show "⊢ $P ∧ ¬ ($P ∧ ¬ P$) ⟶ P$" by auto
qed
with not_always_P show False by simp
qed
qed
finally show ?thesis by simp
qed
lemma
fixes A B C :: temporal
assumes "⊢ A ⟶ B ⟶ C" "sigma ⊨ □A" "sigma ⊨ □B"
shows ABC_imp_box: "sigma ⊨ □C"
using assms by (metis (full_types) STL4E normalT tempD unl_lift2)
lemma shows imp_after_leadsto: "⊢ S ⟶ (P$ ↝ P)"
unfolding Valid_def leadsto_def apply auto
by (metis DmdPrime InitDmd dmdInitD necT tempD temp_imp_trans)
lemma imp_eventually_leadsto_eventually[trans]:
assumes 1: "⊢ S ⟶ ◇P"
assumes 2: "⊢ S ⟶ (P ↝ Q)"
shows "⊢ S ⟶ ◇Q"
proof (intro tempI temp_impI)
fix sigma assume sigma: "sigma ⊨ S"
with 1 2 have 1: "sigma ⊨ ◇P" and 2: "sigma ⊨ P ↝ Q" by auto
from 1 2 show "sigma ⊨ ◇Q"
apply (simp add: leadsto_def)
by (metis DmdImpl2 dmdInit dup_dmdD)
qed
lemma imp_eventually_init:
assumes "⊢ S ⟶ Init P"
shows "⊢ S ⟶ ◇ P"
using assms InitDmd_gen temp_imp_trans by blast
lemma imp_box_before_afterI:
assumes "⊢ S ⟶ □P"
shows "⊢ S ⟶ □($P ∧ P$)"
using assms using BoxPrime temp_imp_trans by blast
lemma imp_box_afterI:
assumes "⊢ S ⟶ □P"
shows "⊢ S ⟶ □(P$)"
proof -
from assms have "⊢ S ⟶ □($P ∧ P$)" by (intro imp_box_before_afterI)
also have "⊢ □($P ∧ P$) ⟶ □(P$)" by auto
finally show ?thesis .
qed
lemma imp_dmd_conj_invariant:
assumes "⊢ S ⟶ □P"
assumes "⊢ S ⟶ ◇Q"
shows "⊢ S ⟶ ◇(P ∧ Q)"
using assms BoxDmd_simple by fastforce
lemma invariantI:
fixes A :: action
assumes "⊢ S ⟶ Init P"
assumes "⊢ S ⟶ □A"
assumes "⋀s t. ⟦ s ⊨ P; (s,t) ⊨ A ⟧ ⟹ t ⊨ P"
shows "⊢ S ⟶ □P"
proof invariant
fix sigma assume sigma: "sigma ⊨ S"
with assms show "sigma ⊨ Init P" by auto
show "sigma ⊨ stable P"
proof (intro Stable actionI temp_impI)
from sigma assms show "sigma ⊨ □A" by auto
fix s t assume "(s,t) ⊨ $P ∧ A" with assms show "(s,t) ⊨ P$" by auto
qed
qed
end
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment