Theory Sequence_LTL

section ‹Linear Temporal Logic on Streams›

theory Sequence_LTL

  subsection ‹Basics›

  text ‹Avoid destroying the constant @{const holds} prematurely.›
  lemmas [simp del] = holds.simps holds_eq1 holds_eq2 not_holds_eq

  (* TODO: these cannot be applied successively to simplify infs due to introduction of ∘
    avoid or add extra simplification rules for infs *)
  lemma ev_smap[iff]: "ev P (smap f w)  ev (P  smap f) w" using ev_smap unfolding comp_apply by this
  lemma alw_smap[iff]: "alw P (smap f w)  alw (P  smap f) w" using alw_smap unfolding comp_apply by this
  lemma holds_smap[iff]: "holds P (smap f w)  holds (P  f) w" unfolding holds.simps by simp

  lemmas [iff] = ev_sconst alw_sconst hld_smap'

  lemmas [iff] = alw_ev_stl
  lemma alw_ev_sdrop[iff]: "alw (ev P) (sdrop n w)  alw (ev P) w"
    using alw_ev_sdrop alw_sdrop by blast
  lemma alw_ev_scons[iff]: "alw (ev P) (a ## w)  alw (ev P) w" by (metis alw_ev_stl stream.sel(2))
  lemma alw_ev_shift[iff]: "alw (ev P) (u @- v)  alw (ev P) v" by (induct u) (auto)

  lemmas [simp del, iff] = ev_alw_stl
  lemma ev_alw_sdrop[iff]: "ev (alw P) (sdrop n w)  ev (alw P) w"
    using alwD alw_alw alw_sdrop ev_alw_imp_alw_ev not_ev_iff by metis
  lemma ev_alw_scons[iff]: "ev (alw P) (a ## w)  ev (alw P) w" by (metis ev_alw_stl stream.sel(2))
  lemma ev_alw_shift[iff]: "ev (alw P) (u @- v)  ev (alw P) v" by (induct u) (auto)

  lemma holds_sconst[iff]: "holds P (sconst a)  P a" unfolding holds.simps by simp
  lemma HLD_sconst[iff]: "HLD A (sconst a)  a  A" unfolding HLD_def holds.simps by simp

  lemma ev_alt_def: "ev φ w  ( u v. w = u @- v  φ v)"
    using ev.base ev_shift ev_imp_shift by metis
  lemma ev_stl_alt_def: "ev φ (stl w)  ( u v. w = u @- v  u  []  φ v)"
    unfolding ev_alt_def by (cases w) (force simp: scons_eq)

  lemma ev_HLD_sset: "ev (HLD A) w  sset w  A  {}" unfolding HLD_def ev_holds_sset by auto

  lemma alw_ev_coinduct[case_names alw_ev, consumes 1]:
    assumes "R w"
    assumes " w. R w  ev φ w  ev R (stl w)"
    shows "alw (ev φ) w"
  proof -
    have "ev R w" using assms(1) by rule
    then show ?thesis using assms(2) by (coinduct) (metis alw_sdrop not_ev_iff sdrop_stl sdrop_wait)

  subsection ‹Infinite Occurrence›

  abbreviation "infs P w  alw (ev (holds P)) w"
  abbreviation "fins P w  ¬ infs P w"

  lemma infs_suffix: "infs P w  ( u v. w = u @- v  Bex (sset v) P)"
    using alwD alw_iff_sdrop alw_shift ev_holds_sset stake_sdrop by (metis (mono_tags, opaque_lifting))
  lemma infs_snth: "infs P w  ( n.  k  n. P (w !! k))"
    by (auto simp: alw_iff_sdrop ev_iff_sdrop holds.simps intro: le_add1 dest: le_Suc_ex)
  lemma infs_infm: "infs P w  ( i. P (w !! i))"
    unfolding infs_snth INFM_nat_le by rule

  lemma infs_coinduct[case_names infs, coinduct pred: infs]:
    assumes "R w"
    assumes " w. R w  Bex (sset w) P  ev R (stl w)"
    shows "infs P w"
    using assms by (coinduct rule: alw_ev_coinduct) (auto simp: ev_holds_sset)
  lemma infs_coinduct_shift[case_names infs, consumes 1]:
    assumes "R w"
    assumes " w. R w   u v. w = u @- v  Bex (set u) P  R v"
    shows "infs P w"
    using assms by (coinduct) (force simp: ev_stl_alt_def)
  lemma infs_flat_coinduct[case_names infs_flat, consumes 1]:
    assumes "R w"
    assumes " u v. R (u ## v)  Bex (set u) P  R v"
    shows "infs P (flat w)"
    using assms by (coinduction arbitrary: w rule: infs_coinduct_shift)
      (metis empty_iff flat_Stream list.set(1) stream.exhaust)
  lemma infs_sscan_coinduct[case_names infs_sscan, consumes 1]:
    assumes "R w a"
    assumes " w a. R w a  P a  ( u v. w = u @- v  u  []  R v (fold f u a))"
    shows "infs P (a ## sscan f w a)"
  using assms(1)
  proof (coinduction arbitrary: w a rule: infs_coinduct_shift)
    case (infs w a)
    obtain u v where 1: "P a" "w = u @- v" "u  []" "R v (fold f u a)" using infs assms(2) by blast
    show ?case
    proof (intro exI conjI bexI)
      have "sscan f w a = scan f u a @- sscan f v (fold f u a)" unfolding 1(2) by simp
      also have "scan f u a = butlast (scan f u a) @ [fold f u a]"
        using 1(3) by (metis last_ConsR scan_eq_nil scan_last snoc_eq_iff_butlast)
      also have "a ##  @- sscan f v (fold f u a) =
        (a # butlast (scan f u a)) @- fold f u a ## sscan f v (fold f u a)" by simp
      finally show "a ## sscan f w a = (a # butlast (scan f u a)) @- fold f u a ## sscan f v (fold f u a)" by this
      show "P a" using 1(1) by this
      show "a  set (a # butlast (scan f u a))" by simp
      show "R v (fold f u a)" using 1(4) by this
    qed rule

  lemma infs_mono: "( a. a  sset w  P a  Q a)  infs P w  infs Q w"
    unfolding infs_snth by force
  lemma infs_mono_strong: "stream_all2 (λ a b. P a  Q b) u v  infs P u  infs Q v"
    unfolding stream_rel_snth infs_snth by blast

  lemma infs_all: "Ball (sset w) P  infs P w" unfolding infs_snth by auto
  lemma infs_any: "infs P w  Bex (sset w) P" unfolding ev_holds_sset by auto

  lemma infs_bot[iff]: "infs bot w  False" using infs_any by auto
  lemma infs_top[iff]: "infs top w  True" by (simp add: infs_all)
  lemma infs_disj[iff]: "infs (λ a. P a  Q a) w  infs P w  infs Q w"
    unfolding infs_snth using le_trans le_cases by metis
  lemma infs_bex[iff]:
    assumes "finite S"
    shows "infs (λ a.  x  S. P x a) w  ( x  S. infs (P x) w)"
    using assms infs_any by induct auto
  lemma infs_bex_le_nat[iff]: "infs (λ a.  k < n :: nat. P k a) w  ( k < n. infs (P k) w)"
  proof -
    have "infs (λ a.  k < n. P k a) w  infs (λ a.  k  {k. k < n}. P k a) w" by simp
    also have "  ( k  {k. k < n}. infs (P k) w)" by blast
    also have "  ( k < n. infs (P k) w)" by simp
    finally show ?thesis by this

  lemma infs_cycle[iff]:
    assumes "w  []"
    shows "infs P (cycle w)  Bex (set w) P"
    show "infs P (cycle w)  Bex (set w) P"
      using assms by (auto simp: ev_holds_sset dest: alwD)
    show "Bex (set w) P  infs P (cycle w)"
      using assms by (coinduction rule: infs_coinduct_shift) (blast dest: cycle_decomp)