Theory Omega_Words_Fun_Stream

(*
    Author:   Benedikt Seidl
    License:  BSD
*)

section ‹Convert between $\omega$-Words and Streams›

theory Omega_Words_Fun_Stream
imports
  "HOL-Library.Omega_Words_Fun" "HOL-Library.Stream"
begin

(* TODO add to HOL-Library.Omega_Words_Fun *)

definition to_omega :: "'a stream ⇒ 'a word" where
  "to_omega ≡ snth"

definition to_stream :: "'a word ⇒ 'a stream" where
  "to_stream w ≡ smap w nats"


lemma to_omega_to_stream[simp]:
  "to_omega (to_stream w) = w"
  unfolding to_omega_def to_stream_def
  by auto

lemma to_stream_to_omega[simp]:
  "to_stream (to_omega s) = s"
  unfolding to_omega_def to_stream_def
  by (metis stream_smap_nats)

lemma bij_to_omega:
  "bij to_omega"
  by (metis bijI' to_omega_to_stream to_stream_to_omega)

lemma bij_to_stream:
  "bij to_stream"
  by (metis bijI' to_omega_to_stream to_stream_to_omega)

lemma image_intersection[simp]:
  "to_omega ` (A ∩ B) = to_omega ` A ∩ to_omega ` B"
  "to_stream ` (C ∩ D) = to_stream ` C ∩ to_stream ` D"
  by (simp_all add: bij_is_inj bij_to_omega bij_to_stream image_Int)

lemma to_stream_snth[simp]:
  "(to_stream w) !! k = w k"
  by (simp add: to_stream_def)

lemma to_omega_index[simp]:
  "(to_omega s) k = s !! k"
  by (metis to_stream_snth to_stream_to_omega)

lemma to_stream_stake[simp]:
  "stake k (to_stream w) = prefix k w"
  by (induction k) (simp add: to_stream_def)+

lemma to_omega_prefix[simp]:
  "prefix k (to_omega s) = stake k s"
  by (metis to_stream_stake to_stream_to_omega)

lemma in_image[simp]:
  "x ∈ to_omega ` X ⟷ to_stream x ∈ X"
  "y ∈ to_stream ` Y ⟷ to_omega y ∈ Y"
  by force+

end