Theory Transition_Systems_and_Automata.Sequence
section ‹Finite and Infinite Sequences›
theory Sequence
imports
"Basic"
"HOL-Library.Stream"
"HOL-Library.Monad_Syntax"
begin
subsection ‹List Basics›
declare upt_Suc[simp del]
declare last.simps[simp del]
declare butlast.simps[simp del]
declare Cons_nth_drop_Suc[simp]
declare list.pred_True[simp]
lemma list_pred_cases:
assumes "list_all P xs"
obtains (nil) "xs = []" | (cons) y ys where "xs = y # ys" "P y" "list_all P ys"
using assms by (cases xs) (auto)
lemma lists_iff_set: "w ∈ lists A ⟷ set w ⊆ A" by auto
lemma fold_const: "fold const xs a = last (a # xs)"
by (induct xs arbitrary: a) (auto simp: last.simps)
lemma take_Suc: "take (Suc n) xs = (if xs = [] then [] else hd xs # take n (tl xs))"
by (simp add: take_Suc)
lemma bind_map[simp]: "map f xs ⤜ g = xs ⤜ g ∘ f" unfolding List.bind_def by simp
lemma ball_bind[iff]: "Ball (set (xs ⤜ f)) P ⟷ (∀ x ∈ set xs. ∀ y ∈ set (f x). P y)"
unfolding set_list_bind by simp
lemma bex_bind[iff]: "Bex (set (xs ⤜ f)) P ⟷ (∃ x ∈ set xs. ∃ y ∈ set (f x). P y)"
unfolding set_list_bind by simp
lemma list_choice: "list_all (λ x. ∃ y. P x y) xs ⟷ (∃ ys. list_all2 P xs ys)"
by (induct xs) (auto simp: list_all2_Cons1)
lemma listset_member: "ys ∈ listset XS ⟷ list_all2 (∈) ys XS"
by (induct XS arbitrary: ys) (auto simp: set_Cons_def list_all2_Cons2)
lemma listset_empty[iff]: "listset XS = {} ⟷ ¬ list_all (λ A. A ≠ {}) XS"
by (induct XS) (auto simp: set_Cons_def)
lemma listset_finite[iff]:
assumes "list_all (λ A. A ≠ {}) XS"
shows "finite (listset XS) ⟷ list_all finite XS"
using assms
proof (induct XS)
case Nil
show ?case by simp
next
case (Cons A XS)
note [simp] = finite_image_iff finite_cartesian_product_iff
have "listset (A # XS) = case_prod Cons ` (A × listset XS)" by (auto simp: set_Cons_def)
also have "finite … ⟷ finite (A × listset XS)" by (simp add: inj_on_def)
also have "… ⟷ finite A ∧ finite (listset XS)" using Cons(2) by simp
also have "finite (listset XS) ⟷ list_all finite XS" using Cons by simp
also have "finite A ∧ … ⟷ list_all finite (A # XS)" by simp
finally show ?case by this
qed
lemma listset_finite'[intro]:
assumes "list_all finite XS"
shows "finite (listset XS)"
using infinite_imp_nonempty assms by blast
lemma listset_card[simp]: "card (listset XS) = prod_list (map card XS)"
proof (induct XS)
case Nil
show ?case by simp
next
case (Cons A XS)
have 1: "inj (case_prod Cons)" unfolding inj_def by simp
have "listset (A # XS) = case_prod Cons ` (A × listset XS)" by (auto simp: set_Cons_def)
also have "card … = card (A × listset XS)" using card_image 1 by auto
also have "… = card A * card (listset XS)" using card_cartesian_product by this
also have "card (listset XS) = prod_list (map card XS)" using Cons by this
also have "card A * … = prod_list (map card (A # XS))" by simp
finally show ?case by this
qed
subsection ‹Stream Basics›
declare stream.map_id[simp]
declare stream.set_map[simp]
declare stream.set_sel(1)[intro!, simp]
declare stream.pred_True[simp]
declare stream.pred_map[iff]
declare stream.rel_map[iff]
declare shift_simps[simp del]
declare stake_sdrop[simp]
declare stake_siterate[simp del]
declare sdrop_snth[simp]
lemma stream_pred_cases:
assumes "pred_stream P xs"
obtains (scons) y ys where "xs = y ## ys" "P y" "pred_stream P ys"
using assms by (cases xs) (auto)
lemma stream_rel_coinduct[case_names stream_rel, coinduct pred: stream_all2]:
assumes "R u v"
assumes "⋀ a u b v. R (a ## u) (b ## v) ⟹ P a b ∧ R u v"
shows "stream_all2 P u v"
using assms by (coinduct) (metis stream.collapse)
lemma stream_rel_coinduct_shift[case_names stream_rel, consumes 1]:
assumes "R u v"
assumes "⋀ u v. R u v ⟹
∃ u⇩1 u⇩2 v⇩1 v⇩2. u = u⇩1 @- u⇩2 ∧ v = v⇩1 @- v⇩2 ∧ u⇩1 ≠ [] ∧ v⇩1 ≠ [] ∧ list_all2 P u⇩1 v⇩1 ∧ R u⇩2 v⇩2"
shows "stream_all2 P u v"
proof -
have "∃ u⇩1 u⇩2 v⇩1 v⇩2. u = u⇩1 @- u⇩2 ∧ v = v⇩1 @- v⇩2 ∧ list_all2 P u⇩1 v⇩1 ∧ R u⇩2 v⇩2"
using assms(1) by force
then show ?thesis using assms(2) by (coinduct) (force elim: list.rel_cases)
qed
lemma stream_pred_coinduct[case_names stream_pred, coinduct pred: pred_stream]:
assumes "R w"
assumes "⋀ a w. R (a ## w) ⟹ P a ∧ R w"
shows "pred_stream P w"
using assms unfolding stream.pred_rel eq_onp_def by (coinduction arbitrary: w) (auto)
lemma stream_pred_coinduct_shift[case_names stream_pred, consumes 1]:
assumes "R w"
assumes "⋀ w. R w ⟹ ∃ u v. w = u @- v ∧ u ≠ [] ∧ list_all P u ∧ R v"
shows "pred_stream P w"
proof -
have "∃ u v. w = u @- v ∧ list_all P u ∧ R v"
using assms(1) by (metis list_all_simps(2) shift.simps(1))
then show ?thesis using assms(2) by (coinduct) (force elim: list_pred_cases)
qed
lemma stream_pred_flat_coinduct[case_names stream_pred, consumes 1]:
assumes "R ws"
assumes "⋀ w ws. R (w ## ws) ⟹ w ≠ [] ∧ list_all P w ∧ R ws"
shows "pred_stream P (flat ws)"
using assms
by (coinduction arbitrary: ws rule: stream_pred_coinduct_shift) (metis stream.exhaust flat_Stream)
lemmas stream_eq_coinduct[case_names stream_eq, coinduct pred: HOL.eq] =
stream_rel_coinduct[where ?P = HOL.eq, unfolded stream.rel_eq]
lemmas stream_eq_coinduct_shift[case_names stream_eq, consumes 1] =
stream_rel_coinduct_shift[where ?P = HOL.eq, unfolded stream.rel_eq list.rel_eq]
lemma stream_pred_shift[iff]: "pred_stream P (u @- v) ⟷ list_all P u ∧ pred_stream P v"
by (induct u) (auto)
lemma stream_rel_shift[iff]:
assumes "length u⇩1 = length v⇩1"
shows "stream_all2 P (u⇩1 @- u⇩2) (v⇩1 @- v⇩2) ⟷ list_all2 P u⇩1 v⇩1 ∧ stream_all2 P u⇩2 v⇩2"
using assms by (induct rule: list_induct2) (auto)
lemma sset_subset_stream_pred: "sset w ⊆ A ⟷ pred_stream (λ a. a ∈ A) w"
unfolding stream.pred_set by auto
lemma eq_scons: "w = a ## v ⟷ a = shd w ∧ v = stl w" by auto
lemma scons_eq: "a ## v = w ⟷ shd w = a ∧ stl w = v" by auto
lemma eq_shift: "w = u @- v ⟷ stake (length u) w = u ∧ sdrop (length u) w = v"
by (induct u arbitrary: w) (force+)
lemma shift_eq: "u @- v = w ⟷ u = stake (length u) w ∧ v = sdrop (length u) w"
by (induct u arbitrary: w) (force+)
lemma scons_eq_shift: "a ## w = u @- v ⟷ ([] = u ∧ a ## w = v) ∨ (∃ u'. a # u' = u ∧ w = u' @- v)"
by (cases u) (auto)
lemma shift_eq_scons: "u @- v = a ## w ⟷ (u = [] ∧ v = a ## w) ∨ (∃ u'. u = a # u' ∧ u' @- v = w)"
by (cases u) (auto)
lemma stream_all2_sset1:
assumes "stream_all2 P xs ys"
shows "∀ x ∈ sset xs. ∃ y ∈ sset ys. P x y"
proof -
have "pred_stream (λ x. ∃ y ∈ S. P x y) xs" if "sset ys ⊆ S" for S
using assms that by (coinduction arbitrary: xs ys) (force elim: stream.rel_cases)
then show ?thesis unfolding stream.pred_set by auto
qed
lemma stream_all2_sset2:
assumes "stream_all2 P xs ys"
shows "∀ y ∈ sset ys. ∃ x ∈ sset xs. P x y"
proof -
have "pred_stream (λ y. ∃ x ∈ S. P x y) ys" if "sset xs ⊆ S" for S
using assms that by (coinduction arbitrary: xs ys) (force elim: stream.rel_cases)
then show ?thesis unfolding stream.pred_set by auto
qed
lemma smap_eq_scons[iff]: "smap f xs = y ## ys ⟷ f (shd xs) = y ∧ smap f (stl xs) = ys"
using smap_ctr by metis
lemma scons_eq_smap[iff]: "y ## ys = smap f xs ⟷ y = f (shd xs) ∧ ys = smap f (stl xs)"
using smap_ctr by metis
lemma smap_eq_shift[iff]:
"smap f w = u @- v ⟷ (∃ w⇩1 w⇩2. w = w⇩1 @- w⇩2 ∧ map f w⇩1 = u ∧ smap f w⇩2 = v)"
using sdrop_smap eq_shift stake_sdrop stake_smap by metis
lemma shift_eq_smap[iff]:
"u @- v = smap f w ⟷ (∃ w⇩1 w⇩2. w = w⇩1 @- w⇩2 ∧ u = map f w⇩1 ∧ v = smap f w⇩2)"
using sdrop_smap eq_shift stake_sdrop stake_smap by metis
lemma szip_eq_scons[iff]: "szip xs ys = z ## zs ⟷ (shd xs, shd ys) = z ∧ szip (stl xs) (stl ys) = zs"
using szip.ctr stream.inject by metis
lemma scons_eq_szip[iff]: "z ## zs = szip xs ys ⟷ z = (shd xs, shd ys) ∧ zs = szip (stl xs) (stl ys)"
using szip.ctr stream.inject by metis
lemma siterate_eq_scons[iff]: "siterate f s = a ## w ⟷ s = a ∧ siterate f (f s) = w"
using siterate.ctr stream.inject by metis
lemma scons_eq_siterate[iff]: "a ## w = siterate f s ⟷ a = s ∧ w = siterate f (f s)"
using siterate.ctr stream.inject by metis
lemma snth_0: "(a ## w) !! 0 = a" by simp
lemma eqI_snth:
assumes "⋀ i. u !! i = v !! i"
shows "u = v"
using assms by (coinduction arbitrary: u v) (metis stream.sel snth.simps)
lemma stream_pred_snth: "pred_stream P w ⟷ (∀ i. P (w !! i))"
unfolding stream.pred_set sset_range by simp
lemma stream_rel_snth: "stream_all2 P u v ⟷ (∀ i. P (u !! i) (v !! i))"
proof safe
show "P (u !! i) (v !! i)" if "stream_all2 P u v" for i
using that by (induct i arbitrary: u v) (auto elim: stream.rel_cases)
show "stream_all2 P u v" if "∀ i. P (u !! i) (v !! i)"
using that by (coinduct) (metis snth_0 snth_Stream)
qed
lemma stream_rel_pred_szip: "stream_all2 P u v ⟷ pred_stream (case_prod P) (szip u v)"
unfolding stream_pred_snth stream_rel_snth by simp
lemma sconst_eq[iff]: "sconst x = sconst y ⟷ x = y" by (auto) (metis siterate.simps(1))
lemma stream_pred__sconst[iff]: "pred_stream P (sconst x) ⟷ P x"
unfolding stream_pred_snth by simp
lemma stream_rel_sconst[iff]: "stream_all2 P (sconst x) (sconst y) ⟷ P x y"
unfolding stream_rel_snth by simp
lemma set_sset_stake[intro!, simp]: "set (stake n xs) ⊆ sset xs"
by (metis sset_shift stake_sdrop sup_ge1)
lemma sset_sdrop[intro!, simp]: "sset (sdrop n xs) ⊆ sset xs"
by (metis sset_shift stake_sdrop sup_ge2)
lemma set_stake_snth: "x ∈ set (stake n xs) ⟷ (∃ i < n. xs !! i = x)"
unfolding in_set_conv_nth by auto
lemma szip_transfer[transfer_rule]:
includes lifting_syntax
shows "(stream_all2 A ===> stream_all2 B ===> stream_all2 (rel_prod A B)) szip szip"
by (intro rel_funI, coinduction) (force elim: stream.rel_cases)
lemma siterate_transfer[transfer_rule]:
includes lifting_syntax
shows "((A ===> A) ===> A ===> stream_all2 A) siterate siterate"
by (intro rel_funI, coinduction) (force dest: rel_funD)
lemma split_stream_first:
assumes "A ∩ sset xs ≠ {}"
obtains ys a zs
where "xs = ys @- a ## zs" "A ∩ set ys = {}" "a ∈ A"
proof
let ?n = "LEAST n. xs !! n ∈ A"
have 1: "xs !! n ∉ A" if "n < ?n" for n using that by (metis (full_types) not_less_Least)
show "xs = stake ?n xs @- (xs !! ?n) ## sdrop (Suc ?n) xs" using id_stake_snth_sdrop by blast
show "A ∩ set (stake ?n xs) = {}" using 1 by (metis (no_types, lifting) disjoint_iff_not_equal set_stake_snth)
show "xs !! ?n ∈ A" using assms unfolding sset_range by (auto intro: LeastI)
qed
lemma split_stream_first':
assumes "x ∈ sset xs"
obtains ys zs
where "xs = ys @- x ## zs" "x ∉ set ys"
proof
let ?n = "LEAST n. xs !! n = x"
have 1: "xs !! ?n = x" using assms unfolding sset_range by (auto intro: LeastI)
have 2: "xs !! n ≠ x" if "n < ?n" for n using that by (metis (full_types) not_less_Least)
show "xs = stake ?n xs @- x ## sdrop (Suc ?n) xs" using 1 by (metis id_stake_snth_sdrop)
show "x ∉ set (stake ?n xs)" using 2 by (meson set_stake_snth)
qed
lemma streams_UNIV[iff]: "streams A = UNIV ⟷ A = UNIV"
proof
show "A = UNIV ⟹ streams A = UNIV" by simp
next
assume "streams A = UNIV"
then have "w ∈ streams A" for w by simp
then have "sset w ⊆ A" for w unfolding streams_iff_sset by this
then have "sset (sconst a) ⊆ A" for a by blast
then have "a ∈ A" for a by simp
then show "A = UNIV" by auto
qed
lemma streams_int[simp]: "streams (A ∩ B) = streams A ∩ streams B" by (auto iff: streams_iff_sset)
lemma streams_Int[simp]: "streams (⋂ S) = ⋂ (streams ` S)" by (auto iff: streams_iff_sset)
lemma pred_list_listsp[pred_set_conv]: "list_all = listsp"
unfolding list.pred_set by auto
lemma pred_stream_streamsp[pred_set_conv]: "pred_stream = streamsp"
unfolding stream.pred_set streams_iff_sset[to_pred] by auto
subsection ‹The scan Function›
primrec (transfer) scan :: "('a ⇒ 'b ⇒ 'b) ⇒ 'a list ⇒ 'b ⇒ 'b list" where
"scan f [] a = []" | "scan f (x # xs) a = f x a # scan f xs (f x a)"
lemma scan_append[simp]: "scan f (xs @ ys) a = scan f xs a @ scan f ys (fold f xs a)"
by (induct xs arbitrary: a) (auto)
lemma scan_eq_nil[iff]: "scan f xs a = [] ⟷ xs = []" by (cases xs) (auto)
lemma scan_eq_cons[iff]:
"scan f xs a = b # w ⟷ (∃ y ys. xs = y # ys ∧ f y a = b ∧ scan f ys (f y a) = w)"
by (cases xs) (auto)
lemma scan_eq_append[iff]:
"scan f xs a = u @ v ⟷ (∃ ys zs. xs = ys @ zs ∧ scan f ys a = u ∧ scan f zs (fold f ys a) = v)"
by (induct u arbitrary: xs a) (auto, metis append_Cons fold_simps(2), blast)
lemma scan_length[simp]: "length (scan f xs a) = length xs"
by (induct xs arbitrary: a) (auto)
lemma scan_last: "last (a # scan f xs a) = fold f xs a"
by (induct xs arbitrary: a) (auto simp: last.simps)
lemma scan_butlast[simp]: "scan f (butlast xs) a = butlast (scan f xs a)"
by (induct xs arbitrary: a) (auto simp: butlast.simps)
lemma scan_const[simp]: "scan const xs a = xs"
by (induct xs arbitrary: a) (auto)
lemma scan_nth[simp]:
assumes "i < length (scan f xs a)"
shows "scan f xs a ! i = fold f (take (Suc i) xs) a"
using assms by (cases xs, simp, induct i arbitrary: xs a, auto simp: take_Suc neq_Nil_conv)
lemma scan_map[simp]: "scan f (map g xs) a = scan (f ∘ g) xs a"
by (induct xs arbitrary: a) (auto)
lemma scan_take[simp]: "take k (scan f xs a) = scan f (take k xs) a"
by (induct k arbitrary: xs a) (auto simp: take_Suc neq_Nil_conv)
lemma scan_drop[simp]: "drop k (scan f xs a) = scan f (drop k xs) (fold f (take k xs) a)"
by (induct k arbitrary: xs a) (auto simp: take_Suc neq_Nil_conv)
primcorec (transfer) sscan :: "('a ⇒ 'b ⇒ 'b) ⇒ 'a stream ⇒ 'b ⇒ 'b stream" where
"sscan f xs a = f (shd xs) a ## sscan f (stl xs) (f (shd xs) a)"
lemma sscan_scons[simp]: "sscan f (x ## xs) a = f x a ## sscan f xs (f x a)"
by (simp add: stream.expand)
lemma sscan_shift[simp]: "sscan f (xs @- ys) a = scan f xs a @- sscan f ys (fold f xs a)"
by (induct xs arbitrary: a) (auto)
lemma sscan_eq_scons[iff]:
"sscan f xs a = b ## w ⟷ f (shd xs) a = b ∧ sscan f (stl xs) (f (shd xs) a) = w"
using sscan.ctr stream.inject by metis
lemma scons_eq_sscan[iff]:
"b ## w = sscan f xs a ⟷ b = f (shd xs) a ∧ w = sscan f (stl xs) (f (shd xs) a)"
using sscan.ctr stream.inject by metis
lemma sscan_const[simp]: "sscan const xs a = xs"
by (coinduction arbitrary: xs a) (auto)
lemma sscan_snth[simp]: "sscan f xs a !! i = fold f (stake (Suc i) xs) a"
by (induct i arbitrary: xs a) (auto)
lemma sscan_scons_snth[simp]: "(a ## sscan f xs a) !! i = fold f (stake i xs) a"
by (induct i arbitrary: xs a) (auto)
lemma sscan_smap[simp]: "sscan f (smap g xs) a = sscan (f ∘ g) xs a"
by (coinduction arbitrary: xs a) (auto)
lemma sscan_stake[simp]: "stake k (sscan f xs a) = scan f (stake k xs) a"
by (induct k arbitrary: a xs) (auto)
lemma sscan_sdrop[simp]: "sdrop k (sscan f xs a) = sscan f (sdrop k xs) (fold f (stake k xs) a)"
by (induct k arbitrary: a xs) (auto)
subsection ‹Transposing Streams›
primcorec (transfer) stranspose :: "'a stream list ⇒ 'a list stream" where
"stranspose ws = map shd ws ## stranspose (map stl ws)"
lemma stranspose_eq_scons[iff]: "stranspose ws = a ## w ⟷ map shd ws = a ∧ stranspose (map stl ws) = w"
using stranspose.ctr stream.inject by metis
lemma scons_eq_stranspose[iff]: "a ## w = stranspose ws ⟷ a = map shd ws ∧ w = stranspose (map stl ws)"
using stranspose.ctr stream.inject by metis
lemma stranspose_nil[simp]: "stranspose [] = sconst []" by coinduction auto
lemma stranspose_cons[simp]: "stranspose (w # ws) = smap2 Cons w (stranspose ws)"
by (coinduction arbitrary: w ws) (metis list.simps(9) smap2.simps stranspose.simps stream.sel)
lemma snth_stranspose[simp]: "stranspose ws !! k = map (λ w. w !! k) ws" by (induct k arbitrary: ws) (auto)
lemma stranspose_nth[simp]:
assumes "k < length ws"
shows "smap (λ xs. xs ! k) (stranspose ws) = ws ! k"
using assms by (auto intro: eqI_snth)
subsection ‹Distinct Streams›
coinductive sdistinct :: "'a stream ⇒ bool" where
scons[intro!]: "x ∉ sset xs ⟹ sdistinct xs ⟹ sdistinct (x ## xs)"
lemma sdistinct_scons_elim[elim!]:
assumes "sdistinct (x ## xs)"
obtains "x ∉ sset xs" "sdistinct xs"
using assms by (auto elim: sdistinct.cases)
lemma sdistinct_coinduct[case_names sdistinct, coinduct pred: sdistinct]:
assumes "P xs"
assumes "⋀ x xs. P (x ## xs) ⟹ x ∉ sset xs ∧ P xs"
shows "sdistinct xs"
using stream.collapse sdistinct.coinduct assms by metis
lemma sdistinct_shift[intro!]:
assumes "distinct xs" "sdistinct ys" "set xs ∩ sset ys = {}"
shows "sdistinct (xs @- ys)"
using assms by (induct xs) (auto)
lemma sdistinct_shift_elim[elim!]:
assumes "sdistinct (xs @- ys)"
obtains "distinct xs" "sdistinct ys" "set xs ∩ sset ys = {}"
using assms by (induct xs) (auto)
lemma sdistinct_infinite_sset:
assumes "sdistinct w"
shows "infinite (sset w)"
using assms by (coinduction arbitrary: w) (force elim: sdistinct.cases)
lemma not_sdistinct_decomp:
assumes "¬ sdistinct w"
obtains u v a w'
where "w = u @- a ## v @- a ## w'"
proof (rule ccontr)
assume 1: "¬ thesis"
assume 2: "w = u @- a ## v @- a ## w' ⟹ thesis" for u a v w'
have 3: "∀ u v a w'. w ≠ u @- a ## v @- a ## w'" using 1 2 by auto
have 4: "sdistinct w" using 3 by (coinduct) (metis id_stake_snth_sdrop imageE shift.simps sset_range)
show False using assms 4 by auto
qed
subsection ‹Sorted Streams›
coinductive (in order) sascending :: "'a stream ⇒ bool" where
"a ≤ b ⟹ sascending (b ## w) ⟹ sascending (a ## b ## w)"
coinductive (in order) sdescending :: "'a stream ⇒ bool" where
"a ≥ b ⟹ sdescending (b ## w) ⟹ sdescending (a ## b ## w)"
lemma sdescending_coinduct[case_names sdescending, coinduct pred: sdescending]:
assumes "P w"
assumes "⋀ a b w. P (a ## b ## w) ⟹ a ≥ b ∧ P (b ## w)"
shows "sdescending w"
using stream.collapse sdescending.coinduct assms by (metis (no_types))
lemma sdescending_scons:
assumes "sdescending (a ## w)"
shows "sdescending w"
using assms by (auto elim: sdescending.cases)
lemma sdescending_sappend:
assumes "sdescending (u @- v)"
obtains "sdescending v"
using assms by (induct u) (auto elim: sdescending.cases)
lemma sdescending_sdrop:
assumes "sdescending w"
shows "sdescending (sdrop k w)"
using assms by (metis sdescending_sappend stake_sdrop)
lemma sdescending_sset_scons:
assumes "sdescending (a ## w)"
assumes "b ∈ sset w"
shows "a ≥ b"
proof -
have "pred_stream (λ b. a ≥ b) w" if "sdescending w" "a ≥ shd w" for w
using that by (coinduction arbitrary: w) (auto elim: sdescending.cases)
then show ?thesis using assms unfolding stream.pred_set by force
qed
lemma sdescending_sset_sappend:
assumes "sdescending (u @- v)"
assumes "a ∈ set u" "b ∈ sset v"
shows "a ≥ b"
using assms by (induct u) (auto elim: sdescending.cases dest: sdescending_sset_scons)
lemma sdescending_snth_antimono:
assumes "sdescending w"
shows "antimono (snth w)"
unfolding antimono_iff_le_Suc
proof
fix k
have "sdescending (sdrop k w)" using sdescending_sdrop assms by this
then obtain a b v where 2: "sdrop k w = a ## b ## v" "a ≥ b" by rule
then show "w !! k ≥ w !! Suc k" by (metis sdrop_simps stream.sel)
qed
lemma sdescending_stuck:
fixes w :: "'a :: wellorder stream"
assumes "sdescending w"
obtains u a
where "w = u @- sconst a"
using assms
proof (induct "shd w" arbitrary: w thesis rule: less_induct)
case less
show ?case
proof (cases "w = sconst (shd w)")
case True
show ?thesis using shift_replicate_sconst less(2) True by metis
next
case False
then obtain u v where 1: "w = u @- v" "u ≠ []" "shd w ≠ shd v"
by (metis empty_iff eqI_snth insert_iff sdrop_simps(1) shift.simps(1) snth_sset sset_sconst stake_sdrop)
have 2: "shd w ≥ shd v" using sdescending_sset_sappend less(3) 1 by (metis hd_in_set shd_sset shift_simps(1))
have 3: "shd w > shd v" using 1(3) 2 by simp
obtain s a where 4: "v = s @- sconst a" using sdescending_sappend less(1, 3) 1(1) 3 by metis
have 5: "w = (u @ s) @- sconst a" unfolding 1(1) 4 by simp
show ?thesis using less(2) 5 by this
qed
qed
end