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

  (* TODO: these should be generated by the transfer option on the primcorec definitions *)
  (* TODO: transfer_prover cannot handle corecursive definitions due to the λ(s1, s2). undefined
    abortion term that is never used *)
  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)
  (* TODO: figure out how this is used, should it be a simp rule? or flipped? also target_alt_def *)
  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