Theory TLS

(*<*)
theory TLS
imports
  "Safety_Logic"
begin

(*>*)
section‹ A Temporal Logic of Safety (TLS) \label{sec:tls} ›

text‹

We model systems with finite and infinite sequences of states, closed
under stuttering following citet‹"Lamport:1994"›. This theory relates
the safety logic of \S\ref{sec:safety_logic} to the powerset
(quotiented by stuttering) representing properties of these sequences
(see \S\ref{sec:tls-safety}). Most of this story is standard but the
addition of finite sequences does have some impact.

References:
 ▪ historical motivations for future-time linear temporal logic (LTL): citet‹"MannaPnueli:1991" and "OwickiLamport:1982"›.
 ▪ a discussion on the merits of proving liveness: 🌐‹https://cs.nyu.edu/acsys/beyond-safety/liveness.htm›

Observations:
 ▪ Lamport (and Abadi et al) treat infinite stuttering as termination
  ▪ citet‹‹p189› in "Lamport:1999"›: ``we can represent a terminating execution of any system by an
   infinite behavior that ends with a sequence of nothing but stuttering steps. We have no need of
   finite behaviors (finite sequences of states), so we consider only infinite ones.''
  ▪ this conflates divergence with termination
  ▪ we separate those concepts here so we can support sequential composition
 ▪ the traditional account of liveness properties breaks down (see \S\ref{sec:safety_closure})

›


subsection‹ Stuttering\label{sec:tls-stuttering} ›

text‹

An infinitary version of const‹trace.natural'›.

Observations:
 ▪ we need to normalize the agent labels for sequences that infinitely stutter

Source materials:
 ▪ 🗏‹$ISABELLE_HOME/src/HOL/Corec_Examples/LFilter.thy›.
 ▪ 🗏‹$AFP/Coinductive/Coinductive_List.thy›
 ▪ 🗏‹$AFP/Coinductive/TLList.thy›
 ▪ 🗏‹$AFP/TLA/Sequence.thy›.

›

definition trailing :: "'c ⇒ ('a, 'b) tllist ⇒ ('c, 'b) tllist" where
  "trailing s xs = (if tfinite xs then TNil (terminal xs) else trepeat s)"

corecursive collapse :: "'s ⇒ ('a × 's, 'v) tllist ⇒ ('a × 's, 'v) tllist" where
  "collapse s xs = (if snd ` tset xs ⊆ {s} then trailing (undefined, s) xs
               else if snd (thd xs) = s then collapse s (ttl xs)
               else TCons (thd xs) (collapse (snd (thd xs)) (ttl xs)))"
proof -
  have "(LEAST i. s ≠ snd (tnth (ttl xs) i)) < (LEAST i. s ≠ snd (tnth xs i))"
    if *: "¬ snd ` tset xs ⊆ {s}"
   and **: "snd (thd xs) = s"
   for s and xs :: "('a × 's, 'v) tllist"
  proof -
    from * obtain a s' where "(a, s') ∈ tset xs" and "s ≠ s'" by fastforce
    then obtain i where "snd (tnth xs i) ≠ s"
      by (atomize_elim, induct rule: tset_induct) (auto intro: exI[of _ 0] exI[of _ "Suc i" for i])
    with * ** have "(LEAST i. s ≠ snd (tnth xs i)) = Suc (LEAST i. s ≠ snd (tnth xs (Suc i)))"
      by (cases xs) (simp_all add: Least_Suc[where n=i])
    with * show "(LEAST i. s ≠ snd (tnth (ttl xs) i)) < (LEAST i. s ≠ snd (tnth xs i))"
      by (cases xs) simp_all
  qed
  then show ?thesis
    by (relation "measure (λ(s, xs). LEAST i. s ≠ snd (tnth xs i))"; simp)
qed

setup ‹Sign.mandatory_path "tmap"›

lemma trailing:
  shows "tmap sf vf (trailing s xs) = trailing (sf s) (tmap sf vf xs)"
by (simp add: trailing_def tmap_trepeat)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "tlength"›

lemma trailing:
  shows "tlength (trailing s xs) ≤ tlength xs"
by (fastforce simp: trailing_def dest: not_lfinite_llength)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "trailing"›

lemma simps[simp]:
  shows TNil: "trailing s (TNil b) = TNil b"
    and TCons: "trailing s (TCons x xs) = trailing s xs"
    and ttl: "ttl (trailing s xs) = trailing s xs"
    and idempotent: "trailing s (trailing s xs) = trailing s xs"
    and tset_finite: "tset (trailing s xs) = (if tfinite xs then {} else {s})"
    and trepeat: "trailing s (trepeat s) = trepeat s"
by (simp_all add: trailing_def)

lemma eq_TNil_conv:
  shows "trailing s xs = TNil b ⟷ tfinite xs ∧ terminal xs = b"
    and "TNil b = trailing s xs ⟷ tfinite xs ∧ terminal xs = b"
    and "is_TNil (trailing s xs) ⟷ tfinite xs"
by (auto simp: trailing_def dest: is_TNil_tfinite)

lemma eq_TCons_conv:
  shows "trailing s xs = TCons y ys ⟷ ¬tfinite xs ∧ TCons y ys = trepeat s"
    and "TCons y ys = trailing s xs ⟷ ¬tfinite xs ∧ TCons y ys = trepeat s"
by (auto simp: trailing_def)

lemma tmap:
  shows "trailing s (tmap sf vf xs) = tmap id vf (trailing s xs)"
by (simp add: trailing_def tmap_trepeat)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "collapse"›

lemma unique:
  assumes "⋀s xs. f s xs = (if snd ` tset xs ⊆ {s} then trailing (undefined, s) xs
                      else if snd (thd xs) = s then f s (ttl xs)
                      else TCons (thd xs) (f (snd (thd xs)) (ttl xs)))"
  shows "f = collapse"
proof(intro ext)
  show "f s xs = collapse s xs" for s xs
  proof(coinduction arbitrary: s xs)
    case (Eq_tllist s xs) show ?case
      apply (induct arg≡"(s, xs)" arbitrary: s xs rule: collapse.inner_induct)
      apply (subst (1 2 3) assms)
      apply (subst (1 2 3) collapse.code)
      apply simp
      apply (subst (1 2 3) assms)
      apply (subst (1 2 3) collapse.code)
      apply simp
      apply (metis assms collapse.code)
      done
  qed
qed

lemma collapse:
  shows "collapse s (collapse s xs) = collapse s xs"
proof -
  have "(λs xs. collapse s (collapse s xs)) = collapse"
    apply (rule collapse.unique)
    apply (subst (1 2 3) collapse.code)
    apply auto
    done
  then show ?thesis
    by (fastforce simp: fun_eq_iff)
qed

lemma simps[simp]:
  shows TNil: "collapse s (TNil b) = TNil b"
    and TCons: "collapse s (TCons x xs) = (if snd x = s then collapse s xs else TCons x (collapse (snd x) xs))"
    and trailing: "collapse s (trailing (undefined, s) xs) = trailing (undefined, s) xs"
by (simp_all add: collapse.code trailing_def)

lemma tshift_stuttering:
  assumes "snd ` set xs ⊆ {s}"
  shows "collapse s (tshift xs ys) = collapse s ys"
using assms by (induct xs) simp_all

lemma infinite_trailing:
  assumes "¬tfinite xs"
  assumes "snd ` tset xs ⊆ {s'}"
  shows "collapse s xs = (if s = s' then trepeat (undefined, s') else TCons (thd xs) (trepeat (undefined, s')))"
using assms by (cases xs) (simp_all add: assms collapse.code trailing_def)

lemma eq_TNil_conv:
  shows "collapse s xs = TNil b ⟷ tfinite xs ∧ snd ` tset xs ⊆ {s} ∧ terminal xs = b" (is "?lhs ⟷ ?rhs")
    and "TNil b = collapse s xs ⟷ tfinite xs ∧ snd ` tset xs ⊆ {s} ∧ terminal xs = b" (is "?thesis1")
proof -
  show "?lhs ⟷ ?rhs"
  proof(rule iffI)
    show "?lhs ⟹ ?rhs"
    proof(induct arg≡"(s, xs)" arbitrary: s xs rule: collapse.inner_induct[case_names step])
      case (step s xs) then show ?case
        by (cases xs; clarsimp split: if_splits)
           (subst (asm) collapse.code; clarsimp simp: trailing.eq_TNil_conv split: if_splits)
    qed
    show "?rhs ⟹ ?lhs"
      by (simp add: conj_explode) (induct arbitrary: s rule: tfinite_induct; simp)
  qed
  then show ?thesis1
    by (rule eq_commute_conv)
qed

lemma is_TNil_conv:
  shows "is_TNil (collapse s xs) ⟷ tfinite xs ∧ snd ` tset xs ⊆ {s}" (is "?thesis2")
by (simp add: is_TNil_def collapse.eq_TNil_conv)

lemma eq_TConsE:
  assumes "collapse s xs = TCons y ys"
  obtains
    (trailing_stuttering) "¬ tfinite xs"
                      and "snd ` tset xs = {s}"
                      and "TCons y ys = trepeat (undefined, s)"
  | (step) us ys' where "xs = tshift us (TCons y ys')"
                    and "snd ` set us ⊆ {s}"
                    and "snd y ≠ s"
                    and "collapse (snd y) ys' = ys"
apply atomize_elim
using assms
proof(induct arg≡"(s, xs)" arbitrary: s xs rule: collapse.inner_induct[case_names step])
  case (step s xs) show ?case
  proof(cases xs)
    case (TNil v) with step.prems show ?thesis by simp
  next
    case (TCons x xs') show ?thesis
    proof(cases "snd ` tset xs' ⊆ {snd x}")
      case True with TCons trans[OF collapse.code[symmetric] step.prems] show ?thesis
        by (force simp: trailing.eq_TCons_conv tshift_eq_TCons_conv split: if_split_asm)
    next
      case False with TCons trans[OF collapse.code[symmetric] step.prems] step.hyps[OF refl]
      show ?thesis
        by (cases x, cases y)
           (simp add: trailing.eq_TCons_conv tshift_eq_TCons_conv trepeat_eq_TCons_conv
                      eq_snd_iff exI[where x="[]"]
               split: if_split_asm; safe; force dest!: spec[where x="(fst x, s) # us" for us])
    qed
  qed
qed

lemma eq_TCons_conv:
  shows "collapse s xs = TCons y ys
     ⟷ (¬tfinite xs ∧ snd ` tset xs = {s} ∧ TCons y ys = trepeat (undefined, s))
       ∨ (∃xs' ys'. xs = tshift xs' (TCons y ys') ∧ snd ` set xs' ⊆ {s} ∧ snd y ≠ s ∧ collapse (snd y) ys' = ys)" (is "?lhs ⟷ ?rhs")
    and "TCons y ys = collapse s xs
     ⟷ (¬tfinite xs ∧ snd ` tset xs = {s} ∧ TCons y ys = trepeat (undefined, s))
       ∨ (∃xs' ys'. xs = tshift xs' (TCons y ys') ∧ snd ` set xs' ⊆ {s} ∧ snd y ≠ s ∧ collapse (snd y) ys' = ys)" (is ?thesis1)
proof -
  show "?lhs ⟷ ?rhs"
    by (auto elim: collapse.eq_TConsE simp: collapse.tshift_stuttering collapse.infinite_trailing)
  then show ?thesis1
    by (rule eq_commute_conv)
qed

lemma tfinite:
  shows "tfinite (collapse s xs) ⟷ tfinite xs" (is "?lhs ⟷ ?rhs")
proof(rule iffI)
  show ?lhs if ?rhs
    using that by (induct arbitrary: s rule: tfinite_induct) simp_all
  show ?rhs if ?lhs
    using that by (induct "collapse s xs" arbitrary: s xs rule: tfinite_induct)
                  (auto simp: collapse.eq_TNil_conv collapse.eq_TCons_conv trepeat_eq_TCons_conv)
qed

lemma tfinite_conv:
  assumes "collapse s xs = collapse s' xs'"
  shows "tfinite xs ⟷ tfinite xs'"
by (metis assms collapse.tfinite)

lemma terminal:
  shows "terminal (collapse s xs) = terminal xs"
proof(cases "tfinite xs")
  case True
  then obtain i where "tlength xs ≤ enat i"
    using llength_eq_infty_conv_lfinite by fastforce
  then show ?thesis
  proof(induct i arbitrary: s xs)
    case (Suc i s xs) then show ?case
      by (cases xs) (simp_all flip: eSuc_enat)
  qed (clarsimp simp: enat_0 tlength_0_conv)
qed (simp add: collapse.tfinite terminal_tinfinite)

lemma tlength:
  shows "tlength (collapse s xs) ≤ tlength xs"
proof(cases "tfinite xs")
  case True then show ?thesis
    by (induct arbitrary: s rule: tfinite_induct) (auto intro: order.trans[OF _ ile_eSuc])
next
  case False then show ?thesis
    by (fastforce dest: not_lfinite_llength)
qed

lemma tset_memberD:
  assumes "(a, s') ∈ tset (collapse s xs)"
  shows "s' ∈ snd ` tset xs"
using assms
by (induct "collapse s xs" arbitrary: s xs rule: tset_induct)
   (auto simp: collapse.eq_TCons_conv trepeat_eq_TCons_conv tset_tshift image_Un)

lemma tset_memberD2:
  assumes "(a, s') ∈ tset xs"
  shows "s = s' ∨ s' ∈ snd ` tset (collapse s xs)"
using assms by (induct xs arbitrary: a s rule: tset_induct; simp; fast)

lemma tshift:
  shows "collapse s (tshift xs ys) = tshift (trace.natural' s xs) (collapse (trace.final' s xs) ys)"
by (induct xs arbitrary: s) simp_all

lemma trepeat:
  shows "collapse s (trepeat (a, s)) = trepeat (undefined, s)"
by (subst collapse.code) (simp add: trailing_def)

lemma eq_trepeat_conv:
  shows "trepeat (undefined, s) = collapse s xs ⟷ ¬tfinite xs ∧ snd ` tset xs = {s}" (is "?thesis1")
    and "collapse s xs = trepeat (undefined, s) ⟷ ¬tfinite xs ∧ snd ` tset xs = {s}" (is "?thesis2")
proof -
  show ?thesis1
    by (rule iffI,
        (subst (asm) trepeat_unfold, simp add: collapse.eq_TCons_conv),
        simp add: collapse.infinite_trailing)
  then show ?thesis2
    by (rule eq_commute_conv)
qed

lemma treplicate:
  shows "collapse s (treplicate i (a, s) v) = TNil v"
by (subst collapse.code) (simp add: trailing.eq_TNil_conv split: nat.split)

lemma eq_tshift_conv:
  shows "collapse s xs = tshift ys zs
     ⟷ (∃xs' xs'' ys'. tshift xs' xs'' = xs ∧ trace.natural' s xs' @ ys' = ys
          ∧ ((¬tfinite xs'' ∧ snd ` tset xs'' = {trace.final' s xs'} ∧ tshift ys' zs = trepeat (undefined, trace.final' s xs'))
            ∨ (ys' = [] ∧ collapse (trace.final' s xs') xs'' = zs)))" (is "?lhs ⟷ ?rhs")
    and "tshift ys zs = collapse s xs
     ⟷ (∃xs' xs'' ys'. tshift xs' xs'' = xs ∧ trace.natural' s xs' @ ys' = ys
          ∧ ((¬tfinite xs'' ∧ snd ` tset xs'' = {trace.final' s xs'} ∧ tshift ys' zs = trepeat (undefined, trace.final' s xs'))
            ∨ (ys' = [] ∧ collapse (trace.final' s xs') xs'' = zs)))" (is ?thesis1)
proof -
  show "?lhs ⟷ ?rhs"
  proof(rule iffI)
    show "?lhs ⟹ ?rhs"
    proof(induct ys arbitrary: s xs)
      case Nil then show ?case
        by (simp add: exI[where x="[]"])
    next
      case (Cons y ys s xs)
      from Cons.prems[simplified] show ?case
      proof(cases rule: collapse.eq_TConsE)
        case trailing_stuttering then show ?thesis
          by (simp add: exI[where x="[]"])
      next
        case (step xs' ys')
        from step(1-3) Cons.hyps[OF step(4)] show ?thesis
          by (fastforce simp: trace.natural'.append tshift_append
                   simp flip: trace.natural'.eq_Nil_conv
                       intro: exI[where x="xs' @ y # ys''" for ys''])
      qed
    qed
    show "?rhs ⟹ ?lhs"
      by (auto simp: collapse.tshift tshift_append collapse.infinite_trailing)
  qed
  then show ?thesis1
    by (rule eq_commute_conv)
qed

lemma eq_collapse_ttake_dropn_conv:
  shows "collapse s xs = collapse s ys
     ⟷ (∃j. trace.natural' s (fst (ttake i xs)) = trace.natural' s (fst (ttake j ys))
            ∧ snd (ttake i xs) = snd (ttake j ys)
            ∧ collapse (trace.final' s (fst (ttake i xs))) (tdropn i xs)
            = collapse (trace.final' s (fst (ttake i xs))) (tdropn j ys))" (is "?lhs ⟷ (∃j. ?rhs i j s xs ys)")
proof(rule iffI)
  show "?lhs ⟹ (∃j. ?rhs i j s xs ys)"
  proof(induct i arbitrary: s xs ys)
    case (Suc i s xs ys) show ?case
    proof(cases xs)
      case (TNil b) with Suc.prems show ?thesis
        by (fastforce intro: exI[where x="case tlength ys of ∞ ⇒ undefined | enat j ⇒ Suc j"]
                       simp: collapse.eq_TNil_conv trace.natural'.eq_Nil_conv
                             ttake_eq_Some_conv tfinite_tlength_conv tdropn_tlength
                       dest: in_set_ttakeD)
    next
      case (TCons x xs') show ?thesis
      proof(cases "snd x = s")
        case True with Suc TCons show ?thesis by simp
      next
        case False
        note Suc.prems TCons False
        moreover from calculation
        obtain us ys'
          where "ys = tshift us (TCons x ys')"
            and "snd ` set us ⊆ {s}"
            and "collapse (snd x) ys' = collapse (snd x) xs'"
          by (auto simp: collapse.eq_TCons_conv trepeat_eq_TCons_conv)
        moreover from calculation Suc.hyps[of "snd x" "xs'" "ys'"]
        obtain j where "?rhs i j (snd x) xs' ys'"
          by presburger
        ultimately show ?thesis
          by (auto simp: ttake_tshift trace.natural'.append tdropn_tshift
              simp flip: trace.natural'.eq_Nil_conv
                  intro: exI[where x="Suc (length us) + j"])
      qed
    qed
  qed (simp add: exI[where x=0])
  show "∃j. ?rhs i j s xs ys ⟹ ?lhs"
    by (metis collapse.tshift trace.final'.natural' tshift_fst_ttake_tdropn_id)
qed

lemmas eq_collapse_ttake_dropnE = exE[OF iffD1[OF collapse.eq_collapse_ttake_dropn_conv]]

lemma tshift_tdropn:
  assumes "trace.natural' s (fst (ttake i xs)) = trace.natural' s ys"
  shows "collapse s (tshift ys (tdropn i xs)) = collapse s xs"
by (metis assms collapse.tshift trace.final'.natural' tshift_fst_ttake_tdropn_id)

lemma map_collapse:
  shows "collapse (sf s) (tmap (map_prod af sf) vf (collapse s xs))
       = collapse (sf s) (tmap (map_prod af sf) vf xs)" (is "?lhs s xs = ?rhs s xs")
proof(coinduction arbitrary: s xs)
  case (Eq_tllist s xs) show ?case
  proof(intro conjI; (intro impI)?)
    have *: "sf s' = sf s"
      if "tfinite xs" and "sf ` snd ` tset (collapse s xs) ⊆ {sf s}" and "(a, s') ∈ tset xs"
    for a s s'
      using that by (induct arbitrary: s rule: tfinite_induct; clarsimp split: if_split_asm; metis)
    show "is_TNil (?lhs s xs) ⟷ is_TNil (?rhs s xs)"
      by (rule iffI,
          fastforce dest!: * simp: collapse.is_TNil_conv collapse.tfinite tllist.set_map snd_image_map_prod,
          fastforce dest!: collapse.tset_memberD simp: collapse.is_TNil_conv collapse.tfinite tllist.set_map)
    show "terminal (?lhs s xs) = terminal (?rhs s xs)"
      if "is_TNil (?lhs s xs)" and "is_TNil (?rhs s xs)"
      using that by (simp add: collapse.is_TNil_conv collapse.terminal)
    assume "¬is_TNil (?lhs s xs)" and "¬is_TNil (?rhs s xs)"
    then obtain y ys z zs where l: "?lhs s xs = TCons y ys" and r: "?rhs s xs = TCons z zs"
      by (simp add: tllist.disc_eq_case(2) split: tllist.split_asm)
    from l show "thd (?lhs s xs) = thd (?rhs s xs)
              ∧ (∃s' xs'. ttl (?lhs s xs) = ?lhs s' xs' ∧ ttl (?rhs s xs) = ?rhs s' xs')"
    proof(cases rule: collapse.eq_TConsE)
      case trailing_stuttering
      note left = this
      from r show ?thesis
      proof(cases rule: collapse.eq_TConsE)
        case trailing_stuttering
        from left(3) trailing_stuttering(3) show ?thesis
          by (fold l r) (simp; metis)
      next
        case (step us zs')
        from left(2) step(1,3) have False
          by (clarsimp simp: tset_tshift tset_tmap tmap_eq_tshift_conv TCons_eq_tmap_conv collapse.tshift
                      split: if_split_asm)
             (use step(2) in ‹fastforce simp flip: trace.final'.map[where af=af]›)
        then show ?thesis ..
      qed
    next
      case (step us ys')
      note left = this
      from r show ?thesis
      proof(cases rule: collapse.eq_TConsE)
        case trailing_stuttering
        have False
          if "sf s' ≠ sf s"
         and "(λx. sf (snd x)) ` tset xs = {sf s}"
         and "(λx. sf (snd x)) ` set us ⊆ {sf s}"
         and "collapse s xs = tshift us (TCons (a, s') vs)"
         for a s' us vs
          using that
          by (force simp: tset_tshift
                   dest!: arg_cong[where f="λxs. s' ∈ snd ` tset xs"] collapse.tset_memberD
                   intro: imageI[where f="λx. sf (snd x)"])
        with l left(3) trailing_stuttering(2) have False
          by (fastforce simp: tset_tmap tmap_eq_tshift_conv TCons_eq_tmap_conv collapse.eq_TCons_conv
                              trepeat_eq_TCons_conv snd_image_map_prod image_image)
        then show ?thesis ..
      next
        case (step vs zs')
        from left step show ?thesis
          unfolding l r
          apply (clarsimp simp: tmap_eq_tshift_conv collapse.tshift TCons_eq_tmap_conv
                                tmap_tshift trace.natural'.map_natural'[where af=af and sf=sf and s=s]
                                iffD2[OF trace.natural'.eq_Nil_conv(1)]
                         dest!: arg_cong[where f="λxs. collapse (sf s) (tmap (map_prod af sf) vf xs)"]
                         split: if_split_asm)
            apply (use step(2) in ‹fastforce simp flip: trace.final'.map[where af=af]›)
           apply (metis list.set_map trace.final'.idle trace.final'.map trace.final'.natural')
          apply metis
          done
      qed
    qed
  qed
qed

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "behavior"›

definition natural :: "('a, 's, 'v) behavior.t ⇒ ('a, 's, 'v) behavior.t" ("♮T") where
  "♮Tω = behavior.B (behavior.init ω) (collapse (behavior.init ω) (behavior.rest ω))"

setup ‹Sign.mandatory_path "sset"›

lemma collapse[simp]:
  shows "behavior.sset (behavior.B s (collapse s xs)) = behavior.sset (behavior.B s xs)"
by (auto simp: behavior.sset.simps collapse.tset_memberD dest: collapse.tset_memberD2[where s=s])

lemma natural[simp]:
  shows "behavior.sset (♮Tω) = behavior.sset ω"
by (simp add: behavior.natural_def)

lemma continue:
  shows "behavior.sset (σ @-B xs) = trace.sset σ ∪ (case trace.term σ of None ⇒ snd ` tset xs | Some _ ⇒ {})"
by (cases σ)
   (simp add: behavior.sset.simps behavior.continue_def tshift2_def tset_tshift image_Un trace.sset.simps
       split: option.split)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "natural"›

lemma sel[simp]:
  shows "behavior.init (♮Tω) = behavior.init ω"
    and "behavior.rest (♮Tω) = collapse (behavior.init ω) (behavior.rest ω)"
by (simp_all add: behavior.natural_def)

lemma TNil:
  shows "♮T(behavior.B s (TNil v)) = behavior.B s (TNil v)"
by (simp add: behavior.natural_def)

lemma tfinite:
  shows "tfinite (behavior.rest (♮T ω)) ⟷ tfinite (behavior.rest ω)"
by (simp add: behavior.natural_def collapse.tfinite)

lemma continue:
  shows "♮T(σ @-B xs) = ♮σ @-B (collapse (trace.final σ) xs)"
by (simp add: behavior.t.expand tshift2_def collapse.tshift split: option.split)

lemma tshift:
  shows "♮T(behavior.B s (tshift as xs)) = behavior.B s (collapse s (tshift as xs))"
by (simp add: behavior.natural_def)

lemma trepeat:
  shows "♮T(behavior.B s (trepeat (a, s))) = behavior.B s (trepeat (undefined, s))"
by (simp add: behavior.natural_def collapse.trepeat)

lemma treplicate:
  shows "♮T(behavior.B s (treplicate i (a, s) v)) = behavior.B s (TNil v)"
by (simp add: behavior.natural_def collapse.treplicate)

lemma map_natural:
  shows "♮T(behavior.map af sf vf (♮Tω)) = ♮T(behavior.map af sf vf ω)"
by (simp add: behavior.natural_def collapse.map_collapse)

lemma idle:
  assumes "behavior.sset ω ⊆ {behavior.init ω}"
  shows "♮Tω = behavior.B (behavior.init ω) (trailing (undefined, behavior.init ω) (behavior.rest ω))"
using assms by (cases ω) (simp add: behavior.natural_def behavior.sset.simps collapse.code)

setup ‹Sign.parent_path›

interpretation stuttering: galois.image_vimage_idempotent "♮T"
by standard (simp add: behavior.natural_def collapse.collapse)

setup ‹Sign.mandatory_path "stuttering"›

setup ‹Sign.mandatory_path "equiv"›

abbreviation syn :: "('a, 's, 'v) behavior.t ⇒ ('a, 's, 'v) behavior.t ⇒ bool" (infix "≃T" 50) where
  "ω1 ≃T ω2 ≡ behavior.stuttering.equivalent ω1 ω2"

lemma map:
  assumes "ω1 ≃T ω2"
  shows "behavior.map af sf vf ω1 ≃T behavior.map af sf vf ω2"
by (metis assms behavior.natural.map_natural)

lemma takeE:
  assumes "ω1 ≃T ω2"
  obtains j where "behavior.take i ω1 ≃S behavior.take j ω2"
using assms
by (fastforce simp: behavior.natural_def trace.natural_def
              elim: collapse.eq_collapse_ttake_dropnE[where s="behavior.init ω2" and i=i and xs="behavior.rest ω1" and ys="behavior.rest ω2"])

lemma idle_dropn:
  assumes "behavior.dropn i ω = Some ω'"
  assumes "behavior.sset ω ⊆ {behavior.init ω}"
  shows "ω ≃T ω'"
proof -
  from behavior.sset.dropn_le[OF assms(1)] assms(2)
  have "behavior.sset ω' ⊆ {behavior.init ω'}" and "behavior.init ω' = behavior.init ω"
    using behavior.t.set_sel(2) subset_singletonD by fastforce+
  from assms(1) behavior.natural.idle[OF assms(2)] behavior.natural.idle[OF this(1)] this(2)
  show ?thesis
    by (simp add: trailing_def)
       (metis  behavior.dropn.tfiniteD behavior.dropn.eq_Some_tdropnD terminal_tdropn)
qed

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "trace.stuttering.equiv.behavior"›

lemma takeE:
  fixes σ :: "('a, 's, 'v) trace.t"
  assumes "behavior.take i ω ≃S σ"
  obtains ω' j where "ω ≃T ω'" and "σ = behavior.take j ω'"
proof atomize_elim
  have "∃ys j. collapse s xs = collapse s ys ∧ trace.T s xs' (snd (ttake i xs)) = behavior.take j (behavior.B s ys)"
    if "trace.natural' s (fst (ttake i xs)) = trace.natural' s xs'"
   for s xs' and xs :: "('a × 's, 'v) tllist"
    using that
    by (cases "snd (ttake i xs)")
       (fastforce simp: behavior.take.tshift ttake_eq_Some_conv tdropn_tlength
                        trace.take.all trace.take.all_iff
                 intro: exI[where x="tshift xs' (tdropn i xs)"]
                        exI[where x="length xs'"] exI[where x="Suc (length xs')"]
                  dest: collapse.tshift_tdropn)+
  with assms show "∃ω' j. ω ≃T ω' ∧ σ = behavior.take j ω'"
    by (cases σ)
       (clarsimp simp: behavior.natural_def trace.natural_def behavior.split_Ex)
qed

lemmas rev_takeE = trace.stuttering.equiv.behavior.takeE[OF sym]

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "trace.natural.behavior"›

lemma takeE:
  fixes ω :: "('a, 's, 'v) behavior.t"
  obtains j where "♮(behavior.take i ω) = behavior.take j (♮Tω)"
proof atomize_elim
  have "∃j. trace.natural' s (fst (ttake i xs)) = fst (ttake j (collapse s xs))
          ∧ snd (ttake i xs) = snd (ttake j (collapse s xs))"
   for s and xs :: "('a × 's, 'v) tllist"
  proof(induct i arbitrary: s xs)
    case 0 show ?case by (fastforce simp: ttake_eq_Nil_conv)
  next
    case (Suc i s xs) show ?case
    proof(cases xs)
      case (TCons x' xs') with Suc[where s="snd x'" and xs=xs'] show ?thesis
        by (fastforce intro: exI[where x="Suc j" for j])
    qed (simp add: exI[where x=1])
  qed
  then show "∃j. ♮ (behavior.take i ω) = behavior.take j (♮T ω)"
    by (simp add: behavior.take_def trace.natural_def split_def)
qed

setup ‹Sign.parent_path›


subsection‹ The ∗‹('a, 's, 'v) tls› lattice \label{sec:tls-tls} ›

text‹

This is our version of Lamport's TLA lattice which we treat in a ``semantic'' way similarly to
citet‹"AbadiMerz:1996"›.

Observations:
 ▪ there is a somewhat natural partial ordering on the ‹tls› lattice induced by the connection with
   the ‹spec› lattice (see \S\ref{sec:tls-safety} and \S\ref{sec:safety_closure}) which we do not use

›

typedef ('a, 's, 'v) tls = "behavior.stuttering.closed :: ('a, 's, 'v) behavior.t set set"
morphisms unTLS TLS
by blast

setup_lifting type_definition_tls

instantiation tls :: (type, type, type) complete_boolean_algebra
begin

lift_definition bot_tls :: "('a, 's, 'v) tls" is empty ..
lift_definition top_tls :: "('a, 's, 'v) tls" is UNIV ..
lift_definition sup_tls :: "('a, 's, 'v) tls ⇒ ('a, 's, 'v) tls ⇒ ('a, 's, 'v) tls" is sup ..
lift_definition inf_tls :: "('a, 's, 'v) tls ⇒ ('a, 's, 'v) tls ⇒ ('a, 's, 'v) tls" is inf ..
lift_definition less_eq_tls :: "('a, 's, 'v) tls ⇒ ('a, 's, 'v) tls ⇒ bool" is less_eq .
lift_definition less_tls :: "('a, 's, 'v) tls ⇒ ('a, 's, 'v) tls ⇒ bool" is less .
lift_definition Inf_tls :: "('a, 's, 'v) tls set ⇒ ('a, 's, 'v) tls" is Inf ..
lift_definition Sup_tls :: "('a, 's, 'v) tls set ⇒ ('a, 's, 'v) tls" is "λX. Sup X ⊔ behavior.stuttering.cl {}" ..
lift_definition minus_tls :: "('a, 's, 'v) tls ⇒ ('a, 's, 'v) tls ⇒ ('a, 's, 'v) tls" is minus ..
lift_definition uminus_tls :: "('a, 's, 'v) tls ⇒ ('a, 's, 'v) tls" is uminus ..

instance
by (standard; transfer;
    auto simp: behavior.stuttering.cl_bot
               behavior.stuttering.closed_strict_complete_distrib_lattice_axiomI[OF behavior.stuttering.cl_bot])

end

declare
  SUPE[where 'a="('a, 's, 'v) tls", intro!]
  SupE[where 'a="('a, 's, 'v) tls", intro!]
  Sup_le_iff[where 'a="('a, 's, 'v) tls", simp]
  SupI[where 'a="('a, 's, 'v) tls", intro]
  SUPI[where 'a="('a, 's, 'v) tls", intro]
  rev_SUPI[where 'a="('a, 's, 'v) tls", intro?]
  INFE[where 'a="('a, 's, 'v) tls", intro]

setup ‹Sign.mandatory_path "tls"›

lemma boolean_implication_transfer[transfer_rule]:
  shows "rel_fun (pcr_tls (=) (=) (=)) (rel_fun (pcr_tls (=) (=) (=)) (pcr_tls (=) (=) (=))) (⟶B) (⟶B)"
unfolding boolean_implication_def by transfer_prover

lemma bot_not_top:
  shows "⊥ ≠ (⊤ :: ('a, 's, 'v) tls)"
by transfer simp

setup ‹Sign.parent_path›


subsection‹ Irreducible elements\label{sec:tls-singleton} ›

setup ‹Sign.mandatory_path "raw"›

definition singleton :: "('a, 's, 'v) behavior.t ⇒ ('a, 's, 'v) behavior.t set" where
  "singleton ω = behavior.stuttering.cl {ω}"

lemma singleton_le_conv:
  shows "raw.singleton σ1 ≤ raw.singleton σ2 ⟷ ♮Tσ1 = ♮Tσ2"
by (rule iffI; fastforce simp: raw.singleton_def simp flip: behavior.stuttering.cl_axiom
                         dest: behavior.stuttering.clE behavior.stuttering.equiv_cl_singleton)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "tls"›

lift_definition singleton :: "('a, 's, 'v) behavior.t ⇒ ('a, 's, 'v) tls" ("⦉_⦊T" [0]) is raw.singleton
by (simp add: raw.singleton_def)

abbreviation singleton_behavior_syn :: "'s ⇒ ('a × 's, 'v) tllist ⇒ ('a, 's, 'v) tls" ("⦉_, _⦊T" [0, 0]) where
  "⦉s, xs⦊T ≡ ⦉behavior.B s xs⦊T"

setup ‹Sign.mandatory_path "singleton"›

lemma Sup_prime:
  shows "Sup_prime ⦉ω⦊T"
by (clarsimp simp: Sup_prime_on_def)
   (transfer; auto simp: raw.singleton_def behavior.stuttering.cl_bot
                  elim!: Sup_prime_onE[OF behavior.stuttering.Sup_prime_on_singleton])

lemma nchotomy:
  shows "∃X∈behavior.stuttering.closed. x = ⨆(tls.singleton ` X)"
by transfer
   (use behavior.stuttering.closed_conv in ‹auto simp add: raw.singleton_def
                                                simp flip: behavior.stuttering.distributive›)

lemmas exhaust = bexE[OF tls.singleton.nchotomy]

lemma collapse[simp]:
  shows "⨆(tls.singleton ` {ω. ⦉ω⦊T ≤ P}) = P"
by (rule tls.singleton.exhaust[of P]) (simp add: antisym SUP_le_iff SUP_upper)

lemmas not_bot = Sup_prime_not_bot[OF tls.singleton.Sup_prime] ―‹ Non-triviality ›

setup ‹Sign.parent_path›

lemma singleton_le_ext_conv:
  shows "P ≤ Q ⟷ (∀ω. ⦉ω⦊T ≤ P ⟶ ⦉ω⦊T ≤ Q)" (is "?lhs ⟷ ?rhs")
proof(rule iffI)
  show "?rhs ⟹ ?lhs"
    by (rule tls.singleton.exhaust[where x=P]; rule tls.singleton.exhaust[where x=Q]; blast)
qed fastforce

lemmas singleton_le_conv = raw.singleton_le_conv[transferred]
lemmas singleton_le_extI = iffD2[OF tls.singleton_le_ext_conv, rule_format]

lemma singleton_eq_conv[simp]:
  shows "⦉ω⦊T = ⦉ω'⦊T ⟷ ω ≃T ω'"
using tls.singleton_le_conv by (force intro: antisym)

lemma singleton_cong:
  assumes "ω ≃T ω'"
  shows "⦉ω⦊T = ⦉ω'⦊T"
using assms by simp

setup ‹Sign.mandatory_path "singleton"›

named_theorems le_conv ‹ simplification rules for ‹⦉σ⦊T ≤ const …› ›

lemma boolean_implication_le_conv[tls.singleton.le_conv]:
  shows "⦉σ⦊T ≤ P ⟶B Q ⟷ (⦉σ⦊T ≤ P ⟶ ⦉σ⦊T ≤ Q)"
by transfer
   (auto simp: raw.singleton_def boolean_implication.set_alt_def
        elim!: behavior.stuttering.clE behavior.stuttering.closed_in[OF _ sym])

lemmas antisym = antisym[OF tls.singleton_le_extI tls.singleton_le_extI]

lemmas top = tls.singleton.collapse[of ⊤, simplified, symmetric]

lemma simps[simp]:
  shows "⦉♮Tω⦊T = ⦉ω⦊T"
    and "⦉s, xs⦊T ≤ ⦉s, collapse s xs⦊T"
    and "snd ` set ys ⊆ {s} ⟹ ⦉s, tshift ys xs⦊T = ⦉s, xs⦊T"
    and "⦉s, TCons (a, s) xs⦊T = ⦉s, xs⦊T"
by (simp_all add: antisym tls.singleton_le_conv behavior.natural_def
                  behavior.stuttering.f_idempotent collapse.collapse collapse.tshift_stuttering)

lemmas Sup_irreducible = iffD1[OF heyting.Sup_prime_Sup_irreducible_iff tls.singleton.Sup_prime]
lemmas sup_irreducible = Sup_irreducible_on_imp_sup_irreducible_on[OF tls.singleton.Sup_irreducible, simplified]
lemmas Sup_leE[elim] = Sup_prime_onE[OF tls.singleton.Sup_prime, simplified]
lemmas sup_le_conv[simp] = sup_irreducible_le_conv[OF tls.singleton.sup_irreducible]
lemmas Sup_le_conv[simp] = Sup_prime_on_conv[OF tls.singleton.Sup_prime, simplified]
lemmas compact_point = Sup_prime_is_compact[OF tls.singleton.Sup_prime]
lemmas compact[cont_intro] = compact_points_are_ccpo_compact[OF tls.singleton.compact_point]

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›


subsection‹ The idle process\label{sec:tls-idle} ›

text‹

The idle process contains no transitions and does not terminate.

›

setup ‹Sign.mandatory_path "raw"›

definition idle :: "('a, 's, 'v) behavior.t set" where
  "idle = (⋃s. raw.singleton (behavior.B s (trepeat (undefined, s))))"

lemma idle_alt_def:
  shows "raw.idle = {ω. ¬tfinite (behavior.rest ω) ∧ behavior.sset ω ⊆ {behavior.init ω}}" (is "?lhs = ?rhs")
proof(rule antisym[OF _ subsetI])
  show "?lhs ⊆ ?rhs"
    by (force simp: raw.idle_def raw.singleton_def behavior.split_all behavior.natural_def
                    behavior.sset.simps collapse.trepeat collapse.eq_trepeat_conv
              elim: behavior.stuttering.clE
              dest: collapse.tfinite_conv)
  show "ω ∈ ?lhs" if "ω ∈ ?rhs" for ω
    using that
    by (cases ω)
       (auto simp: raw.idle_def raw.singleton_def behavior.natural_def behavior.sset.simps
                   behavior.stuttering.idemI collapse.infinite_trailing
             elim: behavior.stuttering.clE
            intro: exI[where x="behavior.init ω"])
qed

setup ‹Sign.mandatory_path "idle"›

lemma not_tfinite:
  assumes "ω ∈ raw.idle"
  shows "¬tfinite (behavior.rest ω)"
using assms by (simp add: raw.idle_alt_def)

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "behavior.stuttering.closed"›

lemma idle[iff]:
  shows "raw.idle ∈ behavior.stuttering.closed"
by (simp add: raw.idle_def raw.singleton_def
              behavior.stuttering.closed_UNION[simplified behavior.stuttering.cl_bot, simplified])

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "tls"›

lift_definition idle :: "('a, 's, 'v) tls" is raw.idle ..

lemma idle_alt_def:
  shows "tls.idle = (⨆s. ⦉s, trepeat (undefined, s)⦊T)"
by transfer (simp add: raw.idle_def behavior.stuttering.cl_bot)

setup ‹Sign.mandatory_path "singleton"›

lemma idle_le_conv[tls.singleton.le_conv]:
  shows "⦉ω⦊T ≤ tls.idle ⟷ ¬tfinite (behavior.rest ω) ∧ behavior.sset ω ⊆ {behavior.init ω}"
by transfer (simp add: raw.singleton_def behavior.stuttering.least_conv; simp add: raw.idle_alt_def)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "idle"›

lemma minimal_le:
  shows "⦉s, trepeat (undefined, s)⦊T ≤ tls.idle"
by (simp add: tls.singleton.idle_le_conv behavior.sset.simps)

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›


subsection‹ Temporal Logic for ∗‹('a, 's, 'v) tls› \label{sec:tls-ltl} ›

text‹

The following is a straightforward shallow embedding of the
now-traditional anchored semantics of LTL citet‹"MannaPnueli:1988"›.

References:
 ▪ 🗏‹$AFP/TLA/Liveness.thy›
 ▪ 🗏‹$ISABELLE_HOME/src/HOL/TLA/TLA.thy›
 ▪ 🌐‹https://en.wikipedia.org/wiki/Linear_temporal_logic›
 ▪ citet‹"KroegerMerz:2008"›
 ▪ citet‹"WarfordVegaStaley:2020"›

Observations:
 ▪ as we lack next/X/‹○› (due to stuttering closure) we do not have induction for ‹𝒰› (until)
 ▪ citet‹"Lamport:1994"› omitted the LTL ``until'' operator from TLA as he considered it too hard to use
 ▪ As citet‹"DeGiacomoVardi:2013"› observe, things get non-standard on finite traces
  ▪ see \S\ref{sec:safety_closure} for an example
  ▪ citet‹"Maier:2004"› provides an alternative account

›

setup ‹Sign.mandatory_path "raw"›

definition state_prop :: "'s pred ⇒ ('a, 's, 'v) behavior.t set" where
  "state_prop P = {ω. P (behavior.init ω)}"

definition
  until :: "('a, 's, 'v) behavior.t set ⇒ ('a, 's, 'v) behavior.t set ⇒ ('a, 's, 'v) behavior.t set"
where
  "until P Q = {ω . ∃i. ∃ω'∈Q. behavior.dropn i ω = Some ω' ∧ (∀j<i. the (behavior.dropn j ω) ∈ P)}"

definition
  eventually :: "('a, 's, 'v) behavior.t set ⇒ ('a, 's, 'v) behavior.t set"
where
  "eventually P = raw.until UNIV P"

definition
  always :: "('a, 's, 'v) behavior.t set ⇒ ('a, 's, 'v) behavior.t set"
where
  "always P = -raw.eventually (-P)"

abbreviation (input) "unless P Q ≡ raw.until P Q ∪ raw.always P"

definition terminated :: "('a, 's, 'v) behavior.t set" where
  "terminated = {ω. tfinite (behavior.rest ω) ∧ behavior.sset ω ⊆ {behavior.init ω}}"

lemma untilI:
  assumes "behavior.dropn i ω = Some ω'"
  assumes "ω' ∈ Q"
  assumes "⋀j. j < i ⟹ the (behavior.dropn j ω) ∈ P"
  shows "ω ∈ raw.until P Q"
using assms unfolding raw.until_def by blast

lemma eventually_alt_def:
  shows "raw.eventually P = {ω . ∃ω'∈P. ∃i. behavior.dropn i ω = Some ω'}"
by (auto simp: raw.eventually_def raw.until_def)

lemma always_alt_def:
  shows "raw.always P = {ω . ∀i ω'. behavior.dropn i ω = Some ω' ⟶ ω' ∈ P}"
by (auto simp: raw.always_def raw.eventually_alt_def)

lemma alwaysI:
  assumes "⋀i ω'. behavior.dropn i ω = Some ω' ⟹ ω' ∈ P"
  shows "ω ∈ raw.always P"
by (simp add: raw.always_alt_def assms)

lemma alwaysD:
  assumes "ω ∈ raw.always P"
  assumes "behavior.dropn i ω = Some ω'"
  shows "ω' ∈ P"
using assms by (simp add: raw.always_alt_def)

setup ‹Sign.mandatory_path "state_prop"›

lemma monotone:
  shows "mono raw.state_prop"
by (fastforce intro: monoI simp: raw.state_prop_def)

lemma simps:
  shows
    "raw.state_prop ⟨False⟩ = {}"
    "raw.state_prop ⊥ = {}"
    "raw.state_prop ⟨True⟩ = UNIV"
    "raw.state_prop ⊤ = UNIV"
    "- raw.state_prop P = raw.state_prop (- P)"
    "raw.state_prop P ∪ raw.state_prop Q = raw.state_prop (P ⊔ Q)"
    "raw.state_prop P ∩ raw.state_prop Q = raw.state_prop (P ⊓ Q)"
    "(raw.state_prop P ⟶B raw.state_prop Q) = raw.state_prop (P ⟶B Q)"
by (auto simp: raw.state_prop_def boolean_implication.set_alt_def)

lemma Inf:
  shows "raw.state_prop (⨅X) = ⋂(raw.state_prop ` X)"
by (fastforce simp: raw.state_prop_def)

lemma Sup:
  shows "raw.state_prop (⨆X) = ⋃(raw.state_prop ` X)"
by (fastforce simp: raw.state_prop_def)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "terminated"›

lemma inf_always_le:
  fixes P :: "('a, 's, 'v) behavior.t set"
  assumes "P ∈ behavior.stuttering.closed"
  shows "raw.terminated ∩ P ⊆ raw.always P"
by (rule subsetI[OF raw.alwaysI])
   (auto simp: raw.terminated_def
         elim: behavior.stuttering.closed_in[OF _ _ assms] behavior.stuttering.equiv.idle_dropn)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "until"›

lemma base:
  shows "ω ∈ Q ⟹ ω ∈ raw.until P Q"
    and "Q ⊆ raw.until P Q"
by (force simp: raw.until_def)+

lemma step:
  assumes "ω ∈ P"
  assumes "behavior.tl ω = Some ω'"
  assumes "ω' ∈ raw.until P Q"
  shows "ω ∈ raw.until P Q"
proof -
  from ‹ω' ∈ raw.until P Q›
  obtain i ω''
    where "ω'' ∈ Q" and "∀j<i. the (behavior.dropn j ω') ∈ P" and "behavior.dropn i ω' = Some ω''"
    by (clarsimp simp: raw.until_def)
  with assms(1,2) show ?thesis
    by (clarsimp simp: raw.until_def behavior.dropn.Suc less_Suc_eq_0_disj
               intro!: exI[where x="Suc i"])
qed

lemmas intro[intro] =
  raw.until.base
  raw.until.step

lemma induct[case_names base step, consumes 1, induct set: raw.until]:
  assumes "ω ∈ raw.until P Q"
  assumes base: "⋀ω. ω ∈ Q ⟹ R ω"
  assumes step: "⋀ω ω'. ⟦ω ∈ P; behavior.tl ω = Some ω'; ω' ∈ raw.until P Q; R ω'⟧ ⟹ R ω"
  shows "R ω"
proof -
  from ‹ω ∈ raw.until P Q› obtain ω' i
    where "behavior.dropn i ω = Some ω'" and "ω' ∈ Q" and "∀j<i. the (behavior.dropn j ω) ∈ P"
    unfolding raw.until_def by blast
  then show ?thesis
  proof(induct i arbitrary: ω)
    case 0 then show ?case
      by (force intro: base)
  next
    case Suc from Suc.prems show ?case
      by (fastforce intro: step Suc.hyps dest: spec[where x="Suc j" for j]
                     simp: behavior.dropn.Suc raw.until_def
                    split: Option.bind_split_asm)
  qed
qed

lemma mono:
  assumes "P ⊆ P'"
  assumes "Q ⊆ Q'"
  shows "raw.until P Q ⊆ raw.until P' Q'"
unfolding raw.until_def using assms by blast

lemma botL:
  shows "raw.until {} Q = Q"
by (force simp: raw.until_def)

lemma botR:
  shows "raw.until P {} = {}"
by (force simp: raw.until_def)

lemma untilR:
  shows "raw.until P (raw.until P Q) = raw.until P Q" (is "?lhs = ?rhs")
proof(rule antisym[OF subsetI])
  show "ω ∈ ?rhs" if "ω ∈ ?lhs" for ω using that by induct blast+
  show "?rhs ⊆ ?lhs" by blast
qed

lemma InfL_not_empty:
  assumes "X ≠ {}"
  shows "raw.until (⋂X) Q = (⋂x∈X. raw.until x Q)" (is "?lhs = ?rhs")
proof(rule antisym[OF _ subsetI])
  show "?lhs ⊆ ?rhs"
    by (simp add: INT_greatest Inter_lower raw.until.mono)
  show "ω ∈ ?lhs" if "ω ∈ ?rhs" for ω
  proof -
    from ‹X ≠ {}› obtain P where "P ∈ X" by blast
    with that obtain i ω'
      where *: "behavior.dropn i ω = Some ω'" "ω' ∈ Q" "∀j<i. the (behavior.dropn j ω) ∈ P"
      unfolding raw.until_def by blast
    from this(1,2) obtain k ω''
      where **: "k ≤ i" "behavior.dropn k ω = Some ω''" "ω'' ∈ Q" "∀j<k. the (behavior.dropn j ω) ∉ Q"
      using ex_has_least_nat[where k=i and P="λk. k ≤ i ∧ (∀ω''. behavior.dropn k ω = Some ω'' ⟶ ω'' ∈ Q)" and m=id]
      by clarsimp (metis (no_types, lifting) behavior.dropn.shorterD leD nle_le option.sel order.trans)
    from that * ** show ?thesis
      by (clarsimp simp: raw.until_def intro!: exI[where x=k])
         (metis order.strict_trans1 linorder_not_le option.sel)
  qed
qed

lemma SupR:
  shows "raw.until P (⋃X) = ⋃(raw.until P ` X)"
unfolding raw.until_def by blast

lemma weakenL:
  shows "raw.until UNIV P = raw.until (- P) P" (is "?lhs = ?rhs")
proof(rule antisym[OF subsetI])
  show "ω ∈ ?rhs" if "ω ∈ ?lhs" for ω using that by induct blast+
  show "?rhs ⊆ ?lhs" by (simp add: raw.until.mono)
qed

lemma implication_ordering_le: ―‹ citet‹‹(16)› in "WarfordVegaStaley:2020"› ›
  shows "raw.until P Q ∩ raw.until (-Q) R ⊆ raw.until P R"
by (clarsimp simp: raw.until_def) (metis order.trans linorder_not_le option.sel)

lemma infR_ordering_le: ―‹ citet‹‹(18)› in "WarfordVegaStaley:2020"› ›
  shows "raw.until P (Q ∩ R) ⊆ raw.until (raw.until P Q) R" (is "?lhs⊆ ?rhs")
proof(rule subsetI)
  show "ω ∈ ?rhs" if "ω ∈ ?lhs" for ω
    using that
  proof induct
    case (step ω ω') then show ?case
      by - (rule raw.until.step, rule raw.until.step;
            blast intro: subsetD[OF raw.until.mono, rotated -1])
  qed blast
qed

lemma untilL:
  shows "raw.until (raw.until P Q) Q ⊆ raw.until P Q" (is "?lhs⊆ ?rhs")
proof(rule subsetI)
  show "ω ∈ ?rhs" if "ω ∈ ?lhs" for ω
    using that by induct auto
qed

lemma alwaysR_le:
  shows "raw.until P (raw.always Q) ⊆ raw.always (raw.until P Q)" (is "?lhs ⊆ ?rhs")
proof(rule subsetI)
  show "ω ∈ ?rhs" if "ω ∈ ?lhs" for ω
    using that
  proof induct
    case (base ω) then show ?case by (auto simp: raw.always_alt_def)
  next
    case (step ω ω') show ?case
    proof(rule raw.alwaysI)
      fix i ω'' assume "behavior.dropn i ω = Some ω''"
      with step "behavior.dropn.0" show "ω'' ∈ raw.until P Q"
        by (cases i; clarsimp simp: raw.always_alt_def behavior.dropn.Suc; blast)
    qed
  qed
qed

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "unless"›

lemma neg:
  shows "- (raw.until P Q ∪ raw.always P) = raw.until (- Q) (- P ∩ - Q)" (is "?lhs = ?rhs")
proof(rule antisym[OF subsetI], (unfold Compl_Un Int_iff conj_explode Compl_iff)[1])
  fix ω
  assume *: "ω ∉ raw.until P Q"
  assume "ω ∉ raw.always P"
  then obtain k ω'
    where "behavior.dropn k ω = Some ω'"
      and "ω' ∉ P"
    by (clarsimp simp: raw.always_alt_def)
  with ex_has_least_nat[where k=k and P="λi. ∃ω'. behavior.dropn i ω = Some ω' ∧ ω' ∉ P" and m=id]
  obtain k ω'
    where "behavior.dropn k ω = Some ω'"
      and "ω' ∉ P"
      and "∀j<k. the (behavior.dropn j ω) ∈ P"
    by clarsimp (metis behavior.dropn.shorterD less_le_not_le option.distinct(1) option.exhaust_sel)
  with * behavior.dropn.shorterD show "ω ∈ ?rhs"
    by (fastforce simp: raw.until_def intro: exI[where x=k])
next
  show "?rhs ⊆ ?lhs"
    by (clarsimp simp: raw.always_alt_def raw.until_def subset_iff; metis nat_neq_iff option.sel)
qed

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "eventually"›

lemma terminated:
  shows "raw.eventually raw.terminated = {ω. tfinite (behavior.rest ω)}" (is "?lhs = ?rhs")
proof(rule antisym[OF _ subsetI])
  show "?lhs ⊆ ?rhs"
    by (clarsimp simp: raw.eventually_alt_def raw.terminated_def behavior.dropn.tfiniteD)
  show "ω ∈ ?lhs" if "ω ∈ ?rhs" for ω
  proof -
    note ‹ω ∈ ?rhs›
    moreover from calculation
    obtain i where "tlength (behavior.rest ω) = enat i"
      by (clarsimp simp: tfinite_tlength_conv)
    moreover from calculation
    obtain ω' where "behavior.dropn i ω = Some ω'"
      using behavior.dropn.eq_Some_tlength_conv by fastforce
    moreover from calculation
    have "behavior.sset ω' ⊆ {behavior.init ω'}"
      by (cases ω')
         (clarsimp dest!: behavior.dropn.eq_Some_tdropnD simp: tdropn_tlength behavior.sset.simps)
    ultimately show "ω ∈ ?lhs"
      by (auto simp: raw.eventually_alt_def raw.terminated_def dest: behavior.dropn.tfiniteD)
  qed
qed

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "behavior.stuttering.closed.raw"›

lemma state_prop[intro]:
  shows "raw.state_prop P ∈ behavior.stuttering.closed"
by (fastforce simp: raw.state_prop_def behavior.natural_def elim: behavior.stuttering.clE)

lemma terminated[intro]:
  shows "raw.terminated ∈ behavior.stuttering.closed"
by (rule behavior.stuttering.closedI)
   (clarsimp simp: raw.terminated_def elim!: behavior.stuttering.clE;
    metis behavior.natural.sel(1) behavior.natural.tfinite behavior.sset.natural)

lemma until[intro]:
  assumes "P ∈ behavior.stuttering.closed"
  assumes "Q ∈ behavior.stuttering.closed"
  shows "raw.until P Q ∈ behavior.stuttering.closed"
proof -
  have "ω2 ∈ raw.until P Q" if "ω1 ∈ raw.until P Q" and "ω1 ≃T ω2" for ω1 ω2
    using that
  proof(induct arbitrary: ω2 rule: raw.until.induct)
    case (base ω1 ω2) with assms(2) show ?case
      by (blast intro: behavior.stuttering.closed_in)
  next
    case (step ω1 ω' ω2)
    show ?case
    proof(cases "ω' ≃T ω1")
      case True with ‹ω1 ≃T ω2› step.hyps(4) show ?thesis
        by simp
    next
      case False
      from assms(1) ‹ω1 ∈ P› ‹ω1 ≃T ω2› have "ω2 ∈ P"
        by (blast intro: behavior.stuttering.closed_in)
      from False ‹ω1 ≃T ω2› ‹behavior.tl ω1 = Some ω'›
      obtain a s0 s1 xs1 xs' ys'
        where ω1: "ω1 = behavior.B s0 (TCons (a, s1) xs1)"
          and ω2: "ω2 = behavior.B s0 (tshift xs' (TCons (a, s1) ys'))"
          and *: "collapse s0 (TCons (a, s1) xs1) = collapse s0 (tshift xs' (TCons (a, s1) ys'))"
                 "s0 ≠ s1"
          and **: "collapse s1 ys' = collapse s1 xs1"
          and xs': "snd ` set xs' ⊆ {s0}"
        by (cases ω1; cases ω2; cases "behavior.rest ω1"; simp)
           (fastforce simp: behavior.natural_def collapse.eq_TCons_conv trepeat_eq_TCons_conv
                     split: if_splits)
      from ω2 ‹ω2 ∈ P› xs' show ?thesis
      proof(induct xs' arbitrary: ω2)
        case Nil with ω1 ** step.hyps(2,4) show ?case
          by (auto simp: behavior.natural_def)
      next
        case (Cons x' xs')
        with behavior.stuttering.closed_in[OF _ _ ‹P ∈ behavior.stuttering.closed›] ω1 ** step(3)
        show ?case
          by (auto simp: behavior.natural_def  behavior.split_all)
      qed
    qed
  qed
  then show ?thesis
    by (fastforce elim: behavior.stuttering.clE)
qed

lemma eventually[intro]:
  assumes "P ∈ behavior.stuttering.closed"
  shows "raw.eventually P ∈ behavior.stuttering.closed"
using assms by (auto simp: raw.eventually_def)

lemma always[intro]:
  assumes "P ∈ behavior.stuttering.closed"
  shows "raw.always P ∈ behavior.stuttering.closed"
using assms by (auto simp: raw.always_def)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "tls"›

definition valid :: "('a, 's, 'v) tls ⇒ bool" where
  "valid P ⟷ P = ⊤"

lift_definition state_prop :: "'s pred ⇒ ('a, 's, 'v) tls" is raw.state_prop ..
lift_definition terminated :: "('a, 's, 'v) tls" is raw.terminated ..
lift_definition until :: "('a, 's, 'v) tls ⇒ ('a, 's, 'v) tls ⇒ ('a, 's, 'v) tls" is raw.until ..

definition eventually :: "('a, 's, 'v) tls ⇒ ('a, 's, 'v) tls" where
  "eventually P = tls.until ⊤ P"

definition always :: "('a, 's, 'v) tls ⇒ ('a, 's, 'v) tls" where
  "always P = -tls.eventually (-P)"

definition release :: "('a, 's, 'v) tls ⇒ ('a, 's, 'v) tls ⇒ ('a, 's, 'v) tls" where
  "release P Q = -(tls.until (-P) (-Q))"

definition unless :: "('a, 's, 'v) tls ⇒ ('a, 's, 'v) tls ⇒ ('a, 's, 'v) tls" where
  "unless P Q = tls.until P Q ⊔ tls.always P"

abbreviation (input) always_imp_syn :: "('a, 's, 'v) tls ⇒ ('a, 's, 'v) tls ⇒ ('a, 's, 'v) tls" where
  "always_imp_syn P Q ≡ tls.always (P ⟶B Q)"

abbreviation (input) leads_to :: "('a, 's, 'v) tls ⇒ ('a, 's, 'v) tls ⇒ ('a, 's, 'v) tls" where
  "leads_to P Q ≡ tls.always_imp_syn P (tls.eventually Q)"

bundle "notation"
begin

notation tls.valid ("⊨ _" [30] 30)
notation tls.state_prop ("⟪_⟫" [0])
notation tls.until (infix "𝒰" 85)
notation tls.eventually ("◇_" [87] 87)
notation tls.always ("□_" [87] 87)
notation tls.release (infixr "ℛ" 85)
notation tls.unless (infixr "𝒲" 85)
notation tls.always_imp_syn (infixr "⟶□" 75)
notation tls.leads_to (infixr "↝" 75)

end

bundle "no_notation"
begin

no_notation tls.valid ("⊨ _" [30] 30)
no_notation tls.state_prop ("⟪_⟫" [0])
no_notation tls.until (infixr "𝒰" 85)
no_notation tls.eventually ("◇_" [87] 87)
no_notation tls.always ("□_" [87] 87)
no_notation tls.release (infixr "ℛ" 85)
no_notation tls.unless (infixr "𝒲" 85)
no_notation tls.always_imp_syn (infixr "⟶□" 75)
no_notation tls.leads_to (infixr "↝" 75)

end

unbundle tls.notation

lemma validI:
  assumes "⊤ ≤ P"
  shows "⊨ P"
by (simp add: assms tls.valid_def top.extremum_uniqueI)

setup ‹Sign.mandatory_path "valid"›

lemma trans[trans]:
  assumes "⊨ P"
  assumes "P ≤ Q"
  shows "⊨ Q"
using assms by (simp add: tls.valid_def top.extremum_unique)

lemma mp:
  assumes "⊨ P ⟶B Q"
  assumes "⊨ P"
  shows "⊨ Q"
using assms by (simp add: tls.valid_def)

lemmas rev_mp = tls.valid.mp[rotated]

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "singleton"›

lemma uminus_le_conv[tls.singleton.le_conv]:
  shows "⦉ω⦊T ≤ -P ⟷ ¬⦉ω⦊T ≤ P"
by transfer
   (simp add: raw.singleton_def behavior.stuttering.closed_uminus behavior.stuttering.least_conv)

lemma state_prop_le_conv[tls.singleton.le_conv]:
  shows "⦉ω⦊T ≤ tls.state_prop P ⟷ P (behavior.init ω)"
by transfer
   (simp add: raw.singleton_def behavior.stuttering.least_conv[OF behavior.stuttering.closed.raw.state_prop];
    simp add: raw.state_prop_def)

lemma terminated_le_conv[tls.singleton.le_conv]:
  shows "⦉ω⦊T ≤ tls.terminated ⟷ tfinite (behavior.rest ω) ∧ behavior.sset ω ⊆ {behavior.init ω}"
by transfer
   (simp add: raw.singleton_def behavior.stuttering.least_conv[OF behavior.stuttering.closed.raw.terminated];
    simp add: raw.terminated_def)

lemma until_le_conv[tls.singleton.le_conv]:
  fixes P :: "('a, 's, 'v) tls"
  shows "⦉ω⦊T ≤ P 𝒰 Q ⟷ (∃i ω'. behavior.dropn i ω = Some ω'
                                ∧ ⦉ω'⦊T ≤ Q
                                ∧ (∀j<i. ⦉the (behavior.dropn j ω)⦊T ≤ P))" (is "?lhs ⟷ ?rhs")
proof(rule iffI)
  show "?lhs ⟹ ?rhs"
  proof transfer
    fix ω and P Q :: "('a, 's, 'v) behavior.t set"
    assume *: "P ∈ behavior.stuttering.closed" "Q ∈ behavior.stuttering.closed"
       and "raw.singleton ω ⊆ raw.until P Q"
    then have "∃i. ∃ω'∈Q. behavior.dropn i ω = Some ω' ∧ (∀j<i. the (behavior.dropn j ω) ∈ P)"
      by (auto simp: raw.singleton_def raw.until_def)
    with * show "∃i ω'. behavior.dropn i ω = Some ω'
                      ∧ raw.singleton ω' ⊆ Q ∧ (∀j<i. raw.singleton (the (behavior.dropn j ω)) ⊆ P)"
      by (auto simp: raw.singleton_def behavior.stuttering.least_conv)
  qed
  show "?rhs ⟹ ?lhs"
    by transfer
       (unfold raw.singleton_def;
        rule behavior.stuttering.least[OF _ behavior.stuttering.closed.raw.until];
        auto 10 0 intro: iffD2[OF eqset_imp_iff[OF raw.until_def]])
qed

lemma eventually_le_conv[tls.singleton.le_conv]:
  shows "⦉ω⦊T ≤ ◇P ⟷ (∃i ω'. behavior.dropn i ω = Some ω' ∧ ⦉ω'⦊T ≤ P)"
by (simp add: tls.eventually_def tls.singleton.le_conv)

lemma always_le_conv[tls.singleton.le_conv]:
  shows "⦉ω⦊T ≤ tls.always P ⟷ (∀i ω'. behavior.dropn i ω = Some ω' ⟶ ⦉ω'⦊T ≤ P)"
by (simp add: tls.always_def tls.singleton.le_conv)

setup ‹Sign.parent_path›

interpretation until: closure_complete_lattice_distributive_class "tls.until P" for P
proof standard
  show "(x ≤ tls.until P y) = (tls.until P x ≤ tls.until P y)" for x y
  by transfer
     (intro iffD2[OF order_class.order.closure_axioms_alt_def[unfolded closure_axioms_def], rule_format]
            conjI allI raw.until.base monoI raw.until.mono order.refl raw.until.untilR, assumption)
  show "tls.until P (⨆X) ≤ ⨆(tls.until P ` X) ⊔ tls.until P ⊥" for X
    by transfer (simp add: raw.until.SupR behavior.stuttering.cl_bot)
qed

setup ‹Sign.mandatory_path "until"›

lemmas botL = raw.until.botL[transferred]
lemmas botR = raw.until.botR[transferred]
lemmas topR = tls.until.cl_top
lemmas expansiveR = tls.until.expansive[of P Q for P Q]

lemmas weakenL = raw.until.weakenL[transferred]

lemmas mono = raw.until.mono[transferred]

lemma strengthen[strg]:
  assumes "st_ord F P P'"
  assumes "st_ord F Q Q'"
  shows "st_ord F (P 𝒰 Q) (P' 𝒰 Q')"
using assms by (cases F) (auto simp: tls.until.mono)

lemma SupL_le:
  shows "(⨆x∈X. x 𝒰 R) ≤ (⨆X) 𝒰 R"
by (simp add: SupI tls.until.mono)

lemma supL_le:
  shows "P 𝒰 R ⊔ Q 𝒰 R ≤ (P ⊔ Q) 𝒰 R"
by (simp add: tls.until.mono)

lemma SupR:
  shows "P 𝒰 (⨆X) = ⨆((𝒰) P ` X)"
by (simp add: tls.until.cl_Sup tls.until.botR)

lemmas supR = tls.until.cl_sup

lemmas InfL_not_empty = raw.until.InfL_not_empty[transferred]
lemmas infL = tls.until.InfL_not_empty[where X="{P, Q}" for P Q, simplified, of P Q R for P Q R]
lemmas InfR_le = tls.until.cl_Inf_le
lemmas infR_le = tls.until.cl_inf_le[of P Q R for P Q R]

lemma implication_ordering_le: ―‹ citet‹‹(16)› in "WarfordVegaStaley:2020"› ›
  shows "P 𝒰 Q ⊓ (-Q) 𝒰 R ≤ P 𝒰 R"
by transfer (rule raw.until.implication_ordering_le)

lemma supL_ordering_le: ―‹ citet‹‹(17)› in "WarfordVegaStaley:2020"› ›
  shows "P 𝒰 (Q 𝒰 R) ≤ (P ⊔ Q) 𝒰 R" (is "?lhs ≤ ?rhs")
proof -
  have "?rhs = (P ⊔ Q) 𝒰 ((P ⊔ Q) 𝒰 R)" by (rule tls.until.idempotent(1)[symmetric])
  also have "?lhs ≤ …" by (blast intro: tls.until.mono le_supI1 le_supI2)
  finally show ?thesis .
qed

lemma infR_ordering_le: ―‹ citet‹‹(18)› in "WarfordVegaStaley:2020"› ›
  shows "P 𝒰 (Q ⊓ R) ≤ (P 𝒰 Q) 𝒰 R"
by transfer (rule raw.until.infR_ordering_le)

lemma boolean_implication_distrib_le: ―‹ citet‹‹(19)› in "WarfordVegaStaley:2020"› ›
  shows "(P ⟶B Q) 𝒰 R ≤ (P 𝒰 R) ⟶B (Q 𝒰 R)"
by (metis galois.conj_imp.galois order.refl tls.until.infL tls.until.mono)

lemma excluded_middleR: ―‹ citet‹‹(23)› in "WarfordVegaStaley:2020"› ›
  shows "⊨ P 𝒰 Q ⊔ P 𝒰 (-Q)"
by (simp add: tls.validI tls.until.cl_top flip: tls.until.cl_sup)

lemmas untilR = tls.until.idempotent(1)[of P Q for P Q]

lemma untilL:
  shows "(P 𝒰 Q) 𝒰 Q = P 𝒰 Q" (is "?lhs = ?rhs")
proof(rule antisym)
  show "?lhs ≤ ?rhs"
    by transfer (rule raw.until.untilL)
  show "?rhs ≤ ?lhs"
    using tls.until.infR_ordering_le[where P=P and Q=Q and R=Q] by simp
qed

lemma absorb:
  shows "P 𝒰 P = P"
by (metis tls.until.botL tls.until.untilL)

lemma absorb_supL: ―‹ citet‹‹(23)› in "WarfordVegaStaley:2020"› ›
  shows "P ⊔ P 𝒰 Q = P ⊔ Q"
by (metis inf_commute inf_sup_absorb le_iff_sup
          tls.until.absorb tls.until.cl_sup tls.until.expansive tls.until.infL)

lemma absorb_supR: ―‹ citet‹‹(23)› in "WarfordVegaStaley:2020"› ›
  shows "Q ⊔ P 𝒰 Q = P 𝒰 Q"
by (simp add: sup.absorb2 tls.until.expansive)

lemma eventually_le:
  shows "P 𝒰 Q ≤ ◇Q"
by (simp add: tls.eventually_def tls.until.mono)

lemma absorb_eventually:
  shows inf_eventually_absorbR: "P 𝒰 Q ⊓ ◇Q = P 𝒰 Q" ―‹ citet‹‹(39)› in "WarfordVegaStaley:2020"› ›
    and sup_eventually_absorbR: "P 𝒰 Q ⊔ ◇Q = ◇Q" ―‹ citet‹‹(40)› in "WarfordVegaStaley:2020"› ›
    and eventually_absorbR: "P 𝒰 ◇Q = ◇Q" ―‹ citet‹‹(41)› in "WarfordVegaStaley:2020"› ›
by (simp_all add: tls.eventually_def sup.absorb2 tls.until.mono
                  order.eq_iff order.trans[OF tls.until.supL_ordering_le] tls.until.expansiveR
            flip: tls.until.infL)

lemma sup_le: ―‹ citet‹‹(28)› in "WarfordVegaStaley:2020"› ›
  shows "P 𝒰 Q ≤ P ⊔ Q"
by (simp add: ac_simps sup.absorb_iff1 tls.until.absorb_supL tls.until.absorb_supR)

lemma ordering: ―‹ citet‹‹(251)› in "WarfordVegaStaley:2020"› ›
  shows "(-P) 𝒰 Q ⊔ (-Q) 𝒰 P = ◇(P ⊔ Q)" (is "?lhs = ?rhs")
proof -
  have "?lhs = ⊤ 𝒰 P ⊓ (- Q) 𝒰 P ⊔ ⊤ 𝒰 Q ⊓ (- P) 𝒰 Q"
    by (simp add: ac_simps inf.absorb2 tls.until.mono)
  also have "… = (- P) 𝒰 P ⊓ (- Q) 𝒰 P ⊔ (- Q) 𝒰 Q ⊓ (- P) 𝒰 Q"
    by (simp add: tls.until.weakenL)
  also have "… = (- (P ⊔ Q)) 𝒰 (P ⊔ Q)"
    by (simp add: ac_simps tls.until.cl_sup flip: tls.until.infL)
  also have "… = ?rhs"
    by (simp add: tls.eventually_def tls.until.weakenL)
  finally show ?thesis .
qed

lemmas simps =
  tls.until.expansiveR
  tls.until.botL
  tls.until.botR
  tls.until.absorb
  tls.until.absorb_supL
  tls.until.absorb_supR
  tls.until.untilL
  tls.until.untilR

setup ‹Sign.parent_path›

interpretation eventually: closure_complete_lattice_distributive_class tls.eventually
unfolding tls.eventually_def
by (simp add: tls.until.closure_complete_lattice_distributive_class_axioms)

lemma eventually_alt_def:
  shows "◇P = (-P) 𝒰 P"
by (simp add: tls.eventually_def tls.until.weakenL)

setup ‹Sign.mandatory_path "eventually"›

lemma transfer[transfer_rule]:
  shows "rel_fun (pcr_tls (=) (=) (=)) (pcr_tls (=) (=) (=)) raw.eventually tls.eventually"
unfolding tls.eventually_def raw.eventually_def by transfer_prover

lemma bot:
  shows "◇⊥ = ⊥"
by (simp add: tls.eventually_def tls.until.simps)

lemma bot_conv:
  shows "◇P = ⊥ ⟷ P = ⊥"
by (auto simp: tls.eventually.bot bot.extremum_uniqueI[OF order.trans[OF tls.eventually.expansive]])

lemmas top = tls.eventually.cl_top

lemmas monotone = tls.eventually.monotone_cl
lemmas mono = tls.eventually.mono_cl

lemmas Sup = tls.eventually.cl_Sup[simplified tls.eventually.bot, simplified]
lemmas sup = tls.eventually.Sup[where X="{P, Q}" for P Q, simplified]

lemmas Inf_le = tls.eventually.cl_Inf_le
lemmas inf_le = tls.eventually.cl_inf_le

lemma neg:
  shows "-◇P = □(-P)"
by (simp add: tls.always_def)

lemma boolean_implication_le:
  shows "◇P ⟶B ◇Q ≤ ◇(P ⟶B Q)"
by (simp add: boolean_implication.conv_sup tls.eventually.sup)
   (meson le_supI1 compl_mono order.trans le_supI1 tls.eventually.expansive)

lemmas simps =
  tls.eventually.bot
  tls.eventually.top
  tls.eventually.expansive
  tls.eventually_def[symmetric]

lemma terminated:
  shows "◇tls.terminated = ⨆(tls.singleton ` {ω. tfinite (behavior.rest ω)})"
by transfer
   (auto elim!: behavior.stuttering.clE
          dest: iffD2[OF behavior.natural.tfinite]
          simp: raw.eventually.terminated behavior.stuttering.cl_bot raw.singleton_def collapse.tfinite)

lemma always_imp_le:
  shows "P ⟶□ Q ≤ ◇P ⟶B ◇Q"
by (simp add: tls.always_def boolean_implication.conv_sup flip: shunt2)
   (metis inf_commute order.refl shunt2 sup.commute tls.eventually.mono tls.eventually.sup)

lemma until:
  shows "◇(P 𝒰 Q) = ◇Q"
by (meson antisym tls.eventually.cl tls.eventually.mono tls.until.eventually_le tls.until.expansiveR)

setup ‹Sign.parent_path›

lemma always_alt_def:
  shows "□P = P 𝒲 ⊥"
by (simp add: tls.unless_def tls.until.simps)

setup ‹Sign.mandatory_path "always"›

lemma transfer[transfer_rule]:
  shows "rel_fun (pcr_tls (=) (=) (=)) (pcr_tls (=) (=) (=)) raw.always tls.always"
unfolding tls.always_def raw.always_def by transfer_prover

text‹ const‹tls.always› is an interior operator ›

lemma idempotent[simp]:
  shows "□□P = □P"
by (simp add: tls.always_def)

lemma contractive:
  shows "□P ≤ P"
by (simp add: tls.always_def compl_le_swap2 tls.eventually.expansive)

lemma monotone[iff]:
  shows "mono tls.always"
by (simp add: tls.always_def monoI tls.eventually.mono)

lemmas strengthen[strg] = st_monotone[OF tls.always.monotone]
lemmas mono[trans] = monoD[OF tls.always.monotone]

lemma bot:
  shows "□⊥ = ⊥"
by (simp add: tls.always_def tls.eventually.simps)

lemma top:
  shows "□⊤ = ⊤"
by (simp add: tls.always_def tls.eventually.simps)

lemma top_conv:
  shows "□P = ⊤ ⟷ P = ⊤"
by (auto simp: tls.always.top intro: top.extremum_uniqueI[OF order.trans[OF _ tls.always.contractive]])

lemma Sup_le:
  shows "⨆(tls.always ` X) ≤ □(⨆X)"
by (simp add: SupI tls.always.mono)

lemma sup_le:
  shows "□P ⊔ □Q ≤ □(P ⊔ Q)"
by (simp add: tls.always.mono)

lemma Inf:
  shows "□(⨅X) = ⨅(tls.always ` X)"
by (rule iffD1[OF compl_eq_compl_iff])
   (simp add: tls.always_def image_image tls.eventually.Sup uminus_Inf)

lemma inf:
  shows "□(P ⊓ Q) = □P ⊓ □Q"
by (simp add: tls.always_def tls.eventually.sup)

lemma neg:
  shows "-□P = ◇(-P)"
by (simp add: tls.always_def)

lemma always_necessitation:
  assumes "⊨ P"
  shows "⊨ □P"
using assms by (simp add: tls.valid_def tls.always.top)

lemma valid_conv:
  shows "⊨ □P ⟷ ⊨ P"
by (simp add: tls.valid_def tls.always.top_conv)

lemma always_imp_le:
  shows "P ⟶□ Q ≤ □P ⟶B □Q"
by (simp add: galois.conj_imp.lower_upper_contractive tls.always.mono
        flip: galois.conj_imp.galois tls.always.inf)

lemma eventually_le:
  shows "□P ≤ ◇P"
using tls.always.contractive tls.eventually.cl tls.eventually.mono by blast

lemma not_until_le: ―‹ citet‹‹(81)› in "WarfordVegaStaley:2020"› ›
  shows "□P ≤ -(Q 𝒰 (-P))"
by (simp add: compl_le_swap1 tls.always.neg tls.until.eventually_le)

lemmas simps =
  tls.always.bot
  tls.always.top
  tls.always.contractive
  tls.always_alt_def[symmetric]

setup ‹Sign.parent_path›

lemma until_alwaysR_le: ―‹ citet‹‹(140)› in "WarfordVegaStaley:2020"› ›
  shows "P 𝒰 □Q ≤ □(P 𝒰 Q)"
by transfer (rule raw.until.alwaysR_le)

lemma until_alwaysR: ―‹ citet‹‹(141)› in "WarfordVegaStaley:2020"› ›
  shows "P 𝒰 □P = □P"
by (simp add: order.eq_iff order.trans[OF tls.until_alwaysR_le] tls.until.simps)

lemma eventually_always_always_eventually_le: ―‹ citet‹‹(145)› in "WarfordVegaStaley:2020"› ›
  shows "◇□P ≤ □◇P"
by (simp add: tls.eventually_def tls.until_alwaysR_le)

lemma always_inf_eventually_eventually_le:
  shows "□P ⊓ ◇Q ≤ ◇(P ⊓ Q)"
by (simp add: shunt1 order.trans[OF _ tls.eventually.always_imp_le] boolean_implication.mp
              tls.always.mono
        flip: boolean_implication_def)

lemma always_always_imp: ―‹citet‹‹\S2.2: T33 frame› in "KroegerMerz:2008"› ›
  shows "⊨ □P ⟶B □Q ⟶B □(P ⊓ Q)"
by (simp add: tls.validI tls.always.inf flip: boolean_implication.infL)

lemma always_eventually_imp: ―‹citet‹‹\S2.2: T34 frame› in "KroegerMerz:2008"› ›
  shows "⊨ □P ⟶B ◇Q ⟶B ◇(P ⊓ Q)"
by (simp add: tls.validI boolean_implication.mp tls.always_inf_eventually_eventually_le)

lemma always_imp_always_generalization: ―‹citet‹‹\S2.2: T35› in "KroegerMerz:2008"› ›
  shows "□P ⟶□ Q ≤ □P ⟶B □Q"
by (simp add: order.trans[OF tls.always.always_imp_le])

lemma always_imp_eventually_generalization: ―‹citet‹‹\S2.2: T36› in "KroegerMerz:2008"› ›
  shows "P ⟶□ ◇Q ≤ ◇P ⟶B ◇Q"
by (metis tls.eventually.always_imp_le tls.eventually.idempotent(1))

text‹

The following show that there is no point nesting const‹tls.always› and const‹tls.eventually›
more than two deep.
›

lemma always_eventually_always_absorption: ―‹citet‹‹\S2.2: T37› in "KroegerMerz:2008"› ›
  shows "◇□◇P = □◇P"
by (metis order.eq_iff tls.eventually.expansive tls.eventually.idempotent(1)
          tls.eventually_always_always_eventually_le)

lemma eventually_always_eventually_absorption: ―‹citet‹‹\S2.2: T38› in "KroegerMerz:2008"› ›
  shows "□◇□P = ◇□P"
by (metis tls.always.neg tls.always_def tls.always_eventually_always_absorption)

lemma always_imp_always_eventually_le: ―‹ citet‹‹(157)› in "WarfordVegaStaley:2020"› ›
  shows "P ⟶□ Q ≤ □◇P ⟶B □◇Q"
by (simp add: order.trans[OF _ tls.always.always_imp_le]
              order.trans[OF _ tls.always.mono[OF tls.eventually.always_imp_le]])

lemma always_imp_eventually_always_le: ―‹ citet‹‹(158)› in "WarfordVegaStaley:2020"› ›
  shows "P ⟶□ Q ≤ ◇□P ⟶B ◇□Q"
by (simp add: order.trans[OF _ tls.eventually.always_imp_le]
              order.trans[OF _ tls.always.mono[OF tls.always.always_imp_le]])

lemma always_eventually_inf_le:
  shows "□◇(P ⊓ Q) ≤ □◇P ⊓ □◇Q" ―‹ citet‹‹(159)› in "WarfordVegaStaley:2020"› ›
by (simp add: tls.always.mono tls.eventually.mono)

lemma eventually_always_sup_le:
  shows "◇□P ⊓ ◇□Q ≤ ◇□(P ⊔ Q)" ―‹ citet‹‹(160)› in "WarfordVegaStaley:2020"› ›
by (simp add: le_infI2 tls.always.mono tls.eventually.mono)

lemma always_eventually_sup: ―‹ citet‹‹(161)› in "WarfordVegaStaley:2020"› ›
  fixes P :: "('a, 's, 'v) tls"
  shows "□◇(P ⊔ Q) = □◇P ⊔ □◇Q" (is "?lhs = ?rhs")
proof(rule antisym)
  show "?lhs ≤ ?rhs"
  proof transfer
    fix P Q :: "('a, 's, 'v) behavior.t set"
    have "∃ω'∈P. ∃i. behavior.dropn i ωj = Some ω'"
      if "∀i ω'. behavior.dropn i ω = Some ω' ⟶ (∃ω''∈P ∪ Q. ∃i. behavior.dropn i ω' = Some ω'')"
     and "behavior.dropn i ω = Some ωi"
     and "∀ω'∈Q. ∀i. behavior.dropn i ωi ≠ Some ω'"
     and "behavior.dropn j ω = Some ωj"
      for ω i j ωi ωj
      using spec[where x="max i j", OF that(1)] that(2,3,4)
      by (clarsimp simp: nat_le_iff_add split: split_asm_max;
          metis add_diff_inverse_nat behavior.dropn.dropn bind.bind_lunit order.asym)
    then show "raw.always (raw.eventually (P ∪ Q))
            ⊆ raw.always (raw.eventually P) ∪ raw.always (raw.eventually Q)"
      by (clarsimp simp: raw.eventually_alt_def raw.always_alt_def)
  qed
  show "?rhs ≤ ?lhs"
    by (simp add: tls.eventually.sup order.trans[OF _ tls.always.sup_le])
qed

lemma eventually_always_inf: ―‹ citet‹‹(162)› in "WarfordVegaStaley:2020"› ›
  shows "◇□(P ⊓ Q) = ◇□P ⊓ ◇□Q"
by (subst compl_eq_compl_iff[symmetric])
   (simp add: tls.always.neg tls.always_eventually_sup tls.eventually.neg)

lemma eventual_latching: ―‹ citet‹‹(163)› in "WarfordVegaStaley:2020"› ›
  shows "◇□(P ⟶B □Q) = ◇□(-P) ⊔ ◇□Q" (is "?lhs = ?rhs")
proof(rule antisym)
  show "?lhs ≤ ?rhs"
    by (rule order.trans[OF tls.eventually.mono[OF tls.always_imp_always_eventually_le]])
       (simp add: boolean_implication.conv_sup tls.always.neg
                  tls.eventually.neg tls.eventually.sup tls.eventually_always_eventually_absorption)
  have "◇□Q ≤ ◇□(- P ⊔ □Q)"
    apply (rule order.trans[OF tls.eventually.mono[OF eq_refl[OF tls.always.idempotent[symmetric]]]])
    apply (rule tls.eventually.mono[OF tls.always.mono])
    apply simp
    done
  then show "?rhs ≤ ?lhs"
    by (simp add: le_sup_iff boolean_implication.conv_sup monoD)
qed

setup ‹Sign.mandatory_path "unless"›

lemma transfer[transfer_rule]:
  shows "rel_fun (pcr_tls (=) (=) (=)) (rel_fun (pcr_tls (=) (=) (=)) (pcr_tls (=) (=) (=)))
                 (λP Q. raw.until P Q ∪ raw.always P)
                 tls.unless"
unfolding tls.unless_def by transfer_prover

lemma neg: ―‹ citet‹‹(170)› in "WarfordVegaStaley:2020"› ›
  shows "-(P 𝒲 Q) = (-Q) 𝒰 (-P ⊓ -Q)"
by transfer (rule raw.unless.neg)

lemma alwaysR_le: ―‹ citet‹‹(177)› in "WarfordVegaStaley:2020"› ›
  shows "P 𝒲 □Q ≤ □(P 𝒲 Q)"
by (simp add: tls.unless_def order.trans[OF tls.until_alwaysR_le] tls.always.mono
              order.trans[OF _ tls.always.sup_le])

lemma sup_le: ―‹ citet‹‹(206)› in "WarfordVegaStaley:2020"› ›
  shows "P 𝒲 Q ≤ P ⊔ Q"
by (rule iffD1[OF compl_le_compl_iff]) (simp add: tls.unless.neg tls.until.expansive)

lemma ordering: ―‹ citet‹‹(252)› in "WarfordVegaStaley:2020"› ›
  shows "⊨ (-P) 𝒲 Q ⊔ (-Q) 𝒲 P"
by (simp add: ac_simps tls.validI tls.unless_def tls.until.ordering tls.eventually.sup flip: tls.eventually.neg)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "until"›

lemma eq_unless_inf_eventually:
  shows "P 𝒰 Q = (P 𝒲 Q) ⊓ ◇Q"
by transfer (force simp: raw.until_def raw.eventually_def raw.always_alt_def behavior.dropn.shorterD)

lemma always_strengthen_le: ―‹ citet‹‹(83)› in "WarfordVegaStaley:2020"› ›
  shows "□P ⊓ (Q 𝒰 R) ≤ (P ⊓ Q) 𝒰 (P ⊓ R)"
by transfer
   (clarsimp simp: raw.until_def raw.always_alt_def;
    fastforce simp: behavior.dropn.shorterD del: exI intro!: exI)

lemma until_weakI:
  shows "□P ⊓ ◇Q ≤ P 𝒰 Q" (is "?lhs ≤ ?rhs") ―‹ citet‹‹(84)› in "WarfordVegaStaley:2020"› ›
by (simp add: tls.eventually_def order.trans[OF tls.until.always_strengthen_le] tls.until.mono)

lemma always_impL: ―‹ citet‹‹(86)› in "WarfordVegaStaley:2020"› ›
  shows "P ⟶□ P' ⊓ P 𝒰 Q ≤ P' 𝒰 Q" (is ?thesis1)
    and "P 𝒰 Q ⊓ P ⟶□ P' ≤ P' 𝒰 Q" (is ?thesis2)
proof -
  show ?thesis1
    by (rule order.trans[OF tls.until.always_strengthen_le])
       (simp add: tls.until.mono boolean_implication.shunt1)
  then show ?thesis2
    by (simp add: inf_commute)
qed

lemma always_impR: ―‹ citet‹‹(85)› in "WarfordVegaStaley:2020"› ›
  shows "Q ⟶□ Q' ⊓ P 𝒰 Q ≤ P 𝒰 Q'" (is ?thesis1)
    and "P 𝒰 Q ⊓ Q ⟶□ Q' ≤ P 𝒰 Q'" (is ?thesis2)
proof -
  show ?thesis1
    by (rule order.trans[OF tls.until.always_strengthen_le])
       (simp add: tls.until.mono boolean_implication.shunt1)
  then show ?thesis2
    by (simp add: inf_commute)
qed

lemma neg: ―‹ citet‹‹(173)› in "WarfordVegaStaley:2020"› ›
  shows "-(P 𝒰 Q) = (-Q) 𝒲 (-P ⊓ -Q)"
unfolding tls.unless_def
by (simp flip: tls.until.eq_unless_inf_eventually tls.unless.neg tls.eventually.neg
               boolean_algebra.de_Morgan_conj)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "state_prop"›

lemmas monotone = raw.state_prop.monotone[transferred]
lemmas strengthen[strg] = st_monotone[OF tls.state_prop.monotone]
lemmas mono = monoD[OF tls.state_prop.monotone]

lemma Sup:
  shows "tls.state_prop (⨆X) = ⨆(tls.state_prop ` X)"
by transfer (simp add: raw.state_prop.Sup behavior.stuttering.cl_bot)

lemma Inf:
  shows "tls.state_prop (⨅X) = ⨅(tls.state_prop ` X)"
by transfer (simp add: raw.state_prop.Inf)

lemmas simps = raw.state_prop.simps[transferred]

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "terminated"›

lemma not_bot:
  shows "tls.terminated ≠ ⊥"
by transfer
   (simp add: raw.terminated_def exI[where x="behavior.B undefined (TNil undefined)"] behavior.sset.simps)

lemma not_top:
  shows "tls.terminated ≠ ⊤"
by transfer
   (fastforce simp: raw.terminated_def
              dest: subsetD[OF Set.equalityD2, where c="behavior.B undefined (trepeat (undefined, undefined))"])

lemma inf_always:
  shows "tls.terminated ⊓ □P = tls.terminated ⊓ P"
by (rule antisym[OF inf.mono[OF order.refl tls.always.contractive]])
   (transfer; simp add: raw.terminated.inf_always_le)

lemma always_le_conv:
  shows "tls.terminated ≤ □P ⟷ tls.terminated ≤ P"
by (simp add: inf.order_iff tls.terminated.inf_always)

lemma inf_eventually:
  shows "tls.terminated ⊓ ◇P = tls.terminated ⊓ P" (is "?lhs = ?rhs")
proof(rule antisym[OF _ inf.mono[OF order.refl tls.eventually.expansive]])
  have "tls.terminated ⊓ - P ≤ tls.terminated ⊓ -◇P"
    by (simp add: tls.terminated.inf_always tls.eventually.neg)
  then show "?lhs ≤ ?rhs"
    by (simp add: boolean_implication.shunt1 boolean_implication.imp_trivialI)
qed

lemma eventually_le_conv:
  shows "tls.terminated ≤ tls.eventually P ⟷ tls.terminated ≤ P"
by (simp add: inf.order_iff tls.terminated.inf_eventually)

lemma eq_always_terminated:
  shows "tls.terminated = □tls.terminated"
by (rule order.antisym[OF _ tls.always.contractive])
   (simp add: tls.terminated.always_le_conv)

setup ‹Sign.parent_path›


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

text‹

So-called ∗‹response› properties are of the form
‹P ⟶□ ◇Q› (pronounced ``‹P› leads to ‹Q›'', written
‹P ↝ Q›) citep‹"MannaPnueli:1991"›. This connective is similar
to the ``ensures'' modality of citet‹‹\S3.4.4› in "ChandyMisra:1989"›.

citet‹"Jackson:1998"› used the more general
``‹P› leads to ‹Q› via ‹I›'' form ‹P ⟶□ I 𝒰 Q›
to establish liveness properties in a sequential setting.

›

lemma leads_to_refl:
  shows "⊨ P ↝ P"
by (simp add: tls.validI boolean_implication.shunt_top tls.always.top_conv tls.eventually.expansive
              top.extremum_unique)

lemma leads_to_mono:
  assumes "P' ≤ P"
  assumes "Q ≤ Q'"
  shows "P ↝ Q ≤ P' ↝ Q'"
by (simp add: assms boolean_implication.mono tls.always.mono tls.eventually.mono)

lemma leads_to_supL:
  shows "(P ↝ R) ⊓ (Q ↝ R) ≤ (P ⊔ Q) ↝ R"
by (simp add: boolean_implication.conv_sup sup_inf_distrib2 tls.always.inf)

lemma always_imp_leads_to:
  shows "P ⟶□ Q ≤ P ↝ Q"
by (simp add: boolean_implication.mono tls.always.mono tls.eventually.expansive)

lemma leads_to_eventually:
  shows "◇P ⊓ (P ↝ Q) ≤ ◇Q"
by (simp add: galois.conj_imp.galois tls.always_imp_eventually_generalization)

lemma leads_to_leads_to_via:
  shows "P ⟶□ Q 𝒰 R ≤ P ↝ R"
by (simp add: boolean_implication.mono tls.always.mono tls.until.eventually_le)

lemma leads_to_trans:
  shows "P ↝ Q ⊓ Q ↝ R ≤ P ↝ R" (is "?lhs ≤ ?rhs")
proof -
  have "?lhs ≤ P ↝ Q ⊓ □(Q ↝ R)"
    by (simp add: tls.always.simps)
  also have "… ≤ P ↝ Q ⊓ ◇Q ↝ R"
    by (meson order.refl inf_mono tls.always.mono tls.always_imp_eventually_generalization)
  also have "… ≤ ?rhs"
    by (simp add: boolean_implication.trans tls.always.mono flip: tls.always.inf)
  finally show ?thesis .
qed

lemma leads_to_via_weakenR:
  shows "Q ⟶□ Q' ⊓ P ⟶□ I 𝒰 Q ≤ P ⟶□ I 𝒰 Q'"
by transfer
   (clarsimp simp: raw.always_alt_def raw.until_def boolean_implication.set_alt_def;
    metis behavior.dropn.dropn Option.bind.bind_lunit)

lemma leads_to_via_supL: ―‹ useful for case distinctions ›
  shows "P ⟶□ I 𝒰 Q ⊓ P' ⟶□ I' 𝒰 Q ≤ P ⊔ P' ⟶□ (I ⊔ I') 𝒰 Q"
by (simp add: boolean_implication.conv_sup ac_simps le_infI2 le_supI2
              monoD[OF tls.always.monotone] tls.until.mono)

lemma leads_to_via_trans:
  shows "(P ⟶□ I 𝒰 Q) ⊓ (Q ⟶□ I' 𝒰 R) ≤ P ⟶□ (I ⊔ I') 𝒰 R" (is "?lhs ≤ ?rhs")
proof -
  have "?lhs ≤ □(P ⟶B I 𝒰 (I' 𝒰 R))"
    by (subst inf.commute) (rule tls.leads_to_via_weakenR)
  also have "… ≤ ?rhs"
    by (strengthen ord_to_strengthen(1)[OF tls.until.supL_ordering_le]) (rule order.refl)
  finally show ?thesis .
qed

lemma leads_to_via_disj: ―‹ more like a chaining rule ›
  shows "(P ⟶□ I 𝒰 Q) ⊓ (Q ⟶□ I' 𝒰 R) ≤ (P ⊔ Q ⟶□ (I ⊔ I') 𝒰 R)"
by (simp add: boolean_implication_def inf.coboundedI2 le_supI2 tls.always.mono tls.until.mono)


subsubsection‹ Fairness\label{sec:tls-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, 's, 'v) tls ⇒ ('a, 's, 'v) tls ⇒ ('a, 's, 'v) tls" where
  "weakly_fair enabled taken = □enabled ⟶□ ◇taken"

lemma weakly_fair_def2:
  shows "tls.weakly_fair enabled taken = □(-(□(enabled ⊓ -taken)))"
by (simp add: tls.weakly_fair_def tls.always_def tls.eventually.sup)

lemma weakly_fair_def3:
  shows "tls.weakly_fair enabled taken = ◇□enabled ⟶B □◇taken"
by (simp add: tls.weakly_fair_def boolean_implication.conv_sup
              tls.always.neg tls.always_eventually_sup tls.eventually.neg
        flip: tls.eventually.sup)

lemma weakly_fair_def4:
  shows "tls.weakly_fair enabled taken = □◇(enabled ⟶B taken)"
by (simp add: tls.weakly_fair_def boolean_implication.conv_sup tls.always.neg tls.eventually.sup)

setup ‹Sign.mandatory_path "weakly_fair"›

lemma mono:
  assumes "P' ≤ P"
  assumes "Q ≤ Q'"
  shows "tls.weakly_fair P Q ≤ tls.weakly_fair P' Q'"
unfolding tls.weakly_fair_def
apply (strengthen ord_to_strengthen(1)[OF assms(1)])
apply (strengthen ord_to_strengthen(1)[OF assms(2)])
apply (rule order.refl)
done

lemma strengthen[strg]:
  assumes "st_ord (¬F) P P'"
  assumes "st_ord F Q Q'"
  shows "st_ord F (tls.weakly_fair P Q) (tls.weakly_fair P' Q')"
using assms by (cases F) (auto simp: tls.weakly_fair.mono)

lemma weakly_fair_triv:
  shows "□◇(-enabled) ≤ tls.weakly_fair enabled taken"
by (simp add: tls.weakly_fair_def3 boolean_implication.conv_sup tls.always.neg tls.eventually.neg)

lemma mp:
  shows "tls.weakly_fair enabled taken ⊓ □enabled ≤ ◇taken"
by (simp add: tls.weakly_fair_def boolean_implication.shunt1 tls.always.contractive)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "always"›

lemma weakly_fair:
  shows "□(tls.weakly_fair enabled taken) = tls.weakly_fair enabled taken"
by (simp add: tls.weakly_fair_def tls.always.simps)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "eventually"›

lemma weakly_fair:
  shows "◇(tls.weakly_fair enabled taken) = tls.weakly_fair enabled taken"
by (simp add: tls.weakly_fair_def4 tls.always_eventually_always_absorption)

setup ‹Sign.parent_path›

text‹

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

›

definition strongly_fair :: "('a, 's, 'v) tls ⇒ ('a, 's, 'v) tls ⇒ ('a, 's, 'v) tls" where
  "strongly_fair enabled taken = □◇enabled ⟶□ ◇taken"

lemma strongly_fair_def2:
  shows "tls.strongly_fair enabled taken = □(-□(◇enabled ⊓ -taken))"
by (simp add: tls.strongly_fair_def boolean_implication.conv_sup tls.always.neg tls.eventually.sup)

lemma strongly_fair_def3:
  shows "tls.strongly_fair enabled taken = □◇enabled ⟶B □◇taken"
by (simp add: tls.strongly_fair_def boolean_implication.conv_sup tls.always.neg tls.eventually.neg
                 tls.always_eventually_sup tls.eventually_always_eventually_absorption
        flip: tls.eventually.sup)

setup ‹Sign.mandatory_path "strongly_fair"›

lemma mono:
  assumes "P' ≤ P"
  assumes "Q ≤ Q'"
  shows "tls.strongly_fair P Q ≤ tls.strongly_fair P' Q'"
unfolding tls.strongly_fair_def
apply (strengthen ord_to_strengthen(1)[OF assms(1)])
apply (strengthen ord_to_strengthen(1)[OF assms(2)])
apply (rule order.refl)
done

lemma strengthen[strg]:
  assumes "st_ord (¬F) P P'"
  assumes "st_ord F Q Q'"
  shows "st_ord F (tls.strongly_fair P Q) (tls.strongly_fair P' Q')"
using assms by (cases F) (auto simp: tls.strongly_fair.mono)

lemma supL: ―‹ does not hold for const‹tls.weakly_fair› ›
  shows "tls.strongly_fair (enabled1 ⊔ enabled2) taken
      = (tls.strongly_fair enabled1 taken ⊓ tls.strongly_fair enabled2 taken)"
by (simp add: boolean_implication.conv_sup sup_inf_distrib2 tls.always.inf tls.always_eventually_sup
              tls.strongly_fair_def)

lemma weakly_fair_le:
  shows "tls.strongly_fair enabled taken ≤ tls.weakly_fair enabled taken"
by (simp add: tls.strongly_fair_def3 tls.weakly_fair_def3 boolean_implication.mono
              tls.eventually_always_always_eventually_le)

lemma always_enabled_weakly_fair_strongly_fair:
  shows "□enabled ≤ tls.weakly_fair enabled taken ⟷B tls.strongly_fair enabled taken"
by (simp add: boolean_eq_def boolean_implication_def)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "always"›

lemma strongly_fair:
  shows "□(tls.strongly_fair enabled taken) = tls.strongly_fair enabled taken"
by (simp add: tls.strongly_fair_def)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "eventually"›

lemma strongly_fair:
  shows "◇(tls.strongly_fair enabled taken) = tls.strongly_fair enabled taken"
by (simp add: tls.strongly_fair_def2 tls.always.neg tls.always_eventually_always_absorption)

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›


subsection‹ Safety Properties\label{sec:tls-safety} ›

text‹

We now carve the safety properties out of the typ‹('a, 's, 'v) tls› lattice.

References:
 ▪ citet‹‹\S2› in "AlpernSchneider:1985" and "AlpernDemersSchneider:1986" and "Schneider:1987"›
  ▪ observes that Lamport's earlier definitions do not work without stuttering
  ▪ provides the now standard definition that works with and without stuttering
 ▪ citet‹‹\S2.2› in "AbadiLamport:1991"›: topological definitions and intuitions
 ▪ citet‹‹\S2.2› in "Sistla:1994"›

We go a different way: we establish a Galois connection with typ‹('a, 's, 'v) spec›.

Observations:
 ▪ our safety closure for typ‹('a, 's, 'v) tls› introduces infinite sequences to stand for the
   prefixes in typ‹('a, 's, 'v) spec›
  ▪ i.e., the non-termination of trace ‹σ› (‹trace.term σ = None›)
    is represented by a behavior ending with ‹trace.final σ› infinitely stuttered
  ▪ citet‹‹\S2.1› in "AbadiLamport:1991"› consider these behaviors to represent terminating processes

›

setup ‹Sign.mandatory_path "raw"›

definition to_spec :: "('a, 's, 'v) behavior.t set ⇒ ('a, 's, 'v) trace.t set" where
  "to_spec T = {behavior.take i ω |ω i. ω ∈ T}"

definition from_spec :: "('a, 's, 'v) trace.t set ⇒ ('a, 's, 'v) behavior.t set" where
  "from_spec S = {ω . ∀i. behavior.take i ω ∈ S}"

interpretation safety: galois.powerset raw.to_spec raw.from_spec
by standard (fastforce simp: raw.to_spec_def raw.from_spec_def)

setup ‹Sign.mandatory_path "from_spec"›

lemma empty:
  shows "raw.from_spec {} = {}"
by (simp add: raw.from_spec_def)

lemma singleton:
  shows "raw.from_spec (Safety_Logic.raw.singleton σ)
       = ⋃(raw.singleton ` {ω . ∀i. behavior.take i ω ∈ Safety_Logic.raw.singleton σ})" (is "?lhs = ?rhs")
proof(rule antisym)
  show "?lhs ⊆ ?rhs" by (force simp: raw.from_spec_def TLS.raw.singleton_def)
  show "?rhs ⊆ ?lhs"
    by (clarsimp simp: raw.from_spec_def TLS.raw.singleton_def Safety_Logic.raw.singleton_def
                 elim!: behavior.stuttering.clE)
       (metis behavior.stuttering.equiv.takeE raw.spec.closed raw.spec.closed.stuttering_closed
              trace.stuttering.clI trace.stuttering.closed_conv)
qed

lemma sup:
  assumes "P ∈ raw.spec.closed"
  assumes "Q ∈ raw.spec.closed"
  shows "raw.from_spec (P ∪ Q) = raw.from_spec P ∪ raw.from_spec Q"
by (rule antisym[OF _ raw.safety.sup_upper_le])
   (clarsimp simp: raw.from_spec_def;
    meson behavior.take.mono downwards.closed_in linorder_le_cases
          raw.spec.closed.downwards_closed[OF assms(1)] raw.spec.closed.downwards_closed[OF assms(2)])

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "to_spec"›

lemma singleton:
  shows "raw.to_spec (TLS.raw.singleton ω)
       = (⋃i. Safety_Logic.raw.singleton (behavior.take i ω))" (is "?lhs = ?rhs")
proof(rule antisym)
  show "?lhs ⊆ ?rhs"
    by (fastforce simp: TLS.raw.singleton_def raw.to_spec_def
                        Safety_Logic.raw.singleton_def raw.spec.cl_def
                  elim: behavior.stuttering.clE behavior.stuttering.equiv.takeE[OF sym]
                        trace.stuttering.clI[OF _ sym, rotated])
  show "?rhs ⊆ ?lhs"
    by (fastforce simp: Safety_Logic.raw.singleton_def raw.spec.cl_def TLS.raw.singleton_def
                        raw.to_spec_def trace.less_eq_take_def trace.take.behavior.take
                  elim: downwards.clE trace.stuttering.clE trace.stuttering.equiv.behavior.takeE)
qed

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "safety"›

lemma cl_altI:
  assumes "⋀i. ∃ω' ∈ P. behavior.take i ω = behavior.take i ω'"
  shows "ω ∈ raw.safety.cl P"
using assms by (fastforce simp: raw.safety.cl_def raw.from_spec_def raw.to_spec_def)

lemma cl_altE:
  assumes "ω ∈ raw.safety.cl P"
  obtains ω' where "ω' ∈ P" and "behavior.take i ω = behavior.take i ω'"
proof(atomize_elim, cases "enat i ≤ tlength (behavior.rest ω)")
  case True with assms show "∃ω'. ω' ∈ P ∧ behavior.take i ω = behavior.take i ω'"
    by (clarsimp simp: raw.safety.cl_def raw.from_spec_def raw.to_spec_def)
       (metis behavior.take.length behavior.take.sel(3)  ttake_eq_None_conv(1)
              min.absorb2 min_enat2_conv_enat the_enat.simps)
next
  case False with assms show "∃ω'. ω' ∈ P ∧ behavior.take i ω = behavior.take i ω'"
    by (clarsimp simp: raw.safety.cl_def raw.from_spec_def raw.to_spec_def)
       (metis behavior.continue.take_drop_id behavior.take.continue_id leI)
qed

lemma cl_alt_def: ―‹ citet‹"AlpernDemersSchneider:1986"›: the classical definition: ‹ω› belongs to the safety closure of ‹P› if every prefix of ‹ω› can be extended to a behavior in ‹P› ›
  shows "raw.safety.cl P = {ω. ∀i. ∃β. behavior.take i ω @-B β ∈ P}" (is "?lhs = ?rhs")
proof(rule antisym)
  show "?lhs ⊆ ?rhs"
    by clarsimp (metis behavior.continue.take_drop_id raw.safety.cl_altE)
  show "?rhs ⊆ ?lhs"
  proof(clarify intro!: raw.safety.cl_altI)
    fix ω i
    assume "∀j. ∃β. behavior.take j ω @-B β ∈ P"
    then show "∃ω'∈P. behavior.take i ω = behavior.take i ω'"
      by (force dest: spec[where x=i]
               intro: exI[where x=i] rev_bexI
                simp: behavior.take.continue trace.take.behavior.take trace.continue.self_conv
                      ttake_eq_None_conv length_ttake
               split: option.split enat.split)
  qed
qed

lemma closed_alt_def: ―‹ If ‹ω› is not in ‹P› then some prefix of ‹ω› has irretrievably gone wrong ›
  shows "raw.safety.closed = {P. ∀ω. ω ∉ P ⟶ (∃i. ∀β. behavior.take i ω @-B β ∉ P)}"
unfolding raw.safety.closed_def raw.safety.cl_alt_def by fast

lemma closed_alt_def2: ―‹ Contraposition gives the customary prefix-closure definition ›
  shows "raw.safety.closed = {P. ∀ω. (∀i. ∃β. behavior.take i ω @-B β ∈ P) ⟶ ω ∈ P}"
unfolding raw.safety.closed_alt_def by fast

lemma closedI2:
  assumes "⋀ω. (⋀i. ∃β. behavior.take i ω @-B β ∈ P) ⟹ ω ∈ P"
  shows "P ∈ raw.safety.closed"
using assms unfolding raw.safety.closed_alt_def2 by fast

lemma closedE2:
  assumes "P ∈ raw.safety.closed"
  assumes "⋀i. ω ∉ P ⟹ ∃β. behavior.take i ω @-B β ∈ P"
  shows "ω ∈ P"
using assms unfolding raw.safety.closed_alt_def2 by blast

setup ‹Sign.mandatory_path "cl"›

lemma state_prop:
  shows "raw.safety.cl (raw.state_prop P) = raw.state_prop P"
by (simp add: raw.safety.cl_alt_def raw.state_prop_def)

lemma terminated_iff:
  assumes "ω ∈ raw.terminated"
  shows "ω ∈ raw.safety.cl P ⟷ ω ∈ P" (is "?lhs ⟷ ?rhs")
proof(rule iffI)
  from assms obtain i where "tlength (behavior.rest ω) = enat i"
    by (clarsimp simp: raw.terminated_def tfinite_tlength_conv)
  then show "?lhs ⟹ ?rhs"
    by (metis raw.safety.cl_altE[where i="Suc i"]
              behavior.continue.take_drop_id behavior.take.continue_id enat_ord_simps(2) lessI)
qed (simp add: raw.safety.expansive')

lemma terminated:
  shows "raw.safety.cl raw.terminated = raw.idle ∪ raw.terminated" (is "?lhs = ?rhs")
proof(rule antisym[OF subsetI subsetI])
  fix ω
  assume "ω ∈ ?lhs"
  then have "snd (tnth (behavior.rest ω) i) = behavior.init ω"
         if "enat i < tlength (behavior.rest ω)"
        for i
    using that
    by (clarsimp simp: raw.terminated_def behavior.take_def behavior.split_all behavior.sset.simps
                       split_def
             simp del: ttake.simps
                elim!: raw.safety.cl_altE[where i="Suc i"])
       (metis (no_types, lifting) Suc_ile_eq in_tset_conv_tnth nth_ttake
              doubleton_eq_iff insert_image insert_absorb2 lessI subset_singletonD ttake_eq_None_conv(1))
  then have "behavior.sset ω ⊆ {behavior.init ω}"
    by (cases ω) (clarsimp simp: behavior.sset.simps tset_conv_tnth)
  then show "ω ∈ ?rhs"
    by (simp add: raw.idle_alt_def raw.terminated_def)
next
  show "ω ∈ ?lhs" if "ω ∈ ?rhs" for ω
    using that
  proof(cases rule: UnE[consumes 1, case_names idle terminated])
    case idle show ?thesis
    proof(rule raw.safety.cl_altI)
      fix i
      let ?ω' = "behavior.take i ω @-B TNil undefined"
      from idle have "?ω' ∈ raw.terminated"
        by (auto simp: raw.idle_alt_def raw.terminated_def behavior.sset.continue
                 dest: subsetD[OF behavior.sset.take_le]
                split: option.split)
      moreover
      from idle have "behavior.take i ω = behavior.take i ?ω'"
        by (simp add: raw.idle_alt_def behavior.take.continue trace.take.behavior.take
                      length_ttake tfinite_tlength_conv)
      ultimately show "∃ω'∈raw.terminated. behavior.take i ω = behavior.take i ω'"
        by blast
    qed
  qed (auto intro: raw.safety.expansive')
qed

lemma le_terminated_bot:
  assumes "P ∈ behavior.stuttering.closed"
  assumes "raw.safety.cl P ⊆ raw.terminated"
  shows "P = {}"
proof(rule ccontr)
  assume ‹P ≠ {}› then obtain ω where "ω ∈ P" by blast
  let ?ω' = "behavior.B (behavior.init ω) (trepeat (undefined, behavior.init ω))"
  from ‹ω ∈ P› have "?ω' ∈ raw.safety.cl P"
    by (fastforce intro: exI[where x="behavior.rest ω"]
                         behavior.stuttering.f_closedI[OF ‹P ∈ behavior.stuttering.closed›]
                   simp: raw.safety.cl_alt_def behavior.take.trepeat behavior.continue.simps
                         behavior.natural.tshift collapse.tshift trace.natural'.replicate
                         trace.final'.replicate
                         behavior.stuttering.f_closed[OF ‹P ∈ behavior.stuttering.closed›]
              simp flip: behavior.natural_def)
  moreover have "?ω' ∉ raw.terminated"
    by (simp add: raw.terminated_def)
  moreover note ‹raw.safety.cl P ⊆ raw.terminated›
  ultimately show False by blast
qed

lemma always_le:
  shows "raw.safety.cl (raw.always P) ⊆ raw.always (raw.safety.cl P)"
unfolding raw.always_alt_def raw.safety.cl_alt_def subset_iff mem_Collect_eq
proof(intro allI impI)
  fix ω i ω' j
  assume *: "∀i. ∃β. ∀k ω'. behavior.dropn k (behavior.take i ω @-B β) = Some ω' ⟶ ω' ∈ P"
     and **: "behavior.dropn i ω = Some ω'"
  from spec[where x="i + j", OF *] ** behavior.take.dropn[OF **, where j=j]
  show "∃β. behavior.take j ω' @-B β ∈ P"
    by (clarsimp dest!: spec[where x=i])
       (subst (asm) behavior.dropn.continue_shorter;
        force simp: length_ttake trace.dropn.behavior.take
              dest: behavior.dropn.eq_Some_tlengthD
             split: enat.split)
qed

lemma eventually:
  assumes "P ≠ ⊥"
  shows "raw.safety.cl (raw.eventually P)
      = -raw.eventually raw.terminated ∪ raw.eventually P" (is "?lhs = ?rhs")
proof(rule antisym[OF subsetI iffD2[OF Un_subset_iff, simplified conj_explode, rule_format, OF subsetI]])
  show "ω ∈ ?rhs" if "ω ∈ ?lhs" for ω
  proof(cases "tlength (behavior.rest ω)")
    case (enat i) with that show ?thesis
      by (fastforce dest: spec[where x="Suc i"]
                    simp: raw.safety.cl_alt_def raw.terminated_def behavior.take.continue_id)
  qed (simp add: raw.eventually.terminated tfinite_tlength_conv)
  from assms obtain ωP where "ωP ∈ P" by blast
  show "ω ∈ ?lhs" if "ω ∈ -raw.eventually raw.terminated" for ω
  proof(intro raw.safety.cl_altI exI bexI)
    fix i
    let ?ω' = "behavior.take i ω @-B TCons (undefined, behavior.init ωP) (behavior.rest ωP)"
    from ‹ωP ∈ P› ‹ω ∈ -raw.eventually raw.terminated› show "?ω' ∈ raw.eventually P"
      unfolding raw.eventually.terminated
      by (auto intro!: exI[where x="Suc i"]
                 simp: raw.eventually_alt_def tfinite_tlength_conv behavior.dropn.continue
                       length_ttake ttake_eq_None_conv)
    from ‹ω ∈ -raw.eventually raw.terminated› show "behavior.take i ω = behavior.take i ?ω'"
      by (simp add: raw.eventually.terminated behavior.take.continue trace.take.behavior.take
                    length_ttake tfinite_tlength_conv
             split: enat.split)
  qed
  show "raw.eventually P ⊆ ?lhs"
    by (fast intro!: order.trans[OF _ raw.safety.expansive])
qed

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "closed"›

lemma always_eventually:
  assumes "P ∈ raw.safety.closed"
  assumes "∀i. ∃j≥i. ∃β. behavior.take j ω @-B β ∈ P"
  shows "ω ∈ P"
using assms(1)
proof(rule raw.safety.closedE2)
  fix i
  from spec[OF assms(2), where x=i] obtain j β where "i ≤ j" and "behavior.take j ω @-B β ∈ P"
    by blast
  then show "∃β. behavior.take i ω @-B β ∈ P" if "ω ∉ P"
    using that
    by (clarsimp simp: tdropn_tshift2 behavior.continue.tshift2 behavior.continue.take_drop_shorter length_ttake
                        behavior.continue.term_Some behavior.take.term_Some_conv ttake_eq_Some_conv
                split: enat.split split_min
               intro!: exI[where x="tdropn i (behavior.rest (behavior.take j ω @-B β))"])
qed

lemma sup:
  assumes "P ∈ raw.safety.closed"
  assumes "Q ∈ raw.safety.closed"
  shows "P ∪ Q ∈ raw.safety.closed"
by (clarsimp simp: raw.safety.closed_alt_def2)
   (meson assms raw.safety.closed.always_eventually sup.cobounded1 sup.cobounded2)

lemma unless: ―‹ citet‹ ‹\S3.1› in "Sistla:1994"› -- minimality is irrelevant ›
  assumes "P ∈ raw.safety.closed"
  assumes "Q ∈ raw.safety.closed"
  shows "raw.unless P Q ∈ raw.safety.closed"
proof(rule raw.safety.closedI2)
  fix ω assume *: "∃β. behavior.take i ω @-B β ∈ raw.unless P Q" for i
  show "ω ∈ raw.unless P Q"
  proof(cases "∀i j ω'. ∃β. behavior.dropn i ω = Some ω' ⟶ behavior.take j ω' @-B β ∈ P")
    case True
    with ‹P ∈ raw.safety.closed› have "behavior.dropn i ω = Some ω' ⟶ ω' ∈ P" for i ω'
      by (blast intro: raw.safety.closedE2)
    then show ?thesis
      by (simp add: raw.always_alt_def)
  next
    case False
    then obtain ω' k l
      where **: "behavior.dropn k ω = Some ω'" "∀β. behavior.take l ω' @-B β ∉ P"
      by clarsimp
    {
      fix i β
      assume kli: "k + l ≤ i"
      moreover
      note **
      moreover
      from kli have "∃j. i - k = l + j" by presburger
      moreover
      from ‹behavior.dropn k ω = Some ω'› kli
      have ***: "k ≤ length (trace.rest (behavior.take i ω))"
        by (fastforce simp: length_ttake split: enat.splits
                      dest: behavior.dropn.eq_Some_tlengthD)
      ultimately have ****: "∀ω''. behavior.dropn k (behavior.take i ω @-B β) = Some ω'' ⟶ ω'' ∉ P"
        by (force simp: behavior.dropn.continue_shorter trace.dropn.behavior.take behavior.take.add
             simp flip: behavior.continue.tshift2)
      {
        assume PQ: "behavior.take i ω @-B β ∈ raw.unless P Q"
        from **** PQ obtain m
          where "m ≤ k"
            and "∀ω'. behavior.dropn m (behavior.take i ω @-B β) = Some ω' ⟶ ω' ∈ Q"
            and "∀p<m. (∀ω'. behavior.dropn p (behavior.take i ω @-B β) = Some ω' ⟶ ω' ∈ P)"
          by (auto 6 0 simp: raw.until_def raw.always_alt_def)
             (metis behavior.dropn.shorterD leI nle_le option.sel)
        with kli ***
        have "(∃m≤k. (∀ω'. behavior.dropn m ω = Some ω' ⟶ behavior.take (i - m) ω' @-B β ∈ Q)
                   ∧ (∀p<m. (∀ω'. behavior.dropn p ω = Some ω' ⟶ behavior.take (i - p) ω' @-B β ∈ P)))"
          by (clarsimp simp: exI[where x=m] behavior.dropn.continue_shorter trace.dropn.behavior.take)
      }
    }
    then have "∀i. ∃n≥i. ∃m≤k. ∃β. (∀ω'. behavior.dropn m ω = Some ω' ⟶ behavior.take (n - m) ω' @-B β ∈ Q)
                                  ∧ (∀p<m. ∀ω'. behavior.dropn p ω = Some ω' ⟶ behavior.take (n - p) ω' @-B β ∈ P)"
      using * by (metis nle_le)
    then obtain m
      where "m ≤ k" "∀i. ∃n≥i. ∃β. (∀ω'. behavior.dropn m ω = Some ω' ⟶ behavior.take (n - m) ω' @-B β ∈ Q)
                              ∧ (∀p<m. ∀ω'. behavior.dropn p ω = Some ω' ⟶ behavior.take (n - p) ω' @-B β ∈ P)"
      by (clarsimp simp: always_eventually_pigeonhole)
    with behavior.dropn.shorterD[OF ‹behavior.dropn k ω = Some ω'› ‹m ≤ k›]
         raw.safety.closed.always_eventually[OF ‹P ∈ raw.safety.closed›]
         raw.safety.closed.always_eventually[OF ‹Q ∈ raw.safety.closed›]
    show "ω ∈ raw.unless P Q"
      apply -
      apply clarsimp
      apply (rule raw.untilI, assumption)
       apply (meson add_le_imp_le_diff)
      apply (metis add_le_imp_le_diff option.sel behavior.dropn.shorterD[OF _ less_imp_le])
      done
  qed
qed

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "downwards.closed"›

lemma to_spec:
  shows "range raw.to_spec ⊆ downwards.closed"
by (fastforce elim: downwards.clE simp: raw.to_spec_def trace.less_eq_take_def trace.take.behavior.take)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "trace.stuttering.closed"›

lemma to_spec:
  shows "raw.to_spec ` behavior.stuttering.closed ⊆ trace.stuttering.closed"
by (fastforce simp: raw.to_spec_def
              elim: trace.stuttering.clE trace.stuttering.equiv.E trace.stuttering.equiv.behavior.takeE
              dest: behavior.stuttering.closed_in)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "raw.spec.closed"›

lemma to_spec:
  shows "raw.to_spec ` behavior.stuttering.closed ⊆ raw.spec.closed"
using downwards.closed.to_spec trace.stuttering.closed.to_spec by (blast intro: raw.spec.closed.I)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "behavior.stuttering.closed"›

lemma from_spec:
  shows "raw.from_spec ` trace.stuttering.closed
      ⊆ (behavior.stuttering.closed :: ('a, 's, 'v) behavior.t set set)"
proof -
  have *: "behavior.take i ω2 ∈ P "
    if "ω1 ≃T ω2" and "∀i. behavior.take i ω1 ∈ P" and "P ∈ trace.stuttering.closed"
   for ω1 ω2 i and P :: "('a, 's, 'v) trace.t set"
    using that(2-)
    by - (rule behavior.stuttering.equiv.takeE[OF sym[OF ‹ω1 ≃T ω2›], where i=i];
          fastforce intro: trace.stuttering.closed_in)
  show ?thesis
    by (fastforce simp: raw.from_spec_def elim: behavior.stuttering.clE *)
qed

lemma safety_cl:
  assumes "P ∈ behavior.stuttering.closed"
  shows "raw.safety.cl P ∈ behavior.stuttering.closed"
unfolding raw.safety.cl_def using assms
by (blast intro: subsetD[OF behavior.stuttering.closed.from_spec]
                 subsetD[OF trace.stuttering.closed.to_spec])

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "tls"›

lift_definition to_spec :: "('a, 's, 'v) tls ⇒ ('a, 's, 'v) spec" is raw.to_spec
using raw.spec.closed.to_spec by blast

lift_definition from_spec :: "('a, 's, 'v) spec ⇒ ('a, 's, 'v) tls" is raw.from_spec
by (meson image_subset_iff behavior.stuttering.closed.from_spec raw.spec.closed.stuttering_closed)

interpretation safety: galois.complete_lattice_class tls.to_spec tls.from_spec
by standard (transfer; simp add: raw.safety.galois)

setup ‹Sign.mandatory_path "from_spec"›

lemma singleton:
  notes spec.singleton.transfer[transfer_rule]
  shows "tls.from_spec (spec.singleton σ)
       = ⨆(tls.singleton ` {ω . ∀i. behavior.take i ω ∈ Safety_Logic.raw.singleton σ})"
by transfer (simp add: behavior.stuttering.cl_bot raw.from_spec.singleton)

lemmas bot = raw.from_spec.empty[transferred]

lemma sup:
  shows "tls.from_spec (P ⊔ Q) = tls.from_spec P ⊔ tls.from_spec Q"
by transfer (rule raw.from_spec.sup)

lemmas Inf = tls.safety.upper_Inf
lemmas inf = tls.safety.upper_inf

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "to_spec"›

lemma singleton:
  notes spec.singleton.transfer[transfer_rule]
  shows "tls.to_spec (tls.singleton ω) = (⨆i. spec.singleton (behavior.take i ω))"
by transfer (simp add: raw.to_spec.singleton)

lemmas bot = tls.safety.lower_bot

lemmas Sup = tls.safety.lower_Sup
lemmas sup = tls.safety.lower_sup

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "safety"›

setup ‹Sign.mandatory_path "cl"›

lemma transfer[transfer_rule]:
  shows "rel_fun (pcr_tls (=) (=) (=)) (pcr_tls (=) (=) (=)) raw.safety.cl tls.safety.cl"
unfolding raw.safety.cl_def tls.safety.cl_def by transfer_prover

lemma bot[iff]:
  shows "tls.safety.cl ⊥ = ⊥"
by (simp add: tls.safety.cl_def tls.from_spec.bot tls.safety.lower_bot)

lemma sup:
  shows "tls.safety.cl (P ⊔ Q) = tls.safety.cl P ⊔ tls.safety.cl Q"
by (simp add: tls.safety.cl_def tls.from_spec.sup tls.to_spec.sup)

lemmas state_prop = raw.safety.cl.state_prop[transferred]
lemmas always_le = raw.safety.cl.always_le[transferred]

lemma eventually: ―‹ all the infinite traces and any finite ones that satisfy ‹◇P› ›
  assumes "P ≠ ⊥"
  shows "tls.safety.cl (◇P) = -◇tls.terminated ⊔ ◇P"
using assms by transfer (rule raw.safety.cl.eventually)

lemma terminated_iff:
  assumes "⦉ω⦊T ≤ tls.terminated"
  shows "⦉ω⦊T ≤ tls.safety.cl P ⟷ ⦉ω⦊T ≤ P" (is "?lhs ⟷ ?rhs")
using assms
by transfer
   (simp add: raw.singleton_def behavior.stuttering.least_conv raw.safety.cl.terminated_iff
              behavior.stuttering.closed.safety_cl behavior.stuttering.closed.raw.terminated)

lemma terminated:
  shows "tls.safety.cl tls.terminated = tls.idle ⊔ tls.terminated"
by transfer (simp add: raw.safety.cl.terminated)

lemma not_terminated:
  shows "tls.safety.cl (- tls.terminated) = - tls.terminated" (is "?lhs = ?rhs")
proof -
  have "?lhs = tls.safety.cl (◇(- tls.terminated))"
    by (simp flip: tls.always.neg tls.terminated.eq_always_terminated)
  also have "… = - ◇tls.terminated ⊔ ◇(- tls.terminated)"
    by (metis tls.safety.cl.eventually tls.terminated.not_top
              boolean_algebra.compl_zero boolean_algebra_class.boolean_algebra.double_compl)
  also have "… = ?rhs"
    by (simp add: sup.absorb2 tls.eventually.expansive
            flip: tls.always.neg tls.terminated.eq_always_terminated)
  finally show ?thesis .
qed

lemma le_terminated_conv:
  shows "tls.safety.cl P ≤ tls.terminated ⟷ P = ⊥" (is "?lhs ⟷ ?rhs")
proof(rule iffI)
  show "?lhs ⟹ ?rhs"
    by transfer (rule raw.safety.cl.le_terminated_bot)
  show "?rhs ⟹ ?lhs"
    by simp
qed

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "closed"›

lemma transfer[transfer_rule]:
  shows "rel_set (pcr_tls (=) (=) (=))
                 (behavior.stuttering.closed ∩ raw.safety.closed)
                 tls.safety.closed" (is "rel_set _ ?lhs ?rhs")
proof(rule rel_setI)
  fix X assume "X ∈ ?lhs" then show "∃Y∈?rhs. pcr_tls (=) (=) (=) X Y"
    by (metis (no_types, opaque_lifting) raw.safety.cl_def raw.safety.closed_conv tls.safety.closed_upper
              tls.from_spec.rep_eq TLS_inverse cr_tls_def tls.pcr_cr_eq tls.to_spec.rep_eq Int_iff)
next
  fix Y assume "Y ∈ ?rhs" then show "∃X∈?lhs. pcr_tls (=) (=) (=) X Y"
    by (metis tls.safety.cl_def tls.safety.closed_conv tls.from_spec.rep_eq
              tls.pcr_cr_eq cr_tls_def unTLS raw.safety.closed_upper Int_iff)
qed

lemma bot:
  shows "⊥ ∈ tls.safety.closed"
by (simp add: tls.safety.closed_clI)

lemma sup:
  assumes "P ∈ tls.safety.closed"
  assumes "Q ∈ tls.safety.closed"
  shows "P ⊔ Q ∈ tls.safety.closed"
by (simp add: assms tls.safety.closed_clI tls.safety.cl.sup flip: tls.safety.closed_conv)

lemmas inf = tls.safety.closed_inf

lemma boolean_implication:
  assumes "-P ∈ tls.safety.closed"
  assumes "Q ∈ tls.safety.closed"
  shows "P ⟶B Q ∈ tls.safety.closed"
by (simp add: assms boolean_implication.conv_sup tls.safety.closed.sup)

lemma state_prop:
  shows "tls.state_prop P ∈ tls.safety.closed"
by (simp add: tls.safety.closed_clI tls.safety.cl.state_prop)

lemma not_terminated:
  shows "- tls.terminated ∈ tls.safety.closed"
by (simp add: tls.safety.closed_clI tls.safety.cl.not_terminated)

lemma unless:
  assumes "P ∈ tls.safety.closed"
  assumes "Q ∈ tls.safety.closed"
  shows "tls.unless P Q ∈ tls.safety.closed"
using assms by transfer (blast intro: raw.safety.closed.unless)

lemma always:
  assumes "P ∈ tls.safety.closed"
  shows "tls.always P ∈ tls.safety.closed"
by (simp add: assms tls.always_alt_def tls.safety.closed.bot tls.safety.closed.unless)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "cl"›

lemma until_unless_le:
  assumes "P ∈ tls.safety.closed"
  assumes "Q ∈ tls.safety.closed"
  shows "tls.safety.cl (tls.until P Q) ≤ tls.unless P Q"
by (simp add: order.trans[OF tls.safety.cl_inf_le] tls.until.eq_unless_inf_eventually
        flip: tls.safety.closed_conv[OF tls.safety.closed.unless[OF assms]])

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "singleton"›

lemma to_spec_le_conv[tls.singleton.le_conv]:
  notes spec.singleton.transfer[transfer_rule]
  shows "⦉σ⦊ ≤ tls.to_spec P ⟷ (∃ω i. ⦉ω⦊T ≤ P ∧ σ = behavior.take i ω)"
by transfer
   (simp add: TLS.raw.singleton_def behavior.stuttering.least_conv Safety_Logic.raw.singleton_def
              raw.spec.least_conv[OF subsetD[OF raw.spec.closed.to_spec]];
    fastforce simp: raw.to_spec_def)

lemma from_spec_le_conv[tls.singleton.le_conv]:
  notes spec.singleton.transfer[transfer_rule]
  shows "⦉ω⦊T ≤ tls.from_spec P ⟷ (∀i. ⦉behavior.take i ω⦊ ≤ P)"
by transfer
   (simp add: TLS.raw.singleton_def Safety_Logic.raw.singleton_def raw.spec.least_conv
              behavior.stuttering.least_conv
              subsetD[OF behavior.stuttering.closed.from_spec
                         imageI[OF raw.spec.closed.stuttering_closed]];
    simp add: raw.from_spec_def)

lemma safety_cl_le_conv[tls.singleton.le_conv]:
  shows "⦉ω⦊T ≤ tls.safety.cl P ⟷ (∀i. ∃ω'. ⦉ω'⦊T ≤ P ∧ behavior.take i ω = behavior.take i ω')"
by transfer
   (simp add: TLS.raw.singleton_def behavior.stuttering.least_conv behavior.stuttering.closed.safety_cl;
    fastforce intro: raw.safety.cl_altI
               elim: raw.safety.cl_altE)

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›


subsection‹ Maps\label{sec:tls-maps} ›

setup ‹Sign.mandatory_path "tls"›

definition map :: "('a ⇒ 'b) ⇒ ('s ⇒ 't) ⇒ ('v ⇒ 'w) ⇒ ('a, 's, 'v) tls ⇒ ('b, 't, 'w) tls" where
  "map af sf vf P = ⨆(tls.singleton ` behavior.map af sf vf ` {σ. ⦉σ⦊T ≤ P})"

definition invmap :: "('a ⇒ 'b) ⇒ ('s ⇒ 't) ⇒ ('v ⇒ 'w) ⇒ ('b, 't, 'w) tls ⇒ ('a, 's, 'v) tls" where
  "invmap af sf vf P = ⨆(tls.singleton ` behavior.map af sf vf -` {σ. ⦉σ⦊T ≤ P})"

abbreviation amap ::"('a ⇒ 'b) ⇒ ('a, 's, 'v) tls ⇒ ('b, 's, 'v) tls" where
  "amap af ≡ tls.map af id id"
abbreviation ainvmap ::"('a ⇒ 'b) ⇒ ('b, 's, 'v) tls ⇒ ('a, 's, 'v) tls" where
  "ainvmap af ≡ tls.invmap af id id"
abbreviation smap ::"('s ⇒ 't) ⇒ ('a, 's, 'v) tls ⇒ ('a, 't, 'v) tls" where
  "smap sf ≡ tls.map id sf id"
abbreviation sinvmap ::"('s ⇒ 't) ⇒ ('a, 't, 'v) tls ⇒ ('a, 's, 'v) tls" where
  "sinvmap sf ≡ tls.invmap id sf id"
abbreviation vmap ::"('v ⇒ 'w) ⇒ ('a, 's, 'v) tls ⇒ ('a, 's, 'w) tls" where ―‹ aka ‹liftM› ›
  "vmap vf ≡ tls.map id id vf"
abbreviation vinvmap ::"('v ⇒ 'w) ⇒ ('a, 's, 'w) tls ⇒ ('a, 's, 'v) tls" where
  "vinvmap vf ≡ tls.invmap id id vf"

interpretation map_invmap: galois.complete_lattice_distributive_class
  "tls.map af sf vf"
  "tls.invmap af sf vf" for af sf vf
proof standard
  show "tls.map af sf vf P ≤ Q ⟷ P ≤ tls.invmap af sf vf Q" (is "?lhs ⟷ ?rhs") for P Q
  proof(rule iffI)
    show "?lhs ⟹ ?rhs"
      by (fastforce simp: tls.map_def tls.invmap_def intro: tls.singleton_le_extI)
    show "?rhs ⟹ ?lhs"
      by (fastforce simp: tls.map_def tls.invmap_def tls.singleton_le_conv
                    dest: order.trans[of _ P] behavior.stuttering.equiv.map[where af=af and sf=sf and vf=vf]
                    cong: tls.singleton_cong)
  qed
  show "tls.invmap af sf vf (⨆X) ≤ ⨆(tls.invmap af sf vf ` X)" for X
    by (fastforce simp: tls.invmap_def)
qed

setup ‹Sign.mandatory_path "singleton"›

lemma map_le_conv[tls.singleton.le_conv]:
  shows "⦉ω⦊T ≤ tls.map af sf vf P ⟷ (∃ω'. ⦉ω'⦊T ≤ P ∧ ⦉ω⦊T ≤ ⦉behavior.map af sf vf ω'⦊T)"
by (simp add: tls.map_def)

lemma invmap_le_conv[tls.singleton.le_conv]:
  shows "⦉ω⦊T ≤ tls.invmap af sf vf P ⟷ ⦉behavior.map af sf vf ω⦊T ≤ P"
by (simp add: tls.invmap_def tls.singleton_le_conv)
   (metis behavior.natural.map_natural tls.singleton_eq_conv)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "map"›

lemmas bot = tls.map_invmap.lower_bot

lemmas monotone = tls.map_invmap.monotone_lower
lemmas mono = monotoneD[OF tls.map.monotone]

lemmas Sup = tls.map_invmap.lower_Sup
lemmas sup = tls.map_invmap.lower_sup

lemmas Inf_le = tls.map_invmap.lower_Inf_le ―‹ Converse does not hold ›
lemmas inf_le = tls.map_invmap.lower_inf_le ―‹ Converse does not hold ›

lemmas invmap_le = tls.map_invmap.lower_upper_contractive

lemma singleton:
  shows "tls.map af sf vf ⦉ω⦊T = ⦉behavior.map af sf vf ω⦊T"
by (auto simp: tls.map_def order.eq_iff tls.singleton_le_conv intro: behavior.stuttering.equiv.map)

lemma top:
  assumes "surj af"
  assumes "surj sf"
  assumes "surj vf"
  shows "tls.map af sf vf ⊤ = ⊤"
by (rule antisym)
   (auto simp: assms tls.singleton.top tls.map.Sup tls.map.singleton surj_f_inv_f
        intro: exI[where x="behavior.map (inv af) (inv sf) (inv vf) σ" for σ])

lemma id:
  shows "tls.map id id id P = P"
    and "tls.map (λx. x) (λx. x) (λx. x) P = P"
by (simp_all add: tls.map_def flip: id_def)

lemma comp:
  shows "tls.map af sf vf ∘ tls.map ag sg vg = tls.map (af ∘ ag) (sf ∘ sg) (vf ∘ vg)" (is "?lhs = ?rhs")
    and "tls.map af sf vf (tls.map ag sg vg P) = tls.map (λa. af (ag a)) (λs. sf (sg s)) (λv. vf (vg v)) P" (is ?thesis1)
proof -
  have "?lhs P = ?rhs P" for P
    by (rule tls.singleton.exhaust[where x=P])
       (simp add: tls.map.Sup tls.map.singleton map_prod.comp image_image comp_def)
  then show "?lhs = ?rhs" and ?thesis1 by (simp_all add: comp_def)
qed

lemmas map = tls.map.comp

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "invmap"›

lemmas bot = tls.map_invmap.upper_bot
lemmas top = tls.map_invmap.upper_top

lemmas monotone = tls.map_invmap.monotone_upper
lemmas mono = monotoneD[OF tls.invmap.monotone]

lemmas Sup = tls.map_invmap.upper_Sup
lemmas sup = tls.map_invmap.upper_sup

lemmas Inf = tls.map_invmap.upper_Inf
lemmas inf = tls.map_invmap.upper_inf

lemma singleton:
  shows "tls.invmap af sf vf ⦉ω⦊T = ⨆(tls.singleton ` {ω'. ⦉behavior.map af sf vf ω'⦊T ≤ ⦉ω⦊T})"
by (simp add: tls.invmap_def)

lemma id:
  shows "tls.invmap id id id P = P"
    and "tls.invmap (λx. x) (λx. x) (λx. x) P = P"
unfolding id_def[symmetric] by (metis tls.map.id(1) tls.map_invmap.lower_upper_lower(2))+

lemma comp:
  shows "tls.invmap af sf vf (tls.invmap ag sg vg P) = tls.invmap (λx. ag (af x)) (λs. sg (sf s)) (λv. vg (vf v)) P"  (is "?lhs P = ?rhs P")
    and "tls.invmap af sf vf ∘ tls.invmap ag sg vg = tls.invmap (ag ∘ af) (sg ∘ sf) (vg ∘ vf)" (is ?thesis1)
proof -
  show "?lhs P = ?rhs P" for P
    by (auto intro: tls.singleton.antisym tls.singleton_le_extI simp: tls.singleton.le_conv)
  then show ?thesis1
    by (simp add: fun_eq_iff comp_def)
qed

lemmas invmap = tls.invmap.comp

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "to_spec"›

lemma map:
  shows "tls.to_spec (tls.map af sf vf P) = spec.map af sf vf (tls.to_spec P)"
by (rule tls.singleton.exhaust[of P])
   (simp add: tls.map.Sup tls.map.singleton spec.map.Sup spec.map.singleton image_image
              tls.to_spec.singleton tls.to_spec.Sup behavior.take.map)

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›


subsection‹ Abadi's axioms for TLA\label{sec:tls-abadi_axioms} ›

text‹

The axioms for ``propositional'' TLA due to citet‹"Abadi:1990"› hold in this model.
These are complete for const‹tls.always› and const‹tls.eventually›.

Observations:
 ▪ Abadi says that the temporal system is D aka S4.3Dum; see citet‹‹\S8› in "Goldblatt:1992"›
  ▪ the only interesting axiom here is 5: the discrete-time Dummett axiom
 ▪ ``propositional'' means that actions are treated separately; we omit this part as we don't have actions ala TLA

›

setup ‹Sign.mandatory_path "tls.Abadi"›

lemma Ax1:
  shows "⊨ □(P ⟶B Q)⟶B □P ⟶B □Q"
by (simp add: tls.valid_def boolean_implication.shunt_top tls.always.always_imp_le)

lemma Ax2:
  shows "⊨ □P ⟶B P"
by (simp add: tls.valid_def boolean_implication.shunt_top tls.always.contractive)

lemma Ax3:
  shows "⊨ □P ⟶B □□P"
by (simp add: tls.validI)

lemma Ax4:
   ―‹ ``a classical way to express that time is linear -- that any two instants in the future are ordered''
       citet‹‹(254) Lemmon formula› in "WarfordVegaStaley:2020"› ›
  shows "⊨ □(□P ⟶B Q) ⊔ □(□Q ⟶B P)"
proof -
  have "⊨ (-□P) 𝒲 □Q ⊔ (-□Q) 𝒲 □P" by (rule tls.unless.ordering)
  also have "… ≤ □((-□P) 𝒲 □Q) ⊔ □((-□Q) 𝒲 □P)"
    by (metis sup_mono tls.always.idempotent tls.unless.alwaysR_le)
  also have "… ≤ □(-□P ⊔ Q) ⊔ □(-□Q ⊔ P)"
    by (strengthen ord_to_strengthen(1)[OF tls.unless.sup_le])
       (meson order.refl sup_mono tls.always.contractive tls.always.mono)
  also have "… = □(□P ⟶B Q) ⊔ □(□Q ⟶B P)"
    by (simp add: boolean_implication.conv_sup)
  finally show ?thesis .
qed

lemma Ax5:
  ―‹ ``expresses the discreteness of time''
      See also citet‹‹\S4.1 ``the Dummett formula''› in "WarfordVegaStaley:2020"›: for them
      ``next'' encodes discreteness ›
  fixes P :: "('a, 's, 'v) tls"
  shows "⊨ □(□(P ⟶B □P) ⟶B P) ⟶B ◇□P ⟶B P" (is "⊨ ?goal")
proof -
  have raw_Ax5: "raw.always (raw.eventually (P ∩ raw.eventually (-P)) ∪ P)
                   ∩ raw.eventually (raw.always P)
               ⊆ P" (is "?lhs ⊆ ?rhs")
   for P :: "('a, 's, 'v) behavior.t set"
proof(rule subsetI)
  fix ω assume "ω ∈ ?lhs"
  from IntD2[OF ‹ω ∈ ?lhs›]
  obtain i
    where "∃ω'. behavior.dropn i ω = Some ω' ∧ ω' ∈ raw.always P"
    by (force simp: raw.always_alt_def raw.eventually_alt_def)
  then obtain i
    where i: "∃ω'. behavior.dropn i ω = Some ω' ∧ ω' ∈ raw.always P"
      and "∀j<i. ∀ω'. behavior.dropn j ω = Some ω' ⟶ ω' ∉ raw.always P"
    using ex_has_least_nat[where k=i and P="λi. ∃ω'. behavior.dropn i ω = Some ω' ∧ ω' ∈ raw.always P" and m=id]
    by (auto dest: leD)
  have "∃ω'. behavior.dropn (i - j) ω = Some ω' ∧ ω' ∈ raw.always P" for j
  proof(induct j)
    case (Suc j) show ?case
    proof(cases "j < i")
      case True show ?thesis
      proof(rule ccontr)
        assume "∄ω'. behavior.dropn (i - Suc j) ω = Some ω' ∧ ω' ∈ raw.always P"
        with ‹∃ω'. behavior.dropn i ω = Some ω' ∧ ω' ∈ raw.always P›
        have "∃ω'. behavior.dropn (i - Suc j) ω = Some ω' ∧ ω' ∉ raw.always P"
          using behavior.dropn.shorterD[OF _ diff_le_self] by blast
        then obtain k where "∃ω'. behavior.dropn (i - Suc j + k) ω = Some ω' ∧ ω' ∉ P"
          by (clarsimp simp: raw.always_alt_def behavior.dropn.add behavior.dropn.Suc) blast
        with Suc.hyps ‹j < i›
        have "∃ω'. behavior.dropn (i - Suc j) ω = Some ω' ∧ ω' ∉ P"
          by (fastforce simp: raw.always_alt_def behavior.dropn.add
                       split: nat_diff_split_asm
                        dest: spec[where x="k - 1"])
        with ‹j < i› IntD1[OF ‹ω ∈ ?lhs›]
        obtain m n where "∃ω' ω'' ω'''. behavior.dropn (i - Suc j) ω = Some ω' ∧ ω' ∉ P
                                      ∧ behavior.dropn m ω' = Some ω''         ∧ ω'' ∈ P
                                      ∧ behavior.dropn n ω'' = Some ω'''       ∧ ω''' ∉ P"
          by (simp add: raw.always_alt_def raw.eventually_alt_def)
             (blast dest: spec[where x="i - Suc j"])
        with ‹j < i› Suc.hyps
        show False
          by (clarsimp simp: raw.always_alt_def dest!: spec[where x="m + n - 1"] split: nat_diff_split_asm)
             (metis behavior.dropn.Suc behavior.dropn.bind_tl_commute behavior.dropn.dropn bind.bind_lunit)
      qed
    qed (use Suc.hyps in simp)
  qed (use i in simp)
  from this[of i] show "ω ∈ P"
    by (fastforce simp: raw.always_alt_def dest: spec[where x=0])
  qed
  show ?thesis
  proof(rule tls.validI)
    have "□(◇(P ⊓ ◇(- P)) ⊔ P) ⊓ ◇□P ≤ P"
      by (rule raw_Ax5[transferred])
    then have "□(◇(P ⊓ ◇(- P)) ⊔ P) ⊓ ◇□P ≤ P"
      by (simp add: boolean_implication.conv_sup tls.always.neg)
    then show "⊤ ≤ ?goal"
      by - (intro iffD1[OF boolean_implication.shunt1];
            simp add: boolean_implication.conv_sup tls.always.neg)
  qed
qed

lemma Ax6:
  assumes "⊨ P"
  shows "⊨ □P"
by (rule tls.always.always_necessitation[OF assms])

―‹ Ax7: propositional tautologies: given by the class‹boolean_algebra› instance ›

lemma Ax8:
  assumes "⊨ P"
  assumes "⊨ P ⟶B Q"
  shows "⊨ Q"
by (rule tls.valid.rev_mp[OF assms])

setup ‹Sign.parent_path›


subsection‹ Tweak syntax ›

unbundle tls.no_notation
no_notation tls.singleton ("⦉_⦊T")

setup ‹Sign.mandatory_path "tls"›

bundle extra_notation
begin

notation tls.singleton ("⦉_⦊T" [0])
notation tls.from_spec ("⦇_⦈" [0])

end

bundle no_extra_notation
begin

no_notation tls.singleton ("⦉_⦊T" [0])
no_notation tls.from_spec ("⦇_⦈" [0])

end

setup ‹Sign.parent_path›
(*<*)

end
(*>*)