Quelle  TLS.thy

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

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

text‹

  model systems with finite and infinite sequences of states, closed
  stuttering following 🚫‹"Lamport:1994"›. This theory relates
  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
  of finite sequences does have some impact.

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

 :
 ▪ Lamport (and Abadi et al) treat infinite stuttering as termination
 ▪ 🚫‹‹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‹

  infinitary version of const‹trace.natural'›.

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

  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
  "ψ₁ ≃_T ψ₂ ≡ behavior.stuttering.equivalent ψ₁ ψ₂"

lemma map:
  assumes "ψ₁ ≃_T ψ₂"
  shows "behavior.map af sf vf ψ₁ ≃_T behavior.map af sf vf ψ₂"
by (metis assms behavior.natural.map_natural)

lemma takeE:
  assumes "ψ₁ ≃_T ψ₂"
  obtains j where "behavior.take i ψ₁ ≃_S behavior.take j ψ₂"
using assms
by (fastforce simp: behavior.natural_def trace.natural_def
              elim: collapse.eq_collapse_ttake_dropnE[where s="behavior.init ψ₂" and i=i and xs="behavior.rest ψ₁" and ys="behavior.rest ψ₂"])

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‹

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

 :
 ▪ 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 (=) (=) (=))) (\<longrightarrow>_B) (\<longrightarrow>_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 σ₁ ≤ raw.singleton σ₂ ⟷ ♮_Tσ₁ = ♮_Tσ₂"
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 \<longrightarrow>_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‹

  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‹

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

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

 :
 ▪ as we lack next/X/‹◯› (due to stuttering closure) we do not have induction for ‹U› (until)
 ▪ 🚫‹"Lamport:1994"› omitted the LTL ``until'' operator from TLA as he considered it too hard to use
 ▪ As 🚫‹"DeGiacomoVardi:2013"› observe, things get non-standard on finite traces
 ▪ see \S\ref{sec:safety_closure} for an example
 ▪ 🚫‹"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 \<longrightarrow>_B raw.state_prop Q) = raw.state_prop (P \<longrightarrow>_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: ―‹ 🚫‹‹(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: ―‹ 🚫‹‹(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 "ψ₂ ∈ raw.until P Q" if "ψ₁ ∈ raw.until P Q" and "ψ₁ ≃_T ψ₂" for ψ₁ ψ₂
    using that
  proof(induct arbitrary: ψ₂ rule: raw.until.induct)
    case (base ψ₁ ψ₂) with assms(2) show ?case
      by (blast intro: behavior.stuttering.closed_in)
  next
    case (step ψ₁ ψ' ψ₂)
    show ?case
    proof(cases "ψ' ≃_T ψ₁")
      case True with ‹ψ₁ ≃_T ψ₂› step.hyps(4) show ?thesis
        by simp
    next
      case False
      from assms(1) ‹ψ₁ ∈ P› ‹ψ₁ ≃_T ψ₂› have "ψ₂ ∈ P"
        by (blast intro: behavior.stuttering.closed_in)
      from False ‹ψ₁ ≃_T ψ₂› ‹behavior.tl ψ₁ = Some ψ'›
      obtain a s₀ s₁ xs₁ xs' ys'
        where ψ₁: "ψ₁ = behavior.B s₀ (TCons (a, s₁) xs₁)"
          and ψ₂: "ψ₂ = behavior.B s₀ (tshift xs' (TCons (a, s₁) ys'))"
          and *: "collapse s₀ (TCons (a, s₁) xs₁) = collapse s₀ (tshift xs' (TCons (a, s₁) ys'))"
                 "s₀ ≠ s₁"
          and **: "collapse s₁ ys' = collapse s₁ xs₁"
          and xs': "snd ` set xs' ⊆ {s₀}"
        by (cases ψ₁; cases ψ₂; cases "behavior.rest ψ₁"; simp)
           (fastforce simp: behavior.natural_def collapse.eq_TCons_conv trepeat_eq_TCons_conv
                     split: if_splits)
      from ψ₂ ‹ψ₂ ∈ P› xs' show ?thesis
      proof(induct xs' arbitrary: ψ₂)
        case Nil with ψ₁ ** 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›] ψ₁ ** 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 \<longrightarrow>_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)"

open_bundle "syntax"
begin
notation tls.valid (‹⊨ _› [30] 30)
notation tls.state_prop (‹《_》› [0])
notation tls.until (infix ‹U› 85)
notation tls.eventually (‹♢_› [87] 87)
notation tls.always (‹◻_› [87] 87)
notation tls.release (infixr ‹R› 85)
notation tls.unless (infixr ‹W› 85)
notation tls.always_imp_syn (infixr ‹\⟶_\◻› 75)
notation tls.leads_to (infixr ‹\↝› 75)
end

bundle "no_syntax"
begin
no_notation tls.valid (‹⊨ _› [30] 30)
no_notation tls.state_prop (‹《_》› [0])
no_notation tls.until (infixr ‹U› 85)
no_notation tls.eventually (‹♢_› [87] 87)
no_notation tls.always (‹◻_› [87] 87)
no_notation tls.release (infixr ‹R› 85)
no_notation tls.unless (infixr ‹W› 85)
no_notation tls.always_imp_syn (infixr ‹\⟶_\◻› 75)
no_notation tls.leads_to (infixr ‹\↝› 75)
end

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 \<longrightarrow>_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 U 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 U Q) (P' U Q')"
using assms by (cases F) (auto simp: tls.until.mono)

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

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

lemma SupR:
  shows "P U (⊔X) = ⊔((U) 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: ―‹ 🚫‹‹(16)› in "WarfordVegaStaley:2020"› ›
  shows "P U Q ⊓ (-Q) U R ≤ P U R"
by transfer (rule raw.until.implication_ordering_le)

lemma supL_ordering_le: ―‹ 🚫‹‹(17)› in "WarfordVegaStaley:2020"› ›
  shows "P U (Q U R) ≤ (P ⊔ Q) U R" (is "?lhs ≤ ?rhs")
proof -
  have "?rhs = (P ⊔ Q) U ((P ⊔ Q) U 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: ―‹ 🚫‹‹(18)› in "WarfordVegaStaley:2020"› ›
  shows "P U (Q ⊓ R) ≤ (P U Q) U R"
by transfer (rule raw.until.infR_ordering_le)

lemma boolean_implication_distrib_le: ―‹ 🚫‹‹(19)› in "WarfordVegaStaley:2020"› ›
  shows "(P \<longrightarrow>_B Q) U R ≤ (P U R) \<longrightarrow>_B (Q U R)"
by (metis galois.conj_imp.galois order.refl tls.until.infL tls.until.mono)

lemma excluded_middleR: ―‹ 🚫‹‹(23)› in "WarfordVegaStaley:2020"› ›
  shows "⊨ P U Q ⊔ P U (-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 U Q) U Q = P U 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 U P = P"
by (metis tls.until.botL tls.until.untilL)

lemma absorb_supL: ―‹ 🚫‹‹(23)› in "WarfordVegaStaley:2020"› ›
  shows "P ⊔ P U 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: ―‹ 🚫‹‹(23)› in "WarfordVegaStaley:2020"› ›
  shows "Q ⊔ P U Q = P U Q"
by (simp add: sup.absorb2 tls.until.expansive)

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

lemma absorb_eventually:
  shows inf_eventually_absorbR: "P U Q ⊓ ♢Q = P U Q" ―‹ 🚫‹‹(39)› in "WarfordVegaStaley:2020"› ›
    and sup_eventually_absorbR: "P U Q ⊔ ♢Q = ♢Q" ―‹ 🚫‹‹(40)› in "WarfordVegaStaley:2020"› ›
    and eventually_absorbR: "P U ♢Q = ♢Q" ―‹ 🚫‹‹(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: ―‹ 🚫‹‹(28)› in "WarfordVegaStaley:2020"› ›
  shows "P U Q ≤ P ⊔ Q"
by (simp add: ac_simps sup.absorb_iff1 tls.until.absorb_supL tls.until.absorb_supR)

lemma ordering: ―‹ 🚫‹‹(251)› in "WarfordVegaStaley:2020"› ›
  shows "(-P) U Q ⊔ (-Q) U P = ♢(P ⊔ Q)" (is "?lhs = ?rhs")
proof -
  have "?lhs = ⊤ U P ⊓ (- Q) U P ⊔ ⊤ U Q ⊓ (- P) U Q"
    by (simp add: ac_simps inf.absorb2 tls.until.mono)
  also have "… = (- P) U P ⊓ (- Q) U P ⊔ (- Q) U Q ⊓ (- P) U Q"
    by (simp add: tls.until.weakenL)
  also have "… = (- (P ⊔ Q)) U (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) U 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 \<longrightarrow>_B ♢Q ≤ ♢(P \<longrightarrow>_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 \<longrightarrow>_\<box> Q ≤ ♢P \<longrightarrow>_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 U 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 W ⊥"
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 \<longrightarrow>_\<box> Q ≤ ◻P \<longrightarrow>_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: ―‹ 🚫‹‹(81)› in "WarfordVegaStaley:2020"› ›
  shows "◻P ≤ -(Q U (-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: ―‹ 🚫‹‹(140)› in "WarfordVegaStaley:2020"› ›
  shows "P U ◻Q ≤ ◻(P U Q)"
by transfer (rule raw.until.alwaysR_le)

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

lemma eventually_always_always_eventually_le: ―‹ 🚫‹‹(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: ―‹🚫‹‹\S2.2: T33 frame› in "KroegerMerz:2008"› ›
  shows "⊨ ◻P \<longrightarrow>_B ◻Q \<longrightarrow>_B ◻(P ⊓ Q)"
by (simp add: tls.validI tls.always.inf flip: boolean_implication.infL)

lemma always_eventually_imp: ―‹🚫‹‹\S2.2: T34 frame› in "KroegerMerz:2008"› ›
  shows "⊨ ◻P \<longrightarrow>_B ♢Q \<longrightarrow>_B ♢(P ⊓ Q)"
by (simp add: tls.validI boolean_implication.mp tls.always_inf_eventually_eventually_le)

lemma always_imp_always_generalization: ―‹🚫‹‹\S2.2: T35› in "KroegerMerz:2008"› ›
  shows "◻P \<longrightarrow>_\<box> Q ≤ ◻P \<longrightarrow>_B ◻Q"
by (simp add: order.trans[OF tls.always.always_imp_le])

lemma always_imp_eventually_generalization: ―‹🚫‹‹\S2.2: T36› in "KroegerMerz:2008"› ›
  shows "P \<longrightarrow>_\<box> ♢Q ≤ ♢P \<longrightarrow>_B ♢Q"
by (metis tls.eventually.always_imp_le tls.eventually.idempotent(1))

text‹

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

lemma always_eventually_always_absorption: ―‹🚫‹‹\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: ―‹🚫‹‹\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: ―‹ 🚫‹‹(157)› in "WarfordVegaStaley:2020"› ›
  shows "P \<longrightarrow>_\<box> Q ≤ ◻♢P \<longrightarrow>_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: ―‹ 🚫‹‹(158)› in "WarfordVegaStaley:2020"› ›
  shows "P \<longrightarrow>_\<box> Q ≤ ♢◻P \<longrightarrow>_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" ―‹ 🚫‹‹(159)› in "WarfordVegaStaley:2020"› ›
by (simp add: tls.always.mono tls.eventually.mono)

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

lemma always_eventually_sup: ―‹ 🚫‹‹(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: ―‹ 🚫‹‹(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: ―‹ 🚫‹‹(163)› in "WarfordVegaStaley:2020"› ›
  shows "♢◻(P \<longrightarrow>_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: ―‹ 🚫‹‹(170)› in "WarfordVegaStaley:2020"› ›
  shows "-(P W Q) = (-Q) U (-P ⊓ -Q)"
by transfer (rule raw.unless.neg)

lemma alwaysR_le: ―‹ 🚫‹‹(177)› in "WarfordVegaStaley:2020"› ›
  shows "P W ◻Q ≤ ◻(P W 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: ―‹ 🚫‹‹(206)› in "WarfordVegaStaley:2020"› ›
  shows "P W Q ≤ P ⊔ Q"
by (rule iffD1[OF compl_le_compl_iff]) (simp add: tls.unless.neg tls.until.expansive)

lemma ordering: ―‹ 🚫‹‹(252)› in "WarfordVegaStaley:2020"› ›
  shows "⊨ (-P) W Q ⊔ (-Q) W 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 U Q = (P W Q) ⊓ ♢Q"
by transfer (force simp: raw.until_def raw.eventually_def raw.always_alt_def behavior.dropn.shorterD)

lemma always_strengthen_le: ―‹ 🚫‹‹(83)› in "WarfordVegaStaley:2020"› ›
  shows "◻P ⊓ (Q U R) ≤ (P ⊓ Q) U (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 U Q" (is "?lhs ≤ ?rhs") ―‹ 🚫‹‹(84)› in "WarfordVegaStaley:2020"› ›
by (simp add: tls.eventually_def order.trans[OF tls.until.always_strengthen_le] tls.until.mono)

lemma always_impL: ―‹ 🚫‹‹(86)› in "WarfordVegaStaley:2020"› ›
  shows "P \<longrightarrow>_\<box> P' ⊓ P U Q ≤ P' U Q" (is ?thesis1)
    and "P U Q ⊓ P \<longrightarrow>_\<box> P' ≤ P' U 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: ―‹ 🚫‹‹(85)› in "WarfordVegaStaley:2020"› ›
  shows "Q \<longrightarrow>_\<box> Q' ⊓ P U Q ≤ P U Q'" (is ?thesis1)
    and "P U Q ⊓ Q \<longrightarrow>_\<box> Q' ≤ P U 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: ―‹ 🚫‹‹(173)› in "WarfordVegaStaley:2020"› ›
  shows "-(P U Q) = (-Q) W (-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‹

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

 🚫‹"Jackson:1998"› used the more general
 `‹P› leads to ‹Q› via ‹I›'' form ‹P \⟶_\◻ I U Q›
  establish liveness properties in a sequential setting.

 ›

lemma leads_to_refl:
  shows "⊨ P \<leadsto> 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 \<leadsto> Q ≤ P' \<leadsto> Q'"
by (simp add: assms boolean_implication.mono tls.always.mono tls.eventually.mono)

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

lemma always_imp_leads_to:
  shows "P \<longrightarrow>_\<box> Q ≤ P \<leadsto> Q"
by (simp add: boolean_implication.mono tls.always.mono tls.eventually.expansive)

lemma leads_to_eventually:
  shows "♢P ⊓ (P \<leadsto> Q) ≤ ♢Q"
by (simp add: galois.conj_imp.galois tls.always_imp_eventually_generalization)

lemma leads_to_leads_to_via:
  shows "P \<longrightarrow>_\<box> Q U R ≤ P \<leadsto> R"
by (simp add: boolean_implication.mono tls.always.mono tls.until.eventually_le)

lemma leads_to_trans:
  shows "P \<leadsto> Q ⊓ Q \<leadsto> R ≤ P \<leadsto> R" (is "?lhs ≤ ?rhs")
proof -
  have "?lhs ≤ P \<leadsto> Q ⊓ ◻(Q \<leadsto> R)"
    by (simp add: tls.always.simps)
  also have "… ≤ P \<leadsto> Q ⊓ ♢Q \<leadsto> 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 \<longrightarrow>_\<box> Q' ⊓ P \<longrightarrow>_\<box> I U Q ≤ P \<longrightarrow>_\<box> I U 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 \<longrightarrow>_\<box> I U Q ⊓ P' \<longrightarrow>_\<box> I' U Q ≤ P ⊔ P' \<longrightarrow>_\<box> (I ⊔ I') U 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 \<longrightarrow>_\<box> I U Q) ⊓ (Q \<longrightarrow>_\<box> I' U R) ≤ P \<longrightarrow>_\<box> (I ⊔ I') U R" (is "?lhs ≤ ?rhs")
proof -
  have "?lhs ≤ ◻(P \<longrightarrow>_B I U (I' U 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 \<longrightarrow>_\<box> I U Q) ⊓ (Q \<longrightarrow>_\<box> I' U R) ≤ (P ⊔ Q \<longrightarrow>_\<box> (I ⊔ I') U R)"
by (simp add: boolean_implication_def inf.coboundedI2 le_supI2 tls.always.mono tls.until.mono)


subsubsection‹ Fairness\label{sec:tls-fairness} ›

text‹

  few renderings of weak fairness. 🚫‹"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 \<longrightarrow>_\<box> ♢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 \<longrightarrow>_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 \<longrightarrow>_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‹

  for strong fairness. 🚫‹"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 \<longrightarrow>_\<box> ♢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 \<longrightarrow>_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 \<longleftrightarrow>_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‹

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

 :
 ▪ 🚫‹‹\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
 ▪ 🚫‹‹\S2.2› in "AbadiLamport:1991"›: topological definitions and intuitions
 ▪ 🚫‹‹\S2.2› in "Sistla:1994"›

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

 :
 ▪ 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
 ▪ 🚫‹‹\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: ―‹ 🚫‹"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: ―‹ 🚫‹ ‹\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 ψ₂ ∈ P "
    if "ψ₁ ≃_T ψ₂" and "∀i. behavior.take i ψ₁ ∈ P" and "P ∈ trace.stuttering.closed"
   for ψ₁ ψ₂ i and P :: "('a, 's, 'v) trace.t set"
    using that(2-)
    by - (rule behavior.stuttering.equiv.takeE[OF sym[OF ‹ψ₁ ≃_T ψ₂›], 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 \<longrightarrow>_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‹

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

 :
 ▪ Abadi says that the temporal system is D aka S4.3Dum; see 🚫‹‹\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 \<longrightarrow>_B Q)\<longrightarrow>_B ◻P \<longrightarrow>_B ◻Q"
by (simp add: tls.valid_def boolean_implication.shunt_top tls.always.always_imp_le)

lemma Ax2:
  shows "⊨ ◻P \<longrightarrow>_B P"
by (simp add: tls.valid_def boolean_implication.shunt_top tls.always.contractive)

lemma Ax3:
  shows "⊨ ◻P \<longrightarrow>_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''
 🚫‹‹(254) Lemmon formula› in "WarfordVegaStaley:2020"› ›
  shows "⊨ ◻(◻P \<longrightarrow>_B Q) ⊔ ◻(◻Q \<longrightarrow>_B P)"
proof -
  have "⊨ (-◻P) W ◻Q ⊔ (-◻Q) W ◻P" by (rule tls.unless.ordering)
  also have "… ≤ ◻((-◻P) W ◻Q) ⊔ ◻((-◻Q) W ◻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 \<longrightarrow>_B Q) ⊔ ◻(◻Q \<longrightarrow>_B P)"
    by (simp add: boolean_implication.conv_sup)
  finally show ?thesis .
qed

lemma Ax5:
  ―‹ ``expresses the discreteness of time''
 See also 🚫‹‹\S4.1 ``the Dummett formula''› in "WarfordVegaStaley:2020"›: for them
 ``next'' encodes discreteness ›
  fixes P :: "('a, 's, 'v) tls"
  shows "⊨ ◻(◻(P \<longrightarrow>_B ◻P) \<longrightarrow>_B P) \<longrightarrow>_B ♢◻P \<longrightarrow>_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 🚫‹boolean_algebra› instance ›

lemma Ax8:
  assumes "⊨ P"
  assumes "⊨ P \<longrightarrow>_B Q"
  shows "⊨ Q"
by (rule tls.valid.rev_mp[OF assms])

setup ‹Sign.parent_path›


subsection‹ Tweak syntax ›

unbundle tls.no_syntax
no_notation tls.singleton (‹(•_•)_T›)

setup ‹Sign.mandatory_path "tls"›

bundle extra_syntax
begin
notation tls.singleton (‹(•_•)_T› [0])
notation tls.from_spec (‹(_)› [0])
end

setup ‹Sign.parent_path›
(*<*)

end
(*>*)