# Theory Fstream

theory Fstream
imports Stream
```(*  Title:      HOL/HOLCF/FOCUS/Fstream.thy
Author:     David von Oheimb, TU Muenchen

FOCUS streams (with lifted elements).

TODO: integrate Fstreams.thy
*)

section ‹FOCUS flat streams›

theory Fstream
imports "HOLCF-Library.Stream"
begin

default_sort type

type_synonym 'a fstream = "'a lift stream"

definition
fscons        :: "'a     ⇒ 'a fstream → 'a fstream" where
"fscons a = (Λ s. Def a && s)"

definition
fsfilter      :: "'a set ⇒ 'a fstream → 'a fstream" where
"fsfilter A = (sfilter⋅(flift2 (λx. x∈A)))"

abbreviation
emptystream   :: "'a fstream"                          ("<>") where
"<> == ⊥"

abbreviation
fscons'       :: "'a ⇒ 'a fstream ⇒ 'a fstream"       ("(_↝_)" [66,65] 65) where
"a↝s == fscons a⋅s"

abbreviation
fsfilter'     :: "'a set ⇒ 'a fstream ⇒ 'a fstream"   ("(_©_)" [64,63] 63) where

notation (ASCII)
fscons'  ("(_~>_)" [66,65] 65) and
fsfilter'  ("(_'(C')_)" [64,63] 63)

lemma Def_maximal: "a = Def d ⟹ a⊑b ⟹ b = Def d"
by simp

section "fscons"

lemma fscons_def2: "a~>s = Def a && s"
apply (unfold fscons_def)
apply (simp)
done

lemma fstream_exhaust: "x = UU ∨ (∃a y. x = a~> y)"
apply (cut_tac stream.nchotomy)
apply (fast dest: not_Undef_is_Def [THEN iffD1])
done

lemma fstream_cases: "[| x = UU ==> P; !!a y. x = a~> y ==> P |] ==> P"
apply (cut_tac fstream_exhaust)
apply (erule disjE)
apply fast
apply fast
done

lemma fstream_exhaust_eq: "(x ≠ UU) = (∃a y. x = a~> y)"
apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE)
done

lemma fscons_not_empty [simp]: "a~> s ≠ <>"

lemma fscons_inject [simp]: "(a~> s = b~> t) = (a = b ∧ s = t)"

lemma fstream_prefix: "a~> s << t ==> ∃tt. t = a~> tt ∧ s << tt"
apply (cases t)
apply (cut_tac fscons_not_empty)
apply (fast dest: bottomI)
done

lemma fstream_prefix' [simp]:
"x << a~> z = (x = <> ∨ (∃y. x = a~> y ∧ y << z))"
apply (simp add: fscons_def2 lift.distinct(2) [THEN stream_prefix'])
apply (safe)
apply (erule_tac [!] contrapos_np)
prefer 2 apply (fast elim: DefE)
apply (rule lift.exhaust)
apply (erule (1) notE)
apply (safe)
apply (drule Def_below_Def [THEN iffD1])
apply fast
done

(* ------------------------------------------------------------------------- *)

section "ft & rt"

lemmas ft_empty = stream.sel_rews (1)
lemma ft_fscons [simp]: "ft⋅(m~> s) = Def m"

lemmas rt_empty = stream.sel_rews (2)
lemma rt_fscons [simp]: "rt⋅(m~> s) = s"

lemma ft_eq [simp]: "(ft⋅s = Def a) = (∃t. s = a~> t)"
apply (unfold fscons_def)
apply (simp)
apply (safe)
apply (erule subst)
apply (rule exI)
apply (rule surjectiv_scons [symmetric])
apply (simp)
done

lemma surjective_fscons_lemma: "(d↝y = x) = (ft⋅x = Def d & rt⋅x = y)"
by auto

lemma surjective_fscons: "ft⋅x = Def d ⟹ d↝rt⋅x = x"

(* ------------------------------------------------------------------------- *)

section "take"

lemma fstream_take_Suc [simp]:
"stream_take (Suc n)⋅(a~> s) = a~> stream_take n⋅s"

(* ------------------------------------------------------------------------- *)

section "slen"

lemma slen_fscons: "#(m~> s) = eSuc (#s)"

lemma slen_fscons_eq:
"(enat (Suc n) < #x) = (∃a y. x = a~> y ∧ enat n < #y)"
apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE)
done

lemma slen_fscons_eq_rev:
"(#x < enat (Suc (Suc n))) = (∀a y. x ≠ a~> y ∨ #y < enat (Suc n))"
apply (tactic ‹step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1›)
apply (tactic ‹step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1›)
apply (tactic ‹step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1›)
apply (tactic ‹step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1›)
apply (tactic ‹step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1›)
apply (tactic ‹step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1›)
apply (erule contrapos_np)
apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE)
done

lemma slen_fscons_less_eq:
"(#(a~> y) < enat (Suc (Suc n))) = (#y < enat (Suc n))"
apply (subst slen_fscons_eq_rev)
apply (fast dest!: fscons_inject [THEN iffD1])
done

(* ------------------------------------------------------------------------- *)

section "induction"

lemma fstream_ind:
"[| adm P; P <>; !!a s. P s ==> P (a~> s) |] ==> P x"
apply (erule stream.induct)
apply (assumption)
apply (unfold fscons_def2)
apply (fast dest: not_Undef_is_Def [THEN iffD1])
done

lemma fstream_ind2:
"[| adm P; P UU; !!a. P (a~> UU); !!a b s. P s ==> P (a~> b~> s) |] ==> P x"
apply (erule stream_ind2)
apply (assumption)
apply (unfold fscons_def2)
apply (fast dest: not_Undef_is_Def [THEN iffD1])
apply (fast dest: not_Undef_is_Def [THEN iffD1])
done

(* ------------------------------------------------------------------------- *)

section "fsfilter"

lemma fsfilter_empty: "A(C)UU = UU"
apply (unfold fsfilter_def)
apply (rule sfilter_empty)
done

lemma fsfilter_fscons:
"A(C)x~> xs = (if x∈A then x~> (A(C)xs) else A(C)xs)"
apply (unfold fsfilter_def)
done

lemma fsfilter_emptys: "{}(C)x = UU"
apply (rule_tac x="x" in fstream_ind)
apply (simp)
apply (rule fsfilter_empty)
done

lemma fsfilter_insert: "(insert a A)(C)a~> x = a~> ((insert a A)(C)x)"

lemma fsfilter_single_in: "{a}(C)a~> x = a~> ({a}(C)x)"
by (rule fsfilter_insert)

lemma fsfilter_single_out: "b ~= a ==> {a}(C)b~> x = ({a}(C)x)"

lemma fstream_lub_lemma1:
"⟦chain Y; (⨆i. Y i) = a↝s⟧ ⟹ ∃j t. Y j = a↝t"
apply (case_tac "max_in_chain i Y")
apply  (drule (1) lub_finch1 [THEN lub_eqI, THEN sym])
apply  (force)
apply (unfold max_in_chain_def)
apply auto
apply (frule (1) chain_mono)
apply (rule_tac x="Y j" in fstream_cases)
apply  (force)
apply (drule_tac x="j" in is_ub_thelub)
apply (force)
done

lemma fstream_lub_lemma:
"⟦chain Y; (⨆i. Y i) = a↝s⟧ ⟹ (∃j t. Y j = a↝t) ∧ (∃X. chain X ∧ (∀i. ∃j. Y j = a↝X i) ∧ (⨆i. X i) = s)"
apply (frule (1) fstream_lub_lemma1)
apply (clarsimp)
apply (rule_tac x="λi. rt⋅(Y(i+j))" in exI)
apply (rule conjI)
apply  (erule chain_shift [THEN chain_monofun])
apply safe
apply  (drule_tac i="j" and j="i+j" in chain_mono)
apply   (simp)
apply  (simp)
apply  (rule_tac x="i+j" in exI)
apply  (drule fstream_prefix)
apply  (clarsimp)
apply  (subst lub_APP)
apply   (rule chainI)
apply   (fast)
apply  (erule chain_shift)
apply (subst lub_const)
apply (subst lub_range_shift)
apply  (assumption)
apply (simp)
done

end
```