(*<*)
theory LTL
imports
  CIMP_pred
  Infinite_Sequences
begin

(*>*)
section‹ Linear Temporal Logic \label{sec:ltl}›

text‹

  talk about liveness we need to consider infinitary behaviour on
 . Traditionally future-time linear temporal logic (LTL) is used to do
  cite‹"MannaPnueli:1991" and "OwickiLamport:1982"›.

  following is a straightforward shallow embedding of the
 -traditional anchored semantics of LTL cite‹"MannaPnueli:1988"›. Some of it is adapted
  the sophisticated TLA development in the AFP due to 🚫‹"TLA-AFP"›.

  🚫‹"Lamport:2002"›, include the
  operator, which is convenient for stating rules. Sometimes it allows us to
  the system, i.e. to state rules as temporally valid
 LTL-valid) rather than just temporally program valid (LTL-cimp-), in Jackson's terminology.

 ›

definition state_prop :: "('a → bool) → 'a seq_pred" (‹⌈_⌉›) where
  "⌈P⌉ = (λσ. P (σ 0))"

definition "next" :: "'a seq_pred → 'a seq_pred" (‹◯_› [80] 80) where
  "(◯P) = (λσ. P (σ |_s 1))"

definition always :: "'a seq_pred → 'a seq_pred" (‹◻_› [80] 80) where
  "(◻P) = (λσ. ∀i. P (σ |_s i))"

definition until :: "'a seq_pred → 'a seq_pred → 'a seq_pred" (infixr ‹U› 30) where (* FIXME priority, binds tighter than \<^bold>\<longrightarrow> *)
  "(P U Q) = (λσ. ∃i. Q (σ |_s i) ∧ (∀k<i. P (σ |_s k)))"

definition eventually :: "'a seq_pred → 'a seq_pred" (‹♢_› [80] 80) where (* FIXME priority, consider making an abbreviation *)
  "(♢P) = (⟨True⟩ U P)"

definition release :: "'a seq_pred → 'a seq_pred → 'a seq_pred" (infixr ‹R› 30) where (* FIXME priority, dual of Until *)
  "(P R Q) = (\<not>(\<not>P U \<not>Q))"

definition unless :: "'a seq_pred → 'a seq_pred → 'a seq_pred" (infixr ‹W› 30) where (* FIXME priority, aka weak until *)
  "(P W Q) = ((P U Q) \<or> ◻P)"

abbreviation (input)
  pred_always_imp_syn :: "'a seq_pred → 'a seq_pred → 'a seq_pred" (infixr ‹\↪› 25) where
  "P \<hookrightarrow> Q ≡ ◻(P \<longrightarrow> Q)"

lemmas defs =
  state_prop_def
  always_def
  eventually_def
  next_def
  release_def
  unless_def
  until_def

lemma suffix_state_prop[simp]:
  shows "⌈P⌉ (σ |_s i) = P (σ i)"
unfolding defs by simp

lemma alwaysI[intro]:
  assumes "∧i. P (σ |_s i)"
  shows "(◻P) σ"
unfolding defs using assms by blast

lemma alwaysD:
  assumes "(◻P) σ"
  shows "P (σ |_s i)"
using assms unfolding defs by blast

lemma alwaysE: "[(◻P) σ; P (σ |_s i) ==> Q] ==> Q"
unfolding defs by blast

lemma always_induct:
  assumes "P σ"
  assumes "(◻(P \<longrightarrow> ◯P)) σ"
  shows "(◻P) σ"
proof(rule alwaysI)
  fix i from assms show "P (σ |_s i)"
    unfolding defs by (induct i) simp_all
qed

lemma seq_comp:
  fixes σ :: "'a seq"
  fixes P :: "'b seq_pred"
  fixes f :: "'a → 'b"
  shows
    "(◻P) (f ∘ σ) ⟷ (◻(λσ. P (f ∘ σ))) σ"
    "(♢P) (f ∘ σ) ⟷ (♢(λσ. P (f ∘ σ))) σ"
    "(P U Q) (f ∘ σ) ⟷ ((λσ. P (f ∘ σ)) U (λσ. Q (f ∘ σ))) σ"
    "(P W Q) (f ∘ σ) ⟷ ((λσ. P (f ∘ σ)) W (λσ. Q (f ∘ σ))) σ"
unfolding defs by simp_all

lemma nextI[intro]:
  assumes "P (σ |_s Suc 0)"
  shows "(◯P) σ"
using assms unfolding defs by simp

lemma untilI[intro]:
  assumes "Q (σ |_s i)"
  assumes "∀k<i. P (σ |_s k)"
  shows "(P U Q) σ"
unfolding defs using assms by blast

lemma untilE:
  assumes "(P U Q) σ"
  obtains i where "Q (σ |_s i)" and "∀k<i. P (σ |_s k)"
using assms unfolding until_def by blast

lemma eventuallyI[intro]:
  assumes "P (σ |_s i)"
  shows "(♢P) σ"
unfolding eventually_def using assms by blast

lemma eventuallyE[elim]:
  assumes "(♢P) σ"
  obtains i where "P (σ |_s i)"
using assms unfolding defs by (blast elim: untilE)

lemma unless_alwaysI:
  assumes "(◻ P) σ"
  shows "(P W Q) σ"
using assms unfolding defs by blast

lemma unless_untilI:
  assumes "Q (σ |_s j)"
  assumes "∧i. i < j ==> P (σ |_s i)"
  shows "(P W Q) σ"
unfolding defs using assms by blast

lemma always_imp_refl[iff]:
  shows "(P \<hookrightarrow> P) σ"
unfolding defs by blast

lemma always_imp_trans:
  assumes "(P \<hookrightarrow> Q) σ"
  assumes "(Q \<hookrightarrow> R) σ"
  shows "(P \<hookrightarrow> R) σ"
using assms unfolding defs by blast

lemma always_imp_mp:
  assumes "(P \<hookrightarrow> Q) σ"
  assumes "P σ"
  shows "Q σ"
using assms unfolding defs by (metis suffix_zero)

lemma always_imp_mp_suffix:
  assumes "(P \<hookrightarrow> Q) σ"
  assumes "P (σ |_s i)"
  shows "Q (σ |_s i)"
using assms unfolding defs by metis

text‹

  basic facts and equivalences, mostly sanity.

 ›

lemma necessitation:
  "(∧s. P s) ==> (◻P) σ"
  "(∧s. P s) ==> (♢P) σ"
  "(∧s. P s) ==> (P W Q) σ"
  "(∧s. Q s) ==> (P U Q) σ"
unfolding defs by auto

lemma cong:
  "(∧s. P s = P' s) ==> ⌈P⌉ = ⌈P'⌉"
  "(∧σ. P σ = P' σ) ==> (◻P) = (◻P')"
  "(∧σ. P σ = P' σ) ==> (♢P) = (♢P')"
  "(∧σ. P σ = P' σ) ==> (◯P) = (◯P')"
  "[∧σ. P σ = P' σ; ∧σ. Q σ = Q' σ] ==> (P U Q) = (P' U Q')"
  "[∧σ. P σ = P' σ; ∧σ. Q σ = Q' σ] ==> (P W Q) = (P' W Q')"
unfolding defs by auto

lemma norm[simp]:
  "⌈⟨False⟩⌉ = ⟨False⟩"
  "⌈⟨True⟩⌉ = ⟨True⟩"
  "(\<not>⌈p⌉) = ⌈\<not>p⌉"
  "(⌈p⌉ \<and> ⌈q⌉) = ⌈p \<and> q⌉"
  "(⌈p⌉ \<or> ⌈q⌉) = ⌈p \<or> q⌉"
  "(⌈p⌉ \<longrightarrow> ⌈q⌉) = ⌈p \<longrightarrow> q⌉"
  "(⌈p⌉ σ ∧ ⌈q⌉ σ) = ⌈p \<and> q⌉ σ"
  "(⌈p⌉ σ ∨ ⌈q⌉ σ) = ⌈p \<or> q⌉ σ"
  "(⌈p⌉ σ ⟶ ⌈q⌉ σ) = ⌈p \<longrightarrow> q⌉ σ"

  "(◯⟨False⟩) = ⟨False⟩"
  "(◯⟨True⟩) = ⟨True⟩"

  "(◻⟨False⟩) = ⟨False⟩"
  "(◻⟨True⟩) = ⟨True⟩"
  "(\<not>◻ P) σ = (♢ (\<not> P)) σ"
  "(◻◻ P) = (◻ P)"

  "(♢⟨False⟩) = ⟨False⟩"
  "(♢⟨True⟩) = ⟨True⟩"
  "(\<not>♢ P) = (◻ (\<not> P))"
  "(♢♢ P) = (♢ P)"

  "(P W ⟨False⟩) = (◻ P)"

  "(\<not>(P U Q)) σ = (\<not>P R \<not>Q) σ"
  "(⟨False⟩ U P) = P"
  "(P U ⟨False⟩) = ⟨False⟩"
  "(P U ⟨True⟩) = ⟨True⟩"
  "(⟨True⟩ U P) = (♢ P)"
  "(P U (P U Q)) = (P U Q)"

  "(\<not>(P R Q)) σ = (\<not>P U \<not>Q) σ"
  "(⟨False⟩ R P) = (◻P)"
  "(P R ⟨False⟩) = ⟨False⟩"
  "(⟨True⟩ R P) = P"
  "(P R ⟨True⟩) = ⟨True⟩"
(*
  "(P \<U> (P \<U> Q)) \<sigma> = (P \<U> Q) \<sigma>" FIXME for Release
*)
unfolding defs
apply (auto simp: fun_eq_iff)
apply (metis suffix_plus suffix_zero)
apply (metis suffix_plus suffix_zero)
  apply fastforce
  apply force
apply (metis add.commute add_diff_inverse_nat less_diff_conv2 not_le)
apply (metis add.right_neutral not_less0)
  apply force
  apply fastforce
done

lemma always_conj_distrib: "(◻(P \<and> Q)) = (◻P \<and> ◻Q)"
unfolding defs by auto

lemma eventually_disj_distrib: "(♢(P \<or> Q)) = (♢P \<or> ♢Q)"
unfolding defs by auto

lemma always_eventually[elim!]:
  assumes "(◻P) σ"
  shows "(♢P) σ"
using assms unfolding defs by auto

lemma eventually_imp_conv_disj: "(♢(P \<longrightarrow> Q)) = (♢(\<not>P) \<or> ♢Q)"
unfolding defs by auto

lemma eventually_imp_distrib:
  "(♢(P \<longrightarrow> Q)) = (◻P \<longrightarrow> ♢Q)"
unfolding defs by auto

lemma unfold:
  "(◻ P) σ = (P \<and> ◯◻P) σ"
  "(♢ P) σ = (P \<or> ◯♢P) σ"
  "(P W Q) σ = (Q \<or> (P \<and> ◯(P W Q))) σ"
  "(P U Q) σ = (Q \<or> (P \<and> ◯(P U Q))) σ"
  "(P R Q) σ = (Q \<and> (P \<or> ◯(P R Q))) σ"
unfolding defs
apply -
apply (metis (full_types) add.commute add_diff_inverse_nat less_one suffix_plus suffix_zero)
apply (metis (full_types) One_nat_def add.right_neutral add_Suc_right lessI less_Suc_eq_0_disj suffix_plus suffix_zero)

apply auto
  apply fastforce
  apply (metis gr0_conv_Suc nat_neq_iff not_less_eq suffix_zero)
  apply (metis suffix_zero)
  apply force
  using less_Suc_eq_0_disj apply fastforce
  apply (metis gr0_conv_Suc nat_neq_iff not_less0 suffix_zero)

  apply fastforce
  apply (case_tac i; auto)
  apply force
  using less_Suc_eq_0_disj apply force

  apply force
  using less_Suc_eq_0_disj apply fastforce
  apply fastforce
  apply (case_tac i; auto)
done

lemma mono:
  "[(◻P) σ; ∧σ. P σ ==> P' σ] ==> (◻P') σ"
  "[(♢P) σ; ∧σ. P σ ==> P' σ] ==> (♢P') σ"
  "[(P U Q) σ; ∧σ. P σ ==> P' σ; ∧σ. Q σ ==> Q' σ] ==> (P' U Q') σ"
  "[(P W Q) σ; ∧σ. P σ ==> P' σ; ∧σ. Q σ ==> Q' σ] ==> (P' W Q') σ"
unfolding defs by force+

lemma always_imp_mono:
  "[(◻P) σ; (P \<hookrightarrow> P') σ] ==> (◻P') σ"
  "[(♢P) σ; (P \<hookrightarrow> P') σ] ==> (♢P') σ"
  "[(P U Q) σ; (P \<hookrightarrow> P') σ; (Q \<hookrightarrow> Q') σ] ==> (P' U Q') σ"
  "[(P W Q) σ; (P \<hookrightarrow> P') σ; (Q \<hookrightarrow> Q') σ] ==> (P' W Q') σ"
unfolding defs by force+

lemma next_conj_distrib:
  "(◯(P \<and> Q)) = (◯P \<and> ◯Q)"
unfolding defs by auto

lemma next_disj_distrib:
  "(◯(P \<or> Q)) = (◯P \<or> ◯Q)"
unfolding defs by auto

lemma until_next_distrib:
  "(◯(P U Q)) = (◯P U ◯Q)"
unfolding defs by (auto simp: fun_eq_iff)

lemma until_imp_eventually:
  "((P U Q) \<longrightarrow> ♢Q) σ"
unfolding defs by auto

lemma until_until_disj:
  assumes "(P U Q U R) σ"
  shows "((P \<or> Q) U R) σ"
using assms unfolding defs
apply clarsimp
apply (metis (full_types) add_diff_inverse_nat nat_add_left_cancel_less)
done

lemma unless_unless_disj:
  assumes "(P W Q W R) σ"
  shows "((P \<or> Q) W R) σ"
using assms unfolding defs
apply auto
 apply (metis add.commute add_diff_inverse_nat leI less_diff_conv2)
apply (metis add_diff_inverse_nat)
done

lemma until_conj_distrib:
  "((P \<and> Q) U R) = ((P U R) \<and> (Q U R))"
unfolding defs
apply (auto simp: fun_eq_iff)
apply (metis dual_order.strict_trans nat_neq_iff)
done

lemma until_disj_distrib:
  "(P U (Q \<or> R)) = ((P U Q) \<or> (P U R))"
unfolding defs by (auto simp: fun_eq_iff)

lemma eventually_until:
  "(♢P) = (\<not>P U P)"
unfolding defs
apply (auto simp: fun_eq_iff)
apply (case_tac "P (x |_s 0)")
 apply blast
apply (drule (1) ex_least_nat_less)
apply (metis le_simps(2))
done

lemma eventually_until_eventually:
  "(♢(P U Q)) = (♢Q)"
unfolding defs by force

lemma eventually_unless_until:
  "((P W Q) \<and> ♢Q) = (P U Q)"
unfolding defs by force

lemma eventually_always_imp_always_eventually:
  assumes "(♢◻P) σ"
  shows "(◻♢P) σ"
using assms unfolding defs by (metis suffix_commute)

lemma eventually_always_next_stable:
  assumes "(♢P) σ"
  assumes "(P \<hookrightarrow> ◯P) σ"
  shows "(♢◻P) σ"
using assms by (metis (no_types) eventuallyI alwaysD always_induct eventuallyE norm(15))

lemma next_stable_imp_eventually_always:
  assumes "(P \<hookrightarrow> ◯P) σ"
  shows "(♢P \<longrightarrow> ♢◻P) σ"
using assms eventually_always_next_stable by blast

lemma always_eventually_always:
  "♢◻♢P = ◻♢P"
unfolding defs by (clarsimp simp: fun_eq_iff) (metis add.left_commute semiring_normalization_rules(25))

(* FIXME define "stable", develop more rules for it *)
lemma stable_unless:
  assumes "(P \<hookrightarrow> ◯(P \<or> Q)) σ"
  shows "(P \<hookrightarrow> (P W Q)) σ"
using assms unfolding defs
apply -
apply (rule ccontr)
apply clarsimp
apply (drule (1) ex_least_nat_less[where P="λj. ¬P (σ |_s i + j)" for i, simplified])
apply clarsimp
apply (metis add_Suc_right le_less less_Suc_eq)
done

lemma unless_induct: ―‹ Rule \texttt{WAIT} from 🚫‹‹Fig~3.3› in "MannaPnueli:1995"››
  assumes I: "(I \<hookrightarrow> ◯(I \<or> R)) σ"
  assumes P: "(P \<hookrightarrow> I \<or> R) σ"
  assumes Q: "(I \<hookrightarrow> Q) σ"
  shows "(P \<hookrightarrow> Q W R) σ"
apply (intro alwaysI impI)
apply (erule impE[OF alwaysD[OF P]])
apply (erule disjE)
 apply (rule always_imp_mono(4)[where P=I and Q=R])
   apply (erule mp[OF alwaysD[OF stable_unless[OF I]]])
  apply (simp add: Q alwaysD)
 apply blast
apply (simp add: unfold)
done


subsection‹ Leads-to and leads-to-via \label{sec:leads-to} ›

text‹

  of our assertions will be of the form @{term "A \⟶ ♢C"} (pronounced ``‹A› leads to ‹C›'')
  @{term "A \⟶ B U C"} (``‹A› leads to ‹C› via ‹B›'').

  of these rules are due to 🚫‹"Jackson:1998"› who used leads-to-via in a sequential setting. Others
  due to 🚫‹"MannaPnueli:1991"›.

  leads-to-via connective is similar to the ``ensures'' modality of 🚫‹‹\S3.4.4› in "ChandyMisra:1989"›.

 ›

abbreviation (input)
  leads_to :: "'a seq_pred → 'a seq_pred → 'a seq_pred" (infixr ‹\↝› 25) where (* FIXME priority *)
  "P \<leadsto> Q ≡ P \<hookrightarrow> ♢Q"

lemma leads_to_refl:
  shows "(P \<leadsto> P) σ"
by (metis (no_types, lifting) necessitation(1) unfold(2))

lemma leads_to_trans:
  assumes "(P \<leadsto> Q) σ"
  assumes "(Q \<leadsto> R) σ"
  shows "(P \<leadsto> R) σ"
using assms unfolding defs by clarsimp (metis semiring_normalization_rules(25))

lemma leads_to_eventuallyE:
  assumes "(P \<leadsto> Q) σ"
  assumes "(♢P) σ"
  shows "(♢Q) σ"
using assms unfolding defs by auto

lemma leads_to_mono:
  assumes "(P' \<hookrightarrow> P) σ"
  assumes "(Q \<hookrightarrow> Q') σ"
  assumes "(P \<leadsto> Q) σ"
  shows "(P' \<leadsto> Q') σ"
using assms unfolding defs by clarsimp blast

lemma leads_to_eventually:
  shows "(P \<leadsto> Q \<longrightarrow> ♢P \<longrightarrow> ♢Q) σ"
by (metis (no_types, lifting) alwaysI unfold(2))

lemma leads_to_disj:
  assumes "(P \<leadsto> R) σ"
  assumes "(Q \<leadsto> R) σ"
  shows "((P \<or> Q) \<leadsto> R) σ"
using assms unfolding defs by simp

lemma leads_to_leads_to_viaE:
  shows "((P \<hookrightarrow> P U Q) \<longrightarrow> P \<leadsto> Q) σ"
unfolding defs by clarsimp blast

lemma leads_to_via_concl_weaken:
  assumes "(R \<hookrightarrow> R') σ"
  assumes "(P \<hookrightarrow> Q U R) σ"
  shows "(P \<hookrightarrow> Q U R') σ"
using assms unfolding LTL.defs by force

lemma leads_to_via_trans:
  assumes "(A \<hookrightarrow> B U C) σ"
  assumes "(C \<hookrightarrow> D U E) σ"
  shows "(A \<hookrightarrow> (B \<or> D) U E) σ"
proof(rule alwaysI, rule impI)
  fix i assume "A (σ |_s i)" with assms show "((B \<or> D) U E) (σ |_s i)"
    apply -
    apply (erule alwaysE[where i=i])
    apply clarsimp
    apply (erule untilE)
    apply clarsimp (* suffix *)
    apply (drule (1) always_imp_mp_suffix)
    apply (erule untilE)
    apply clarsimp (* suffix *)
    apply (rule_tac i="ia + iaa" in untilI; simp add: ac_simps)
    apply (metis (full_types) add.assoc leI le_Suc_ex nat_add_left_cancel_less) (* arithmetic *)
    done
qed

lemma leads_to_via_disj: ― ‹ useful for case distinctions ›
  assumes "(P \<hookrightarrow> Q U R) σ"
  assumes "(P' \<hookrightarrow> Q' U R) σ"
  shows "(P \<or> P' \<hookrightarrow> (Q \<or> Q') U R) σ"
using assms unfolding defs by (auto 10 0)

lemma leads_to_via_disj': ― ‹ more like a chaining rule ›
  assumes "(A \<hookrightarrow> B U C) σ"
  assumes "(C \<hookrightarrow> D U E) σ"
  shows "(A \<or> C \<hookrightarrow> (B \<or> D) U E) σ"
proof(rule alwaysI, rule impI, erule disjE)
  fix i assume "A (σ |_s i)" with assms show "((B \<or> D) U E) (σ |_s i)"
    apply -
    apply (erule alwaysE[where i=i])
    apply clarsimp
    apply (erule untilE)
    apply clarsimp (* suffix *)
    apply (drule (1) always_imp_mp_suffix)
    apply (erule untilE)
    apply clarsimp (* suffix *)
    apply (rule_tac i="ia + iaa" in untilI; simp add: ac_simps)
    apply (metis (full_types) add.assoc leI le_Suc_ex nat_add_left_cancel_less) (* arithmetic *)
    done
next
  fix i assume "C (σ |_s i)" with assms(2) show "((B \<or> D) U E) (σ |_s i)"
    apply -
    apply (erule alwaysE[where i=i])
    apply (simp add: mono)
    done
qed

lemma leads_to_via_stable_augmentation:
  assumes stable: "(P \<and> Q \<hookrightarrow> ◯Q) σ"
  assumes U: "(A \<hookrightarrow> P U C) σ"
  shows "((A \<and> Q) \<hookrightarrow> P U (C \<and> Q)) σ"
proof(intro alwaysI impI, elim conjE)
  fix i assume AP: "A (σ |_s i)" "Q (σ |_s i)"
  have "Q (σ |_s (j + i))" if "Q (σ |_s i)" and "∀k<j. P (σ |_s (k + i))" for j
    using that stable by (induct j; force simp: defs)
  with U AP show "(P U (λσ. C σ ∧ Q σ)) (σ |_s i)"
    unfolding defs by clarsimp (metis (full_types) add.commute)
qed

lemma leads_to_via_wf:
  assumes "wf R"
  assumes indhyp: "∧t. (A \<and> ⌈δ = ⟨t⟩⌉ \<hookrightarrow> B U (A \<and> ⌈δ \<otimes> ⟨t⟩ \<in> ⟨R⟩⌉ \<or> C)) σ"
  shows "(A \<hookrightarrow> B U C) σ"
proof(intro alwaysI impI)
  fix i assume "A (σ |_s i)" with ‹wf R› show "(B U C) (σ |_s i)"
  proof(induct "δ (σ i)" arbitrary: i)
    case (less i) with indhyp[where t="δ (σ i)"] show ?case
      apply -
      apply (drule alwaysD[where i=i])
      apply clarsimp
      apply (erule untilE)
      apply (rename_tac j)
       apply (erule disjE; clarsimp)
       apply (drule_tac x="i + j" in meta_spec; clarsimp)
       apply (erule untilE; clarsimp)
       apply (rename_tac j k)
       apply (rule_tac i="j + k" in untilI)
        apply (simp add: add.assoc)
       apply clarsimp
       apply (metis add.assoc add.commute add_diff_inverse_nat less_diff_conv2 not_le)
      apply auto
      done
  qed
qed

text‹

  well-founded response rule due to 🚫‹‹Fig~1.23: \texttt{WELL} (well-founded response)› in"MannaPnueli:2010"›,
  to an arbitrary set of assertions and sequence predicates.
 ▪ ‹W1› generalised to be contingent.
 ▪ ‹W2› is a well-founded set of assertions that by ‹W1› includes ‹P›

 ›

(* FIXME: Does \<open>Is\<close> need to be consistent? *)
lemma leads_to_wf:
  fixes Is :: "('a seq_pred × ('a → 'b)) set"
  assumes "wf (R :: 'b rel)"
  assumes W1: "(◻(\<exists>φ. ⌈⟨φ∈fst ` Is⟩⌉ \<and> (P \<longrightarrow> φ))) σ"
  assumes W2: "∀(φ, δ)∈Is. ∃(φ', δ')∈insert (Q, δ0) Is. ∀t. (φ \<and> ⌈δ = ⟨t⟩⌉ \<leadsto> φ' \<and> ⌈δ' \<otimes> ⟨t⟩ \<in> ⟨R⟩⌉) σ"
  shows "(P \<leadsto> Q) σ"
proof -
  have "(φ \<and> ⌈δ = ⟨t⟩⌉ \<leadsto> Q) σ" if "(φ, δ) ∈ Is" for φ δ t
    using ‹wf R› that W2
    apply (induct t arbitrary: φ δ)
    unfolding LTL.defs split_def
    apply clarsimp
    apply (metis (no_types, opaque_lifting) ab_semigroup_add_class.add_ac(1) fst_eqD snd_conv surjective_pairing)
    done
  with W1 show ?thesis
    apply -
    apply (rule alwaysI)
    apply clarsimp
    apply (erule_tac i=i in alwaysE)
    apply clarsimp
    using alwaysD suffix_state_prop apply blast
    done
qed


subsection‹Fairness›

text‹

  few renderings of weak fairness. 🚫‹"vanGlabbeekHofner:2019"› call this
 response to insistence" as a generalisation of weak fairness.

 ›

definition weakly_fair :: "'a seq_pred → 'a seq_pred → 'a seq_pred" where
  "weakly_fair enabled taken = (◻enabled \<hookrightarrow> ♢taken)"

lemma weakly_fair_def2:
  shows "weakly_fair enabled taken = ◻(\<not>◻(enabled \<and> \<not>taken))"
unfolding weakly_fair_def by (metis (full_types) always_conj_distrib norm(18))

lemma weakly_fair_def3:
  shows "weakly_fair enabled taken = (♢◻enabled \<longrightarrow> ◻♢taken)"
unfolding weakly_fair_def2
apply (clarsimp simp: fun_eq_iff)

unfolding defs (* True, but can we get there deductively? *)
apply auto
apply (metis (full_types) add.left_commute semiring_normalization_rules(25))
done

lemma weakly_fair_def4:
  shows "weakly_fair enabled taken = ◻♢(enabled \<longrightarrow> taken)"
using weakly_fair_def2 by force

lemma mp_weakly_fair:
  assumes "weakly_fair enabled taken σ"
  assumes "(◻enabled) σ"
  shows "(♢taken) σ"
using assms unfolding weakly_fair_def using always_imp_mp by blast

lemma always_weakly_fair:
  shows "◻(weakly_fair enabled taken) = weakly_fair enabled taken"
unfolding weakly_fair_def by simp

lemma eventually_weakly_fair:
  shows "♢(weakly_fair enabled taken) = weakly_fair enabled taken"
unfolding weakly_fair_def2 by (simp add: always_eventually_always)

lemma weakly_fair_weaken:
  assumes "(enabled' \<hookrightarrow> enabled) σ"
  assumes "(taken \<hookrightarrow> taken') σ"
  shows "(weakly_fair enabled taken \<hookrightarrow> weakly_fair enabled' taken') σ"
using assms unfolding weakly_fair_def defs by simp blast

lemma weakly_fair_unless_until:
  shows "(weakly_fair enabled taken \<and> (enabled \<hookrightarrow> enabled W taken)) = (enabled \<hookrightarrow> enabled U taken)"
unfolding defs weakly_fair_def
apply (auto simp: fun_eq_iff)
apply (metis add.right_neutral)
done

lemma stable_leads_to_eventually:
  assumes "(enabled \<hookrightarrow> ◯(enabled \<or> taken)) σ"
  shows "(enabled \<hookrightarrow> (◻enabled \<or> ♢taken)) σ"
using assms unfolding defs
apply -
apply (rule ccontr)
apply clarsimp
apply (drule (1) ex_least_nat_less[where P="λj. ¬ enabled (σ |_s i + j)" for i, simplified])
apply clarsimp
apply (metis add_Suc_right leI less_irrefl_nat)
done

lemma weakly_fair_stable_leads_to:
  assumes "(weakly_fair enabled taken) σ"
  assumes "(enabled \<hookrightarrow> ◯(enabled \<or> taken)) σ"
  shows "(enabled \<leadsto> taken) σ"
using stable_leads_to_eventually[OF assms(2)] assms(1) unfolding defs weakly_fair_def
by (auto simp: fun_eq_iff)

lemma weakly_fair_stable_leads_to_via:
  assumes "(weakly_fair enabled taken) σ"
  assumes "(enabled \<hookrightarrow> ◯(enabled \<or> taken)) σ"
  shows "(enabled \<hookrightarrow> enabled U taken) σ"
using stable_unless[OF assms(2)] assms(1) by (metis (mono_tags) weakly_fair_unless_until)

text‹

  for strong fairness. 🚫‹"vanGlabbeekHofner:2019"› call this
 response to persistence" as a generalisation of strong fairness.

 ›

definition strongly_fair :: "'a seq_pred → 'a seq_pred → 'a seq_pred" where
  "strongly_fair enabled taken = (◻♢enabled \<hookrightarrow> ♢taken)"

lemma strongly_fair_def2:
  "strongly_fair enabled taken = ◻(\<not>◻(♢enabled \<and> \<not>taken))"
unfolding strongly_fair_def by (metis weakly_fair_def weakly_fair_def2)

lemma strongly_fair_def3:
  "strongly_fair enabled taken = (◻♢enabled \<longrightarrow> ◻♢taken)"
unfolding strongly_fair_def2 by (metis (full_types) always_eventually_always weakly_fair_def2 weakly_fair_def3)

lemma always_strongly_fair:
  "◻(strongly_fair enabled taken) = strongly_fair enabled taken"
unfolding strongly_fair_def by simp

lemma eventually_strongly_fair:
  "♢(strongly_fair enabled taken) = strongly_fair enabled taken"
unfolding strongly_fair_def2 by (simp add: always_eventually_always)

lemma strongly_fair_disj_distrib: ― ‹not true for ‹weakly_fair››
  "strongly_fair (enabled1 \<or> enabled2) taken = (strongly_fair enabled1 taken \<and> strongly_fair enabled2 taken)"
unfolding strongly_fair_def defs
apply (auto simp: fun_eq_iff)
  apply blast
  apply blast
  apply (metis (full_types) semiring_normalization_rules(25))
done

lemma strongly_fair_imp_weakly_fair:
  assumes "strongly_fair enabled taken σ"
  shows "weakly_fair enabled taken σ"
using assms unfolding strongly_fair_def3 weakly_fair_def3 by (simp add: eventually_always_imp_always_eventually)

lemma always_enabled_weakly_fair_strongly_fair:
  assumes "(◻enabled) σ"
  shows "weakly_fair enabled taken σ = strongly_fair enabled taken σ"
using assms by (metis strongly_fair_def3 strongly_fair_imp_weakly_fair unfold(2) weakly_fair_def3)


subsection‹Safety and liveness \label{sec:ltl-safety-liveness}›

text‹

 🚫‹"Sistla:1994"› shows some characterisations
  LTL formulas in terms of safety and liveness. Note his @{term
 (U)"} is actually @{term "(W)"}.

  also 🚫‹"ChangMannaPnueli:1992"›.

 ›

lemma safety_state_prop:
  shows "safety ⌈P⌉"
unfolding defs by (rule safety_state_prop)

lemma safety_Next:
  assumes "safety P"
  shows "safety (◯P)"
using assms unfolding defs safety_def
apply clarsimp
apply (metis (mono_tags) One_nat_def list.sel(3) nat.simps(3) stake.simps(2))
done

lemma safety_unless:
  assumes "safety P"
  assumes "safety Q"
  shows "safety (P W Q)"
proof(rule safetyI2)
  fix σ assume X: "∃β. (P W Q) (stake i σ @- β)" for i
  then show "(P W Q) σ"
  proof(cases "∀i j. ∃β. P (σ(i → j) @- β)")
    case True
    with ‹safety P› have "∀i. P (σ |_s i)" unfolding safety_def2 by blast
    then show ?thesis by (blast intro: unless_alwaysI)
  next
    case False
    then obtain k k' where "∀β. ¬ P (σ(k → k') @- β)" by clarsimp
    then have "∀i u. k + k' ≤ i ⟶ ¬P ((stake i σ @- u) |_s k)"
      by (metis add.commute diff_add stake_shift_stake_shift stake_suffix_drop suffix_shift)
    then have "∀i u. k + k' ≤ i ∧ (P W Q) (stake i σ @- u) ⟶ (∃m≤k. Q ((stake i σ @- u) |_s m) ∧ (∀p<m. P ((stake i σ @- u) |_s p)))"
      unfolding defs using leI by blast
    then have "∀i u. k + k' ≤ i ∧ (P W Q) (stake i σ @- u) ⟶ (∃m≤k. Q (σ(m → i - m) @- u) ∧ (∀p<m. P (σ(p → i - p) @- u)))"
      by (metis stake_suffix add_leE nat_less_le order_trans)
    then have "∀i. ∃n≥i. ∃m≤k. ∃u. Q (σ(m → n - m) @- u) ∧ (∀p<m. P (σ(p → n - p) @- u))"
      using X by (metis add.commute le_add1)
    then have "∃m≤k. ∀i. ∃n≥i. ∃u. Q (σ(m → n - m) @- u) ∧ (∀p<m. P (σ(p → n - p) @- u))"
      by (simp add: always_eventually_pigeonhole)
    with ‹safety P› ‹safety Q› show "(P W Q) σ"
        unfolding defs by (metis Nat.le_diff_conv2 add_leE safety_always_eventually)
  qed
qed

lemma safety_always:
  assumes "safety P"
  shows "safety (◻P)"
using assms by (metis norm(20) safety_def safety_unless)

lemma absolute_liveness_eventually:
  shows "absolute_liveness P ⟷ (∃σ. P σ) ∧ P = ♢P"
unfolding absolute_liveness_def defs
by (metis cancel_comm_monoid_add_class.diff_cancel drop_eq_Nil order_refl shift.simps(1) stake_suffix_id suffix_shift suffix_zero)

lemma stable_always:
  shows "stable P ⟷ (∃σ. P σ) ∧ P = ◻P"
unfolding stable_def defs by (metis suffix_zero)

(* FIXME Sistla's examples of stable properties are boring and follow directly from this lemma.
   FIXME the fairness "type of formulas" follow from the above and the fairness def. *)

text‹

  show that @{const ‹weakly_fair›} is a @{const ‹fairness›} property requires some constraints on ‹enabled› and ‹taken›:
 ▪ it is reasonable to assume they are state formulas
 ▪ ‹taken› must be satisfiable

 ›

lemma fairness_weakly_fair:
  assumes "∃s. taken s"
  shows "fairness (weakly_fair ⌈enabled⌉ ⌈taken⌉)"
unfolding fairness_def stable_def absolute_liveness_def weakly_fair_def
using assms
apply auto
   apply (rule_tac x="λ_ .s" in exI)
   apply fastforce
  apply (simp add: alwaysD)
 apply (rule_tac x="λ_ .s" in exI)
 apply fastforce
apply (metis (full_types) absolute_liveness_def absolute_liveness_eventually eventually_weakly_fair weakly_fair_def)
done

lemma fairness_strongly_fair:
  assumes "∃s. taken s"
  shows "fairness (strongly_fair ⌈enabled⌉# SDX-License-Identifier: GPL-2.0-onl
unfolding fairness_def stable_def absolute_liveness_def strongly_fair_def
using assms
apply auto
   apply (rule_tac x="λ_ .s" in exI)
   apply fastforce
  apply (simp add: alwaysD)
 apply (rule_tac x="λ_ .s" in exI)
 apply fastforce
apply (metis (full_types) absolute_liveness_def absolute_liveness_eventually eventually_weakly_fair weakly_fair_def)
done

(*<*)

end
(*>*)