# Theory Coinductive.Coinductive_Stream

```(*  Title:      Coinductive/Coinductive_Stream.thy
Author:     Peter Gammie and Andreas Lochbihler
*)
section ‹Infinite lists as a codatatype›

theory Coinductive_Stream
imports
"HOL-Library.Stream"
"HOL-Library.Linear_Temporal_Logic_on_Streams"
Coinductive_List
begin

lemma eq_onpI: "P x ⟹ eq_onp P x x"

primcorec unfold_stream :: "('a ⇒ 'b) ⇒ ('a ⇒ 'a) ⇒ 'a ⇒ 'b stream" where
"unfold_stream g1 g2 a = g1 a ## unfold_stream g1 g2 (g2 a)"

text ‹
The following setup should be done by the BNF package.
›

text ‹congruence rule›

declare stream.map_cong [cong]

lemma eq_SConsD: "xs = SCons y ys ⟹ shd xs = y ∧ stl xs = ys"
by auto

declare stream.map_ident[simp]

lemma smap_eq_SCons_conv:
"smap f xs = y ## ys ⟷
(∃x xs'. xs = x ## xs' ∧ y = f x ∧ ys = smap f xs')"
by(cases xs)(auto)

lemma smap_unfold_stream:
"smap f (unfold_stream SHD STL b) = unfold_stream (f ∘ SHD) STL b"
by(coinduction arbitrary: b) auto

lemma smap_corec_stream:
"smap f (corec_stream SHD endORmore STL_end STL_more b) =
corec_stream (f ∘ SHD) endORmore (smap f ∘ STL_end) STL_more b"
by(coinduction arbitrary: b rule: stream.coinduct_strong) auto

lemma unfold_stream_ltl_unroll:
"unfold_stream SHD STL (STL b) = unfold_stream (SHD ∘ STL) STL b"
by(coinduction arbitrary: b) auto

lemma unfold_stream_eq_SCons [simp]:
"unfold_stream SHD STL b = x ## xs ⟷
x = SHD b ∧ xs = unfold_stream SHD STL (STL b)"
by(subst unfold_stream.ctr) auto

lemma unfold_stream_id [simp]: "unfold_stream shd stl xs = xs"
by(coinduction arbitrary: xs) simp_all

lemma sset_neq_empty [simp]: "sset xs ≠ {}"
by(cases xs) simp_all

declare stream.set_sel(1)[simp]

lemma sset_stl: "sset (stl xs) ⊆ sset xs"
by(cases xs) auto

text ‹induction rules›

lemmas stream_set_induct = sset_induct

subsection ‹Lemmas about operations from @{theory "HOL-Library.Stream"}›

lemma szip_iterates:
"szip (siterate f a) (siterate g b) = siterate (map_prod f g) (a, b)"
by(coinduction arbitrary: a b) auto

lemma szip_smap1: "szip (smap f xs) ys = smap (apfst f) (szip xs ys)"
by(coinduction arbitrary: xs ys) auto

lemma szip_smap2: "szip xs (smap g ys) = smap (apsnd g) (szip xs ys)"
by(coinduction arbitrary: xs ys) auto

lemma szip_smap [simp]: "szip (smap f xs) (smap g ys) = smap (map_prod f g) (szip xs ys)"
by(coinduction arbitrary: xs ys) auto

lemma smap_fst_szip [simp]: "smap fst (szip xs ys) = xs"
by(coinduction arbitrary: xs ys) auto

lemma smap_snd_szip [simp]: "smap snd (szip xs ys) = ys"
by(coinduction arbitrary: xs ys) auto

lemma snth_shift: "snth (shift xs ys) n = (if n < length xs then xs ! n else snth ys (n - length xs))"
by simp

declare szip_unfold [simp, nitpick_simp]

lemma szip_shift:
"length xs = length us
⟹ szip (xs @- ys) (us @- zs) = zip xs us @- szip ys zs"
by(induct xs arbitrary: us)(auto simp add: Suc_length_conv)

subsection ‹Link @{typ "'a stream"} to @{typ "'a llist"}›

definition llist_of_stream :: "'a stream ⇒ 'a llist"
where "llist_of_stream = unfold_llist (λ_. False) shd stl"

definition stream_of_llist :: "'a llist ⇒ 'a stream"
where "stream_of_llist = unfold_stream lhd ltl"

lemma lnull_llist_of_stream [simp]: "¬ lnull (llist_of_stream xs)"

lemma ltl_llist_of_stream [simp]: "ltl (llist_of_stream xs) = llist_of_stream (stl xs)"

lemma stl_stream_of_llist [simp]: "stl (stream_of_llist xs) = stream_of_llist (ltl xs)"

lemma shd_stream_of_llist [simp]: "shd (stream_of_llist xs) = lhd xs"

lemma lhd_llist_of_stream [simp]: "lhd (llist_of_stream xs) = shd xs"

lemma stream_of_llist_llist_of_stream [simp]:
"stream_of_llist (llist_of_stream xs) = xs"
by(coinduction arbitrary: xs) simp_all

lemma llist_of_stream_stream_of_llist [simp]:
"¬ lfinite xs ⟹ llist_of_stream (stream_of_llist xs) = xs"
by(coinduction arbitrary: xs) auto

lemma lfinite_llist_of_stream [simp]: "¬ lfinite (llist_of_stream xs)"
proof
assume "lfinite (llist_of_stream xs)"
thus False
by(induct "llist_of_stream xs" arbitrary: xs rule: lfinite_induct) auto
qed

lemma stream_from_llist: "type_definition llist_of_stream stream_of_llist {xs. ¬ lfinite xs}"
by(unfold_locales) simp_all

interpretation stream: type_definition llist_of_stream stream_of_llist "{xs. ¬ lfinite xs}"
by(fact stream_from_llist)

declare stream.exhaust[cases type: stream]

locale stream_from_llist_setup
begin
setup_lifting stream_from_llist
end

context
begin

interpretation stream_from_llist_setup .

lemma cr_streamI: "¬ lfinite xs ⟹ cr_stream xs (stream_of_llist xs)"

lemma llist_of_stream_unfold_stream [simp]:
"llist_of_stream (unfold_stream SHD STL x) = unfold_llist (λ_. False) SHD STL x"
by(coinduction arbitrary: x) auto

lemma llist_of_stream_corec_stream [simp]:
"llist_of_stream (corec_stream SHD endORmore STL_more STL_end x) =
corec_llist (λ_. False) SHD endORmore (llist_of_stream ∘ STL_more) STL_end x"
by(coinduction arbitrary: x rule: llist.coinduct_strong) auto

lemma LCons_llist_of_stream [simp]: "LCons x (llist_of_stream xs) = llist_of_stream (x ## xs)"

lemma lmap_llist_of_stream [simp]:
"lmap f (llist_of_stream xs) = llist_of_stream (smap f xs)"
by(coinduction arbitrary: xs) auto

lemma lset_llist_of_stream [simp]: "lset (llist_of_stream xs) = sset xs" (is "?lhs = ?rhs")
proof(intro set_eqI iffI)
fix x
assume "x ∈ ?lhs"
thus "x ∈ ?rhs"
by(induct "llist_of_stream xs" arbitrary: xs rule: llist_set_induct)
(auto dest: stream.set_sel(2))
next
fix x
assume "x ∈ ?rhs"
thus "x ∈ ?lhs"
proof(induct)
case (shd xs)
thus ?case using llist.set_sel(1)[of "llist_of_stream xs"] by simp
next
case stl
thus ?case
by(auto simp add: ltl_llist_of_stream[symmetric] simp del: ltl_llist_of_stream dest: in_lset_ltlD)
qed
qed

lemma lnth_list_of_stream [simp]:
"lnth (llist_of_stream xs) = snth xs"
proof
fix n
show "lnth (llist_of_stream xs) n = snth xs n"
by(induction n arbitrary: xs)(simp_all add: lnth_0_conv_lhd lnth_ltl[symmetric])
qed

lemma llist_of_stream_siterates [simp]: "llist_of_stream (siterate f x) = iterates f x"
by(coinduction arbitrary: x) auto

lemma lappend_llist_of_stream_conv_shift [simp]:
"lappend (llist_of xs) (llist_of_stream ys) = llist_of_stream (xs @- ys)"
by(induct xs) simp_all

lemma lzip_llist_of_stream [simp]:
"lzip (llist_of_stream xs) (llist_of_stream ys) = llist_of_stream (szip xs ys)"
by(coinduction arbitrary: xs ys) auto

context includes lifting_syntax
begin

lemma lmap_infinite_transfer [transfer_rule]:
"((=) ===> eq_onp (λxs. ¬ lfinite xs) ===> eq_onp (λxs. ¬ lfinite xs)) lmap lmap"

lemma lset_infinite_transfer [transfer_rule]:
"(eq_onp (λxs. ¬ lfinite xs) ===> (=)) lset lset"

lemma unfold_stream_transfer [transfer_rule]:
"((=) ===> (=) ===> (=) ===> pcr_stream (=)) (unfold_llist (λ_. False)) unfold_stream"
by(auto simp add: stream.pcr_cr_eq cr_stream_def intro!: rel_funI)

lemma corec_stream_transfer [transfer_rule]:
"((=) ===> (=) ===> ((=) ===> pcr_stream (=)) ===> (=) ===> (=) ===> pcr_stream (=))
(corec_llist (λ_. False)) corec_stream"
apply(auto intro!: rel_funI simp add: cr_stream_def stream.pcr_cr_eq)
apply(rule fun_cong) back
apply(rule_tac x=yc in fun_cong)
apply(rule_tac x=xb in arg_cong)
apply(auto elim: rel_funE)
done

lemma shd_transfer [transfer_rule]: "(pcr_stream A ===> A) lhd shd"
by(auto simp add: pcr_stream_def cr_stream_def intro!: rel_funI relcomppI)(frule llist_all2_lhdD, auto dest: llist_all2_lnullD)

lemma stl_transfer [transfer_rule]: "(pcr_stream A ===> pcr_stream A) ltl stl"
by(auto simp add: pcr_stream_def cr_stream_def intro!: rel_funI relcomppI dest: llist_all2_ltlI)

lemma llist_of_stream_transfer [transfer_rule]: "(pcr_stream (=) ===> (=)) id llist_of_stream"

lemma stream_of_llist_transfer [transfer_rule]:
"(eq_onp (λxs. ¬ lfinite xs) ===> pcr_stream (=)) (λxs. xs) stream_of_llist"
by(simp add: eq_onp_def rel_fun_def stream.pcr_cr_eq cr_stream_def)

lemma SCons_transfer [transfer_rule]:
"(A ===> pcr_stream A ===> pcr_stream A) LCons (##)"
by(auto simp add: cr_stream_def pcr_stream_def intro!: rel_funI relcomppI intro: llist_all2_expand)

lemma sset_transfer [transfer_rule]: "(pcr_stream A ===> rel_set A) lset sset"
by(auto 4 3 simp add: pcr_stream_def cr_stream_def intro!: rel_funI relcomppI rel_setI dest: llist_all2_lsetD1 llist_all2_lsetD2)

lemma smap_transfer [transfer_rule]:
"((A ===> B) ===> pcr_stream A ===> pcr_stream B) lmap smap"
by(auto simp add: cr_stream_def pcr_stream_def intro!: rel_funI relcomppI dest: lmap_transfer[THEN rel_funD] elim: rel_funD)

lemma snth_transfer [transfer_rule]: "(pcr_stream (=) ===> (=)) lnth snth"
by(rule rel_funI)(clarsimp simp add: stream.pcr_cr_eq cr_stream_def fun_eq_iff)

lemma siterate_transfer [transfer_rule]:
"((=) ===> (=) ===> pcr_stream (=)) iterates siterate"
by(rule rel_funI)+(clarsimp simp add: stream.pcr_cr_eq cr_stream_def)

context
fixes xs
assumes inf: "¬ lfinite xs"
notes [transfer_rule] = eq_onpI[where P="λxs. ¬ lfinite xs", OF inf]
begin

lemma smap_stream_of_llist [simp]:
shows "smap f (stream_of_llist xs) = stream_of_llist (lmap f xs)"
by transfer simp

lemma sset_stream_of_llist [simp]:
assumes "¬ lfinite xs"
shows "sset (stream_of_llist xs) = lset xs"
by transfer simp

end

lemma llist_all2_llist_of_stream [simp]:
"llist_all2 P (llist_of_stream xs) (llist_of_stream ys) = stream_all2 P xs ys"
apply(cases xs ys rule: stream.Abs_cases[case_product stream.Abs_cases])
apply(safe elim!: GrpE)
apply(rule_tac b="stream_of_llist b" in relcomppI; auto intro!: GrpI)
apply(rule_tac b="llist_of_stream b" in relcomppI; auto intro!: GrpI)
done

lemma stream_all2_transfer [transfer_rule]:
"((=) ===> pcr_stream (=) ===> pcr_stream (=) ===> (=)) llist_all2 stream_all2"

lemma stream_all2_coinduct:
assumes "X xs ys"
and "⋀xs ys. X xs ys ⟹ P (shd xs) (shd ys) ∧ (X (stl xs) (stl ys) ∨ stream_all2 P (stl xs) (stl ys))"
shows "stream_all2 P xs ys"
using assms
apply transfer
apply(rule_tac X="λxs ys. ¬ lfinite xs ∧ ¬ lfinite ys ∧ X xs ys" in llist_all2_coinduct)
apply auto
done

lemma shift_transfer [transfer_rule]:
"((=) ===> pcr_stream (=) ===> pcr_stream (=)) (lappend ∘ llist_of) shift"
by(clarsimp simp add: rel_fun_def stream.pcr_cr_eq cr_stream_def)

lemma szip_transfer [transfer_rule]:
"(pcr_stream (=) ===> pcr_stream (=) ===> pcr_stream (=)) lzip szip"

subsection ‹Link @{typ "'a stream"} with @{typ "nat ⇒ 'a"}›

lift_definition of_seq :: "(nat ⇒ 'a) ⇒ 'a stream" is "inf_llist" by simp

lemma of_seq_rec [code]: "of_seq f = f 0 ## of_seq (f ∘ Suc)"
by transfer (subst inf_llist_rec, simp add: o_def)

lemma snth_of_seq [simp]: "snth (of_seq f) = f"

lemma snth_SCons: "snth (x ## xs) n = (case n of 0 ⇒ x | Suc n' ⇒ snth xs n')"
by(simp split: nat.split)

lemma snth_SCons_simps [simp]:
shows snth_SCons_0: "(x ## xs) !! 0 = x"
and snth_SCons_Suc: "(x ## xs) !! Suc n = xs !! n"

lemma of_seq_snth [simp]: "of_seq (snth xs) = xs"
by transfer simp

lemma shd_of_seq [simp]: "shd (of_seq f) = f 0"
by transfer simp

lemma stl_of_seq [simp]: "stl (of_seq f) = of_seq (λn. f (Suc n))"
by transfer simp

lemma sset_of_seq [simp]: "sset (of_seq f) = range f"
by transfer simp

lemma smap_of_seq [simp]: "smap f (of_seq g) = of_seq (f ∘ g)"
by transfer simp
end

subsection‹Function iteration @{const siterate}  and @{term sconst}›

lemmas siterate [nitpick_simp] = siterate.code

lemma smap_iterates: "smap f (siterate f x) = siterate f (f x)"
by transfer (rule lmap_iterates)

lemma siterate_smap: "siterate f x = x ## (smap f (siterate f x))"
by transfer (rule iterates_lmap)

lemma siterate_conv_of_seq: "siterate f a = of_seq (λn. (f ^^ n) a)"
by transfer (rule iterates_conv_inf_llist)

lemma sconst_conv_of_seq: "sconst a = of_seq (λ_. a)"

lemma szip_sconst1 [simp]: "szip (sconst a) xs = smap (Pair a) xs"
by(coinduction arbitrary: xs) auto

lemma szip_sconst2 [simp]: "szip xs (sconst b) = smap (λx. (x, b)) xs"
by(coinduction arbitrary: xs) auto

end

subsection ‹ Counting elements ›

partial_function (lfp) scount :: "('s stream ⇒ bool) ⇒ 's stream ⇒ enat" where
"scount P ω = (if P ω then eSuc (scount P (stl ω)) else scount P (stl ω))"

lemma scount_simps:
"P ω ⟹ scount P ω = eSuc (scount P (stl ω))"
"¬ P ω ⟹ scount P ω = scount P (stl ω)"
using scount.simps[of P ω] by auto

lemma scount_eq_0I: "alw (not P) ω ⟹ scount P ω = 0"
by (induct arbitrary: ω rule: scount.fixp_induct)

lemma scount_eq_0D: "scount P ω = 0 ⟹ alw (not P) ω"
proof (induction rule: alw.coinduct)
case (alw ω) with scount.simps[of P ω] show ?case
by (simp split: if_split_asm)
qed

lemma scount_eq_0_iff: "scount P ω = 0 ⟷ alw (not P) ω"
by (metis scount_eq_0D scount_eq_0I)

lemma
assumes "ev (alw (not P)) ω"
shows scount_eq_card: "scount P ω = enat (card {i. P (sdrop i ω)})"
and ev_alw_not_HLD_finite: "finite {i. P (sdrop i ω)}"
using assms
proof (induction ω)
case (step ω)
have eq: "{i. P (sdrop i ω)} = (if P ω then {0} else {}) ∪ (Suc ` {i. P (sdrop i (stl ω))})"
apply (intro set_eqI)
apply (case_tac x)
apply (auto simp: image_iff)
done
{ case 1 show ?case
using step unfolding eq by (auto simp: scount_simps card_image zero_notin_Suc_image eSuc_enat) }
{ case 2 show ?case
using step unfolding eq by auto }
next
case (base ω)
then have [simp]: "{i. P (sdrop i ω)} = {}"
{ case 1 show ?case using base by (simp add: scount_eq_0I enat_0) }
{ case 2 show ?case by simp }
qed

lemma scount_finite: "ev (alw (not P)) ω ⟹ scount P ω < ∞"
using scount_eq_card[of P ω] by auto

lemma scount_infinite:
"alw (ev P) ω ⟹ scount P ω = ∞"
proof (coinduction arbitrary: ω rule: enat_coinduct)
case (Eq_enat ω)
then have "ev P ω" "alw (ev P) ω"
by auto
then show ?case
by (induction rule: ev_induct_strong) (auto simp add: scount_simps)
qed

lemma scount_infinite_iff: "scount P ω = ∞ ⟷ alw (ev P) ω"
by (metis enat_ord_simps(4) not_alw_not scount_finite scount_infinite)

lemma scount_eq:
"scount P ω = (if alw (ev P) ω then ∞ else enat (card {i. P (sdrop i ω)}))"
by (auto simp: scount_infinite_iff scount_eq_card not_alw_iff not_ev_iff)

subsection ‹ First index of an element ›

partial_function (gfp) sfirst :: "('s stream ⇒ bool) ⇒ 's stream ⇒ enat" where
"sfirst P ω = (if P ω then 0 else eSuc (sfirst P (stl ω)))"

lemma sfirst_eq_0: "sfirst P ω = 0 ⟷ P ω"
by (subst sfirst.simps) auto

lemma sfirst_0[simp]: "P ω ⟹ sfirst P ω = 0"
by (subst sfirst.simps) auto

lemma sfirst_eSuc[simp]: "¬ P ω ⟹ sfirst P ω = eSuc (sfirst P (stl ω))"
by (subst sfirst.simps) auto

lemma less_sfirstD:
fixes n :: nat
assumes "enat n < sfirst P ω" shows "¬ P (sdrop n ω)"
using assms
proof (induction n arbitrary: ω)
case (Suc n) then show ?case
by (auto simp: sfirst.simps[of _ ω] eSuc_enat[symmetric] split: if_split_asm)

lemma sfirst_finite: "sfirst P ω < ∞ ⟷ ev P ω"
proof
assume "sfirst P ω < ∞"
then obtain n where "sfirst P ω = enat n" by auto
then show "ev P ω"
proof (induction n arbitrary: ω)
case (Suc n) then show ?case
by (auto simp add: eSuc_enat[symmetric] sfirst.simps[of P ω] split: if_split_asm)
qed (auto simp add: enat_0 sfirst_eq_0)
next
assume "ev P ω" then show "sfirst P ω < ∞"
by (induction rule: ev_induct_strong) (auto simp: eSuc_enat)
qed

lemma sfirst_Stream: "sfirst P (s ## x) = (if P (s ## x) then 0 else eSuc (sfirst P x))"
by (subst sfirst.simps) (simp add: HLD_iff)

lemma less_sfirst_iff: "(not P until (alw P)) ω ⟹ enat n < sfirst P ω ⟷ ¬ P (sdrop n ω)"
proof (induction n arbitrary: ω)
case 0 then show ?case
by (simp add: enat_0 sfirst_eq_0 HLD_iff)
next
case (Suc n)
from Suc.prems have **: "P ω ⟹ P (stl ω)"
by (auto elim: UNTIL.cases)
have *: "¬ P (sdrop n (stl ω)) ⟷ enat n < sfirst P (stl ω)"
using Suc.prems by (intro Suc.IH[symmetric]) (auto intro: UNTIL.intros elim: UNTIL.cases)
show ?case
unfolding sdrop.simps * by (cases "P ω") (simp_all add: ** eSuc_enat[symmetric])
qed

lemma sfirst_eq_Inf: "sfirst P ω = Inf {enat i | i. P (sdrop i ω)}"
proof (rule antisym)
show "sfirst P ω ≤ ⨅{enat i |i. P (sdrop i ω)}"
proof (safe intro!: Inf_greatest)
fix ω i assume "P (sdrop i ω)" then show "sfirst P ω ≤ enat i"
proof (induction i arbitrary: ω)
case (Suc i) then show ?case
by (auto simp add: sfirst.simps[of P ω] eSuc_enat[symmetric])
qed auto
qed
show "⨅{enat i |i. P (sdrop i ω)} ≤ sfirst P ω"
proof (induction arbitrary: ω rule: sfirst.fixp_induct)
case (3 f)
have "{enat i |i. P (sdrop i ω)} = (if P ω then {0} else {}) ∪ eSuc ` {enat i |i. P (sdrop i (stl ω))}"
apply (intro set_eqI)
apply (case_tac x rule: enat_coexhaust)
apply (auto simp add: enat_0_iff image_iff eSuc_enat_iff)
done
with 3[of "stl ω"] show ?case
by (auto simp: inf.absorb1 eSuc_Inf[symmetric])
qed simp_all
qed

lemma sfirst_eq_enat_iff: "sfirst P ω = enat n ⟷ ev_at P n ω"
by (induction n arbitrary: ω)

subsection ‹‹stakeWhile››

definition stakeWhile :: "('a ⇒ bool) ⇒ 'a stream ⇒ 'a llist"
where "stakeWhile P xs = ltakeWhile P (llist_of_stream xs)"

lemma stakeWhile_SCons [simp]:
"stakeWhile P (x ## xs) = (if P x then LCons x (stakeWhile P xs) else LNil)"
by(simp add: stakeWhile_def LCons_llist_of_stream[symmetric] del: LCons_llist_of_stream)

lemma lnull_stakeWhile [simp]: "lnull (stakeWhile P xs) ⟷ ¬ P (shd xs)"

lemma lhd_stakeWhile [simp]: "P (shd xs) ⟹ lhd (stakeWhile P xs) = shd xs"

lemma ltl_stakeWhile [simp]:
"ltl (stakeWhile P xs) = (if P (shd xs) then stakeWhile P (stl xs) else LNil)"

lemma stakeWhile_K_False [simp]: "stakeWhile (λ_. False) xs = LNil"