Theory Omega_Words_Fun_Stream

    Author:   Benedikt Seidl
    License:  BSD

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

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

(* 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+