Theory Partial_Order_Reduction.Coinductive_List_Extensions

section ‹Coinductive Lists›

theory Coinductive_List_Extensions
imports
  Coinductive.Coinductive_List
  Coinductive.Coinductive_List_Prefix
  Coinductive.Coinductive_Stream
  "../Extensions/List_Extensions"
  "../Extensions/ESet_Extensions"
begin

  hide_const (open) Sublist.prefix
  hide_const (open) Sublist.suffix

  declare list_of_lappend[simp]
  declare lnth_lappend1[simp]
  declare lnth_lappend2[simp]
  declare lprefix_llength_le[dest]
  declare Sup_llist_def[simp]
  declare length_list_of[simp]
  declare llast_linfinite[simp]
  declare lnth_ltake[simp]
  declare lappend_assoc[simp]
  declare lprefix_lappend[simp]

  lemma lprefix_lSup_revert: "lSup = Sup" "lprefix = less_eq" by auto
  lemma admissible_lprefixI[cont_intro]:
    assumes "mcont lub ord lSup lprefix f"
    assumes "mcont lub ord lSup lprefix g"
    shows "ccpo.admissible lub ord (λ x. lprefix (f x) (g x))"
    using ccpo_class.admissible_leI assms unfolding lprefix_lSup_revert by this
  lemma llist_lift_admissible:
    assumes "ccpo.admissible lSup lprefix P"
    assumes " u. u  v  lfinite u  P u"
    shows "P v"
    using assms by (metis LNil_lprefix le_llist_conv_lprefix lfinite.simps llist_gen_induct)

  abbreviation "linfinite w  ¬ lfinite w"

  notation LNil ("<>")
  notation LCons (infixr "%" 65)
  notation lzip (infixr "¦¦" 51)
  notation lappend (infixr "$" 65)
  notation lnth (infixl "?!" 100)

  syntax "_llist" :: "args  'a llist" ("<_>")
  translations
    "<a, x>"  "a % <x>"
    "<a>"  "a % <>"

  lemma eq_LNil_conv_lnull[simp]: "w = <>  lnull w" by auto
  lemma Collect_lnull[simp]: "{w. lnull w} = {<>}" by auto

  lemma inj_on_ltake: "inj_on (λ k. ltake k w) {.. llength w}"
    by (rule inj_onI, auto, metis llength_ltake min_def)

  lemma lnth_inf_llist'[simp]: "lnth (inf_llist f) = f" by auto

  lemma not_lnull_lappend_startE[elim]:
    assumes "¬ lnull w"
    obtains a v
    where "w = <a> $ v"
    using not_lnull_conv assms by (simp, metis)
  lemma not_lnull_lappend_endE[elim]:
    assumes "¬ lnull w"
    obtains a v
    where "w = v $ <a>"
  proof (cases "lfinite w")
    case False
    show ?thesis
    proof
      show "w = w $ <a>" using lappend_inf False by force
    qed
  next
    case True
    show ?thesis
    using True assms that
    proof (induct arbitrary: thesis)
      case (lfinite_LNil)
      show ?case using lfinite_LNil by auto
    next
      case (lfinite_LConsI w a)
      show ?case
      proof (cases "lnull w")
        case False
        obtain b v where 1: "w = v $ <b>" using lfinite_LConsI(2) False by this
        show ?thesis
        proof (rule lfinite_LConsI(4))
          show "a % w = (a % v) $ <b>" unfolding 1 by simp
        qed
      next
        case True
        show ?thesis
        proof (rule lfinite_LConsI(4))
          show "a % w = <> $ <a>" using True by simp
        qed
      qed
    qed
  qed

  lemma llength_lappend_startE[elim]:
    assumes "llength w  eSuc n"
    obtains a v
    where "w = <a> $ v" "llength v  n"
  proof -
    have 1: "¬ lnull w" using assms by auto
    show ?thesis using assms 1 that by auto
  qed
  lemma llength_lappend_endE[elim]:
    assumes "llength w  eSuc n"
    obtains a v
    where "w = v $ <a>" "llength v  n"
  proof -
    have 1: "¬ lnull w" using assms by auto
    show ?thesis using assms 1 that by auto
  qed

  lemma llength_lappend_start'E[elim]:
    assumes "llength w = enat (Suc n)"
    obtains a v
    where "w = <a> $ v" "llength v = enat n"
  proof -
    have 1: "llength w  eSuc (enat n)" using assms by simp
    obtain a v where 2: "w = <a> $ v" using 1 by blast
    show ?thesis
    proof
      show "w = <a> $ v" using 2(1) by this
      show "llength v = enat n" using assms unfolding 2(1) by (simp, metis eSuc_enat eSuc_inject)
    qed
  qed
  lemma llength_lappend_end'E[elim]:
    assumes "llength w = enat (Suc n)"
    obtains a v
    where "w = v $ <a>" "llength v = enat n"
  proof -
    have 1: "llength w  eSuc (enat n)" using assms by simp
    obtain a v where 2: "w = v $ <a>" using 1 by blast
    show ?thesis
    proof
      show "w = v $ <a>" using 2(1) by this
      show "llength v = enat n" using assms unfolding 2(1) by (simp, metis eSuc_enat eSuc_inject)
    qed
  qed

  lemma ltake_llast[simp]:
    assumes "enat k < llength w"
    shows "llast (ltake (enat (Suc k)) w) = w ?! k"
  proof -
    have 1: "llength (ltake (enat (Suc k)) w) = eSuc (enat k)"using min.absorb_iff1 assms by auto
    have "llast (ltake (enat (Suc k)) w) = ltake (enat (Suc k)) w ?! k"
      using llast_conv_lnth 1 by this
    also have " = w ?! k" by (rule lnth_ltake, simp)
    finally show ?thesis by this
  qed

  lemma linfinite_llength[dest, simp]:
    assumes "linfinite w"
    shows "enat k < llength w"
    using assms not_lfinite_llength by force

  lemma llist_nth_eqI[intro]:
    assumes "llength u = llength v"
    assumes " i. enat i < llength u  enat i < llength v  u ?! i = v ?! i"
    shows "u = v"
  using assms
  proof (coinduction arbitrary: u v)
    case Eq_llist
    have 10: "llength u = llength v" using Eq_llist by auto
    have 11: " i. enat i < llength u   enat i < llength v  u ?! i = v ?! i"
      using Eq_llist by auto
    show ?case
    proof (intro conjI impI exI allI)
      show "lnull u  lnull v" using 10 by auto
    next
      assume 20: "¬ lnull u" "¬ lnull v"
      show "lhd u = lhd v" using lhd_conv_lnth enat_0 11 20 by force
    next
      show "ltl u = ltl u" by rule
    next
      show "ltl v = ltl v" by rule
    next
      assume 30: "¬ lnull u" "¬ lnull v"
      show "llength (ltl u) = llength (ltl v)" using 10 30 by force
    next
      fix i
      assume 40: "¬ lnull u" "¬ lnull v" "enat i < llength (ltl u)" "enat i < llength (ltl v)"
      have 41: "u ?! Suc i = v ?! Suc i"
      proof (rule 11)
        show "enat (Suc i) < llength u" using Suc_ile_eq 40(1) 40(3) by auto
        show "enat (Suc i) < llength v" using Suc_ile_eq 40(2) 40(4) by auto
      qed
      show "ltl u ?! i = ltl v ?! i" using lnth_ltl 40(1-2) 41 by metis
    qed
  qed

  primcorec lscan :: "('a  'b  'b)  'a llist  'b  'b llist"
    where "lscan f w a = (case w of <>  <a> | x % xs  a % lscan f xs (f x a))"

  lemma lscan_simps[simp]:
    "lscan f <> a = <a>"
    "lscan f (x % xs) a = a % lscan f xs (f x a)"
    by (metis llist.simps(4) lscan.code, metis llist.simps(5) lscan.code)

  lemma lscan_lfinite[iff]: "lfinite (lscan f w a)  lfinite w"
  proof
    assume "lfinite (lscan f w a)"
    thus "lfinite w"
    proof (induct "lscan f w a" arbitrary: w a rule: lfinite_induct)
      case LNil
      show ?case using LNil by simp
    next
      case LCons
      show ?case by (cases w, simp, simp add: LCons(3))
    qed
  next
    assume "lfinite w"
    thus "lfinite (lscan f w a)" by (induct arbitrary: a, auto)
  qed
  lemma lscan_llength[simp]: "llength (lscan f w a) = eSuc (llength w)"
  proof (cases "lfinite w")
    case False
    have 1: "llength (lscan f w a) = " using not_lfinite_llength False by auto
    have 2: "llength w = " using not_lfinite_llength False by auto
    show ?thesis using 1 2 by simp
  next
    case True
    show ?thesis using True by (induct arbitrary: a, auto)
  qed

  function lfold :: "('a  'b  'b)  'a llist  'b  'b"
    where "lfinite w  lfold f w = fold f (list_of w)" | "linfinite w  lfold f w = id"
    by (auto, metis) termination by lexicographic_order

  lemma lfold_llist_of[simp]: "lfold f (llist_of xs) = fold f xs" by simp

  lemma finite_UNIV_llength_eq:
    assumes "finite (UNIV :: 'a set)"
    shows "finite {w :: 'a llist. llength w = enat n}"
  proof (induct n)
    case (0)
    show ?case by simp
  next
    case (Suc n)
    have 1: "finite ({v. llength v = enat n} × UNIV :: ('a llist × 'a) set)"
      using Suc assms by simp
    have 2: "finite ((λ (v, a). v $ <a> :: 'a llist ) ` ({v. llength v = enat n} × UNIV))"
      using 1 by auto
    have 3: "finite {v $ <a> :: 'a llist |v a. llength v = enat n}"
    proof -
      have 0: "{v $ <a> :: 'a llist  |v a. llength v = enat n} =
        (λ (v, a). v $ <a> :: 'a llist ) ` ({v. llength v = enat n} × UNIV)" by auto
      show ?thesis using 2 unfolding 0 by this
    qed
    have 4: "finite {w :: 'a llist . llength w = enat (Suc n)}"
    proof -
      have 0: "{w :: 'a llist . llength w = enat (Suc n)} =
        {v $ <a> :: 'a llist  |v a. llength v = enat n}" by force
      show ?thesis using 3 unfolding 0 by this
    qed
    show ?case using 4 by this
  qed
  lemma finite_UNIV_llength_le:
    assumes "finite (UNIV :: 'a set)"
    shows "finite {w :: 'a llist. llength w  enat n}"
  proof -
    have 1: "{w. llength w  enat n} = ( k  n. {w. llength w = enat k})"
      by (auto, metis atMost_iff enat_ile enat_ord_simps(1))
    show ?thesis unfolding 1 using finite_UNIV_llength_eq assms by auto
  qed

  lemma lprefix_ltake[dest]: "u  v  u = ltake (llength u) v"
    by (metis le_llist_conv_lprefix lprefix_conv_lappend ltake_all ltake_lappend1 order_refl)
  lemma prefixes_set: "{v. v  w} = {ltake k w |k. k  llength w}" by fastforce
  lemma esize_prefixes[simp]: "esize {v. v  w} = eSuc (llength w)"
  proof -
    have "esize {v. v  w} = esize {ltake k w |k. k  llength w}" unfolding prefixes_set by rule
    also have " = esize ((λ k. ltake k w) ` {.. llength w})"
      unfolding atMost_def image_Collect by rule
    also have " = esize {.. llength w}" using inj_on_ltake esize_image by blast
    also have " = eSuc (llength w)" by simp
    finally show ?thesis by this
  qed
  lemma prefix_subsume: "v  w  u  w  llength v  llength u  v  u"
    by (metis le_llist_conv_lprefix lprefix_conv_lappend
      lprefix_ltake ltake_is_lprefix ltake_lappend1)

  lemma ltake_infinite[simp]: "ltake  w = w" by (metis enat_ord_code(3) ltake_all)

  lemma lprefix_infinite:
    assumes "u  v" "linfinite u"
    shows "u = v"
  proof -
    have 1: "llength u = " using not_lfinite_llength assms(2) by this
    have "u = ltake (llength u) v" using lprefix_ltake assms(1) by this
    also have " = v" using 1 by simp
    finally show ?thesis by this
  qed

  instantiation llist :: (type) esize_order
  begin

    definition [simp]: "esize  llength"

    instance
    proof
      fix w :: "'a llist"
      assume 1: "esize w  "
      show "finite {v. v  w}"
        using esize_prefixes 1 by (metis eSuc_eq_infinity_iff esize_set.simps(2) esize_llist_def)
    next
      fix u v :: "'a llist"
      assume 1: "u  v"
      show "esize u  esize v" using lprefix_llength_le 1 by auto
    next
      fix u v :: "'a llist"
      assume 1: "u < v"
      show "esize u < esize v" using lstrict_prefix_llength_less 1 by auto
    qed

  end

  subsection ‹Index Sets›
  
    definition liset :: "'a set  'a llist  nat set"
      where "liset A w  {i. enat i < llength w  w ?! i  A}"

    lemma lisetI[intro]:
      assumes "enat i < llength w" "w ?! i  A"
      shows "i  liset A w"
      using assms unfolding liset_def by auto
    lemma lisetD[dest]:
      assumes "i  liset A w"
      shows "enat i < llength w" "w ?! i  A"
      using assms unfolding liset_def by auto

    lemma liset_finite:
      assumes "lfinite w"
      shows "finite (liset A w)"
    proof
      show "liset A w  {i. enat i < llength w}" by auto
      show "finite {i. enat i < llength w}" using lfinite_finite_index assms by this
    qed

    lemma liset_nil[simp]: "liset A <> = {}" by auto
    lemma liset_cons_not_member[simp]:
      assumes "a  A"
      shows "liset A (a % w) = Suc ` liset A w"
    proof -
      have "liset A (a % w) = {i. enat i < llength (a % w)  (a % w) ?! i  A}" by auto
      also have " = Suc ` {i. enat (Suc i) < llength (a % w)  (a % w) ?! Suc i  A}"
        using Collect_split_Suc(1) assms by simp
      also have " = Suc ` {i. enat i < llength w  w ?! i  A}" using Suc_ile_eq by simp
      also have " = Suc ` liset A w" by auto
      finally show ?thesis by this
    qed
    lemma liset_cons_member[simp]:
      assumes "a  A"
      shows "liset A (a % w) = {0}  Suc ` liset A w"
    proof -
      have "liset A (a % w) = {i. enat i < llength (a % w)  (a % w) ?! i  A}" by auto
      also have " = {0}  Suc ` {i. enat (Suc i) < llength (a % w)  (a % w) ?! Suc i  A}"
        using Collect_split_Suc(2) assms by simp
      also have " = {0}  Suc ` {i. enat i < llength w  w ?! i  A}" using Suc_ile_eq by simp
      also have " = {0}  Suc ` liset A w" by auto
      finally show ?thesis by this
    qed
  
    lemma liset_prefix:
      assumes "i  liset A v" "u  v" "enat i < llength u"
      shows "i  liset A u"
    unfolding liset_def
    proof (intro CollectI conjI)
      have 1: "v ?! i  A" using assms(1) by auto
      show "enat i < llength u" using assms(3) by this
      show "u ?! i  A" using lprefix_lnthD assms(2, 3) 1 by force
    qed
    lemma liset_suffix:
      assumes "i  liset A u" "u  v"
      shows "i  liset A v"
    unfolding liset_def
    proof (intro CollectI conjI)
      have 1: "enat i < llength u" "u ?! i  A" using assms(1) by auto
      show "enat i < llength v" using lprefix_llength_le 1(1) assms(2) by fastforce
      show "v ?! i  A" using lprefix_lnthD assms(2) 1 by force
    qed

    lemma liset_ltake[simp]: "liset A (ltake (enat k) w) = liset A w  {..< k}"
    proof (intro equalityI subsetI)
      fix i
      assume 1: "i  liset A (ltake (enat k) w)"
      have 2: "enat i < enat k" using 1 by auto
      have 3: "ltake (enat k) w ?! i = w ?! i" using lnth_ltake 2 by this
      show "i  liset A w  {..< k}" using 1 3 by fastforce
    next
      fix i
      assume 1: "i  liset A w  {..< k}"
      have 2: "enat i < enat k" using 1 by auto
      have 3: "ltake (enat k) w ?! i = w ?! i" using lnth_ltake 2 by this
      show "i  liset A (ltake (enat k) w)" using 1 3 by fastforce
    qed

    lemma liset_mono[dest]: "u  v  liset A u  liset A v"
      unfolding liset_def using lprefix_lnthD by fastforce
    lemma liset_cont[dest]:
      assumes "Complete_Partial_Order.chain less_eq C" "C  {}"
      shows "liset A ( C) = ( w  C. liset A w)"
    proof safe
      fix i
      assume 1: "i  liset A ( C)"
      show "i  ( w  C. liset A w)"
      proof (cases "finite C")
        case False
        obtain w where 2: "w  C" "enat i < llength w"
          using esize_llist_def infinite_chain_arbitrary_esize assms(1) False Suc_ile_eq by metis
        have 3: "w   C" using chain_lprefix_lSup assms(1) 2(1) by simp
        have 4: "i  liset A w" using liset_prefix 1 3 2(2) by this
        show ?thesis using 2(1) 4 by auto
      next
        case True
        have 2: " C  C" using in_chain_finite assms(1) True assms(2) by this
        show ?thesis using 1 2 by auto
      qed
    next
      fix w i
      assume 1: "w  C" "i  liset A w"
      have 2: "w   C" using chain_lprefix_lSup assms(1) 1(1) by simp
      show "i  liset A ( C)" using liset_suffix 1(2) 2 by this
    qed

    lemma liset_mcont: "Complete_Partial_Order2.mcont lSup lprefix Sup less_eq (liset A)"
      unfolding lprefix_lSup_revert by (blast intro: mcontI monotoneI contI)

    lemmas mcont2mcont_liset = liset_mcont[THEN lfp.mcont2mcont, simp, cont_intro]

  subsection ‹Selections›

    (* TODO: thm lfitler_K_False *)

    abbreviation "lproject A  lfilter (λ a. a  A)"
    abbreviation "lselect s w  lnths w s"

    lemma lselect_to_lproject: "lselect s w = lmap fst (lproject (UNIV × s) (w ¦¦ iterates Suc 0))"
    proof -
      have 1: "{(x, y). y  s} = UNIV × s" by auto
      have "lselect s w = lmap fst (lproject {(x, y). y  s} (w ¦¦ iterates Suc 0))"
        unfolding lnths_def by simp
      also have " = lmap fst (lproject (UNIV × s) (w ¦¦ iterates Suc 0))" unfolding 1 by rule
      finally show ?thesis by this
    qed
    lemma lproject_to_lselect: "lproject A w = lselect (liset A w) w"
      unfolding lfilter_conv_lnths liset_def by rule

    lemma lproject_llength[simp]: "llength (lproject A w) = esize (liset A w)"
      by (induct rule: llist_induct) (auto)
    lemma lproject_lfinite[simp]: "lfinite (lproject A w)  finite (liset A w)"
      using lproject_llength esize_iff_infinite llength_eq_infty_conv_lfinite by metis

    lemma lselect_restrict_indices[simp]: "lselect {i  s. enat i < llength w} w = lselect s w"
    proof (rule lnths_cong)
      show "w = w" by rule
    next
      fix n
      assume 1: "enat n < llength w"
      show "n  {i  s. enat i < llength w}  n  s" using 1 by blast
    qed

    lemma lselect_llength: "llength (lselect s w) = esize {i  s. enat i < llength w}"
    proof -
      have 1: " i. enat i < llength w  (w ¦¦ iterates Suc 0) ?! i = (w ?! i, i)"
        by (metis Suc_funpow enat.distinct(1) enat_ord_simps(4) llength_iterates lnth_iterates
          lnth_lzip monoid_add_class.add.right_neutral)
      have 2: "{i. enat i < llength w  (w ¦¦ iterates Suc 0) ?! i  UNIV × s} =
        {i  s. enat i < llength w}" using 1 by auto
      have "llength (lselect s w) = esize (liset (UNIV × s) (w ¦¦ iterates Suc 0))"
        unfolding lselect_to_lproject by simp
      also have " = esize {i. enat i < llength w  (w ¦¦ iterates Suc 0) ?! i  UNIV × s}"
        unfolding liset_def by simp
      also have " = esize {i  s. enat i < llength w}" unfolding 2 by rule
      finally show ?thesis by this
    qed
    lemma lselect_llength_le[simp]: "llength (lselect s w)  esize s"
    proof -
      have "llength (lselect s w) = esize {i  s. enat i < llength w}"
        unfolding lselect_llength by rule
      also have " = esize (s  {i. enat i < llength w})" unfolding Collect_conj_eq by simp
      also have "  esize s" by blast
      finally show ?thesis by this
    qed
    lemma least_lselect_llength:
      assumes "¬ lnull (lselect s w)"
      shows "enat (least s) < llength w"
    proof -
      have 0: "llength (lselect s w) > 0" using assms by auto
      have 1: " i. i  s  least s  i" using Least_le 0 by fast
      obtain i where 2: "i  s" "enat i < llength w" using 0 unfolding lselect_llength by auto
      have "enat (least s)  enat i" using 1 2(1) by auto
      also have " < llength w" using 2(2) by this
      finally show "enat (least s) < llength w" by this
    qed
    lemma lselect_lnull: "lnull (lselect s w)  ( i  s. enat i  llength w)"
      unfolding llength_eq_0[symmetric] lselect_llength by auto

    lemma lselect_discard_start:
      assumes " i. i  s  k  i"
      shows "lselect {i. k + i  s} (ldropn k w) = lselect s w"
    proof -
      have 1: "lselect s (ltake (enat k) w) = <>"
        using assms by (fastforce simp add: lselect_lnull min_le_iff_disj)
      have "lselect {m. k + m  s} (ldropn k w) =
        lselect s (ltake (enat k) w) $ lselect {m. k + m  s} (ldropn k w)" unfolding 1 by simp
      also have " = lselect s w" using lnths_split by rule
      finally show ?thesis by this
    qed
    lemma lselect_discard_end:
      assumes " i. i  s  i < k"
      shows "lselect s (ltake (enat k) w) = lselect s w"
    proof -
      have 1: "lselect {m. k + m  s} (ldropn k w) = <>"
        using assms by (fastforce simp add: lselect_lnull min_le_iff_disj)
      have "lselect s (ltake (enat k) w) =
        lselect s (ltake (enat k) w) $ lselect {m. k + m  s} (ldropn k w)" unfolding 1 by simp
      also have " = lselect s w" using lnths_split by rule
      finally show ?thesis by this
    qed

    lemma lselect_least:
      assumes "¬ lnull (lselect s w)"
      shows "lselect s w = w ?! least s % lselect (s - {least s}) w"
    proof -
      have 0: "s  {}" using assms by auto
      have 1: "least s  s" using LeastI 0 by fast
      have 2: " i. i  s  least s  i" using Least_le 0 by fast
      have 3: " i. i  s - {least s}  Suc (least s)  i" using least_unique 2 by force
      have 4: "insert (least s) (s - {least s}) = s" using 1 by auto
      have 5: "enat (least s) < llength w" using least_lselect_llength assms by this
      have 6: "lselect (s - {least s}) (ltake (enat (least s)) w) = <>"
        by (rule, auto simp: lselect_llength dest: least_not_less)
      have 7: "lselect {i. Suc (least s) + i  s - {least s}} (ldropn (Suc (least s)) w) =
        lselect (s - {least s}) w" using lselect_discard_start 3 by this
      have "lselect s w = lselect (insert (least s) (s - {least s})) w" unfolding 4 by simp
      also have " = lselect (s - {least s}) (ltake (enat (least s)) w) $ <w ?! least s> $
        lselect {m. Suc (least s) + m  s - {least s}} (ldropn (Suc (least s)) w)"
        unfolding lnths_insert[OF 5] by simp
      also have " = <w ?! least s> $
        lselect {m. Suc (least s) + m  s - {least s}} (ldropn (Suc (least s)) w)"
        unfolding 6 by simp
      also have " = w ?! (least s) % lselect (s - {least s}) w" unfolding 7 by simp
      finally show ?thesis by this
    qed

    lemma lselect_lnth[simp]:
      assumes "enat i < llength (lselect s w)"
      shows "lselect s w ?! i = w ?! nth_least s i"
    using assms
    proof (induct i arbitrary: s)
      case 0
      have 1: "¬ lnull (lselect s w)" using 0 by auto
      show ?case using lselect_least 1 by force
    next
      case (Suc i)
      have 1: "¬ lnull (lselect s w)" using Suc(2) by auto
      have 2: "lselect s w = w ?! least s % lselect (s - {least s}) w" using lselect_least 1 by this
      have 3: "llength (lselect s w) = eSuc (llength (lselect (s - {least s}) w))" using 2 by simp
      have 4: "enat i < llength (lselect (s - {least s}) w)" using 3 Suc(2) by simp
      have "lselect s w ?! Suc i = (w ?! least s % lselect (s - {least s}) w) ?! Suc i" using 2 by simp
      also have " = lselect (s - {least s}) w ?! i" by simp
      also have " = w ?! nth_least (s - {least s}) i" using Suc(1) 4 by simp
      also have " = w ?! nth_least s (Suc i)" by simp
      finally show ?case by this
    qed
    lemma lproject_lnth[simp]:
      assumes "enat i < llength (lproject A w)"
      shows "lproject A w ?! i = w ?! nth_least (liset A w) i"
      using assms unfolding lproject_to_lselect by simp

    lemma lproject_ltake[simp]:
      assumes "enat k  llength (lproject A w)"
      shows "lproject A (ltake (enat (nth_least (lift (liset A w)) k)) w) =
        ltake (enat k) (lproject A w)"
    proof
      have "llength (lproject A (ltake (enat (nth_least (lift (liset A w)) k)) w)) =
        enat (card (liset A w  {..< nth_least (lift (liset A w)) k}))" by simp
      also have " = enat (card {i  liset A w. i < nth_least (lift (liset A w)) k})"
        unfolding lessThan_def Collect_conj_eq by simp
      also have " = enat k" using assms by simp
      also have " = llength (ltake (enat k) (lproject A w))" using min_absorb1 assms by force
      finally show "llength (lproject A (ltake (enat (nth_least (lift (liset A w)) k)) w)) =
        llength (ltake (enat k) (lproject A w))" by this
    next
      fix i
      assume 1: "enat i < llength (lproject A (ltake (enat (nth_least (lift (liset A w)) k)) w))"
      assume 2: "enat i < llength (ltake (enat k) (lproject A w))"
      obtain k' where 3: "k = Suc k'" using 2 nat.exhaust by auto
      have 4: "enat k' < llength (lproject A w)" using assms 3 by simp
      have 5: "i  k'" using 2 3 by simp
      have 6: "nth_least (lift (liset A w)) k = Suc (nth_least (liset A w) k')"
        using 3 4 by (simp del: nth_least.simps)
      have 7: "nth_least (liset A w) i < Suc (nth_least (liset A w) k')"
      proof -
        have "nth_least (liset A w) i  nth_least (liset A w) k'" using 4 5 by simp
        also have " < Suc (nth_least (liset A w) k')" by simp
        finally show ?thesis by this
      qed
      have 8: "nth_least (liset A w  {..< Suc (nth_least (liset A w) k')}) i =
        nth_least (liset A w) i"
      proof (rule nth_least_eq)
        show "enat i < esize (liset A w  {..< Suc (nth_least (liset A w) k')})" using 1 6 by simp
        have "enat i  enat k'" using 5 by simp
        also have "enat k' < esize (liset A w)" using 4 by simp
        finally show "enat i < esize (liset A w)" by this
      next
        fix j
        assume 1: "j  nth_least (liset A w) i"
        show "j  liset A w  {..< Suc (nth_least (liset A w) k')}  j  liset A w"
          using 1 7 by simp
      qed
      have "lproject A (ltake (enat (nth_least (lift (liset A w)) k)) w) ?! i =
        ltake (enat (Suc (nth_least (liset A w) k'))) w ?!
        nth_least (liset A w  {..< Suc (nth_least (liset A w) k')}) i"
        using 1 6 by simp
      also have " = ltake (enat (Suc (nth_least (liset A w) k'))) w ?! nth_least (liset A w) i"
        using 8 by simp
      also have " = w ?! nth_least (liset A w) i" using 7 by simp
      also have " = lproject A w ?! i" using 2 by simp
      also have " = ltake (enat k) (lproject A w) ?! i" using 2 by simp
      finally show "lproject A (ltake (enat (nth_least (lift (liset A w)) k)) w) ?! i =
        ltake (enat k) (lproject A w) ?! i" by this
    qed

    lemma llength_less_llength_lselect_less:
      "enat i < esize s  enat (nth_least s i) < llength w  enat i < llength (lselect s w)"
      using nth_least_less_esize_less unfolding lselect_llength by this

    lemma lselect_lselect'':
      assumes " i. i  s  enat i < llength w"
      assumes " i. i  t  enat i < llength (lselect s w)"
      shows "lselect t (lselect s w) = lselect (nth_least s ` t) w"
    proof
      note lselect_llength[simp]
      have 1: " i. i  nth_least s ` t  enat i < llength w" using assms by auto
      have 2: "t  {i. enat i < esize s}"
        using assms(2) lselect_llength_le less_le_trans by blast
      have 3: "inj_on (nth_least s) t" using subset_inj_on nth_least.inj_on 2 by this
      have "llength (lselect t (lselect s w)) = esize t" using assms(2) by simp
      also have " = esize (nth_least s ` t)" using 3 by auto
      also have " = llength (lselect (nth_least s ` t) w)" using 1 by simp
      finally show "llength (lselect t (lselect s w)) = llength (lselect (nth_least s ` t) w)"
        by this
    next
      fix i
      assume 1: "enat i < llength (lselect t (lselect s w))"
      assume 2: "enat i < llength (lselect (nth_least s ` t) w)"
      have 3: "enat i < esize t" using less_le_trans 1 lselect_llength_le by this
      have 4: " i. i  t  enat i < esize s"
        using assms(2) lselect_llength_le less_le_trans by blast
      have "lselect t (lselect s w) ?! i = lselect s w ?! nth_least t i" using 1 by simp
      also have " = w ?! nth_least s (nth_least t i)" using assms(2) 3 by simp
      also have " = w ?! nth_least (nth_least s ` t) i" using 3 4 by simp
      also have " = lselect (nth_least s ` t) w ?! i" using 2 by simp
      finally show "lselect t (lselect s w) ?! i = lselect (nth_least s ` t) w ?! i" by this
    qed

    lemma lselect_lselect'[simp]:
      assumes " i. i  t  enat i < esize s"
      shows "lselect t (lselect s w) = lselect (nth_least s ` t) w"
    proof -
      have 1: "nth_least {i  s. enat i < llength w} ` {i  t. enat i < llength (lselect s w)} =
        {i  nth_least s ` t. enat i < llength w}"
      unfolding Compr_image_eq
      proof (rule image_cong)
        show "{i  t. enat i < llength (lselect s w)} = {i  t. enat (nth_least s i) < llength w}"
          using llength_less_llength_lselect_less assms by blast
      next
        fix i
        assume 1: "i  {i  t. enat (nth_least s i) < llength w}"
        have 2: "enat i < esize {i  s. enat i < llength w}"
          using nth_least_less_esize_less assms 1 by blast
        show "nth_least {i  s. enat i < llength w} i = nth_least s i" using 2 by simp
      qed
      have "lselect t (lselect s w) =
        lselect {i  t. enat i < llength (lselect s w)} (lselect {i  s. enat i < llength w} w)"
        by simp
      also have " = lselect (nth_least {i  s. enat i < llength w} `
        {i  t. enat i < llength (lselect s w)}) w"
        by (rule lselect_lselect'', auto simp: lselect_llength)
      also have " = lselect {i  nth_least s ` t. enat i < llength w} w" unfolding 1 by rule
      also have " = lselect (nth_least s ` t) w" by simp
      finally show ?thesis by this
    qed

    lemma lselect_lselect:
      "lselect t (lselect s w) = lselect (nth_least s ` {i  t. enat i < esize s}) w"
    proof -
      have "lselect t (lselect s w) = lselect {i  t. enat i < llength (lselect s w)} (lselect s w)"
        by simp
      also have " = lselect (nth_least s ` {i  t. enat i < llength (lselect s w)}) w"
        using lselect_llength_le less_le_trans by (blast intro: lselect_lselect')
      also have " = lselect (nth_least s ` {i  t. enat i < esize s}) w"
        using llength_less_llength_lselect_less by (auto intro!: lnths_cong)
      finally show ?thesis by this
    qed

    lemma lselect_lproject':
      assumes " i. i  s  enat i < llength w"
      shows "lproject A (lselect s w) = lselect (s  liset A w) w"
    proof -
      have 1: " i. i  liset A (lselect s w)  enat i < esize s" using less_le_trans by force
      have 2: "{i  liset A (lselect s w). enat i < esize s} = liset A (lselect s w)"
        using 1 by auto
      have 3: "nth_least s ` liset A (lselect s w) = s  liset A w"
      proof safe
        fix k
        assume 4: "k  liset A (lselect s w)"
        show "nth_least s k  s" using 1 4 by simp
        show "nth_least s k  liset A w"
          using llength_less_llength_lselect_less 4 unfolding liset_def by auto
      next
        fix k
        assume 1: "k  s" "k  liset A w"
        have 2: "nth_least s (card {i  s. i < k}) = k" using nth_least_card 1(1) by this
        have 3: "enat (card {i  s. i < k}) < llength (lselect s w)"
          unfolding lselect_llength using assms 1(1) by simp
        show "k  nth_least s ` liset A (lselect s w)"
        proof
          show "k = nth_least s (card {i  s. i < k})" using 2 by simp
          show "card {i  s. i < k}  liset A (lselect s w)" using 1(2) 2 3 by fastforce
        qed
      qed
      have "lproject A (lselect s w) = lselect (liset A (lselect s w)) (lselect s w)"
        unfolding lproject_to_lselect by rule
      also have " = lselect (nth_least s ` {i  liset A (lselect s w). enat i < esize s}) w"
        unfolding lselect_lselect by rule
      also have " = lselect (nth_least s ` liset A (lselect s w)) w" unfolding 2 by rule
      also have " = lselect (s  liset A w) w" unfolding 3 by rule
      finally show ?thesis by this
    qed

    lemma lselect_lproject[simp]: "lproject A (lselect s w) = lselect (s  liset A w) w"
    proof -
      have 1: "{i  s. enat i < llength w}  liset A w = s  liset A w" by auto
      have "lproject A (lselect s w) = lproject A (lselect {i  s. enat i < llength w} w)" by simp
      also have " = lselect ({i  s. enat i < llength w}  liset A w) w"
        by (rule lselect_lproject', simp)
      also have " = lselect (s  liset A w) w" unfolding 1 by rule
      finally show ?thesis by this
    qed

    lemma lproject_lselect_subset[simp]:
      assumes "liset A w  s"
      shows "lproject A (lselect s w) = lproject A w"
    proof -
      have 1: "s  liset A w = liset A w" using assms by auto
      have "lproject A (lselect s w) = lselect (s  liset A w) w" by simp
      also have " = lselect (liset A w) w" unfolding 1 by rule
      also have " = lproject A w" unfolding lproject_to_lselect by rule
      finally show ?thesis by this
    qed

    lemma lselect_prefix[intro]:
      assumes "u  v"
      shows "lselect s u  lselect s v"
    proof (cases "lfinite u")
      case False
      show ?thesis using lprefix_infinite assms False by auto
    next
      case True
      obtain k where 1: "llength u = enat k" using True length_list_of by metis
      obtain w where 2: "v = u $ w" using lprefix_conv_lappend assms by auto
      have "lselect s u  lselect s u $ lselect {n. n + k  s} w" by simp
      also have " = lselect s (u $ w)" using lnths_lappend_lfinite[symmetric] 1 by this
      also have " = lselect s v" unfolding 2 by rule
      finally show ?thesis by this
    qed
    lemma lproject_prefix[intro]:
      assumes "u  v"
      shows "lproject A u  lproject A v"
      using lprefix_lfilterI assms by auto

    lemma lproject_prefix_limit[intro?]:
      assumes " v. v  w  lfinite v  lproject A v  x"
      shows "lproject A w  x"
    proof -
      have 1: "ccpo.admissible lSup lprefix (λ v. lproject A v  x)" by simp
      show ?thesis using llist_lift_admissible 1 assms(1) by this
    qed
    lemma lproject_prefix_limit':
      assumes " k.  v. v  w  enat k < llength v  lproject A v  x"
      shows "lproject A w  x"
    proof (rule lproject_prefix_limit)
      fix u
      assume 1: "u  w" "lfinite u"
      obtain k where 2: "llength u = enat k" using 1(2) by (metis length_list_of)
      obtain v where 3: "v  w" "llength u < llength v" "lproject A v  x"
        unfolding 2 using assms(1) by auto
      have 4: "llength u  llength v" using 3(2) by simp
      have 5: "u  v" using prefix_subsume 1(1) 3(1) 4 by this
      have "lproject A u  lproject A v" using 5 by rule
      also have "  x" using 3(3) by this
      finally show "lproject A u  x" by this
    qed

end