Theory LTL

(*<*)
theory LTL
imports
  CIMP_pred
  Infinite_Sequences
begin

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

text‹

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

The following is a straightforward shallow embedding of the
now-traditional anchored semantics of LTL \<^cite>‹"MannaPnueli:1988"›. Some of it is adapted
from the sophisticated TLA development in the AFP due to \<^citet>‹"TLA-AFP"›.

Unlike \<^citet>‹"Lamport:2002"›, include the
next operator, which is convenient for stating rules. Sometimes it allows us to
ignore 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 ‹𝒰› 30) where (* FIXME priority, binds tighter than ❙⟶ *)
  "(P 𝒰 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⟩ 𝒰 P)"

definition release :: "'a seq_pred ⇒ 'a seq_pred ⇒ 'a seq_pred" (infixr ‹ℛ› 30) where (* FIXME priority, dual of Until *)
  "(P ℛ Q) = (❙¬(❙¬P 𝒰 ❙¬Q))"

definition unless :: "'a seq_pred ⇒ 'a seq_pred ⇒ 'a seq_pred" (infixr ‹𝒲› 30) where (* FIXME priority, aka weak until *)
  "(P 𝒲 Q) = ((P 𝒰 Q) ❙∨ □P)"

abbreviation (input)
  pred_always_imp_syn :: "'a seq_pred ⇒ 'a seq_pred ⇒ 'a seq_pred" (infixr ‹❙↪› 25) where
  "P ❙↪ Q ≡ □(P ❙⟶ 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 ❙⟶ ○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 𝒰 Q) (f ∘ σ) ⟷ ((λσ. P (f ∘ σ)) 𝒰 (λσ. Q (f ∘ σ))) σ"
    "(P 𝒲 Q) (f ∘ σ) ⟷ ((λσ. P (f ∘ σ)) 𝒲 (λσ. 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 𝒰 Q) σ"
unfolding defs using assms by blast

lemma untilE:
  assumes "(P 𝒰 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 𝒲 Q) σ"
using assms unfolding defs by blast

lemma unless_untilI:
  assumes "Q (σ |⇩s j)"
  assumes "⋀i. i < j ⟹ P (σ |⇩s i)"
  shows "(P 𝒲 Q) σ"
unfolding defs using assms by blast

lemma always_imp_refl[iff]:
  shows "(P ❙↪ P) σ"
unfolding defs by blast

lemma always_imp_trans:
  assumes "(P ❙↪ Q) σ"
  assumes "(Q ❙↪ R) σ"
  shows "(P ❙↪ R) σ"
using assms unfolding defs by blast

lemma always_imp_mp:
  assumes "(P ❙↪ Q) σ"
  assumes "P σ"
  shows "Q σ"
using assms unfolding defs by (metis suffix_zero)

lemma always_imp_mp_suffix:
  assumes "(P ❙↪ Q) σ"
  assumes "P (σ |⇩s i)"
  shows "Q (σ |⇩s i)"
using assms unfolding defs by metis

text‹

Some basic facts and equivalences, mostly sanity.

›

lemma necessitation:
  "(⋀s. P s) ⟹ (□P) σ"
  "(⋀s. P s) ⟹ (◇P) σ"
  "(⋀s. P s) ⟹ (P 𝒲 Q) σ"
  "(⋀s. Q s) ⟹ (P 𝒰 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 𝒰 Q) = (P' 𝒰 Q')"
  "⟦⋀σ. P σ = P' σ; ⋀σ. Q σ = Q' σ⟧ ⟹ (P 𝒲 Q) = (P' 𝒲 Q')"
unfolding defs by auto

lemma norm[simp]:
  "⌈⟨False⟩⌉ = ⟨False⟩"
  "⌈⟨True⟩⌉ = ⟨True⟩"
  "(❙¬⌈p⌉) = ⌈❙¬p⌉"
  "(⌈p⌉ ❙∧ ⌈q⌉) = ⌈p ❙∧ q⌉"
  "(⌈p⌉ ❙∨ ⌈q⌉) = ⌈p ❙∨ q⌉"
  "(⌈p⌉ ❙⟶ ⌈q⌉) = ⌈p ❙⟶ q⌉"
  "(⌈p⌉ σ ∧ ⌈q⌉ σ) = ⌈p ❙∧ q⌉ σ"
  "(⌈p⌉ σ ∨ ⌈q⌉ σ) = ⌈p ❙∨ q⌉ σ"
  "(⌈p⌉ σ ⟶ ⌈q⌉ σ) = ⌈p ❙⟶ q⌉ σ"

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

  "(□⟨False⟩) = ⟨False⟩"
  "(□⟨True⟩) = ⟨True⟩"
  "(❙¬□ P) σ = (◇ (❙¬ P)) σ"
  "(□□ P) = (□ P)"

  "(◇⟨False⟩) = ⟨False⟩"
  "(◇⟨True⟩) = ⟨True⟩"
  "(❙¬◇ P) = (□ (❙¬ P))"
  "(◇◇ P) = (◇ P)"

  "(P 𝒲 ⟨False⟩) = (□ P)"

  "(❙¬(P 𝒰 Q)) σ = (❙¬P ℛ ❙¬Q) σ"
  "(⟨False⟩ 𝒰 P) = P"
  "(P 𝒰 ⟨False⟩) = ⟨False⟩"
  "(P 𝒰 ⟨True⟩) = ⟨True⟩"
  "(⟨True⟩ 𝒰 P) = (◇ P)"
  "(P 𝒰 (P 𝒰 Q)) = (P 𝒰 Q)"

  "(❙¬(P ℛ Q)) σ = (❙¬P 𝒰 ❙¬Q) σ"
  "(⟨False⟩ ℛ P) = (□P)"
  "(P ℛ ⟨False⟩) = ⟨False⟩"
  "(⟨True⟩ ℛ P) = P"
  "(P ℛ ⟨True⟩) = ⟨True⟩"
(*
  "(P 𝒰 (P 𝒰 Q)) σ = (P 𝒰 Q) σ" 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 ❙∧ Q)) = (□P ❙∧ □Q)"
unfolding defs by auto

lemma eventually_disj_distrib: "(◇(P ❙∨ Q)) = (◇P ❙∨ ◇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 ❙⟶ Q)) = (◇(❙¬P) ❙∨ ◇Q)"
unfolding defs by auto

lemma eventually_imp_distrib:
  "(◇(P ❙⟶ Q)) = (□P ❙⟶ ◇Q)"
unfolding defs by auto

lemma unfold:
  "(□ P) σ = (P ❙∧ ○□P) σ"
  "(◇ P) σ = (P ❙∨ ○◇P) σ"
  "(P 𝒲 Q) σ = (Q ❙∨ (P ❙∧ ○(P 𝒲 Q))) σ"
  "(P 𝒰 Q) σ = (Q ❙∨ (P ❙∧ ○(P 𝒰 Q))) σ"
  "(P ℛ Q) σ = (Q ❙∧ (P ❙∨ ○(P ℛ 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 𝒰 Q) σ; ⋀σ. P σ ⟹ P' σ; ⋀σ. Q σ ⟹ Q' σ⟧ ⟹ (P' 𝒰 Q') σ"
  "⟦(P 𝒲 Q) σ; ⋀σ. P σ ⟹ P' σ; ⋀σ. Q σ ⟹ Q' σ⟧ ⟹ (P' 𝒲 Q') σ"
unfolding defs by force+

lemma always_imp_mono:
  "⟦(□P) σ; (P ❙↪ P') σ⟧ ⟹ (□P') σ"
  "⟦(◇P) σ; (P ❙↪ P') σ⟧ ⟹ (◇P') σ"
  "⟦(P 𝒰 Q) σ; (P ❙↪ P') σ; (Q ❙↪ Q') σ⟧ ⟹ (P' 𝒰 Q') σ"
  "⟦(P 𝒲 Q) σ; (P ❙↪ P') σ; (Q ❙↪ Q') σ⟧ ⟹ (P' 𝒲 Q') σ"
unfolding defs by force+

lemma next_conj_distrib:
  "(○(P ❙∧ Q)) = (○P ❙∧ ○Q)"
unfolding defs by auto

lemma next_disj_distrib:
  "(○(P ❙∨ Q)) = (○P ❙∨ ○Q)"
unfolding defs by auto

lemma until_next_distrib:
  "(○(P 𝒰 Q)) = (○P 𝒰 ○Q)"
unfolding defs by (auto simp: fun_eq_iff)

lemma until_imp_eventually:
  "((P 𝒰 Q) ❙⟶ ◇Q) σ"
unfolding defs by auto

lemma until_until_disj:
  assumes "(P 𝒰 Q 𝒰 R) σ"
  shows "((P ❙∨ Q) 𝒰 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 𝒲 Q 𝒲 R) σ"
  shows "((P ❙∨ Q) 𝒲 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 ❙∧ Q) 𝒰 R) = ((P 𝒰 R) ❙∧ (Q 𝒰 R))"
unfolding defs
apply (auto simp: fun_eq_iff)
apply (metis dual_order.strict_trans nat_neq_iff)
done

lemma until_disj_distrib:
  "(P 𝒰 (Q ❙∨ R)) = ((P 𝒰 Q) ❙∨ (P 𝒰 R))"
unfolding defs by (auto simp: fun_eq_iff)

lemma eventually_until:
  "(◇P) = (❙¬P 𝒰 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 𝒰 Q)) = (◇Q)"
unfolding defs by force

lemma eventually_unless_until:
  "((P 𝒲 Q) ❙∧ ◇Q) = (P 𝒰 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 ❙↪ ○P) σ"
  shows "(◇□P) σ"
using assms by (metis (no_types) eventuallyI alwaysD always_induct eventuallyE norm(15))

lemma next_stable_imp_eventually_always:
  assumes "(P ❙↪ ○P) σ"
  shows "(◇P ❙⟶ ◇□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 ❙↪ ○(P ❙∨ Q)) σ"
  shows "(P ❙↪ (P 𝒲 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 \<^citet>‹‹Fig~3.3› in "MannaPnueli:1995"››
  assumes I: "(I ❙↪ ○(I ❙∨ R)) σ"
  assumes P: "(P ❙↪ I ❙∨ R) σ"
  assumes Q: "(I ❙↪ Q) σ"
  shows "(P ❙↪ Q 𝒲 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‹

Most of our assertions will be of the form @{term "A ❙⟶ ◇C"} (pronounced ``‹A› leads to ‹C›'')
or @{term "A ❙⟶ B 𝒰 C"} (``‹A› leads to ‹C› via ‹B›'').

Most of these rules are due to \<^citet>‹"Jackson:1998"› who used leads-to-via in a sequential setting. Others
are due to \<^citet>‹"MannaPnueli:1991"›.

The leads-to-via connective is similar to the ``ensures'' modality of \<^citet>‹‹\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 ❙↝ Q ≡ P ❙↪ ◇Q"

lemma leads_to_refl:
  shows "(P ❙↝ P) σ"
by (metis (no_types, lifting) necessitation(1) unfold(2))

lemma leads_to_trans:
  assumes "(P ❙↝ Q) σ"
  assumes "(Q ❙↝ R) σ"
  shows "(P ❙↝ R) σ"
using assms unfolding defs by clarsimp (metis semiring_normalization_rules(25))

lemma leads_to_eventuallyE:
  assumes "(P ❙↝ Q) σ"
  assumes "(◇P) σ"
  shows "(◇Q) σ"
using assms unfolding defs by auto

lemma leads_to_mono:
  assumes "(P' ❙↪ P) σ"
  assumes "(Q ❙↪ Q') σ"
  assumes "(P ❙↝ Q) σ"
  shows "(P' ❙↝ Q') σ"
using assms unfolding defs by clarsimp blast

lemma leads_to_eventually:
  shows "(P ❙↝ Q ❙⟶ ◇P ❙⟶ ◇Q) σ"
by (metis (no_types, lifting) alwaysI unfold(2))

lemma leads_to_disj:
  assumes "(P ❙↝ R) σ"
  assumes "(Q ❙↝ R) σ"
  shows "((P ❙∨ Q) ❙↝ R) σ"
using assms unfolding defs by simp

lemma leads_to_leads_to_viaE:
  shows "((P ❙↪ P 𝒰 Q) ❙⟶ P ❙↝ Q) σ"
unfolding defs by clarsimp blast

lemma leads_to_via_concl_weaken:
  assumes "(R ❙↪ R') σ"
  assumes "(P ❙↪ Q 𝒰 R) σ"
  shows "(P ❙↪ Q 𝒰 R') σ"
using assms unfolding LTL.defs by force

lemma leads_to_via_trans:
  assumes "(A ❙↪ B 𝒰 C) σ"
  assumes "(C ❙↪ D 𝒰 E) σ"
  shows "(A ❙↪ (B ❙∨ D) 𝒰 E) σ"
proof(rule alwaysI, rule impI)
  fix i assume "A (σ |⇩s i)" with assms show "((B ❙∨ D) 𝒰 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 ❙↪ Q 𝒰 R) σ"
  assumes "(P' ❙↪ Q' 𝒰 R) σ"
  shows "(P ❙∨ P' ❙↪ (Q ❙∨ Q') 𝒰 R) σ"
using assms unfolding defs by (auto 10 0)

lemma leads_to_via_disj': ― ‹ more like a chaining rule ›
  assumes "(A ❙↪ B 𝒰 C) σ"
  assumes "(C ❙↪ D 𝒰 E) σ"
  shows "(A ❙∨ C ❙↪ (B ❙∨ D) 𝒰 E) σ"
proof(rule alwaysI, rule impI, erule disjE)
  fix i assume "A (σ |⇩s i)" with assms show "((B ❙∨ D) 𝒰 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 ❙∨ D) 𝒰 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 ❙∧ Q ❙↪ ○Q) σ"
  assumes U: "(A ❙↪ P 𝒰 C) σ"
  shows "((A ❙∧ Q) ❙↪ P 𝒰 (C ❙∧ 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 𝒰 (λσ. 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 ❙∧ ⌈δ ❙= ⟨t⟩⌉ ❙↪ B 𝒰 (A ❙∧ ⌈δ ❙⊗ ⟨t⟩ ❙∈ ⟨R⟩⌉ ❙∨ C)) σ"
  shows "(A ❙↪ B 𝒰 C) σ"
proof(intro alwaysI impI)
  fix i assume "A (σ |⇩s i)" with ‹wf R› show "(B 𝒰 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‹

The well-founded response rule due to \<^citet>‹‹Fig~1.23: \texttt{WELL} (well-founded response)› in"MannaPnueli:2010"›,
generalised 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 ‹Is› need to be consistent? *)
lemma leads_to_wf:
  fixes Is :: "('a seq_pred × ('a ⇒ 'b)) set"
  assumes "wf (R :: 'b rel)"
  assumes W1: "(□(❙∃φ. ⌈⟨φ∈fst ` Is⟩⌉ ❙∧ (P ❙⟶ φ))) σ"
  assumes W2: "∀(φ, δ)∈Is. ∃(φ', δ')∈insert (Q, δ0) Is. ∀t. (φ ❙∧ ⌈δ ❙= ⟨t⟩⌉ ❙↝ φ' ❙∧ ⌈δ' ❙⊗ ⟨t⟩ ❙∈ ⟨R⟩⌉) σ"
  shows "(P ❙↝ Q) σ"
proof -
  have "(φ ❙∧ ⌈δ ❙= ⟨t⟩⌉ ❙↝ 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‹

A few renderings of weak fairness. \<^citet>‹"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 ❙↪ ◇taken)"

lemma weakly_fair_def2:
  shows "weakly_fair enabled taken = □(❙¬□(enabled ❙∧ ❙¬taken))"
unfolding weakly_fair_def by (metis (full_types) always_conj_distrib norm(18))

lemma weakly_fair_def3:
  shows "weakly_fair enabled taken = (◇□enabled ❙⟶ □◇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 ❙⟶ 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' ❙↪ enabled) σ"
  assumes "(taken ❙↪ taken') σ"
  shows "(weakly_fair enabled taken ❙↪  weakly_fair enabled' taken') σ"
using assms unfolding weakly_fair_def defs by simp blast

lemma weakly_fair_unless_until:
  shows "(weakly_fair enabled taken ❙∧ (enabled ❙↪ enabled 𝒲 taken)) = (enabled ❙↪ enabled 𝒰 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 ❙↪ ○(enabled ❙∨ taken)) σ"
  shows "(enabled ❙↪ (□enabled ❙∨ ◇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 ❙↪ ○(enabled ❙∨ taken)) σ"
  shows "(enabled ❙↝ 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 ❙↪ ○(enabled ❙∨ taken)) σ"
  shows "(enabled ❙↪ enabled 𝒰 taken) σ"
using stable_unless[OF assms(2)] assms(1) by (metis (mono_tags) weakly_fair_unless_until)

text‹

Similarly for strong fairness. \<^citet>‹"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 ❙↪ ◇taken)"

lemma strongly_fair_def2:
  "strongly_fair enabled taken = □(❙¬□(◇enabled ❙∧ ❙¬taken))"
unfolding strongly_fair_def by (metis weakly_fair_def weakly_fair_def2)

lemma strongly_fair_def3:
  "strongly_fair enabled taken = (□◇enabled ❙⟶ □◇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 ❙∨ enabled2) taken = (strongly_fair enabled1 taken ❙∧ 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‹

\<^citet>‹"Sistla:1994"› shows some characterisations
of LTL formulas in terms of safety and liveness. Note his @{term
"(𝒰)"} is actually @{term "(𝒲)"}.

See also \<^citet>‹"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 𝒲 Q)"
proof(rule safetyI2)
  fix σ assume X: "∃β. (P 𝒲 Q) (stake i σ @- β)" for i
  then show "(P 𝒲 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 𝒲 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 𝒲 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 𝒲 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‹

To 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⌉ ⌈taken⌉)"
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
(*>*)