# Theory Fstreams

theory Fstreams
imports Stream

theory Fstreams
imports
begin

default_sort type

type_synonym 'a fstream =

definition
fsingleton    ::   ( [1000] 999) where
fsingleton_def2:

definition
fsfilter      ::  where

definition
fsmap         ::  where

definition
jth           ::  where

definition
first         ::  where

definition
last          ::  where

abbreviation
emptystream ::   () where

abbreviation
fsfilter' ::        ( [64,63] 63) where

notation (ASCII)
fsfilter'  ( [64,63] 63)

lemma ft_fsingleton[simp]:

lemma slen_fsingleton[simp]:

lemma slen_fstreams[simp]:

lemma slen_fstreams2[simp]:
apply (cases )
apply (insert slen_sconc [of _ s  ], auto)
done

lemma j_th_0_fsingleton[simp]:
done

lemma jth_0[simp]:
done

lemma first_sconc[simp]:

lemma first_fsingleton[simp]:

lemma jth_n[simp]:
apply (simp add: enat_defs split: enat.splits)
done

lemma last_sconc[simp]:
apply (drule sym, auto)
done

lemma last_fsingleton[simp]:

lemma first_UU[simp]:

lemma last_UU[simp]:
by (simp add: last_def jth_def enat_defs)

lemma last_infinite[simp]:

lemma jth_slen_lemma1:
by (simp add: jth_def enat_defs split:enat.splits, auto)

lemma jth_UU[simp]:

lemma ext_last:
apply (case_tac , auto)
apply (subgoal_tac )
apply (drule slen_take_lemma1, auto)
apply (case_tac )
apply auto
apply (case_tac , auto)
apply (drule i_rt_slen [THEN iffD1])
apply (drule slen_take_eq_rev [rule_format, THEN iffD2],auto)
apply (drule not_Undef_is_Def [THEN iffD1], auto)
done

lemma fsingleton_lemma1[simp]:

lemma fsingleton_lemma2[simp]:

lemma fsingleton_sconc:

lemma fstreams_ind:

apply (rule stream.induct, auto)
apply (drule not_Undef_is_Def [THEN iffD1], auto)
done

lemma fstreams_ind2:

apply (rule stream_ind2, auto)
apply (drule not_Undef_is_Def [THEN iffD1], auto)+
done

lemma fstreams_take_Suc[simp]:

lemma fstreams_not_empty[simp]:

lemma fstreams_not_empty2[simp]:
by (case_tac , auto)

lemma fstreams_exhaust:
apply (erule contrapos_pp, auto)
apply (drule stream_exhaust_eq [THEN iffD1], auto)
apply (drule not_Undef_is_Def [THEN iffD1], auto)
done

lemma fstreams_cases:
by (insert fstreams_exhaust [of x], auto)

lemma fstreams_exhaust_eq:
apply (drule stream_exhaust_eq [THEN iffD1], auto)
apply (drule not_Undef_is_Def [THEN iffD1], auto)
done

lemma fstreams_inject:

lemma fstreams_prefix:
apply (insert stream_prefix [of  s t], auto)
done

lemma fstreams_prefix':
apply (auto, case_tac , auto)
apply (drule stream_exhaust_eq [THEN iffD1], auto)
apply (drule ax_flat, simp)
apply (erule sconc_mono)
done

lemma ft_fstreams[simp]:

lemma rt_fstreams[simp]:

lemma ft_eq[simp]:
apply (cases s, auto)
done

lemma surjective_fstreams:
by auto

lemma fstreams_mono:

lemma fsmap_UU[simp]:

lemma fsmap_fsingleton_sconc:
by (simp add: fsmap_def fsingleton_def2 flift2_def)

lemma fsmap_fsingleton[simp]:
by (simp add: fsmap_def fsingleton_def2 flift2_def)

lemma fstreams_chain_lemma[rule_format]:

apply (induct_tac n, auto)
apply (case_tac , auto)
apply (drule stream_exhaust_eq [THEN iffD1], auto)
apply (case_tac , auto)
apply (drule stream_exhaust_eq [THEN iffD1], auto)
apply (case_tac , auto)
apply (drule stream_exhaust_eq [THEN iffD1], auto)
apply (erule_tac x= in allE)
apply (drule stream_prefix, auto)
apply (case_tac ,auto)
apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
apply auto
apply (erule_tac x= in allE)
apply (erule_tac x= in allE, auto)
done

lemma fstreams_lub_lemma1:
apply (subgoal_tac )
apply (frule lub_eq_bottom_iff, auto)
apply (drule_tac x= in is_ub_thelub, auto)
apply (drule fstreams_prefix' [THEN iffD1], auto)
done

lemma fstreams_lub1:

apply (rule_tac x= in exI, auto)
apply (induct_tac i, auto)
apply (drule fstreams_lub_lemma1, auto)
apply (rule_tac x= in exI, auto)
apply (case_tac )
apply (frule lub_finch1 [THEN lub_eqI], auto)
apply (rule_tac x= in exI)
apply (erule subst) back back
apply (rule_tac x= in exI)
apply (subgoal_tac )
apply (drule fstreams_prefix, auto)+
apply (rule sconc_mono)
apply (rule fstreams_chain_lemma, auto)
apply (subgoal_tac , clarsimp)
apply (drule fstreams_mono, simp)
apply (rule is_ub_thelub, simp)
apply (blast intro: chain_mono)
by (rule stream_reach2)

lemma lub_Pair_not_UU_lemma:

apply (frule lub_prod, clarsimp)
apply (clarsimp simp add: lub_eq_bottom_iff [where Y=])
apply (case_tac , clarsimp)
apply (case_tac )
apply (drule maxinch_is_thelub, auto)
apply (rule_tac x= in exI, auto)
apply (subgoal_tac ,auto)
apply (drule ax_flat, auto)
apply (case_tac ,auto)
apply (case_tac , auto)
apply (rule_tac x= in exI)
apply (case_tac ,auto)
apply (drule chain_mono, auto)
done

lemma fstreams_lub_lemma2:

apply (frule lub_Pair_not_UU_lemma, auto)
apply (drule_tac x= in is_ub_thelub, auto)
apply (drule ax_flat, clarsimp)
apply (drule fstreams_prefix' [THEN iffD1], auto)
done

lemma fstreams_lub2:

apply (rule_tac x= in exI, auto)
apply (induct_tac i, auto)
apply (drule fstreams_lub_lemma2, auto)
apply (rule_tac x= in exI, auto)
apply (case_tac )
apply (frule lub_finch1 [THEN lub_eqI], auto)
apply (rule_tac x= in exI)
apply (erule subst) back back
apply (rule_tac x= in exI)
apply (subgoal_tac )
apply (drule below_trans)
apply (drule fstreams_prefix, auto)+
apply (rule sconc_mono)
apply (subgoal_tac  )
apply (blast intro: fstreams_chain_lemma)
apply (frule lub_prod, auto)
apply (subgoal_tac , clarsimp)
apply (drule fstreams_mono, simp)
apply (rule is_ub_thelub chainI)
apply (subgoal_tac , simp)
apply (drule ax_flat, simp)+
apply (drule prod_eqI, auto)