Theory StreamFusion

section ‹Stream Fusion›

theory StreamFusion
imports Stream
begin

subsection ‹Type constructors for state types›

domain Switch = S1 | S2

domain 'a Maybe = Nothing | Just 'a

hide_const (open) Left Right

domain ('a, 'b) Either = Left 'a | Right 'b

domain ('a, 'b) Both  (infixl ‹:!:› 25) = Both 'a 'b (infixl ‹:!:› 75)

domain 'a L = L (lazy 'a)


subsection ‹Map function›

fixrec
  mapStep :: "('a → 'b) → ('s → ('a, 's) Step) → 's → ('b, 's) Step"
where
  "mapStep⋅f⋅h⋅⊥ = ⊥"
| "s ≠ ⊥ ⟹ mapStep⋅f⋅h⋅s = (case h⋅s of
    Done ⇒ Done
  | Skip⋅s' ⇒ Skip⋅s'
  | Yield⋅x⋅s' ⇒ Yield⋅(f⋅x)⋅s')"

fixrec
  mapS :: "('a → 'b) → ('a, 's) Stream → ('b, 's) Stream"
where
  "s ≠ ⊥ ⟹ mapS⋅f⋅(Stream⋅h⋅s) = Stream⋅(mapStep⋅f⋅h)⋅s"

lemma unfold_mapStep:
  fixes f :: "'a → 'b" and h :: "'s → ('a, 's) Step"
  assumes "s ≠ ⊥"
  shows "unfold⋅(mapStep⋅f⋅h)⋅s = mapL⋅f⋅(unfold⋅h⋅s)"
proof (rule below_antisym)
  show "unfold⋅(mapStep⋅f⋅h)⋅s ⊑ mapL⋅f⋅(unfold⋅h⋅s)"
  using ‹s ≠ ⊥›
  apply (induct arbitrary: s rule: unfold_ind [where h="mapStep⋅f⋅h"])
  apply (simp, simp)
  apply (case_tac "h⋅s", simp_all add: unfold)
  done
next
  show "mapL⋅f⋅(unfold⋅h⋅s) ⊑ unfold⋅(mapStep⋅f⋅h)⋅s"
  using ‹s ≠ ⊥›
  apply (induct arbitrary: s rule: unfold_ind [where h="h"])
  apply (simp, simp)
  apply (case_tac "h⋅s", simp_all add: unfold)
  done
qed

lemma unstream_mapS:
  fixes f :: "'a → 'b" and a :: "('a, 's) Stream"
  shows "a ≠ ⊥ ⟹ unstream⋅(mapS⋅f⋅a) = mapL⋅f⋅(unstream⋅a)"
by (induct a, simp, simp add: unfold_mapStep)

lemma mapS_defined: "a ≠ ⊥ ⟹ mapS⋅f⋅a ≠ ⊥"
by (induct a, simp_all)

lemma mapS_cong:
  fixes f :: "'a → 'b"
  fixes a :: "('a, 's) Stream"
  fixes b :: "('a, 't) Stream"
  shows "f = g ⟹ a ≈ b ⟹ mapS⋅f⋅a ≈ mapS⋅g⋅b"
unfolding bisimilar_def
by (simp add: unstream_mapS mapS_defined)

lemma mapL_eq: "mapL⋅f⋅xs = unstream⋅(mapS⋅f⋅(stream⋅xs))"
by (simp add: unstream_mapS)


subsection ‹Filter function›

fixrec
  filterStep :: "('a → tr) → ('s → ('a, 's) Step) → 's → ('a, 's) Step"
where
  "filterStep⋅p⋅h⋅⊥ = ⊥"
| "s ≠ ⊥ ⟹ filterStep⋅p⋅h⋅s = (case h⋅s of
    Done ⇒ Done
  | Skip⋅s' ⇒ Skip⋅s'
  | Yield⋅x⋅s' ⇒ (If p⋅x then Yield⋅x⋅s' else Skip⋅s'))"

fixrec
  filterS :: "('a → tr) → ('a, 's) Stream → ('a, 's) Stream"
where
  "s ≠ ⊥ ⟹ filterS⋅p⋅(Stream⋅h⋅s) = Stream⋅(filterStep⋅p⋅h)⋅s"

lemma unfold_filterStep:
  fixes p :: "'a → tr" and h :: "'s → ('a, 's) Step"
  assumes "s ≠ ⊥"
  shows "unfold⋅(filterStep⋅p⋅h)⋅s = filterL⋅p⋅(unfold⋅h⋅s)"
proof (rule below_antisym)
  show "unfold⋅(filterStep⋅p⋅h)⋅s ⊑ filterL⋅p⋅(unfold⋅h⋅s)"
  using ‹s ≠ ⊥›
  apply (induct arbitrary: s rule: unfold_ind [where h="filterStep⋅p⋅h"])
  apply (simp, simp)
  apply (case_tac "h⋅s", simp_all add: unfold)
  apply (case_tac "p⋅a" rule: trE, simp_all)
  done
next
  show "filterL⋅p⋅(unfold⋅h⋅s) ⊑ unfold⋅(filterStep⋅p⋅h)⋅s"
  using ‹s ≠ ⊥›
  apply (induct arbitrary: s rule: unfold_ind [where h="h"])
  apply (simp, simp)
  apply (case_tac "h⋅s", simp_all add: unfold)
  apply (case_tac "p⋅a" rule: trE, simp_all add: unfold)
  done
qed

lemma unstream_filterS:
  "a ≠ ⊥ ⟹ unstream⋅(filterS⋅p⋅a) = filterL⋅p⋅(unstream⋅a)"
by (induct a, simp, simp add: unfold_filterStep)

lemma filterS_defined: "a ≠ ⊥ ⟹ filterS⋅p⋅a ≠ ⊥"
by (induct a, simp_all)

lemma filterS_cong:
  fixes p :: "'a → tr"
  fixes a :: "('a, 's) Stream"
  fixes b :: "('a, 't) Stream"
  shows "p = q ⟹ a ≈ b ⟹ filterS⋅p⋅a ≈ filterS⋅q⋅b"
unfolding bisimilar_def
by (simp add: unstream_filterS filterS_defined)

lemma filterL_eq: "filterL⋅p⋅xs = unstream⋅(filterS⋅p⋅(stream⋅xs))"
by (simp add: unstream_filterS)


subsection ‹Foldr function›

fixrec
  foldrS :: "('a → 'b → 'b) → 'b → ('a, 's) Stream → 'b"
where
  foldrS_Stream:
  "s ≠ ⊥ ⟹ foldrS⋅f⋅z⋅(Stream⋅h⋅s) =
    (case h⋅s of Done ⇒ z
               | Skip⋅s' ⇒ foldrS⋅f⋅z⋅(Stream⋅h⋅s')
               | Yield⋅x⋅s' ⇒ f⋅x⋅(foldrS⋅f⋅z⋅(Stream⋅h⋅s')))"

lemma unfold_foldrS:
  assumes "s ≠ ⊥" shows "foldrS⋅f⋅z⋅(Stream⋅h⋅s) = foldrL⋅f⋅z⋅(unfold⋅h⋅s)"
proof (rule below_antisym)
  show "foldrS⋅f⋅z⋅(Stream⋅h⋅s) ⊑ foldrL⋅f⋅z⋅(unfold⋅h⋅s)"
  using ‹s ≠ ⊥›
  apply (induct arbitrary: s rule: foldrS.induct)
  apply (simp, simp, simp)
  apply (case_tac "h⋅s", simp_all add: monofun_cfun unfold)
  done
next
  show "foldrL⋅f⋅z⋅(unfold⋅h⋅s) ⊑ foldrS⋅f⋅z⋅(Stream⋅h⋅s)"
  using ‹s ≠ ⊥›
  apply (induct arbitrary: s rule: unfold_ind)
  apply (simp, simp)
  apply (case_tac "h⋅s", simp_all add: monofun_cfun unfold)
  done
qed

lemma unstream_foldrS:
  "a ≠ ⊥ ⟹ foldrS⋅f⋅z⋅a = foldrL⋅f⋅z⋅(unstream⋅a)"
by (induct a, simp, simp del: foldrS_Stream add: unfold_foldrS)

lemma foldrS_cong:
  fixes a :: "('a, 's) Stream"
  fixes b :: "('a, 't) Stream"
  shows "f = g ⟹ z = w ⟹ a ≈ b ⟹ foldrS⋅f⋅z⋅a = foldrS⋅g⋅w⋅b"
by (simp add: bisimilar_def unstream_foldrS)

lemma foldrL_eq:
  "foldrL⋅f⋅z⋅xs = foldrS⋅f⋅z⋅(stream⋅xs)"
by (simp add: unstream_foldrS)


subsection ‹EnumFromTo function›

type_synonym int' = "int⇩⊥"

fixrec
  enumFromToStep :: "int' → (int')⇩⊥ → (int', (int')⇩⊥) Step"
where
  "enumFromToStep⋅(up⋅y)⋅(up⋅(up⋅x)) =
    (if x ≤ y then Yield⋅(up⋅x)⋅(up⋅(up⋅(x+1))) else Done)"

lemma enumFromToStep_strict [simp]:
  "enumFromToStep⋅⊥⋅x'' = ⊥"
  "enumFromToStep⋅(up⋅y)⋅⊥ = ⊥"
  "enumFromToStep⋅(up⋅y)⋅(up⋅⊥) = ⊥"
by fixrec_simp+

lemma enumFromToStep_simps' [simp]:
  "x ≤ y ⟹ enumFromToStep⋅(up⋅y)⋅(up⋅(up⋅x)) =
    Yield⋅(up⋅x)⋅(up⋅(up⋅(x+1)))"
  "¬ x ≤ y ⟹ enumFromToStep⋅(up⋅y)⋅(up⋅(up⋅x)) = Done"
  by simp_all

declare enumFromToStep.simps [simp del]

fixrec
  enumFromToS :: "int' → int' → (int', (int')⇩⊥) Stream"
where
  "enumFromToS⋅x⋅y = Stream⋅(enumFromToStep⋅y)⋅(up⋅x)"

declare enumFromToS.simps [simp del]

lemma unfold_enumFromToStep:
  "unfold⋅(enumFromToStep⋅(up⋅y))⋅(up⋅n) = enumFromToL⋅n⋅(up⋅y)"
proof (rule below_antisym)
  show "unfold⋅(enumFromToStep⋅(up⋅y))⋅(up⋅n) ⊑ enumFromToL⋅n⋅(up⋅y)"
    apply (induct arbitrary: n rule: unfold_ind [where h="enumFromToStep⋅(up⋅y)"])
    apply (simp, simp)
    apply (case_tac n, simp, simp)
    apply (case_tac "x ≤ y", simp_all)
    done
next
  show "enumFromToL⋅n⋅(up⋅y) ⊑ unfold⋅(enumFromToStep⋅(up⋅y))⋅(up⋅n)"
    apply (induct arbitrary: n rule: enumFromToL.induct)
    apply (simp, simp)
    apply (rename_tac e n)
    apply (case_tac n, simp)
    apply (case_tac "x ≤ y", simp_all add: unfold)
    done
qed

lemma unstream_enumFromToS:
  "unstream⋅(enumFromToS⋅x⋅y) = enumFromToL⋅x⋅y"
apply (simp add: enumFromToS.simps)
apply (induct y, simp add: unfold)
apply (induct x, simp add: unfold)
apply (simp add: unfold_enumFromToStep)
done

lemma enumFromToS_defined: "enumFromToS⋅x⋅y ≠ ⊥"
  by (simp add: enumFromToS.simps)

lemma enumFromToS_cong:
  "x = x' ⟹ y = y' ⟹ enumFromToS⋅x⋅y ≈ enumFromToS⋅x'⋅y'"
unfolding bisimilar_def by (simp add: enumFromToS_defined)

lemma enumFromToL_eq: "enumFromToL⋅x⋅y = unstream⋅(enumFromToS⋅x⋅y)"
by (simp add: unstream_enumFromToS)


subsection ‹Append function›

fixrec
  appendStep ::
    "('s → ('a, 's) Step) →
     ('t → ('a, 't) Step) →
     't → ('s, 't) Either → ('a, ('s, 't) Either) Step"
where
  "sa ≠ ⊥ ⟹ appendStep⋅ha⋅hb⋅sb0⋅(Left⋅sa) =
    (case ha⋅sa of
      Done ⇒ Skip⋅(Right⋅sb0)
    | Skip⋅sa' ⇒ Skip⋅(Left⋅sa')
    | Yield⋅x⋅sa' ⇒ Yield⋅x⋅(Left⋅sa'))"
| "sb ≠ ⊥ ⟹ appendStep⋅ha⋅hb⋅sb0⋅(Right⋅sb) =
    (case hb⋅sb of
      Done ⇒ Done
    | Skip⋅sb' ⇒ Skip⋅(Right⋅sb')
    | Yield⋅x⋅sb' ⇒ Yield⋅x⋅(Right⋅sb'))"

lemma appendStep_strict [simp]: "appendStep⋅ha⋅hb⋅sb0⋅⊥ = ⊥"
by fixrec_simp

fixrec
  appendS ::
    "('a, 's) Stream → ('a, 't) Stream → ('a, ('s, 't) Either) Stream"
where
  "sa0 ≠ ⊥ ⟹ sb0 ≠ ⊥ ⟹
    appendS⋅(Stream⋅ha⋅sa0)⋅(Stream⋅hb⋅sb0) =
      Stream⋅(appendStep⋅ha⋅hb⋅sb0)⋅(Left⋅sa0)"

lemma unfold_appendStep:
  fixes ha :: "'s → ('a, 's) Step"
  fixes hb :: "'t → ('a, 't) Step"
  assumes sb0 [simp]: "sb0 ≠ ⊥"
  shows
  "(∀sa. sa ≠ ⊥ ⟶ unfold⋅(appendStep⋅ha⋅hb⋅sb0)⋅(Left⋅sa) =
         appendL⋅(unfold⋅ha⋅sa)⋅(unfold⋅hb⋅sb0)) ∧
   (∀sb. sb ≠ ⊥ ⟶ unfold⋅(appendStep⋅ha⋅hb⋅sb0)⋅(Right⋅sb) =
         unfold⋅hb⋅sb)"
proof -
  note unfold [simp]
  let ?h = "appendStep⋅ha⋅hb⋅sb0"

  have 1:
  "(∀sa. sa ≠ ⊥ ⟶
         unfold⋅?h⋅(Left⋅sa) ⊑
         appendL⋅(unfold⋅ha⋅sa)⋅(unfold⋅hb⋅sb0))
   ∧
   (∀sb. sb ≠ ⊥ ⟶ unfold⋅?h⋅(Right⋅sb) ⊑ unfold⋅hb⋅sb)"
    apply (rule unfold_ind [where h="?h"])
      apply simp
     apply simp
    apply (intro conjI allI impI)
     apply (case_tac "ha⋅sa", simp, simp, simp, simp)
    apply (case_tac "hb⋅sb", simp, simp, simp, simp)
    done

  let ?P = "λua ub. ∀sa. sa ≠ ⊥ ⟶
        appendL⋅(ua⋅sa)⋅(ub⋅sb0) ⊑ unfold⋅?h⋅(Left⋅sa)"

  let ?Q = "λub. ∀sb. sb ≠ ⊥ ⟶ ub⋅sb ⊑ unfold⋅?h⋅(Right⋅sb)"

  have P_base: "⋀ub. ?P ⊥ ub"
    by simp

  have Q_base: "?Q ⊥"
    by simp

  have P_step: "⋀ua ub. ?P ua ub ⟹ ?Q ub ⟹ ?P (unfoldF⋅ha⋅ua) ub"
    apply (intro allI impI)
    apply (case_tac "ha⋅sa", simp, simp, simp, simp)
    done

  have Q_step: "⋀ua ub. ?Q ub ⟹ ?Q (unfoldF⋅hb⋅ub)"
    apply (intro allI impI)
    apply (case_tac "hb⋅sb", simp, simp, simp, simp)
    done

  have Q: "?Q (unfold⋅hb)"
    apply (rule unfold_ind [where h="hb"], simp)
     apply (rule Q_base)
    apply (erule Q_step)
    done

  have P: "?P (unfold⋅ha) (unfold⋅hb)"
    apply (rule unfold_ind [where h="ha"], simp)
     apply (rule P_base)
    apply (erule P_step)
    apply (rule Q)
    done

  have 2: "?P (unfold⋅ha) (unfold⋅hb) ∧ ?Q (unfold⋅hb)"
    using P Q by (rule conjI)

  from 1 2 show ?thesis
    by (simp add: po_eq_conv [where 'a="'a LList"])
qed

lemma appendS_defined: "xs ≠ ⊥ ⟹ ys ≠ ⊥ ⟹ appendS⋅xs⋅ys ≠ ⊥"
by (cases xs, simp, cases ys, simp, simp)

lemma unstream_appendS:
  "a ≠ ⊥ ⟹ b ≠ ⊥ ⟹
    unstream⋅(appendS⋅a⋅b) = appendL⋅(unstream⋅a)⋅(unstream⋅b)"
apply (cases a, simp, cases b, simp)
apply (simp add: unfold_appendStep)
done

lemma appendS_cong:
  fixes f :: "'a → 'b"
  fixes a :: "('a, 's) Stream"
  fixes b :: "('a, 't) Stream"
  shows "a ≈ a' ⟹ b ≈ b' ⟹ appendS⋅a⋅b ≈ appendS⋅a'⋅b'"
unfolding bisimilar_def
by (simp add: unstream_appendS appendS_defined)

lemma appendL_eq: "appendL⋅xs⋅ys = unstream⋅(appendS⋅(stream⋅xs)⋅(stream⋅ys))"
by (simp add: unstream_appendS)


subsection ‹ZipWith function›

fixrec
  zipWithStep ::
    "('a → 'b → 'c) →
     ('s → ('a, 's) Step) →
     ('t → ('b, 't) Step) →
      's :!: 't :!: 'a L Maybe → ('c, 's :!: 't :!: 'a L Maybe) Step"
where
  "sa ≠ ⊥ ⟹ sb ≠ ⊥ ⟹
   zipWithStep⋅f⋅ha⋅hb⋅(sa :!: sb :!: Nothing) =
   (case ha⋅sa of
     Done ⇒ Done
   | Skip⋅sa' ⇒ Skip⋅(sa' :!: sb :!: Nothing)
   | Yield⋅a⋅sa' ⇒ Skip⋅(sa' :!: sb :!: Just⋅(L⋅a)))"
| "sa ≠ ⊥ ⟹ sb ≠ ⊥ ⟹
   zipWithStep⋅f⋅ha⋅hb⋅(sa :!: sb :!: Just⋅(L⋅a)) =
   (case hb⋅sb of
     Done ⇒ Done
   | Skip⋅sb' ⇒ Skip⋅(sa :!: sb' :!: Just⋅(L⋅a))
   | Yield⋅b⋅sb' ⇒ Yield⋅(f⋅a⋅b)⋅(sa :!: sb' :!: Nothing))"

lemma zipWithStep_strict [simp]: "zipWithStep⋅f⋅ha⋅hb⋅⊥ = ⊥"
by fixrec_simp

fixrec
  zipWithS :: "('a → 'b → 'c) →
      ('a, 's) Stream → ('b, 't) Stream → ('c, 's :!: 't :!: 'a L Maybe) Stream"
where
  "sa0 ≠ ⊥ ⟹ sb0 ≠ ⊥ ⟹ zipWithS⋅f⋅(Stream⋅ha⋅sa0)⋅(Stream⋅hb⋅sb0) =
    Stream⋅(zipWithStep⋅f⋅ha⋅hb)⋅(sa0 :!: sb0 :!: Nothing)"

lemma zipWithS_fix_ind_lemma:
  fixes P Q :: "nat ⇒ nat ⇒ bool"
  assumes P_0: "⋀j. P 0 j" and P_Suc: "⋀i j. P i j ⟹ Q i j ⟹ P (Suc i) j"
  assumes Q_0: "⋀i. Q i 0" and Q_Suc: "⋀i j. P i j ⟹ Q i j ⟹ Q i (Suc j)"
  shows "P i j ∧ Q i j"
apply (induct n ≡ "i + j" arbitrary: i j)
apply (simp add: P_0 Q_0)
apply (rule conjI)
apply (case_tac i, simp add: P_0, simp add: P_Suc)
apply (case_tac j, simp add: Q_0, simp add: Q_Suc)
done

lemma zipWithS_fix_ind:
  assumes x: "x = fix⋅f" and y: "y = fix⋅g"
  assumes adm_P: "adm (λx. P (fst x) (snd x))"
  assumes adm_Q: "adm (λx. Q (fst x) (snd x))"
  assumes P_0: "⋀b. P ⊥ b" and P_Suc: "⋀a b. P a b ⟹ Q a b ⟹ P (f⋅a) b"
  assumes Q_0: "⋀a. Q a ⊥" and Q_Suc: "⋀a b. P a b ⟹ Q a b ⟹ Q a (g⋅b)"
  shows "P x y ∧ Q x y"
proof -
  have 1: "⋀i j. P (iterate i⋅f⋅⊥) (iterate j⋅g⋅⊥) ∧ Q (iterate i⋅f⋅⊥) (iterate j⋅g⋅⊥)"
    apply (rule_tac i=i and j=j in zipWithS_fix_ind_lemma)
    apply (simp add: P_0)
    apply (simp add: P_Suc)
    apply (simp add: Q_0)
    apply (simp add: Q_Suc)
    done
  have "case_prod P (⨆i. (iterate i⋅f⋅⊥, iterate i⋅g⋅⊥))"
    apply (rule admD)
    apply (simp add: split_def adm_P)
    apply simp
    apply (simp add: 1)
    done
  then have P: "P x y"
    unfolding x y fix_def2
    by (simp add: lub_prod)
  have "case_prod Q (⨆i. (iterate i⋅f⋅⊥, iterate i⋅g⋅⊥))"
    apply (rule admD)
    apply (simp add: split_def adm_Q)
    apply simp
    apply (simp add: 1)
    done
  then have Q: "Q x y"
    unfolding x y fix_def2
    by (simp add: lub_prod)
  from P Q show ?thesis by simp
qed

lemma unfold_zipWithStep:
  fixes f :: "'a → 'b → 'c"
  fixes ha :: "'s → ('a, 's) Step"
  fixes hb :: "'t → ('b, 't) Step"
  defines h_def: "h ≡ zipWithStep⋅f⋅ha⋅hb"
  shows
  "(∀sa sb. sa ≠ ⊥ ⟶ sb ≠ ⊥ ⟶
    unfold⋅h⋅(sa :!: sb :!: Nothing) =
      zipWithL⋅f⋅(unfold⋅ha⋅sa)⋅(unfold⋅hb⋅sb)) ∧
   (∀sa sb a. sa ≠ ⊥ ⟶ sb ≠ ⊥ ⟶
    unfold⋅h⋅(sa :!: sb :!: Just⋅(L⋅a)) =
      zipWithL⋅f⋅(LCons⋅a⋅(unfold⋅ha⋅sa))⋅(unfold⋅hb⋅sb))"
proof -
  note unfold [simp]
  have h_simps [simp]:
    "⋀sa sb. sa ≠ ⊥ ⟹ sb ≠ ⊥ ⟹ h⋅(sa :!: sb :!: Nothing) =
      (case ha⋅sa of
        Done ⇒ Done
      | Skip⋅sa' ⇒ Skip⋅(sa' :!: sb :!: Nothing)
      | Yield⋅a⋅sa' ⇒ Skip⋅(sa' :!: sb :!: Just⋅(L⋅a)))"
    "⋀sa sb a. sa ≠ ⊥ ⟹ sb ≠ ⊥ ⟹ h⋅(sa :!: sb :!: Just⋅(L⋅a)) =
      (case hb⋅sb of
        Done ⇒ Done
      | Skip⋅sb' ⇒ Skip⋅(sa :!: sb' :!: Just⋅(L⋅a))
      | Yield⋅b⋅sb' ⇒ Yield⋅(f⋅a⋅b)⋅(sa :!: sb' :!: Nothing))"
    "h⋅⊥ = ⊥"
    unfolding h_def by simp_all

  have 1:
  "(∀sa sb. sa ≠ ⊥ ⟶ sb ≠ ⊥ ⟶
    unfold⋅h⋅(sa :!: sb :!: Nothing) ⊑
      zipWithL⋅f⋅(unfold⋅ha⋅sa)⋅(unfold⋅hb⋅sb))
   ∧
   (∀sa sb a. sa ≠ ⊥ ⟶ sb ≠ ⊥ ⟶
    unfold⋅h⋅(sa :!: sb :!: Just⋅(L⋅a)) ⊑
      zipWithL⋅f⋅(LCons⋅a⋅(unfold⋅ha⋅sa))⋅(unfold⋅hb⋅sb))"
    apply (rule unfold_ind [where h="h"], simp)
     apply simp
    apply (intro conjI allI impI)
     apply (case_tac "ha⋅sa", simp, simp, simp, simp)
    apply (case_tac "hb⋅sb", simp, simp, simp, simp)
    done

  let ?P = "λua ub. ∀sa sb. sa ≠ ⊥ ⟶ sb ≠ ⊥ ⟶
        zipWithL⋅f⋅(ua⋅sa)⋅(ub⋅sb) ⊑ unfold⋅h⋅(sa :!: sb :!: Nothing)"

  let ?Q = "λua ub. ∀sa sb a. sa ≠ ⊥ ⟶ sb ≠ ⊥ ⟶
        zipWithL⋅f⋅(LCons⋅a⋅(ua⋅sa))⋅(ub⋅sb) ⊑
          unfold⋅h⋅(sa :!: sb :!: Just⋅(L⋅a))"

  have P_base: "⋀ub. ?P ⊥ ub"
    by simp

  have Q_base: "⋀ua. ?Q ua ⊥"
    by simp

  have P_step: "⋀ua ub. ?P ua ub ⟹ ?Q ua ub ⟹ ?P (unfoldF⋅ha⋅ua) ub"
    by (clarsimp, case_tac "ha⋅sa", simp_all)

  have Q_step: "⋀ua ub. ?P ua ub ⟹ ?Q ua ub ⟹ ?Q ua (unfoldF⋅hb⋅ub)"
    by (clarsimp, case_tac "hb⋅sb", simp_all)

  have 2: "?P (unfold⋅ha) (unfold⋅hb) ∧ ?Q (unfold⋅ha) (unfold⋅hb)"
    apply (rule zipWithS_fix_ind [OF unfold_eq_fix [of ha] unfold_eq_fix [of hb]])
    apply (simp, simp) (* admissibility *)
    apply (rule P_base)
    apply (erule (1) P_step)
    apply (rule Q_base)
    apply (erule (1) Q_step)
    done

  from 1 2 show ?thesis
    by (simp_all add: po_eq_conv [where 'a="'c LList"])
qed

lemma zipWithS_defined: "a ≠ ⊥ ⟹ b ≠ ⊥ ⟹ zipWithS⋅f⋅a⋅b ≠ ⊥"
by (cases a, simp, cases b, simp, simp)

lemma unstream_zipWithS:
  "a ≠ ⊥ ⟹ b ≠ ⊥ ⟹
    unstream⋅(zipWithS⋅f⋅a⋅b) = zipWithL⋅f⋅(unstream⋅a)⋅(unstream⋅b)"
apply (cases a, simp, cases b, simp)
apply (simp add: unfold_zipWithStep)
done

lemma zipWithS_cong:
  "f = f' ⟹ a ≈ a' ⟹ b ≈ b' ⟹
    zipWithS⋅f⋅a⋅b ≈ zipWithS⋅f⋅a'⋅b'"
unfolding bisimilar_def
by (simp add: unstream_zipWithS zipWithS_defined)

lemma zipWithL_eq:
  "zipWithL⋅f⋅xs⋅ys = unstream⋅(zipWithS⋅f⋅(stream⋅xs)⋅(stream⋅ys))"
by (simp add: unstream_zipWithS)


subsection ‹ConcatMap function›

fixrec
  concatMapStep ::
    "('a → ('b, 't) Stream) →
     ('s → ('a, 's) Step) →
     's :!: ('b, 't) Stream Maybe →
     ('b, 's :!: ('b, 't) Stream Maybe) Step"
where
  "sa ≠ ⊥ ⟹ concatMapStep⋅f⋅ha⋅(sa :!: Nothing) =
    (case ha⋅sa of
      Done ⇒ Done
    | Skip⋅sa' ⇒ Skip⋅(sa' :!: Nothing)
    | Yield⋅a⋅sa' ⇒ Skip⋅(sa' :!: Just⋅(f⋅a)))"
| "sa ≠ ⊥ ⟹ sb ≠ ⊥ ⟹
    concatMapStep⋅f⋅ha⋅(sa :!: Just⋅(Stream⋅hb⋅sb)) =
    (case hb⋅sb of
      Done ⇒ Skip⋅(sa :!: Nothing)
    | Skip⋅sb' ⇒ Skip⋅(sa :!: Just⋅(Stream⋅hb⋅sb'))
    | Yield⋅b⋅sb' ⇒ Yield⋅b⋅(sa :!: Just⋅(Stream⋅hb⋅sb')))"

lemma concatMapStep_strict [simp]: "concatMapStep⋅f⋅ha⋅⊥ = ⊥"
by fixrec_simp

fixrec
  concatMapS ::
    "('a → ('b, 't) Stream) → ('a, 's) Stream →
     ('b, 's :!: ('b, 't) Stream Maybe) Stream"
where
  "s ≠ ⊥ ⟹ concatMapS⋅f⋅(Stream⋅h⋅s) = Stream⋅(concatMapStep⋅f⋅h)⋅(s :!: Nothing)"

lemma concatMapS_strict [simp]: "concatMapS⋅f⋅⊥ = ⊥"
by fixrec_simp

lemma unfold_concatMapStep:
  fixes ha :: "'s → ('a, 's) Step"
  fixes f :: "'a → ('b, 't) Stream"
  defines h_def: "h ≡ concatMapStep⋅f⋅ha"
  defines f'_def: "f' ≡ unstream oo f"
  shows
  "(∀sa. sa ≠ ⊥ ⟶
      unfold⋅h⋅(sa :!: Nothing) = concatMapL⋅f'⋅(unfold⋅ha⋅sa)) ∧
   (∀sa hb sb. sa ≠ ⊥ ⟶ sb ≠ ⊥ ⟶
      unfold⋅h⋅(sa :!: Just⋅(Stream⋅hb⋅sb)) =
        appendL⋅(unfold⋅hb⋅sb)⋅(concatMapL⋅f'⋅(unfold⋅ha⋅sa)))"
proof -
  note unfold [simp]
  have h_simps [simp]:
    "⋀sa. sa ≠ ⊥ ⟹ h⋅(sa :!: Nothing) =
      (case ha⋅sa of Done ⇒ Done
      | Skip⋅sa' ⇒ Skip⋅(sa' :!: Nothing)
      | Yield⋅a⋅sa' ⇒ Skip⋅(sa' :!: Just⋅(f⋅a)))"
    "⋀sa hb sb. sa ≠ ⊥ ⟹ sb ≠ ⊥ ⟹ h⋅(sa :!: Just⋅(Stream⋅hb⋅sb)) =
      (case hb⋅sb of Done ⇒ Skip⋅(sa :!: Nothing)
      | Skip⋅sb' ⇒ Skip⋅(sa :!: Just⋅(Stream⋅hb⋅sb'))
      | Yield⋅b⋅sb' ⇒ Yield⋅b⋅(sa :!: Just⋅(Stream⋅hb⋅sb')))"
    "h⋅⊥ = ⊥"
    unfolding h_def by simp_all

  have f'_beta [simp]: "⋀a. f'⋅a = unstream⋅(f⋅a)"
    unfolding f'_def by simp

  have 1:
  "(∀sa. sa ≠ ⊥ ⟶
      unfold⋅h⋅(sa :!: Nothing) ⊑ concatMapL⋅f'⋅(unfold⋅ha⋅sa))
   ∧
   (∀sa hb sb. sa ≠ ⊥ ⟶ sb ≠ ⊥ ⟶
      unfold⋅h⋅(sa :!: Just⋅(Stream⋅hb⋅sb)) ⊑
        appendL⋅(unfold⋅hb⋅sb)⋅(concatMapL⋅f'⋅(unfold⋅ha⋅sa)))"
    apply (rule unfold_ind [where h="h"], simp)
     apply simp
    apply (intro conjI allI impI)
     apply (case_tac "ha⋅sa", simp, simp, simp)
     apply (rename_tac a sa')
     apply (case_tac "f⋅a", simp, simp)
    apply (case_tac "hb⋅sb", simp, simp, simp, simp)
    done

  let ?P = "λua. ∀sa. sa ≠ ⊥ ⟶
        concatMapL⋅f'⋅(ua⋅sa) ⊑ unfold⋅h⋅(sa :!: Nothing)"

  let ?Q = "λhb ua ub. ∀sa sb. sa ≠ ⊥ ⟶ sb ≠ ⊥ ⟶
        appendL⋅(ub⋅sb)⋅(concatMapL⋅f'⋅(ua⋅sa)) ⊑
            unfold⋅h⋅(sa :!: Just⋅(Stream⋅hb⋅sb))"

  have P_base: "?P ⊥"
    by simp

  have P_step: "⋀ua. ?P ua ⟹ ∀hb. ?Q hb ua (unfold⋅hb) ⟹ ?P (unfoldF⋅ha⋅ua)"
    apply (intro allI impI)
    apply (case_tac "ha⋅sa", simp, simp, simp)
    apply (rename_tac a sa')
    apply (case_tac "f⋅a", simp, simp)
    done

  have Q_base: "⋀ua hb. ?Q hb ua ⊥"
    by simp

  have Q_step: "⋀hb ua ub. ?P ua ⟹ ?Q hb ua ub ⟹ ?Q hb ua (unfoldF⋅hb⋅ub)"
    apply (intro allI impI)
    apply (case_tac "hb⋅sb", simp, simp, simp, simp)
    done

  have 2: "?P (unfold⋅ha) ∧ (∀hb. ?Q hb (unfold⋅ha) (unfold⋅hb))"
    apply (rule unfold_ind [where h="ha"], simp)
     apply (rule conjI)
      apply (rule P_base)
     apply (rule allI, rule_tac h=hb in unfold_ind, simp)
      apply (rule Q_base)
     apply (erule Q_step [OF P_base])
    apply (erule conjE)
    apply (rule conjI)
     apply (erule (1) P_step)
    apply (rule allI, rule_tac h=hb in unfold_ind, simp)
     apply (rule Q_base)
    apply (erule (2) Q_step [OF P_step])
    done

  from 1 2 show ?thesis
    by (simp_all add: po_eq_conv [where 'a="'b LList"])
qed

lemma unstream_concatMapS:
  "unstream⋅(concatMapS⋅f⋅a) = concatMapL⋅(unstream oo f)⋅(unstream⋅a)"
by (cases a, simp, simp add: unfold_concatMapStep)

lemma concatMapS_defined: "a ≠ ⊥ ⟹ concatMapS⋅f⋅a ≠ ⊥"
by (induct a, simp_all)

lemma concatMapS_cong:
  fixes f :: "'a ⇒ ('b, 's) Stream"
  fixes g :: "'a ⇒ ('b, 't) Stream"
  fixes a :: "('a, 'u) Stream"
  fixes b :: "('a, 'v) Stream"
  shows "(⋀x. f x ≈ g x) ⟹ a ≈ b ⟹ cont f ⟹ cont g ⟹
    concatMapS⋅(Λ x. f x)⋅a ≈ concatMapS⋅(Λ x. g x)⋅b"
unfolding bisimilar_def
by (simp add: unstream_concatMapS oo_def concatMapS_defined)

lemma concatMapL_eq:
  "concatMapL⋅f⋅xs = unstream⋅(concatMapS⋅(stream oo f)⋅(stream⋅xs))"
by (simp add: unstream_concatMapS oo_def eta_cfun)


subsection ‹Examples›

lemmas stream_eqs =
  mapL_eq
  filterL_eq
  foldrL_eq
  enumFromToL_eq
  appendL_eq
  zipWithL_eq
  concatMapL_eq

lemmas stream_congs =
  unstream_cong
  stream_cong
  stream_unstream_cong
  mapS_cong
  filterS_cong
  foldrS_cong
  enumFromToS_cong
  appendS_cong
  zipWithS_cong
  concatMapS_cong

lemma
  "mapL⋅f oo filterL⋅p oo mapL⋅g =
   unstream oo mapS⋅f oo filterS⋅p oo mapS⋅g oo stream"
apply (rule cfun_eqI, simp)
apply (unfold stream_eqs)
apply (intro stream_congs refl)
done

lemma
  "foldrL⋅f⋅z⋅(mapL⋅g⋅(filterL⋅p⋅(enumFromToL⋅x⋅y))) =
    foldrS⋅f⋅z⋅(mapS⋅g⋅(filterS⋅p⋅(enumFromToS⋅x⋅y)))"
apply (unfold stream_eqs)
apply (intro stream_congs refl)
done

lemma oo_LAM [simp]: "cont g ⟹ f oo (Λ x. g x) = (Λ x. f⋅(g x))"
  unfolding oo_def by simp

lemma
  "concatMapL⋅(Λ k.
    mapL⋅(Λ m. f⋅k⋅m)⋅(enumFromToL⋅one⋅k))⋅(enumFromToL⋅one⋅n) =
   unstream⋅(concatMapS⋅(Λ k.
    mapS⋅(Λ m. f⋅k⋅m)⋅(enumFromToS⋅one⋅k))⋅(enumFromToS⋅one⋅n))"
unfolding stream_eqs
apply simp
apply (simp add: stream_congs)
done

end