Isabelle model of example of dependent specs from https://www.hillelwayne.com/post/spec-composition/

Blink.thy

(* 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...? *)

TLA-Utils.thy

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