Theory Stream_More

theory Stream_More
imports
  Sequence_LTL
  Instantiate_Existentials
  "HOL-Library.Rewrite"
begin

(*

(* TODO: can be replaced by stream.rel_cases *)
lemma stream_all2_Cons1:
  "stream_all2 P (y ## ys) xs ⟷ (∃ x xs'. xs = x ## xs' ∧ P y x ∧ stream_all2 P ys xs')"
  by (cases xs) auto
lemma stream_all2_Cons2:
  "stream_all2 P xs (y ## ys) ⟷ (∃ x xs'. xs = x ## xs' ∧ P x y ∧ stream_all2 P xs' ys)"
  by (cases xs) auto

(* TODO: inline? *)
lemma filter_list_all_iff: "filter P xs = [] ⟷ list_all (Not ∘ P) xs"
  unfolding filter_empty_conv list.pred_set by simp

(* TODO: inline? *)
lemma append_single_shift: "(xs @ [x]) @- ys = xs @- x ## ys" by simp

(* TODO: inline? *)
lemma sset_finite_decomp:
  assumes "finite (sset w)"
  obtains u v a w'
  where "w = u @- a ## v @- a ## w'"
  using sdistinct_infinite_sset not_sdistinct_decomp assms by metis

*)

lemma list_all_stake_least:
  "list_all (Not ∘ P) (stake (LEAST n. P (xs !! n)) xs)" (is "?G") if "∃ n. P (xs !! n)"
proof (rule ccontr)
  let ?n = "LEAST n. P (xs !! n)"
  assume "¬ ?G"
  then have "∃ x ∈ set (stake ?n xs). P x" unfolding list_all_iff by auto
  then obtain n' where "n' < ?n" "P (xs !! n')" using set_stake_snth by metis
  with Least_le[of "λ n. P (xs !! n)" n'] show False by auto
qed

lemma alw_stream_all2_mono:
  assumes "stream_all2 P xs ys" "alw Q xs" "⋀ xs ys. stream_all2 P xs ys ⟹ Q xs ⟹ R ys"
  shows "alw R ys"
  using assms stream.rel_sel by (coinduction arbitrary: xs ys) (blast)

lemma alw_ev_HLD_cycle:
  assumes "stream_all2 (∈) xs (cycle as)" "a ∈ set as"
  shows "infs a xs"
using assms(1)
proof coinduct
  case (infs xs)
  have 1: "as ≠ []" using assms(2) by auto
  have 2:
    "list_all2 (∈) (stake (length as) xs) (stake (length as) (cycle as))"
    "stream_all2 (∈) (sdrop (length as) xs) (sdrop (length as) (cycle as))"
    using infs stream_rel_shift stake_sdrop length_stake by metis+
  have 3: "stake (length as) (cycle as) = as" using 1 by simp
  have 4: "sdrop (length as) (cycle as) = cycle as" using sdrop_cycle_eq 1 by this
  have 5: "set (stake (length as) xs) ∩ a ≠ {}"
    using assms(2) 2(1) unfolding list.in_rel 3
    by (auto) (metis IntI empty_iff mem_Collect_eq set_zip_leftD split_conv subsetCE zip_map_fst_snd)
  show ?case using 2 5 unfolding 4 by force
qed

lemma alw_ev_mono:
  assumes "alw (ev φ) xs" and "⋀ xs. φ xs ⟹ ψ xs"
  shows "alw (ev ψ) xs"
  by (rule alw_mp[OF assms(1)]) (auto intro: ev_mono assms(2) simp: alw_iff_sdrop)

lemma alw_ev_lockstep:
  assumes
    "alw (ev (holds P)) xs" "stream_all2 Q xs as"
    "⋀ x a. P x ⟹ Q x a ⟹ R a"
  shows
    "alw (ev (holds R)) as"
  using assms(1,2)
  apply (coinduction arbitrary: xs as)
  apply auto
  subgoal
    by (metis alw.cases assms(3) ev_holds_sset stream_all2_sset1)
  subgoal
    by (meson alw.cases stream.rel_sel)
  done

subsection ‹sfilter, wait, nxt›

text ‹Useful?›
lemma nxt_holds_iff_snth: "(nxt ^^ y) (holds P) xs ⟷ P (xs !! y)"
  by (induction y arbitrary: xs; simp)

text ‹Useful?›
lemma wait_LEAST:
  "wait (holds P) xs = (LEAST n. P (xs !! n))" unfolding wait_def nxt_holds_iff_snth ..

lemma sfilter_SCons_decomp:
  assumes "sfilter P xs = x ## zs" "ev (holds P) xs"
  shows "∃ ys' zs'. xs = ys' @- x ## zs' ∧ list_all (Not o P) ys' ∧ P x ∧ sfilter P zs' = zs"
proof -
  from ev_imp_shift[OF assms(2)] obtain as bs where "xs = as @- bs" "holds P bs"
    by auto
  then have "P (shd bs)" by auto
  with ‹xs = _› have "∃ n. P (xs !! n)" using assms(2) sdrop_wait by fastforce
  from sdrop_while_sdrop_LEAST[OF this] have *:
    "sdrop_while (Not ∘ P) xs = sdrop (LEAST n. P (xs !! n)) xs" .
  let ?xs = "sdrop_while (Not ∘ P) xs" let ?n = "LEAST n. P (xs !! n)"
  from assms(1) have "x = shd ?xs" "zs = sfilter P (stl ?xs)"
    by (subst (asm) sfilter.ctr; simp)+
  have "xs = stake ?n xs @- sdrop ?n xs" by simp
  moreover have "P x" using assms(1) unfolding sfilter_eq[OF assms(2)] ..
  moreover from ‹∃ n. P _› have "list_all (Not o P) (stake ?n xs)" by (rule list_all_stake_least)
  ultimately show ?thesis
    using ‹x = _› ‹zs = _› *[symmetric] by (inst_existentials "stake ?n xs" "stl ?xs") auto
qed

lemma sfilter_SCons_decomp':
  assumes "sfilter P xs = x ## zs" "ev (holds P) xs"
  shows
    "list_all (Not o P) (stake (wait (holds P) xs) xs)" (is "?G1")
    "P x"
    "∃ zs'. xs = stake (wait (holds P) xs) xs @- x ## zs' ∧ sfilter P zs' = zs" (is "?G2")
proof -
  from ev_imp_shift[OF assms(2)] obtain as bs where "xs = as @- bs" "holds P bs"
    by auto
  then have "P (shd bs)" by auto
  with ‹xs = _› have "∃ n. P (xs !! n)" using assms(2) sdrop_wait by fastforce thm sdrop_wait
  from sdrop_while_sdrop_LEAST[OF this] have *:
    "sdrop_while (Not ∘ P) xs = sdrop (LEAST n. P (xs !! n)) xs" .
  let ?xs = "sdrop_while (Not ∘ P) xs" let ?n = "wait (holds P) xs"
  from assms(1) have "x = shd ?xs" "zs = sfilter P (stl ?xs)"
    by (subst (asm) sfilter.ctr; simp)+
  have "xs = stake ?n xs @- sdrop ?n xs" by simp
  moreover show "P x" using assms(1) unfolding sfilter_eq[OF assms(2)] ..
  moreover from ‹∃ n. P _› show "list_all (Not o P) (stake ?n xs)"
    by (auto intro: list_all_stake_least simp: wait_LEAST)
  ultimately show ?G2
    using ‹x = _› ‹zs = _› *[symmetric] by (inst_existentials "stl ?xs") (auto simp: wait_LEAST)
qed

lemma sfilter_shift_decomp:
  assumes "sfilter P xs = ys @- zs" "alw (ev (holds P)) xs"
  shows "∃ ys' zs'. xs = ys' @- zs' ∧ filter P ys' = ys ∧ sfilter P zs' = zs"
  using assms(1,2)
proof (induction ys arbitrary: xs)
  case Nil
  then show ?case by (inst_existentials "[] :: 'a list" xs; simp)
next
  case (Cons y ys)
  from alw_ev_imp_ev_alw[OF ‹alw (ev _) xs›] have "ev (holds P) xs"
    by (auto elim: ev_mono)
  with Cons.prems(1) sfilter_SCons_decomp[of P xs y "ys @- zs"]
  obtain ys' zs' where *:
      "xs = ys' @- y ## zs'"
      "list_all (Not ∘ P) ys'"
      "P y"
      "sfilter P zs' = ys @- zs"
    by auto
  then have "sfilter P zs' = ys @- zs" by auto
  from ‹alw (ev _) xs› ‹xs = _› have "alw (ev (holds P)) zs'"
    by (metis ev.intros(2) ev_shift not_alw_iff stream.sel(2))
  from Cons.IH[OF ‹sfilter P zs' = _› this]
  obtain zs1 zs2 where
    "zs' = zs1 @- zs2"
    "ys = filter P zs1"
    "zs = sfilter P zs2"
    by auto
  with * show ?case
    by (inst_existentials "ys' @ y # zs1" zs2; simp add: list.pred_set)
qed

lemma finite_sset_sfilter_decomp:
  assumes "finite (sset (sfilter P xs))" "alw (ev (holds P)) xs"
  obtains x ws ys zs where "xs = ws @- x ## ys @- x ## zs" "P x"
proof atomize_elim
  let ?xs = "sfilter P xs"
  have 1: "¬ sdistinct (sfilter P xs)" using sdistinct_infinite_sset assms(1) by auto
  from not_sdistinct_decomp[OF 1]
  obtain ws ys x zs where 1: "sfilter P xs = ws @- x ## ys @- x ## zs" .
  from sfilter_shift_decomp[OF this assms(2)]
  obtain ys' zs' where 2: "xs = ys' @- zs'" "sfilter P zs' = x ## ys @- x ## zs" by auto
  then have "ev (holds P) zs'" using alw_shift assms(2) by blast
  from sfilter_SCons_decomp[OF 2(2) this]
  obtain zs1 zs2 where 3:
    "zs' = zs1 @- x ## zs2" "list_all (Not ∘ P) zs1" "P x" "sfilter P zs2 = ys @- x ## zs"
    by auto
  have "alw (ev (holds P)) zs2"
    by (metis alw_ev_stl alw_shift assms(2) 2(1) 3(1) stream.sel(2))
  from sfilter_shift_decomp[OF 3(4) this]
  obtain zs3 zs4 where 4: "zs2 = zs3 @- zs4" "sfilter P zs4 = x ## zs" by auto
  have "ev (holds P) zs4"
    using ‹alw (ev (holds P)) zs2› alw_shift 4(1) by blast
  from sfilter_SCons_decomp[OF 4(2) this]
  obtain zs5 zs6 where "zs4 = zs5 @- x ## zs6" "list_all (Not ∘ P) zs5" "P x" "zs = sfilter P zs6"
    by auto
  with 1 2 3 4 show "∃ws x ys zs. xs = ws @- x ## ys @- x ## zs ∧ P x"
    by (inst_existentials "ys' @ zs1" x "zs3 @ zs5" zs6; force)
qed

text ‹Useful?›
lemma sfilter_shd_LEAST:
  "shd (sfilter P xs) = xs !! (LEAST n. P (xs !! n))" if "ev (holds P) xs"
proof -
  from sdrop_wait[OF ‹ev _ xs›] have "∃ n. P (xs !! n)" by auto
  from sdrop_while_sdrop_LEAST[OF this] show ?thesis by simp
qed

lemma alw_nxt_holds_cong:
  "(nxt ^^ n) (holds (λx. P x ∧ Q x)) xs = (nxt ^^ n) (holds Q) xs" if "alw (holds P) xs"
  using that unfolding nxt_holds_iff_snth alw_iff_sdrop by simp

lemma alw_wait_holds_cong:
  "wait (holds (λx. P x ∧ Q x)) xs = wait (holds Q) xs" if "alw (holds P) xs"
  unfolding wait_def alw_nxt_holds_cong[OF that] ..

lemma alw_sfilter:
  "sfilter (λ x. P x ∧ Q x) xs = sfilter Q xs" if "alw (holds P) xs" "alw (ev (holds Q)) xs"
  using that
proof (coinduction arbitrary: xs)
  case prems: stream_eq
  from prems(3,4) have ev_one: "ev (holds (λx. P x ∧ Q x)) xs"
    by (subst ev_cong[of _ _ _ "holds Q"]) (assumption | auto)+
  from prems have "a = shd (sfilter (λx. P x ∧ Q x) xs)" "b = shd (sfilter Q xs)"
    by (metis stream.sel(1))+
  with prems(3,4) have
    "a = xs !! (LEAST n. P (xs !! n) ∧ Q (xs !! n))" "b = xs !! (LEAST n. Q (xs !! n))"
    using ev_one by (auto 4 3 dest: sfilter_shd_LEAST)
  with alw_wait_holds_cong[unfolded wait_LEAST, OF ‹alw (holds P) xs›] have "a = b" by simp
  from sfilter_SCons_decomp'[OF prems(1)[symmetric], OF ev_one]
  obtain u2 where u2:
    "xs = stake (wait (holds (λx. P x ∧ Q x)) xs) xs @- a ## u2"
    "u = sfilter (λx. P x ∧ Q x) u2"
    by auto
  have "ev (holds Q) xs" using prems(4) by blast
  from sfilter_SCons_decomp'[OF prems(2)[symmetric], OF this]
  obtain v2 where
    "list_all (Not ∘ Q) (stake (wait (holds Q) xs) xs)"
    "xs = stake (wait (holds Q) xs) xs @- b ## v2"
    "v = sfilter Q v2"
    by auto
  with u2 ‹a = b› show ?case
    apply (intro conjI exI)
        apply assumption+
      apply (simp add: alw_wait_holds_cong[OF prems(3)], metis shift_left_inj stream.inject)
    by (metis alw.cases alw_shift prems(3,4) stream.sel(2))+
qed

lemma alw_ev_holds_mp:
  "alw (holds P) xs ⟹ ev (holds Q) xs ⟹ ev (holds (λx. P x ∧ Q x)) xs"
  by (subst ev_cong, assumption) auto

lemma alw_ev_conjI:
  "alw (ev (holds (λ x. P x ∧ Q x))) xs" if "alw (holds P) xs" "alw (ev (holds Q)) xs"
  using that(2,1) by - (erule alw_mp, coinduction arbitrary: xs, auto intro: alw_ev_holds_mp)

subsection ‹Useful?›

lemma alw_holds_pred_stream_iff:
  "alw (holds P) xs ⟷ pred_stream P xs"
  by (simp add: alw_iff_sdrop stream_pred_snth)

lemma alw_holds_sset:
  "alw (holds P) xs = (∀ x ∈ sset xs. P x)"
  by (simp add: alw_holds_pred_stream_iff stream.pred_set)

lemma pred_stream_sfilter:
  assumes alw_ev: "alw (ev (holds P)) xs"
  shows "pred_stream P (sfilter P xs)"
  using alw_ev
proof (coinduction arbitrary: xs)
  case (stream_pred xs)
  then have "ev (holds P) xs" by auto
  have "sfilter P xs = shd (sfilter P xs) ## stl (sfilter P xs)"
    by (cases "sfilter P xs") auto
  from sfilter_SCons_decomp[OF this ‹ev (holds P) xs›]
  obtain ys' zs' where
    "xs = ys' @- shd (sdrop_while (Not ∘ P) xs) ## zs'"
    "P (shd (sdrop_while (Not ∘ P) xs))"
    "sfilter P zs' = sfilter P (stl (sdrop_while (Not ∘ P) xs))"
    by auto
  then show ?case
    apply (inst_existentials zs')
    apply (metis sfilter.simps(1) stream.sel(1) stream_pred(1))
    apply (metis scons_eq sfilter.simps(2) stream_pred(1))
    apply (metis alw_ev_stl alw_shift stream.sel(2) stream_pred(2))
    done
qed

lemma alw_ev_sfilter_mono:
  assumes alw_ev: "alw (ev (holds P)) xs"
    and mono: "⋀ x. P x ⟹ Q x"
  shows "pred_stream Q (sfilter P xs)"
  using stream.pred_mono[of P Q] assms pred_stream_sfilter by blast

lemma sset_sfilter:
  "sset (sfilter P xs) ⊆ sset xs" if "alw (ev (holds P)) xs"
proof -
  have "alw (holds (λ x. x ∈ sset xs)) xs" by (simp add: alw_iff_sdrop)
  with ‹alw (ev _) _› alw_sfilter[OF this ‹alw (ev _) _›, symmetric]
    have "pred_stream (λ x. x ∈ sset xs) (sfilter P xs)"
    by (simp) (rule alw_ev_sfilter_mono; auto intro: alw_ev_conjI)
  then have "∀ x ∈ sset (sfilter P xs). x ∈ sset xs" unfolding stream.pred_set by this
  then show ?thesis by blast
qed

lemma stream_all2_weaken:
  "stream_all2 Q xs ys" if "stream_all2 P xs ys" "⋀ x y. P x y ⟹ Q x y"
  using that by (coinduction arbitrary: xs ys) auto

lemma stream_all2_SCons1:
  "stream_all2 P (x ## xs) ys = (∃z zs. ys = z ## zs ∧ P x z ∧ stream_all2 P xs zs)"
  by (subst (3) stream.collapse[symmetric], simp del: stream.collapse, force)

lemma stream_all2_SCons2:
  "stream_all2 P xs (y ## ys) = (∃z zs. xs = z ## zs ∧ P z y ∧ stream_all2 P zs ys)"
  by (subst stream.collapse[symmetric], simp del: stream.collapse, force)

lemma stream_all2_combine:
  "stream_all2 R xs zs" if
  "stream_all2 P xs ys" "stream_all2 Q ys zs" "⋀ x y z. P x y ∧ Q y z ⟹ R x z"
  using that(1,2)
  by (coinduction arbitrary: xs ys zs)
     (auto intro: that(3) simp: stream_all2_SCons1 stream_all2_SCons2)

lemma stream_all2_shift1:
  "stream_all2 P (xs1 @- xs2) ys =
  (∃ ys1 ys2. ys = ys1 @- ys2 ∧ list_all2 P xs1 ys1 ∧ stream_all2 P xs2 ys2)"
  apply (induction xs1 arbitrary: ys)
   apply (simp; fail)
  apply (simp add: stream_all2_SCons1 list_all2_Cons1)
  apply safe
  subgoal for a xs1 ys z zs ys1 ys2
    by (inst_existentials "z # ys1" ys2; simp)
  subgoal for a xs1 ys ys1 ys2 z zs
    by (inst_existentials z "zs @- ys2" zs "ys2"; simp)
  done

lemma stream_all2_shift2:
  "stream_all2 P ys (xs1 @- xs2) =
  (∃ ys1 ys2. ys = ys1 @- ys2 ∧ list_all2 P ys1 xs1 ∧ stream_all2 P ys2 xs2)"
  by (meson list.rel_flip stream.rel_flip stream_all2_shift1)

lemma stream_all2_bisim:
  assumes "stream_all2 (∈) xs as" "stream_all2 (∈) ys as" "sset as ⊆ S"
  shows "stream_all2 (λ x y. ∃ a. x ∈ a ∧ y ∈ a ∧ a ∈ S) xs ys"
  using assms
  apply (coinduction arbitrary: as xs ys)
  subgoal for a u b v as xs ys
    apply (rule conjI)
     apply (inst_existentials "shd as", auto simp: stream_all2_SCons1; fail)
    apply (inst_existentials "stl as", auto 4 3 simp: stream_all2_SCons1; fail)
    done
  done



end