Created
June 11, 2021 10:33
-
-
Save DaveCTurner/60eb3d9f8ceaabb7c4d693831c2ebf64 to your computer and use it in GitHub Desktop.
Isabelle model of example of dependent specs from https://www.hillelwayne.com/post/spec-composition/
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* Isabelle model of example of dependent specs from https://www.hillelwayne.com/post/spec-composition/ *) | |
theory Blink | |
imports "./TLA-Utils" | |
begin | |
definition Blink :: "bool stfun ⇒ action" | |
where "Blink v ≡ ACT ($v ⟶ ¬v$ ∧ ¬$v ⟶ v$)" | |
definition TurnOn :: "bool stfun ⇒ action" | |
where "TurnOn v ≡ ACT (¬$v ∧ v$)" | |
definition TurnOff :: "bool stfun ⇒ action" | |
where "TurnOff v ≡ ACT ($v ∧ ¬v$)" | |
definition blinks :: "bool stfun ⇒ temporal" | |
where "blinks v ≡ TEMP □◇v ∧ □◇¬v" | |
lemma | |
fixes v :: "bool stfun" | |
fixes Spec :: temporal | |
assumes step: "⊢ Spec ⟶ □[Blink v]_v" | |
assumes fair: "⊢ Spec ⟶ WF(Blink v)_v" | |
assumes base: "basevars v" | |
shows blinksI: "⊢ Spec ⟶ blinks v" | |
proof - | |
have unstable: "⊢ Spec ⟶ ((v = #b) ↝ (v ≠ #b))" for b | |
proof - | |
from assms have "⊢ Spec ⟶ □[Blink v]_v ∧ WF(Blink v)_v" by (simp add: temp_imp_conjI) | |
also have "⊢ □[Blink v]_v ∧ WF(Blink v)_v ⟶ ((v = #b) ↝ (v ≠ #b))" | |
proof (intro WF1) | |
show "⊢ $(v = #b) ∧ [Blink v]_v ⟶ (v = #b)$ ∨ (v ≠ #b)$" by fastforce | |
show "⊢ ($(v = #b) ∧ [Blink v]_v) ∧ <Blink v>_v ⟶ (v ≠ #b)$" by fastforce | |
show "⊢ $(v = #b) ∧ [Blink v]_v ⟶ $Enabled (<Blink v>_v)" | |
by (intro actionI temp_impI, elim temp_conjE, simp, intro base_enabled [OF base], | |
auto simp add: square_def angle_def Blink_def) | |
qed | |
finally show ?thesis . | |
qed | |
have [simp]: "(PRED (v = #False)) = (PRED (¬v))" by auto | |
note unstable [of False] | |
also have "⊢ ((v = #False) ↝ (v ≠ #False)) ⟶ □◇v" by (intro unstable_implies_infinitely_often, simp) | |
finally have 1: "⊢ Spec ⟶ □◇v". | |
note unstable [of True] | |
also have "⊢ ((v = #True) ↝ (v ≠ #True)) ⟶ □◇¬v" by (intro unstable_implies_infinitely_often, simp) | |
finally have 2: "⊢ Spec ⟶ □◇¬v". | |
from 1 2 show ?thesis by (simp add: temp_imp_conjI blinks_def) | |
qed | |
locale BlinkerX = | |
fixes x :: "bool stfun" | |
fixes f :: "bool stfun" | |
assumes bvs: "basevars (x, f)" | |
begin | |
definition Initl :: stpred where "Initl ≡ PRED #True" | |
definition Next :: action where "Next ≡ ACT (Blink x ∧ (TurnOn f ∨ ($f ∧ f$)))" | |
definition Env :: action where "Env ≡ ACT (¬f$ ∧ unchanged x)" | |
definition Fair :: temporal where "Fair ≡ TEMP WF(Blink x)_x" | |
definition Spec :: temporal where "Spec ≡ TEMP (Initial Initl ∧ □[Next ∨ Env]_(f,x) ∧ Fair)" | |
definition BadSpec :: temporal where "BadSpec ≡ TEMP (Initial Initl ∧ □[Next ]_(f,x) ∧ Fair)" | |
lemma "⊢ Spec ⟶ blinks x" | |
proof (intro blinksI) | |
from bvs show "basevars x" using base_pair1 by blast | |
show "⊢ Spec ⟶ WF(Blink x)_x" by (auto simp add: Spec_def Fair_def) | |
have "⊢ Spec ⟶ □[Next ∨ Env]_(f,x)" by (simp add: Spec_def intI) | |
also have "⊢ □[Next ∨ Env]_(f,x) ⟶ □[Blink x]_x" | |
by (intro STL4, auto simp add: square_def Next_def Blink_def) | |
finally show "⊢ Spec ⟶ □[Blink x]_x" . | |
qed | |
end | |
locale BlinkerY = | |
fixes y :: "bool stfun" | |
fixes f :: "bool stfun" | |
assumes bvs: "basevars (y, f)" | |
begin | |
definition Initl :: stpred where "Initl ≡ PRED #True" | |
definition Next :: action where "Next ≡ ACT (Blink y ∧ (TurnOff f ∨ (¬$f ∧ ¬f$)))" | |
definition Env :: action where "Env ≡ ACT (f$ ∧ unchanged y)" | |
definition Fair :: temporal where "Fair ≡ TEMP WF(Blink y)_y" | |
definition Spec :: temporal where "Spec ≡ TEMP (Initial Initl ∧ □[Next ∨ Env]_(f,y) ∧ Fair)" | |
definition BadSpec :: temporal where "BadSpec ≡ TEMP (Initial Initl ∧ □[Next ]_(f,y) ∧ Fair)" | |
lemma "⊢ Spec ⟶ blinks y" | |
proof (intro blinksI) | |
from bvs show "basevars y" using base_pair1 by blast | |
show "⊢ Spec ⟶ WF(Blink y)_y" by (auto simp add: Spec_def Fair_def) | |
have "⊢ Spec ⟶ □[Next ∨ Env]_(f,y)" by (simp add: Spec_def intI) | |
also have "⊢ □[Next ∨ Env]_(f,y) ⟶ □[Blink y]_y" | |
by (intro STL4, auto simp add: square_def Next_def Blink_def) | |
finally show "⊢ Spec ⟶ □[Blink y]_y" . | |
qed | |
end | |
locale Combined = X: BlinkerX x f + Y: BlinkerY y f | |
for x y f | |
begin | |
lemma temp_imp_diamond: "⊢ A ⟶ D" | |
if "⊢ A ⟶ (B ∨ C)" "⊢ B ⟶ D" "⊢ C ⟶ D" for A B C D | |
using that by fastforce | |
lemma "⊢ X.BadSpec ∧ Y.BadSpec ⟶ #False" | |
proof - | |
have "⊢ X.BadSpec ∧ Y.BadSpec ⟶ □([X.Next]_(f,x) ∧ [Y.Next]_(f,y))" | |
unfolding X.BadSpec_def Y.BadSpec_def by auto | |
also have "⊢ □([X.Next]_(f,x) ∧ [Y.Next]_(f,y)) ⟶ □(unchanged f)" | |
by (intro STL4, auto simp add: X.Next_def Blink_def TurnOn_def Y.Next_def TurnOff_def square_def) | |
finally have "⊢ X.BadSpec ∧ Y.BadSpec ⟶ □(unchanged f) ∧ X.BadSpec ∧ Y.BadSpec" by auto | |
also have "⊢ □(unchanged f) ∧ X.BadSpec ∧ Y.BadSpec ⟶ #False" | |
proof (rule temp_imp_diamond) | |
show "⊢ □(unchanged f) ∧ X.BadSpec ∧ Y.BadSpec | |
⟶ (□(unchanged f) ∧ Y.BadSpec ∧ Init f) | |
∨ (□(unchanged f) ∧ X.BadSpec ∧ Init ¬f)" | |
by (auto simp add: Init_simps2) | |
have "⊢ □(unchanged f) ∧ Y.BadSpec ∧ Init f ⟶ □[Y.Next]_(f,y) ∧ WF(Blink y)_y" | |
unfolding Y.BadSpec_def Y.Fair_def by auto | |
also have "⊢ □[Y.Next]_(f,y) ∧ WF(Blink y)_y ⟶ (((#True)::stpred) ↝ ¬f)" | |
proof (intro WF1) | |
show "⊢ $#True ∧ [Y.Next]_(f, y) ⟶ $Enabled (<Blink y>_y)" | |
by (intro actionI temp_impI, elim temp_conjE, simp, intro base_enabled [OF Y.bvs], | |
auto simp add: square_def angle_def Blink_def) | |
qed (auto simp add: angle_def Blink_def square_def Y.Next_def TurnOff_def) | |
also have "⊢ (((#True)::stpred) ↝ ¬f) ⟶ ¬ □f" | |
by (simp add: leadsto_def more_temp_simps3 reflT) | |
finally have "⊢ □unchanged f ∧ Y.BadSpec ∧ Init f ⟶ ¬ □f" . | |
moreover have "⊢ □(unchanged f) ∧ Y.BadSpec ∧ Init f ⟶ □f" by auto_invariant | |
ultimately show " ⊢ □unchanged f ∧ Y.BadSpec ∧ Init f ⟶ #False" by fastforce | |
have "⊢ □(unchanged f) ∧ X.BadSpec ∧ Init ¬f ⟶ □[X.Next]_(f,x) ∧ WF(Blink x)_x" | |
unfolding X.BadSpec_def X.Fair_def by auto | |
also have "⊢ □[X.Next]_(f,x) ∧ WF(Blink x)_x ⟶ (((#True)::stpred) ↝ f)" | |
proof (intro WF1) | |
show "⊢ $#True ∧ [X.Next]_(f, x) ⟶ $Enabled (<Blink x>_x)" | |
by (intro actionI temp_impI, elim temp_conjE, simp, intro base_enabled [OF X.bvs], | |
auto simp add: square_def angle_def Blink_def) | |
qed (auto simp add: angle_def Blink_def square_def X.Next_def TurnOn_def) | |
also have "⊢ (((#True)::stpred) ↝ f) ⟶ ¬ □ ¬f" | |
by (simp add: leadsto_def more_temp_simps3 reflT) | |
finally have "⊢ □unchanged f ∧ X.BadSpec ∧ Init ¬f ⟶ ¬ □ ¬f" . | |
moreover have "⊢ □(unchanged f) ∧ X.BadSpec ∧ Init ¬f ⟶ □ ¬f" by auto_invariant | |
ultimately show " ⊢ □unchanged f ∧ X.BadSpec ∧ Init ¬f ⟶ #False" by fastforce | |
qed | |
finally show ?thesis. | |
qed | |
lemma obtains sigma where "sigma ⊨ X.Spec ∧ Y.Spec" | |
proof - | |
(* now what...? *) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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) | |
text ‹The 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