# 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
```