# Theory Sequence

(* Author: Julian Brunner *)
(* This is originally a part of the CAVA model checker *)
theory Sequence
imports
Basic

begin

(* list basics *)

declare upt_Suc[simp del]
declare last.simps[simp del]
declare butlast.simps[simp del]
declare Cons_nth_drop_Suc[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 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))"

(* stream basics *)

declare stream.map_id[simp]
declare stream.set_map[simp]
declare stream.set_sel(1)[intro!, 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
u1 u2 v1 v2. u = u1 @- u2  v = v1 @- v2  u1  []  v1  []  list_all2 P u1 v1  R u2 v2"
shows "stream_all2 P u v"
proof -
have " u1 u2 v1 v2. u = u1 @- u2  v = v1 @- v2  list_all2 P u1 v1  R u2 v2"
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 sset_subset_stream_pred: "sset w  A  pred_stream (λ a. a  A) w"
unfolding stream.pred_set by auto
lemma stream_pred_snth: "pred_stream P w  ( i. P (w !! i))"
unfolding stream.pred_set sset_range by simp

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 u1 = length v1"
shows "stream_all2 P (u1 @- u2) (v1 @- v2)  list_all2 P u1 v1  stream_all2 P u2 v2"
using assms by (induct rule: list_induct2) (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  ( w1 w2. w = w1 @- w2  map f w1 = u  smap f w2 = v)"
using sdrop_smap eq_shift stake_sdrop stake_smap by metis
lemma shift_eq_smap[iff]:
"u @- v = smap f w  ( w1 w2. w = w1 @- w2  u = map f w1  v = smap f w2)"
using sdrop_smap eq_shift stake_sdrop stake_smap 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 eqI_snth:
assumes " i. u !! i = v !! i"
shows "u = v"
using assms by (coinduction arbitrary: u v) (metis stream.sel snth.simps)

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 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

(* scans *)

fun 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_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 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)"
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)

(* sdistinct *)

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

(* 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_sdrop:
assumes "sdescending w"
shows "sdescending (sdrop k w)"
using assms by (induct k) (auto, metis sdescending.cases sdrop_stl stream.sel(2))

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 k
where "sdrop k w = sconst (w !! k)"
using assms
proof (induct "w !! 0" arbitrary: w thesis rule: less_induct)
case less
show ?case
proof (cases "w = sconst (w !! 0)")
case True
show ?thesis using less(2)[of 0] True by simp
next
case False
obtain k where 1: "w !! k  w !! 0"
using False by (metis empty_iff eqI_snth insert_iff snth_sset sset_sconst)
have 2: "antimono (snth w)" using sdescending_snth_antimono less(3) by this
have 3: "w !! k  w !! 0" using 1 2 by (blast dest: antimonoD)
have 4: "sdrop k w !! 0 < w !! 0" using 1 3 by auto
have 5: "sdescending (sdrop k w)" using sdescending_sdrop less(3) by this
obtain l where 5: "sdrop l (sdrop k w) = sconst (sdrop k w !! l)"
using less(1)[OF 4 _ 5] by this
show ?thesis using less(2) 5 by simp
qed
qed

end