Theory 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"
by(simp add: eq_onp_def)

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]

text ‹lemmas about generated constants›

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)"
by(simp add: llist_of_stream_def)

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

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

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

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

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)"
by(simp add: cr_stream_def Abs_stream_inverse)

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)"
by(rule sym)(simp add: llist_of_stream_def)

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"
by(simp add: rel_fun_def eq_onp_def)

lemma lset_infinite_transfer [transfer_rule]:
  "(eq_onp (λxs. ¬ lfinite xs) ===> (=)) lset lset"
by(simp add: rel_fun_def eq_onp_def)

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"
by(simp add: rel_fun_def stream.pcr_cr_eq cr_stream_def)

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(simp add: llist_all2_def stream_all2_def)
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"
by(simp add: rel_fun_def stream.pcr_cr_eq cr_stream_def)

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"
by(simp add: stream.pcr_cr_eq cr_stream_def rel_fun_def)

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"
by transfer (simp add: fun_eq_iff)

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"
by(simp_all add: snth_SCons)

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)"
by(simp add: siterate_conv_of_seq)

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)
     (auto simp: bot_enat_def intro!: admissible_all admissible_imp admissible_eq_mcontI mcont_const)

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 ω)} = {}"
     by (simp add: not_HLD alw_iff_sdrop)
   { 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)
qed (simp add: enat_0 sfirst_eq_0)

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: ω)
     (simp_all add: eSuc_enat[symmetric] sfirst.simps enat_0)

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)"
by(simp add: stakeWhile_def)

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

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

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

lemma stakeWhile_K_True [simp]: "stakeWhile (λ_. True) xs = llist_of_stream xs"
by(simp add: stakeWhile_def)

lemma stakeWhile_smap: "stakeWhile P (smap f xs) = lmap f (stakeWhile (P ∘ f) xs)"
by(simp add: stakeWhile_def ltakeWhile_lmap[symmetric] del: o_apply)

lemma lfinite_stakeWhile [simp]: "lfinite (stakeWhile P xs) ⟷ (∃x∈sset xs. ¬ P x)"
by(simp add: stakeWhile_def lfinite_ltakeWhile)

end