Session Coinductive

Theory Coinductive_Nat

(*  Title:       Coinductive natural numbers
    Author:      Andreas Lochbihler
    Maintainer:  Andreas Lochbihler
*)

section ‹Extended natural numbers as a codatatype›

theory Coinductive_Nat imports
  "HOL-Library.Extended_Nat"
  "HOL-Library.Complete_Partial_Order2"
begin

lemma inj_enat [simp]: "inj_on enat A"
by(simp add: inj_on_def)

lemma Sup_range_enat [simp]: "Sup (range enat) = "
by(auto dest: finite_imageD simp add: Sup_enat_def)

lemmas eSuc_plus = iadd_Suc

lemmas plus_enat_eq_0_conv = iadd_is_0

lemma enat_add_sub_same:
  fixes a b :: enat shows "a    a + b - a = b"
by(cases b) auto

lemma enat_the_enat: "n    enat (the_enat n) = n"
by auto

lemma enat_min_eq_0_iff:
  fixes a b :: enat
  shows "min a b = 0  a = 0  b = 0"
by(auto simp add: min_def)

lemma enat_le_plus_same: "x  (x :: enat) + y" "x  y + x"
by(auto simp add: less_eq_enat_def plus_enat_def split: enat.split)

lemma the_enat_0 [simp]: "the_enat 0 = 0"
by(simp add: zero_enat_def)

lemma the_enat_eSuc: "n    the_enat (eSuc n) = Suc (the_enat n)"
by(cases n)(simp_all add: eSuc_enat)

coinductive_set enat_set :: "enat set"
where "0  enat_set"
  | "n  enat_set  (eSuc n)  enat_set"

lemma enat_set_eq_UNIV [simp]: "enat_set = UNIV"
proof
  show "enat_set  UNIV" by blast
  show "UNIV  enat_set"
  proof
    fix x :: enat
    assume "x  UNIV"
    thus "x  enat_set"
    proof coinduct
      case (enat_set x)
      show ?case
      proof(cases "x = 0")
        case True thus ?thesis by simp
      next
        case False
        then obtain n where "x = eSuc n"
          by(cases x)(fastforce simp add: eSuc_def zero_enat_def gr0_conv_Suc
                               split: enat.splits)+
        thus ?thesis by auto
      qed
    qed
  qed
qed

subsection ‹Case operator›

lemma enat_coexhaust:
  obtains (0) "n = 0"
     | (eSuc) n' where "n = eSuc n'"
proof -
  have "n  enat_set" by auto
  thus thesis by cases (erule that)+
qed

locale co begin

free_constructors (plugins del: code) case_enat for
    "0::enat"
  | eSuc epred
where
  "epred 0 = 0"
  apply (erule enat_coexhaust, assumption)
 apply (rule eSuc_inject)
by (rule zero_ne_eSuc)

end

lemma enat_cocase_0 [simp]: "co.case_enat z s 0 = z"
by (rule co.enat.case(1))

lemma enat_cocase_eSuc [simp]: "co.case_enat z s (eSuc n) = s n"
by (rule co.enat.case(2))

lemma neq_zero_conv_eSuc: "n  0  (n'. n = eSuc n')"
by(cases n rule: enat_coexhaust) simp_all

lemma enat_cocase_cert:
  assumes "CASE  co.case_enat c d"
  shows "(CASE 0  c) &&& (CASE (eSuc n)  d n)"
  using assms by simp_all

lemma enat_cosplit_asm:
  "P (co.case_enat c d n) = (¬ (n = 0  ¬ P c  (m. n = eSuc m  ¬ P (d m))))"
by (rule co.enat.split_asm)

lemma enat_cosplit:
  "P (co.case_enat c d n) = ((n = 0  P c)  (m. n = eSuc m  P (d m)))"
by (rule co.enat.split)

abbreviation epred :: "enat => enat" where "epred  co.epred"

lemma epred_0 [simp]: "epred 0 = 0" by(rule co.enat.sel(1))
lemma epred_eSuc [simp]: "epred (eSuc n) = n" by(rule co.enat.sel(2))
declare co.enat.collapse[simp]
lemma epred_conv_minus: "epred n = n - 1"
by(cases n rule: co.enat.exhaust)(simp_all)

subsection ‹Corecursion for @{typ enat}

lemma case_enat_numeral [simp]: "case_enat f i (numeral v) = (let n = numeral v in f n)"
by(simp add: numeral_eq_enat)

lemma case_enat_0 [simp]: "case_enat f i 0 = f 0"
by(simp add: zero_enat_def)

lemma [simp]:
  shows max_eSuc_eSuc: "max (eSuc n) (eSuc m) = eSuc (max n m)"
  and min_eSuc_eSuc: "min (eSuc n) (eSuc m) = eSuc (min n m)"
by(simp_all add: eSuc_def split: enat.split)


definition epred_numeral :: "num  enat"
where [code del]: "epred_numeral = enat  pred_numeral"

lemma numeral_eq_eSuc: "numeral k = eSuc (epred_numeral k)"
by(simp add: numeral_eq_Suc eSuc_def epred_numeral_def numeral_eq_enat)

lemma epred_numeral_simps [simp]:
  "epred_numeral num.One = 0"
  "epred_numeral (num.Bit0 k) = numeral (Num.BitM k)"
  "epred_numeral (num.Bit1 k) = numeral (num.Bit0 k)"
by(simp_all add: epred_numeral_def enat_numeral zero_enat_def)

lemma [simp]:
  shows eq_numeral_eSuc: "numeral k = eSuc n  epred_numeral k = n"
  and Suc_eq_numeral: "eSuc n = numeral k  n = epred_numeral k"
  and less_numeral_Suc: "numeral k < eSuc n  epred_numeral k < n"
  and less_eSuc_numeral: "eSuc n < numeral k  n < epred_numeral k"
  and le_numeral_eSuc: "numeral k  eSuc n  epred_numeral k  n"
  and le_eSuc_numeral: "eSuc n  numeral k  n  epred_numeral k"
  and diff_eSuc_numeral: "eSuc n - numeral k = n - epred_numeral k"
  and diff_numeral_eSuc: "numeral k - eSuc n = epred_numeral k - n"
  and max_eSuc_numeral: "max (eSuc n) (numeral k) = eSuc (max n (epred_numeral k))"
  and max_numeral_eSuc: "max (numeral k) (eSuc n) = eSuc (max (epred_numeral k) n)"
  and min_eSuc_numeral: "min (eSuc n) (numeral k) = eSuc (min n (epred_numeral k))"
  and min_numeral_eSuc: "min (numeral k) (eSuc n) = eSuc (min (epred_numeral k) n)"
by(simp_all add: numeral_eq_eSuc)

lemma enat_cocase_numeral [simp]:
  "co.case_enat a f (numeral v) = (let pv = epred_numeral v in f pv)"
by(simp add: numeral_eq_eSuc)

lemma enat_cocase_add_eq_if [simp]:
  "co.case_enat a f ((numeral v) + n) = (let pv = epred_numeral v in f (pv + n))"
by(simp add: numeral_eq_eSuc iadd_Suc)


lemma [simp]:
  shows epred_1: "epred 1 = 0"
  and epred_numeral: "epred (numeral i) = epred_numeral i"
  and epred_Infty: "epred  = "
  and epred_enat: "epred (enat m) = enat (m - 1)"
by(simp_all add: epred_conv_minus one_enat_def zero_enat_def eSuc_def epred_numeral_def numeral_eq_enat split: enat.split)

lemmas epred_simps = epred_0 epred_1 epred_numeral epred_eSuc epred_Infty epred_enat

lemma epred_iadd1: "a  0  epred (a + b) = epred a + b"
apply(cases a b rule: enat.exhaust[case_product enat.exhaust])
apply(simp_all add: epred_conv_minus eSuc_def one_enat_def zero_enat_def split: enat.splits)
done

lemma epred_min [simp]: "epred (min a b) = min (epred a) (epred b)"
by(cases a b rule: enat_coexhaust[case_product enat_coexhaust]) simp_all

lemma epred_le_epredI: "n  m  epred n  epred m"
by(cases m n rule: enat_coexhaust[case_product enat_coexhaust]) simp_all

lemma epred_minus_epred [simp]:
  "m  0  epred n - epred m = n - m"
by(cases n m rule: enat_coexhaust[case_product enat_coexhaust])(simp_all add: epred_conv_minus)

lemma eSuc_epred: "n  0  eSuc (epred n) = n"
by(cases n rule: enat_coexhaust) simp_all

lemma epred_inject: " x  0; y  0   epred x = epred y  x = y"
by(cases x y rule: enat.exhaust[case_product enat.exhaust])(auto simp add: zero_enat_def)

lemma monotone_fun_eSuc[partial_function_mono]:
    "monotone (fun_ord (λy x. x  y)) (λy x. x  y) (λf. eSuc (f x))"
  by (auto simp: monotone_def fun_ord_def)

partial_function (gfp) enat_unfold :: "('a  bool)  ('a  'a)  'a  enat" where
  enat_unfold [code, nitpick_simp]:
  "enat_unfold stop next a = (if stop a then 0 else eSuc (enat_unfold stop next (next a)))"

lemma enat_unfold_stop [simp]: "stop a  enat_unfold stop next a = 0"
by(simp add: enat_unfold)

lemma enat_unfold_next: "¬ stop a  enat_unfold stop next a = eSuc (enat_unfold stop next (next a))"
by(simp add: enat_unfold)

lemma enat_unfold_eq_0 [simp]:
  "enat_unfold stop next a = 0  stop a"
by(simp add: enat_unfold)

lemma epred_enat_unfold [simp]:
  "epred (enat_unfold stop next a) = (if stop a then 0 else enat_unfold stop next (next a))"
by(simp add: enat_unfold_next)

lemma epred_max: "epred (max x y) = max (epred x) (epred y)"
by(cases x y rule: enat.exhaust[case_product enat.exhaust]) simp_all

lemma epred_Max:
  assumes "finite A" "A  {}"
  shows "epred (Max A) = Max (epred ` A)"
using assms
proof induction
  case (insert x A)
  thus ?case by(cases "A = {}")(simp_all add: epred_max)
qed simp

lemma finite_imageD2: " finite (f ` A); inj_on f (A - B); finite B   finite A"
by (metis Diff_subset finite_Diff2 image_mono inj_on_finite)

lemma epred_Sup: "epred (Sup A) = Sup (epred ` A)"
by(auto 4 4 simp add: bot_enat_def Sup_enat_def epred_Max inj_on_def neq_zero_conv_eSuc dest: finite_imageD2[where B="{0}"])


subsection ‹Less as greatest fixpoint›

coinductive_set Le_enat :: "(enat × enat) set"
where
  Le_enat_zero: "(0, n)  Le_enat"
| Le_enat_add: " (m, n)  Le_enat; k  0   (eSuc m, n + k)  Le_enat"

lemma ile_into_Le_enat:
  "m  n  (m, n)  Le_enat"
proof -
  assume "m  n"
  hence "(m, n)  {(m, n)|m n. m  n}" by simp
  thus ?thesis
  proof coinduct
    case (Le_enat m n)
    hence "m  n" by simp
    show ?case
    proof(cases "m = 0")
      case True
      hence ?Le_enat_zero by simp
      thus ?thesis ..
    next
      case False
      with m  n obtain m' n' where "m = eSuc m'" "n = n' + 1" "m'  n'"
        by(cases m rule: enat_coexhaust, simp)
          (cases n rule: enat_coexhaust, auto simp add: eSuc_plus_1[symmetric])
      hence ?Le_enat_add by fastforce
      thus ?thesis ..
    qed
  qed
qed

lemma Le_enat_imp_ile_enat_k:
  "(m, n)  Le_enat  n < enat l  m < enat l"
proof(induct l arbitrary: m n)
  case 0
  thus ?case by(simp add: zero_enat_def[symmetric])
next
  case (Suc l)
  from (m, n)  Le_enat› show ?case
  proof cases
    case Le_enat_zero
    with n < enat (Suc l) show ?thesis by auto
  next
    case (Le_enat_add M N K)
    from n = N + K n < enat (Suc l) K  0
    have "N < enat l" by(cases N)(cases K, auto simp add: zero_enat_def)
    with (M, N)  Le_enat› have "M < enat l" by(rule Suc)
    with m = eSuc M show ?thesis by(simp add: eSuc_enat[symmetric])
  qed
qed

lemma enat_less_imp_le:
  assumes k: "!!k. n < enat k  m < enat k"
  shows "m  n"
proof(cases n)
  case (enat n')
  with k[of "Suc n'"] show ?thesis by(cases m) simp_all
qed simp

lemma Le_enat_imp_ile:
  "(m, n)  Le_enat  m  n"
by(rule enat_less_imp_le)(erule Le_enat_imp_ile_enat_k)

lemma Le_enat_eq_ile:
  "(m, n)  Le_enat  m  n"
by(blast intro: Le_enat_imp_ile ile_into_Le_enat)

lemma enat_leI [consumes 1, case_names Leenat, case_conclusion Leenat zero eSuc]:
  assumes major: "(m, n)  X"
  and step:
    "m n. (m, n)  X 
      m = 0  (m' n' k. m = eSuc m'  n = n' + enat k  k  0 
                           ((m', n')  X  m'  n'))"
  shows "m  n"
apply(rule Le_enat.coinduct[unfolded Le_enat_eq_ile, where X="λx y. (x, y)  X"])
apply(fastforce simp add: zero_enat_def dest: step intro: major)+
done

lemma enat_le_coinduct[consumes 1, case_names le, case_conclusion le 0 eSuc]:
  assumes P: "P m n"
  and step:
    "m n. P m n 
      (n = 0  m = 0) 
         (m  0  n  0  (k n'. P (epred m) n'  epred n = n' + k)  epred m  epred n)"
  shows "m  n"
proof -
  from P have "(m, n)  {(m, n). P m n}" by simp
  thus ?thesis
  proof(coinduct rule: enat_leI)
    case (Leenat m n)
    hence "P m n" by simp
    show ?case
    proof(cases m rule: enat_coexhaust)
      case 0 
      thus ?thesis by simp
    next
      case (eSuc m')
      with step[OF P m n]
      have "n  0" and disj: "(k n'. P m' n'  epred n = n' + k)  m'  epred n" by auto
      from n  0 obtain n' where n': "n = eSuc n'"
        by(cases n rule: enat_coexhaust) auto
      from disj show ?thesis
      proof
        assume "m'  epred n"
        with eSuc n' show ?thesis 
          by(auto 4 3 intro: exI[where x="Suc 0"] simp add: eSuc_enat[symmetric] iadd_Suc_right zero_enat_def[symmetric])
      next
        assume "k n'. P m' n'  epred n = n' + k"
        then obtain k n'' where n'': "epred n = n'' + k" and k: "P m' n''" by blast
        show ?thesis using eSuc k n' n''
          by(cases k)(auto 4 3 simp add: iadd_Suc_right[symmetric] eSuc_enat intro: exI[where x=])
      qed
    qed
  qed
qed

subsection ‹Equality as greatest fixpoint›

lemma enat_equalityI [consumes 1, case_names Eq_enat,
                                  case_conclusion Eq_enat zero eSuc]:
  assumes major: "(m, n)  X"
  and step:
    "m n. (m, n)  X
      m = 0  n = 0  (m' n'. m = eSuc m'  n = eSuc n'  ((m', n')  X  m' = n'))"
  shows "m = n"
proof(rule antisym)
  from major show "m  n"
    by(coinduct rule: enat_leI)
      (drule step, auto simp add: eSuc_plus_1 enat_1[symmetric])

  from major have "(n, m)  {(n, m). (m, n)  X}" by simp
  thus "n  m"
  proof(coinduct rule: enat_leI)
    case (Leenat n m)
    hence "(m, n)  X" by simp
    from step[OF this] show ?case
      by(auto simp add: eSuc_plus_1 enat_1[symmetric])
  qed
qed

lemma enat_coinduct [consumes 1, case_names Eq_enat, case_conclusion Eq_enat zero eSuc]:
  assumes major: "P m n"
  and step: "m n. P m n 
     (m = 0  n = 0) 
       (m  0  n  0  P (epred m) (epred n)  epred m = epred n)"
  shows "m = n"
proof -
  from major have "(m, n)  {(m, n). P m n}" by simp
  thus ?thesis
  proof(coinduct rule: enat_equalityI)
    case (Eq_enat m n)
    hence "P m n" by simp
    from step[OF this] show ?case
      by(cases m n rule: enat_coexhaust[case_product enat_coexhaust]) auto
  qed
qed

lemma enat_coinduct2 [consumes 1, case_names zero eSuc]:
  " P m n; m n. P m n  m = 0  n = 0; 
     m n.  P m n; m  0; n  0   P (epred m) (epred n)  epred m = epred n 
   m = n"
by(erule enat_coinduct) blast

subsection ‹Uniqueness of corecursion›

lemma enat_unfold_unique:
  assumes h: "!!x. h x = (if stop x then 0 else eSuc (h (next x)))"
  shows "h x = enat_unfold stop next x"
by(coinduction arbitrary: x rule: enat_coinduct)(subst (1 3) h, auto)

subsection ‹Setup for partial\_function›

lemma enat_diff_cancel_left: " m  x; m  y   x - m = y - m  x = (y :: enat)"
by(cases x y m rule: enat.exhaust[case_product enat.exhaust[case_product enat.exhaust]])(simp_all, arith)

lemma finite_lessThan_enatI: 
  assumes "m  "
  shows "finite {..<m :: enat}"
proof -
  from assms obtain m' where m: "m = enat m'" by auto
  have "{..<enat m'}  enat ` {..<m'}"
    by(rule subsetI)(case_tac x, auto)
  thus ?thesis unfolding m by(rule finite_subset) simp
qed

lemma infinite_lessThan_infty: "¬ finite {..< :: enat}"
proof
  have "range enat  {..<}" by auto
  moreover assume "finite {..< :: enat}"
  ultimately have "finite (range enat)" by(rule finite_subset)
  hence "finite (UNIV :: nat set)"
    by(rule finite_imageD)(simp add: inj_on_def)
  thus False by simp
qed

lemma finite_lessThan_enat_iff:
  "finite {..<m :: enat}  m  "
by(cases m)(auto intro: finite_lessThan_enatI simp add: infinite_lessThan_infty)

lemma enat_minus_mono1: "x  y  x - m  y - (m :: enat)"
by(cases m x y rule: enat.exhaust[case_product enat.exhaust[case_product enat.exhaust]]) simp_all

lemma max_enat_minus1: "max n m - k = max (n - k) (m - k :: enat)"
by(cases n m k rule: enat.exhaust[case_product enat.exhaust[case_product enat.exhaust]]) simp_all

lemma Max_enat_minus1:
  assumes "finite A" "A  {}"
  shows "Max A - m = Max ((λn :: enat. n - m) ` A)"
using assms proof induct
  case (insert x A)
  thus ?case by(cases "A = {}")(simp_all add: max_enat_minus1)
qed simp

lemma Sup_enat_minus1: 
  assumes "m  "
  shows "A - m = ((λn :: enat. n - m) ` A)"
proof -
  from assms obtain m' where "m = enat m'" by auto
  thus ?thesis
    by(auto simp add: Sup_enat_def Max_enat_minus1 finite_lessThan_enat_iff enat_diff_cancel_left inj_on_def dest!: finite_imageD2[where B="{..<enat m'}"])
qed

lemma Sup_image_eadd1:
  assumes "Y  {}"
  shows "Sup ((λy :: enat. y+x) ` Y) = Sup Y + x"
proof(cases "finite Y")
  case True
  thus ?thesis by(simp add: Sup_enat_def Max_add_commute assms)
next
  case False
  thus ?thesis
  proof(cases x)
    case (enat x')
    hence "¬ finite ((λy. y+x) ` Y)" using False
      by(auto dest!: finite_imageD intro: inj_onI)
    with False show ?thesis by(simp add: Sup_enat_def assms)
  next
    case infinity
    hence "(+) x ` Y = {}" using assms by auto
    thus ?thesis using infinity by(simp add: image_constant_conv assms)
  qed
qed

lemma Sup_image_eadd2:
  "Y  {}  Sup ((λy :: enat. x + y) ` Y) = x + Sup Y"
by(simp add: Sup_image_eadd1 add.commute)

lemma mono2mono_eSuc [THEN lfp.mono2mono, cont_intro, simp]:
  shows monotone_eSuc: "monotone (≤) (≤) eSuc"
by(rule monotoneI) simp

lemma mcont2mcont_eSuc [THEN lfp.mcont2mcont, cont_intro, simp]:
  shows mcont_eSuc: "mcont Sup (≤) Sup (≤) eSuc"
by(intro mcontI contI)(simp_all add: monotone_eSuc eSuc_Sup)

lemma mono2mono_epred [THEN lfp.mono2mono, cont_intro, simp]:
  shows monotone_epred: "monotone (≤) (≤) epred"
by(rule monotoneI)(simp add: epred_le_epredI)

lemma mcont2mcont_epred [THEN lfp.mcont2mcont, cont_intro, simp]:
  shows mcont_epred: "mcont Sup (≤) Sup (≤) epred"
by(simp add: mcont_def monotone_epred cont_def epred_Sup)

lemma enat_cocase_mono [partial_function_mono, cont_intro]: 
  " monotone orda ordb zero; n. monotone orda ordb (λf. esuc f n) 
   monotone orda ordb (λf. co.case_enat (zero f) (esuc f) x)"
by(cases x rule: co.enat.exhaust) simp_all

lemma enat_cocase_mcont [cont_intro, simp]:
  " mcont luba orda lubb ordb zero; n. mcont luba orda lubb ordb (λf. esuc f n) 
   mcont luba orda lubb ordb (λf. co.case_enat (zero f) (esuc f) x)"
by(cases x rule: co.enat.exhaust) simp_all

lemma eSuc_mono [partial_function_mono]:
  "monotone (fun_ord (≤)) (≤) f  monotone (fun_ord (≤)) (≤) (λx. eSuc (f x))"
by(rule mono2mono_eSuc)

lemma mono2mono_enat_minus1 [THEN lfp.mono2mono, cont_intro, simp]:
  shows monotone_enat_minus1: "monotone (≤) (≤) (λn. n - m :: enat)"
by(rule monotoneI)(rule enat_minus_mono1)

lemma mcont2mcont_enat_minus [THEN lfp.mcont2mcont, cont_intro, simp]:
  shows mcont_enat_minus: "m    mcont Sup (≤) Sup (≤) (λn. n - m :: enat)"
by(rule mcontI)(simp_all add: monotone_enat_minus1 contI Sup_enat_minus1)

lemma monotone_eadd1: "monotone (≤) (≤) (λx. x + y :: enat)"
by(auto intro!: monotoneI)

lemma monotone_eadd2: "monotone (≤) (≤) (λy. x + y :: enat)"
by(auto intro!: monotoneI)

lemma mono2mono_eadd[THEN lfp.mono2mono2, cont_intro, simp]:
  shows monotone_eadd: "monotone (rel_prod (≤) (≤)) (≤) (λ(x, y). x + y :: enat)"
by(simp add: monotone_eadd1 monotone_eadd2)

lemma mcont_eadd2: "mcont Sup (≤) Sup (≤) (λy. x + y :: enat)"
by(auto intro: mcontI monotone_eadd2 contI Sup_image_eadd2[symmetric])

lemma mcont_eadd1: "mcont Sup (≤) Sup (≤) (λx. x + y :: enat)"
by(auto intro: mcontI monotone_eadd1 contI Sup_image_eadd1[symmetric])

lemma mcont2mcont_eadd [cont_intro, simp]:
  " mcont lub ord Sup (≤) (λx. f x);
    mcont lub ord Sup (≤) (λx. g x) 
   mcont lub ord Sup (≤) (λx. f x + g x :: enat)"
by(best intro: ccpo.mcont2mcont'[OF complete_lattice_ccpo] mcont_eadd1 mcont_eadd2 ccpo.mcont_const[OF complete_lattice_ccpo])

lemma eadd_partial_function_mono [partial_function_mono]:
  " monotone (fun_ord (≤)) (≤) f; monotone (fun_ord (≤)) (≤) g 
   monotone (fun_ord (≤)) (≤) (λx. f x + g x :: enat)"
by(rule mono2mono_eadd)

lemma monotone_max_enat1: "monotone (≤) (≤) (λx. max x y :: enat)"
by(auto intro!: monotoneI simp add: max_def)

lemma monotone_max_enat2: "monotone (≤) (≤) (λy. max x y :: enat)"
by(auto intro!: monotoneI simp add: max_def)

lemma mono2mono_max_enat[THEN lfp.mono2mono2, cont_intro, simp]:
  shows monotone_max_enat: "monotone (rel_prod (≤) (≤)) (≤) (λ(x, y). max x y :: enat)"
by(simp add: monotone_max_enat1 monotone_max_enat2)

lemma max_Sup_enat2:
  assumes "Y  {}"
  shows "max x (Sup Y) = Sup ((λy :: enat. max x y) ` Y)"
proof(cases "finite Y")
  case True
  hence "max x (Max Y) = Max (max x ` Y)" using assms
  proof(induct)
    case (insert y Y)
    thus ?case
      by(cases "Y = {}")(simp_all, metis max.assoc max.left_commute max.left_idem)
  qed simp
  thus ?thesis using True by(simp add: Sup_enat_def assms)
next
  case False
  show ?thesis
  proof(cases x)
    case infinity
    hence "max x ` Y = {}" using assms by auto
    thus ?thesis using False by(simp add: Sup_enat_def assms)
  next
    case (enat x')
    { assume "finite (max x ` Y)"
      hence "finite (max x ` {y  Y. y > x})"
        by(rule finite_subset[rotated]) auto
      hence "finite {y  Y. y > x}"
        by(rule finite_imageD)(auto intro!: inj_onI simp add: max_def split: if_split_asm)
      moreover have "finite {y  Y. y  x}"
        by(rule finite_enat_bounded)(auto simp add: enat)
      ultimately have "finite ({y  Y. y > x}  {y  Y. y  x})" by simp
      also have "{y  Y. y > x}  {y  Y. y  x} = Y" by auto
      finally have "finite Y" . }
    thus ?thesis using False by(auto simp add: Sup_enat_def assms)
  qed
qed

lemma max_Sup_enat1:
  "Y  {}  max (Sup Y) x = Sup ((λy :: enat. max y x) ` Y)"
by(subst (1 2) max.commute)(rule max_Sup_enat2)

lemma mcont_max_enat1: "mcont Sup (≤) Sup (≤) (λx. max x y :: enat)"
by(auto intro!: mcontI contI max_Sup_enat1 simp add: monotone_max_enat1)

lemma mcont_max_enat2: "mcont Sup (≤) Sup (≤) (λy. max x y :: enat)"
by(auto intro!: mcontI contI max_Sup_enat2 simp add: monotone_max_enat2)

lemma mcont2mcont_max_enat [cont_intro, simp]:
  " mcont lub ord Sup (≤) (λx. f x);
    mcont lub ord Sup (≤) (λx. g x) 
   mcont lub ord Sup (≤) (λx. max (f x) (g x) :: enat)"
by(best intro: ccpo.mcont2mcont'[OF complete_lattice_ccpo] mcont_max_enat1 mcont_max_enat2 ccpo.mcont_const[OF complete_lattice_ccpo])

lemma max_enat_partial_function_mono [partial_function_mono]:
  " monotone (fun_ord (≤)) (≤) f; monotone (fun_ord (≤)) (≤) g 
   monotone (fun_ord (≤)) (≤) (λx. max (f x) (g x) :: enat)"
by(rule mono2mono_max_enat)

lemma chain_epredI:
  "Complete_Partial_Order.chain (≤) Y
   Complete_Partial_Order.chain (≤) (epred ` (Y  {x. x  0}))"
by(auto intro: chainI dest: chainD)

lemma monotone_enat_le_case:
  fixes bot
  assumes mono: "monotone (≤) ord (λx. f x (eSuc x))"
  and ord: "x. ord bot (f x (eSuc x))"
  and bot: "ord bot bot"
  shows "monotone (≤) ord (λx. case x of 0  bot | eSuc x'  f x' x)"
proof -
  have "monotone (≤) ord (λx. if x  0 then bot else f (epred x) x)"
  proof(rule monotone_if_bot)
    fix x y :: enat
    assume "x  y" "¬ x  0"
    thus "ord (f (epred x) x) (f (epred y) y)"
      by(cases x y rule: co.enat.exhaust[case_product co.enat.exhaust])(auto intro: monotoneD[OF mono])
  next
    fix x :: enat
    assume "¬ x  0"
    thus "ord bot (f (epred x) x)"
      by(cases x rule: co.enat.exhaust)(auto intro: ord)
  qed(rule bot)
  also have "(λx. if x  0 then bot else f (epred x) x) = (λx. case x of 0  bot | eSuc x'  f x' x)"
    by(auto simp add: fun_eq_iff split: co.enat.split)
  finally show ?thesis .
qed

lemma mcont_enat_le_case:
  fixes bot
  assumes ccpo: "class.ccpo lub ord (mk_less ord)"
  and mcont: "mcont Sup (≤) lub ord (λx. f x (eSuc x))"
  and ord: "x. ord bot (f x (eSuc x))"
  shows "mcont Sup (≤) lub ord (λx. case x of 0  bot | eSuc x'  f x' x)"
proof -
  from ccpo
  have "mcont Sup (≤) lub ord (λx. if x  0 then bot else f (epred x) x)"
  proof(rule mcont_if_bot)
    fix x y :: enat
    assume "x  y" "¬ x  0"
    thus "ord (f (epred x) x) (f (epred y) y)"
      by(cases x y rule: co.enat.exhaust[case_product co.enat.exhaust])(auto intro: mcont_monoD[OF mcont])
  next
    fix Y :: "enat set"
    assume chain: "Complete_Partial_Order.chain (≤) Y"
      and Y: "Y  {}" "x. x  Y  ¬ x  0"
    from Y have Y': "Y  {x. x  0}  {}" by auto
    from Y(2) have eq: "Y = eSuc ` (epred ` (Y  {x. x  0}))"
      by(fastforce intro: rev_image_eqI)
    let ?Y = "epred ` (Y  {x. x  0})"
    from chain_epredI [OF chain] Y'
    have "f (?Y) (eSuc (?Y)) = lub ((λx. f x (eSuc x)) ` ?Y)"
      using mcont [THEN mcont_contD] by blast
    moreover from chain_epredI [OF chain] Y'
      have "(eSuc ` ?Y) = eSuc (?Y)"
      using mcont_eSuc [THEN mcont_contD, symmetric] by blast
    ultimately show "f (epred (Sup Y)) (Sup Y) = lub ((λx. f (epred x) x) ` Y)"
      by (subst (1 2 3) eq) (simp add: image_image)
  next
    fix x :: enat
    assume "¬ x  0"
    thus "ord bot (f (epred x) x)"
      by(cases x rule: co.enat.exhaust)(auto intro: ord)
  qed
  also have "(λx. if x  0 then bot else f (epred x) x) = (λx. case x of 0  bot | eSuc x'  f x' x)"
    by(auto simp add: fun_eq_iff split: co.enat.split)
  finally show ?thesis .
qed


subsection ‹Misc.›

lemma enat_add_mono [simp]:
  "enat x + y < enat x + z  y < z"
by(cases y)(case_tac [!] z, simp_all)

lemma enat_add1_eq [simp]: "enat x + y = enat x + z  y = z"
by (metis enat_add_mono add.commute neq_iff)

lemma enat_add2_eq [simp]: "y + enat x = z + enat x  y = z"
by (metis enat_add1_eq add.commute)

lemma enat_less_enat_plusI: "x < y  enat x < enat y + z"
by(cases z) simp_all

lemma enat_less_enat_plusI2:
  "enat y < z  enat (x + y) < enat x + z"
by (metis enat_add_mono plus_enat_simps(1))

lemma min_enat1_conv_enat: "a b. min (enat a) b = enat (case b of enat b'  min a b' |   a)"
  and min_enat2_conv_enat: "a b. min a (enat b) = enat (case a of enat a'  min a' b |   b)"
by(simp_all split: enat.split)

lemma eSuc_le_iff: "eSuc x  y  (y'. y = eSuc y'  x  y')"
by(cases y rule: co.enat.exhaust) simp_all

lemma eSuc_eq_infinity_iff: "eSuc n =   n = "
by(cases n)(simp_all add: zero_enat_def eSuc_enat)

lemma infinity_eq_eSuc_iff: " = eSuc n  n = "
by(cases n)(simp_all add: zero_enat_def eSuc_enat)

lemma enat_cocase_inf: "(case  of 0  a | eSuc b  f b) = f "
by(auto split: co.enat.split simp add: infinity_eq_eSuc_iff)

lemma eSuc_Inf: "eSuc (Inf A) = Inf (eSuc ` A)"
proof -
  { assume "A  {}"
    then obtain a where "a  A" by blast
    then have "eSuc (LEAST a. a  A) = (LEAST a. a  eSuc ` A)"
    proof (rule LeastI2_wellorder)
      fix a assume "a  A" and b: "b. b  A  a  b"
      then have a: "eSuc a  eSuc ` A"
        by auto
      then show "eSuc a = (LEAST a. a  eSuc ` A)"
        by (rule LeastI2_wellorder) (metis (full_types) b a antisym eSuc_le_iff imageE)
    qed }
  then show ?thesis
    by (simp add: Inf_enat_def)
qed

end

Theory Coinductive_List

(*  Title:      Coinductive_List.thy
    Author:     Andreas Lochbihler
*)

section ‹Coinductive lists and their operations›

theory Coinductive_List
imports
  "HOL-Library.Infinite_Set"
  "HOL-Library.Sublist"
  "HOL-Library.Simps_Case_Conv"
  Coinductive_Nat
begin

subsection ‹Auxiliary lemmata›

lemma funpow_Suc_conv [simp]: "(Suc ^^ n) m = m + n"
by(induct n arbitrary: m) simp_all

lemma wlog_linorder_le [consumes 0, case_names le symmetry]:
  assumes le: "a b :: 'a :: linorder. a  b  P a b"
  and sym: "P b a  P a b"
  shows "P a b"
proof(cases "a  b")
  case True thus ?thesis by(rule le)
next
  case False
  hence "b  a" by simp
  hence "P b a" by(rule le)
  thus ?thesis by(rule sym)
qed

subsection ‹Type definition›

codatatype (lset: 'a) llist =
    lnull: LNil
  | LCons (lhd: 'a) (ltl: "'a llist")
for
  map: lmap
  rel: llist_all2
where
  "lhd LNil = undefined"
| "ltl LNil = LNil"


text ‹
  Coiterator setup.
›

primcorec unfold_llist :: "('a  bool)  ('a  'b)  ('a  'a)  'a  'b llist" where
  "p a  unfold_llist p g21 g22 a = LNil" |
  "_  unfold_llist p g21 g22 a = LCons (g21 a) (unfold_llist p g21 g22 (g22 a))"

declare
  unfold_llist.ctr(1) [simp]
  llist.corec(1) [simp]

text ‹
  The following setup should be done by the BNF package.
›

text ‹congruence rule›

declare llist.map_cong [cong]

text ‹Code generator setup›

lemma corec_llist_never_stop: "corec_llist IS_LNIL LHD (λ_. False) MORE LTL x = unfold_llist IS_LNIL LHD LTL x"
by(coinduction arbitrary: x) auto

text ‹lemmas about generated constants›

lemma eq_LConsD: "xs = LCons y ys  xs  LNil  lhd xs = y  ltl xs = ys"
by auto

lemma
  shows LNil_eq_lmap: "LNil = lmap f xs  xs = LNil"
  and lmap_eq_LNil: "lmap f xs = LNil  xs = LNil"
by(cases xs,simp_all)+

declare llist.map_sel(1)[simp]

lemma ltl_lmap[simp]: "ltl (lmap f xs) = lmap f (ltl xs)"
by(cases xs, simp_all)

declare llist.map_ident[simp]

lemma lmap_eq_LCons_conv:
  "lmap f xs = LCons y ys 
  (x xs'. xs = LCons x xs'  y = f x  ys = lmap f xs')"
by(cases xs)(auto)

lemma lmap_conv_unfold_llist:
  "lmap f = unfold_llist (λxs. xs = LNil) (f  lhd) ltl" (is "?lhs = ?rhs")
proof
  fix x
  show "?lhs x = ?rhs x" by(coinduction arbitrary: x) auto
qed

lemma lmap_unfold_llist:
  "lmap f (unfold_llist IS_LNIL LHD LTL b) = unfold_llist IS_LNIL (f  LHD) LTL b"
by(coinduction arbitrary: b) auto

lemma lmap_corec_llist:
  "lmap f (corec_llist IS_LNIL LHD endORmore TTL_end TTL_more b) =
   corec_llist IS_LNIL (f  LHD) endORmore (lmap f  TTL_end) TTL_more b"
by(coinduction arbitrary: b rule: llist.coinduct_strong) auto

lemma unfold_llist_ltl_unroll:
  "unfold_llist IS_LNIL LHD LTL (LTL b) = unfold_llist (IS_LNIL  LTL) (LHD  LTL) LTL b"
by(coinduction arbitrary: b) auto

lemma ltl_unfold_llist:
  "ltl (unfold_llist IS_LNIL LHD LTL a) =
  (if IS_LNIL a then LNil else unfold_llist IS_LNIL LHD LTL (LTL a))"
by(simp)

lemma unfold_llist_eq_LCons [simp]:
  "unfold_llist IS_LNIL LHD LTL b = LCons x xs 
  ¬ IS_LNIL b  x = LHD b  xs = unfold_llist IS_LNIL LHD LTL (LTL b)"
by(subst unfold_llist.code) auto

lemma unfold_llist_id [simp]: "unfold_llist lnull lhd ltl xs = xs"
by(coinduction arbitrary: xs) simp_all

lemma lset_eq_empty [simp]: "lset xs = {}  lnull xs"
by(cases xs) simp_all

declare llist.set_sel(1)[simp]

lemma lset_ltl: "lset (ltl xs)  lset xs"
by(cases xs) auto

lemma in_lset_ltlD: "x  lset (ltl xs)  x  lset xs"
using lset_ltl[of xs] by auto

text ‹induction rules›

theorem llist_set_induct[consumes 1, case_names find step]:
  assumes "x  lset xs" and "xs. ¬ lnull xs  P (lhd xs) xs"
  and "xs y. ¬ lnull xs; y  lset (ltl xs); P y (ltl xs)  P y xs"
  shows "P x xs"
using assms by(induct)(fastforce simp del: llist.disc(2) iff: llist.disc(2), auto)

text ‹Test quickcheck setup›

lemma "xs. xs = LNil"
quickcheck[random, expect=counterexample]
quickcheck[exhaustive, expect=counterexample]
oops

lemma "LCons x xs = LCons x xs"
quickcheck[narrowing, expect=no_counterexample]
oops

subsection ‹Properties of predefined functions›

lemmas lhd_LCons = llist.sel(1)
lemmas ltl_simps = llist.sel(2,3)

lemmas lhd_LCons_ltl = llist.collapse(2)

lemma lnull_ltlI [simp]: "lnull xs  lnull (ltl xs)"
unfolding lnull_def by simp

lemma neq_LNil_conv: "xs  LNil  (x xs'. xs = LCons x xs')"
by(cases xs) auto

lemma not_lnull_conv: "¬ lnull xs  (x xs'. xs = LCons x xs')"
unfolding lnull_def by(simp add: neq_LNil_conv)

lemma lset_LCons:
  "lset (LCons x xs) = insert x (lset xs)"
by simp

lemma lset_intros:
  "x  lset (LCons x xs)"
  "x  lset xs  x  lset (LCons x' xs)"
by simp_all

lemma lset_cases [elim?]:
  assumes "x  lset xs"
  obtains xs' where "xs = LCons x xs'"
  | x' xs' where "xs = LCons x' xs'" "x  lset xs'"
using assms by(cases xs) auto

lemma lset_induct' [consumes 1, case_names find step]:
  assumes major: "x  lset xs"
  and 1: "xs. P (LCons x xs)"
  and 2: "x' xs.  x  lset xs; P xs   P (LCons x' xs)"
  shows "P xs"
using major apply(induct y"x" xs rule: llist_set_induct)
using 1 2 by(auto simp add: not_lnull_conv)

lemma lset_induct [consumes 1, case_names find step, induct set: lset]:
  assumes major: "x  lset xs"
  and find: "xs. P (LCons x xs)"
  and step: "x' xs.  x  lset xs; x  x'; P xs   P (LCons x' xs)"
  shows "P xs"
using major
apply(induct rule: lset_induct')
 apply(rule find)
apply(case_tac "x'=x")
apply(simp_all add: find step)
done

lemmas lset_LNil = llist.set(1)

lemma lset_lnull: "lnull xs  lset xs = {}"
by(auto dest: llist.collapse)

text ‹Alternative definition of @{term lset} for nitpick›

inductive lsetp :: "'a llist  'a  bool"
where
  "lsetp (LCons x xs) x"
| "lsetp xs x  lsetp (LCons x' xs) x"

lemma lset_into_lsetp:
  "x  lset xs  lsetp xs x"
by(induct rule: lset_induct)(blast intro: lsetp.intros)+

lemma lsetp_into_lset:
  "lsetp xs x  x  lset xs"
by(induct rule: lsetp.induct)(blast intro: lset_intros)+

lemma lset_eq_lsetp [nitpick_unfold]:
  "lset xs = {x. lsetp xs x}"
by(auto intro: lset_into_lsetp dest: lsetp_into_lset)

hide_const (open) lsetp
hide_fact (open) lsetp.intros lsetp.cases lsetp.induct lset_into_lsetp lset_eq_lsetp

text ‹code setup for @{term lset}

definition gen_lset :: "'a set  'a llist  'a set"
where "gen_lset A xs = A  lset xs"

lemma gen_lset_code [code]:
  "gen_lset A LNil = A"
  "gen_lset A (LCons x xs) = gen_lset (insert x A) xs"
by(auto simp add: gen_lset_def)

lemma lset_code [code]:
  "lset = gen_lset {}"
by(simp add: gen_lset_def fun_eq_iff)

definition lmember :: "'a  'a llist  bool"
where "lmember x xs  x  lset xs"

lemma lmember_code [code]:
  "lmember x LNil  False"
  "lmember x (LCons y ys)  x = y  lmember x ys"
by(simp_all add: lmember_def)

lemma lset_lmember [code_unfold]:
  "x  lset xs  lmember x xs"
by(simp add: lmember_def)

lemmas lset_lmap [simp] = llist.set_map

subsection ‹The subset of finite lazy lists @{term "lfinite"}

inductive lfinite :: "'a llist  bool"
where
  lfinite_LNil:  "lfinite LNil"
| lfinite_LConsI: "lfinite xs  lfinite (LCons x xs)"

declare lfinite_LNil [iff]

lemma lnull_imp_lfinite [simp]: "lnull xs  lfinite xs"
by(auto dest: llist.collapse)

lemma lfinite_LCons [simp]: "lfinite (LCons x xs) = lfinite xs"
by(auto elim: lfinite.cases intro: lfinite_LConsI)

lemma lfinite_ltl [simp]: "lfinite (ltl xs) = lfinite xs"
by(cases xs) simp_all

lemma lfinite_code [code]:
  "lfinite LNil = True"
  "lfinite (LCons x xs) = lfinite xs"
by simp_all

lemma lfinite_induct [consumes 1, case_names LNil LCons]:
  assumes lfinite: "lfinite xs"
  and LNil: "xs. lnull xs  P xs"
  and LCons: "xs.  lfinite xs; ¬ lnull xs; P (ltl xs)   P xs"
  shows "P xs"
using lfinite by(induct)(auto intro: LCons LNil)

lemma lfinite_imp_finite_lset:
  assumes "lfinite xs"
  shows "finite (lset xs)"
using assms by induct auto

subsection ‹Concatenating two lists: @{term "lappend"}

primcorec lappend :: "'a llist  'a llist  'a llist"
where
  "lappend xs ys = (case xs of LNil  ys | LCons x xs'  LCons x (lappend xs' ys))"

simps_of_case lappend_code [code, simp, nitpick_simp]: lappend.code

lemmas lappend_LNil_LNil = lappend_code(1)[where ys = LNil]

lemma lappend_simps [simp]:
  shows lhd_lappend: "lhd (lappend xs ys) = (if lnull xs then lhd ys else lhd xs)"
  and ltl_lappend: "ltl (lappend xs ys) = (if lnull xs then ltl ys else lappend (ltl xs) ys)"
by(case_tac [!] xs) simp_all

lemma lnull_lappend [simp]:
  "lnull (lappend xs ys)  lnull xs  lnull ys"
by(auto simp add: lappend_def)

lemma lappend_eq_LNil_iff:
  "lappend xs ys = LNil  xs = LNil  ys = LNil"
using lnull_lappend unfolding lnull_def .

lemma LNil_eq_lappend_iff:
  "LNil = lappend xs ys  xs = LNil  ys = LNil"
by(auto dest: sym simp add: lappend_eq_LNil_iff)

lemma lappend_LNil2 [simp]: "lappend xs LNil = xs"
by(coinduction arbitrary: xs) simp_all

lemma shows lappend_lnull1: "lnull xs  lappend xs ys = ys"
  and lappend_lnull2: "lnull ys  lappend xs ys = xs"
unfolding lnull_def by simp_all

lemma lappend_assoc: "lappend (lappend xs ys) zs = lappend xs (lappend ys zs)"
by(coinduction arbitrary: xs rule: llist.coinduct_strong) auto

lemma lmap_lappend_distrib:
  "lmap f (lappend xs ys) = lappend (lmap f xs) (lmap f ys)"
by(coinduction arbitrary: xs rule: llist.coinduct_strong) auto

lemma lappend_snocL1_conv_LCons2:
  "lappend (lappend xs (LCons y LNil)) ys = lappend xs (LCons y ys)"
by(simp add: lappend_assoc)

lemma lappend_ltl: "¬ lnull xs  lappend (ltl xs) ys = ltl (lappend xs ys)"
by simp

lemma lfinite_lappend [simp]:
  "lfinite (lappend xs ys)  lfinite xs  lfinite ys"
  (is "?lhs  ?rhs")
proof
  assume ?lhs thus ?rhs
  proof(induct zs"lappend xs ys" arbitrary: xs ys)
    case lfinite_LNil
    thus ?case by(simp add: LNil_eq_lappend_iff)
  next
    case (lfinite_LConsI zs z)
    thus ?case by(cases xs)(cases ys, simp_all)
  qed
next
  assume ?rhs (is "?xs  ?ys")
  then obtain ?xs ?ys ..
  thus ?lhs by induct simp_all
qed

lemma lappend_inf: "¬ lfinite xs  lappend xs ys = xs"
by(coinduction arbitrary: xs) auto

lemma lfinite_lmap [simp]:
  "lfinite (lmap f xs) = lfinite xs"
  (is "?lhs  ?rhs")
proof
  assume ?lhs
  thus ?rhs
    by(induct zs"lmap f xs" arbitrary: xs rule: lfinite_induct) fastforce+
next
  assume ?rhs
  thus ?lhs by(induct) simp_all
qed

lemma lset_lappend_lfinite [simp]:
  "lfinite xs  lset (lappend xs ys) = lset xs  lset ys"
by(induct rule: lfinite.induct) auto

lemma lset_lappend: "lset (lappend xs ys)  lset xs  lset ys"
proof(cases "lfinite xs")
  case True
  thus ?thesis by simp
next
  case False
  thus ?thesis by(auto simp add: lappend_inf)
qed

lemma lset_lappend1: "lset xs  lset (lappend xs ys)"
by(rule subsetI)(erule lset_induct, simp_all)

lemma lset_lappend_conv: "lset (lappend xs ys) = (if lfinite xs then lset xs  lset ys else lset xs)"
by(simp add: lappend_inf)

lemma in_lset_lappend_iff: "x  lset (lappend xs ys)  x  lset xs  lfinite xs  x  lset ys"
by(simp add: lset_lappend_conv)

lemma split_llist_first:
  assumes "x  lset xs"
  shows "ys zs. xs = lappend ys (LCons x zs)  lfinite ys  x  lset ys"
using assms
proof(induct)
  case find thus ?case by(auto intro: exI[where x=LNil])
next
  case step thus ?case by(fastforce intro: exI[where x="LCons a b" for a b])
qed

lemma split_llist: "x  lset xs  ys zs. xs = lappend ys (LCons x zs)  lfinite ys"
by(blast dest: split_llist_first)

subsection ‹The prefix ordering on lazy lists: @{term "lprefix"}

coinductive lprefix :: "'a llist  'a llist  bool" (infix "" 65)
where
  LNil_lprefix [simp, intro!]: "LNil  xs"
| Le_LCons: "xs  ys  LCons x xs  LCons x ys"

lemma lprefixI [consumes 1, case_names lprefix,
                case_conclusion lprefix LeLNil LeLCons]:
  assumes major: "(xs, ys)  X"
  and step:
      "xs ys. (xs, ys)  X
        lnull xs  (x xs' ys'. xs = LCons x xs'  ys = LCons x ys' 
                                   ((xs', ys')  X  xs'  ys'))"
  shows "xs  ys"
using major by(rule lprefix.coinduct)(auto dest: step)

lemma lprefix_coinduct [consumes 1, case_names lprefix, case_conclusion lprefix LNil LCons, coinduct pred: lprefix]:
  assumes major: "P xs ys"
  and step: "xs ys. P xs ys
     (lnull ys  lnull xs) 
       (¬ lnull xs  ¬ lnull ys  lhd xs = lhd ys  (P (ltl xs) (ltl ys)  ltl xs  ltl ys))"
  shows "xs  ys"
proof -
  from major have "(xs, ys)  {(xs, ys). P xs ys}" by simp
  thus ?thesis
  proof(coinduct rule: lprefixI)
    case (lprefix xs ys)
    hence "P xs ys" by simp
    from step[OF this] show ?case
      by(cases xs)(auto simp add: not_lnull_conv)
  qed
qed

lemma lprefix_refl [intro, simp]: "xs  xs"
by(coinduction arbitrary: xs) simp_all

lemma lprefix_LNil [simp]: "xs  LNil  lnull xs"
unfolding lnull_def by(subst lprefix.simps)simp

lemma lprefix_lnull: "lnull ys  xs  ys  lnull xs"
unfolding lnull_def by auto

lemma lnull_lprefix: "lnull xs  lprefix xs ys"
by(simp add: lnull_def)

lemma lprefix_LCons_conv:
  "xs  LCons y ys 
   xs = LNil  (xs'. xs = LCons y xs'  xs'  ys)"
by(subst lprefix.simps) simp

lemma LCons_lprefix_LCons [simp]:
  "LCons x xs  LCons y ys  x = y  xs  ys"
by(simp add: lprefix_LCons_conv)

lemma LCons_lprefix_conv:
  "LCons x xs  ys  (ys'. ys = LCons x ys'  xs  ys')"
by(cases ys)(auto)

lemma lprefix_ltlI: "xs  ys  ltl xs  ltl ys"
by(cases ys)(auto simp add: lprefix_LCons_conv)

lemma lprefix_code [code]:
  "LNil  ys  True"
  "LCons x xs  LNil  False"
  "LCons x xs  LCons y ys  x = y  xs  ys"
by simp_all

lemma lprefix_lhdD: " xs  ys; ¬ lnull xs   lhd xs = lhd ys"
by(clarsimp simp add: not_lnull_conv LCons_lprefix_conv)

lemma lprefix_lnullD: " xs  ys; lnull ys   lnull xs"
by(auto elim: lprefix.cases)

lemma lprefix_not_lnullD: " xs  ys; ¬ lnull xs   ¬ lnull ys"
by(auto elim: lprefix.cases)

lemma lprefix_expand:
  "(¬ lnull xs  ¬ lnull ys  lhd xs = lhd ys  ltl xs  ltl ys)  xs  ys"
by(cases xs ys rule: llist.exhaust[case_product llist.exhaust])(simp_all)

lemma lprefix_antisym:
  " xs  ys; ys  xs   xs = ys"
by(coinduction arbitrary: xs ys)(auto simp add: not_lnull_conv lprefix_lnull)

lemma lprefix_trans [trans]:
  " xs  ys; ys  zs   xs  zs"
by(coinduction arbitrary: xs ys zs)(auto 4 3 dest: lprefix_lnullD lprefix_lhdD intro: lprefix_ltlI)

lemma preorder_lprefix [cont_intro]:
  "class.preorder (⊑) (mk_less (⊑))"
by(unfold_locales)(auto simp add: mk_less_def intro: lprefix_trans)

lemma lprefix_lsetD:
  assumes "xs  ys"
  shows "lset xs  lset ys"
proof
  fix x
  assume "x  lset xs"
  thus "x  lset ys" using assms
    by(induct arbitrary: ys)(auto simp add: LCons_lprefix_conv)
qed

lemma lprefix_lappend_sameI:
  assumes "xs  ys"
  shows "lappend zs xs  lappend zs ys"
proof(cases "lfinite zs")
  case True
  thus ?thesis using assms by induct auto
qed(simp add: lappend_inf)

lemma not_lfinite_lprefix_conv_eq:
  assumes nfin: "¬ lfinite xs"
  shows "xs  ys  xs = ys"
proof
  assume "xs  ys"
  with nfin show "xs = ys"
    by(coinduction arbitrary: xs ys)(auto dest: lprefix_lnullD lprefix_lhdD intro: lprefix_ltlI)
qed simp

lemma lprefix_lappend: "xs  lappend xs ys"
by(coinduction arbitrary: xs) auto

lemma lprefix_down_linear:
  assumes "xs  zs" "ys  zs"
  shows "xs  ys  ys  xs"
proof(rule disjCI)
  assume "¬ ys  xs"
  with assms show "xs  ys"
    by(coinduction arbitrary: xs ys zs)(auto simp add: not_lnull_conv LCons_lprefix_conv, simp add: lnull_def)
qed

lemma lprefix_lappend_same [simp]:
  "lappend xs ys  lappend xs zs  (lfinite xs  ys  zs)"
  (is "?lhs  ?rhs")
proof
  assume "?lhs"
  show "?rhs"
  proof
    assume "lfinite xs"
    thus "ys  zs" using ?lhs by(induct) simp_all
  qed
next
  assume "?rhs"
  show ?lhs
  proof(cases "lfinite xs")
    case True
    hence yszs: "ys  zs" by(rule ?rhs[rule_format])
    from True show ?thesis by induct (simp_all add: yszs)
  next
    case False thus ?thesis by(simp add: lappend_inf)
  qed
qed

subsection ‹Setup for partial\_function›

primcorec lSup :: "'a llist set  'a llist"
where
  "lSup A =
  (if xA. lnull x then LNil
   else LCons (THE x. x  lhd ` (A  {xs. ¬ lnull xs})) (lSup (ltl ` (A  {xs. ¬ lnull xs}))))"

declare lSup.simps[simp del]

lemma lnull_lSup [simp]: "lnull (lSup A)  (xA. lnull x)"
by(simp add: lSup_def)

lemma lhd_lSup [simp]: "xA. ¬ lnull x  lhd (lSup A) = (THE x. x  lhd ` (A  {xs. ¬ lnull xs}))"
by(auto simp add: lSup_def)

lemma ltl_lSup [simp]: "ltl (lSup A) = lSup (ltl ` (A  {xs. ¬ lnull xs}))"
by(cases "xsA. lnull xs")(auto 4 3 simp add: lSup_def intro: llist.expand)

lemma lhd_lSup_eq:
  assumes chain: "Complete_Partial_Order.chain (⊑) Y"
  shows " xs  Y; ¬ lnull xs   lhd (lSup Y) = lhd xs"
by(subst lhd_lSup)(auto 4 3 dest: chainD[OF chain] lprefix_lhdD intro!: the_equality)

lemma lSup_empty [simp]: "lSup {} = LNil"
by(simp add: lSup_def)

lemma lSup_singleton [simp]: "lSup {xs} = xs"
by(coinduction arbitrary: xs) simp_all

lemma LCons_image_Int_not_lnull: "(LCons x ` A  {xs. ¬ lnull xs}) = LCons x ` A"
by auto

lemma lSup_LCons: "A  {}  lSup (LCons x ` A) = LCons x (lSup A)"
by(rule llist.expand)(auto simp add: image_image lhd_lSup exI LCons_image_Int_not_lnull intro!: the_equality)

lemma lSup_eq_LCons_iff:
  "lSup Y = LCons x xs  (xY. ¬ lnull x)  x = (THE x. x  lhd ` (Y  {xs. ¬ lnull xs}))  xs = lSup (ltl ` (Y  {xs. ¬ lnull xs}))"
by(auto dest: eq_LConsD simp add: lnull_def[symmetric] intro: llist.expand)

lemma lSup_insert_LNil: "lSup (insert LNil Y) = lSup Y"
by(rule llist.expand) simp_all

lemma lSup_minus_LNil: "lSup (Y - {LNil}) = lSup Y"
using lSup_insert_LNil[where Y="Y - {LNil}", symmetric]
by(cases "LNil  Y")(simp_all add: insert_absorb)

lemma chain_lprefix_ltl:
  assumes chain: "Complete_Partial_Order.chain (⊑) A"
  shows "Complete_Partial_Order.chain (⊑) (ltl ` (A  {xs. ¬ lnull xs}))"
by(auto intro!: chainI dest: chainD[OF chain] intro: lprefix_ltlI)

lemma lSup_finite_prefixes: "lSup {ys. ys  xs  lfinite ys} = xs" (is "lSup (?C xs) = _")
proof(coinduction arbitrary: xs)
  case (Eq_llist xs)
  have ?lnull
    by(cases xs)(auto simp add: lprefix_LCons_conv)
  moreover
  have "¬ lnull xs  ltl ` ({ys. ys  xs  lfinite ys}  {xs. ¬ lnull xs}) = {ys. ys  ltl xs  lfinite ys}"
    by(auto 4 4 intro!: rev_image_eqI[where x="LCons (lhd xs) ys" for ys] intro: llist.expand lprefix_ltlI simp add: LCons_lprefix_conv)
  hence ?LCons by(auto 4 3 intro!: the_equality dest: lprefix_lhdD intro: rev_image_eqI)
  ultimately show ?case ..
qed

lemma lSup_finite_gen_prefixes:
  assumes "zs  xs" "lfinite zs"
  shows "lSup {ys. ys  xs  zs  ys  lfinite ys} = xs"
using ‹lfinite zs zs  xs
proof(induction arbitrary: xs)
  case lfinite_LNil
  thus ?case by(simp add: lSup_finite_prefixes)
next
  case (lfinite_LConsI zs z)
  from ‹LCons z zs  xs obtain xs' where xs: "xs = LCons z xs'"
    and "zs  xs'" by(auto simp add: LCons_lprefix_conv)
  show ?case (is "?lhs = ?rhs")
  proof(rule llist.expand)
    show "lnull ?lhs = lnull ?rhs" using xs lfinite_LConsI
      by(auto 4 3 simp add: lprefix_LCons_conv del: disjCI intro: disjI2)
  next
    assume lnull: "¬ lnull ?lhs" "¬ lnull ?rhs"
    have "lhd ?lhs = lhd ?rhs" using lnull xs
      by(auto intro!: rev_image_eqI simp add: LCons_lprefix_conv)
    moreover
    have "ltl ` ({ys. ys  xs  LCons z zs  ys  lfinite ys}  {xs. ¬ lnull xs}) =
          {ys. ys  xs'  zs  ys  lfinite ys}"
      using xs ¬ lnull ?rhs
      by(auto 4 3 simp add: lprefix_LCons_conv intro: rev_image_eqI del: disjCI intro: disjI2)
    hence "ltl ?lhs = ltl ?rhs" using lfinite_LConsI.IH[OF zs  xs'] xs by simp
    ultimately show "lhd ?lhs = lhd ?rhs  ltl ?lhs = ltl ?rhs" ..
  qed
qed

lemma lSup_strict_prefixes:
  "¬ lfinite xs  lSup {ys. ys  xs  ys  xs} = xs"
  (is "_  lSup (?C xs) = _")
proof(coinduction arbitrary: xs)
  case (Eq_llist xs)
  then obtain x x' xs' where xs: "xs = LCons x (LCons x' xs')" "¬ lfinite xs'"
    by(cases xs)(simp, rename_tac xs', case_tac xs', auto)
  hence ?lnull by(auto intro: exI[where x="LCons x (LCons x' LNil)"])
  moreover hence "¬ lnull (lSup {ys. ys  xs  ys  xs})" using xs by auto
  hence "lhd (lSup {ys. ys  xs  ys  xs}) = lhd xs" using xs
    by(auto 4 3 intro!: the_equality intro: rev_image_eqI dest: lprefix_lhdD)
  moreover from xs
  have "ltl ` ({ys. ys  xs  ys  xs}  {xs. ¬ lnull xs}) = {ys. ys  ltl xs  ys  ltl xs}"
    by(auto simp add: lprefix_LCons_conv intro: image_eqI[where x="LCons x (LCons x' ys)" for ys] image_eqI[where x="LCons x LNil"])
  ultimately show ?case using Eq_llist by clarsimp
qed

lemma chain_lprefix_lSup:
  " Complete_Partial_Order.chain (⊑) A; xs  A 
   xs  lSup A"
proof(coinduction arbitrary: xs A)
  case (lprefix xs A)
  note chain = ‹Complete_Partial_Order.chain (⊑) A
  from xs  A show ?case
    by(auto 4 3 dest: chainD[OF chain] lprefix_lhdD intro: chain_lprefix_ltl[OF chain] intro!: the_equality[symmetric])
qed

lemma chain_lSup_lprefix:
  " Complete_Partial_Order.chain (⊑) A; xs. xs  A  xs  zs 
   lSup A  zs"
proof(coinduction arbitrary: A zs)
  case (lprefix A zs)
  note chain = ‹Complete_Partial_Order.chain (⊑) A
  from xs. xs  A  xs  zs
  show ?case
    by(auto 4 4 dest: lprefix_lnullD lprefix_lhdD intro: chain_lprefix_ltl[OF chain] lprefix_ltlI rev_image_eqI intro!: the_equality)
qed

lemma llist_ccpo [simp, cont_intro]: "class.ccpo lSup (⊑) (mk_less (⊑))"
by(unfold_locales)(auto dest: lprefix_antisym intro: lprefix_trans chain_lprefix_lSup chain_lSup_lprefix simp add: mk_less_def)

lemmas [cont_intro] = ccpo.admissible_leI[OF llist_ccpo]

lemma llist_partial_function_definitions:
  "partial_function_definitions (⊑) lSup"
by(unfold_locales)(auto dest: lprefix_antisym intro: lprefix_trans chain_lprefix_lSup chain_lSup_lprefix)

interpretation llist: partial_function_definitions "(⊑)" lSup
  rewrites "lSup {}  LNil"
by(rule llist_partial_function_definitions)(simp)

abbreviation "mono_llist  monotone (fun_ord (⊑)) (⊑)"

interpretation llist_lift: partial_function_definitions "fun_ord lprefix" "fun_lub lSup"
  rewrites "fun_lub lSup {}  λ_. LNil"
by(rule llist_partial_function_definitions[THEN partial_function_lift])(simp)

abbreviation "mono_llist_lift  monotone (fun_ord (fun_ord lprefix)) (fun_ord lprefix)"

lemma lprefixes_chain:
  "Complete_Partial_Order.chain (⊑) {ys. lprefix ys xs}"
by(rule chainI)(auto dest: lprefix_down_linear)

lemma llist_gen_induct:
  assumes adm: "ccpo.admissible lSup (⊑) P"
  and step: "zs. zs  xs  lfinite zs  (ys. zs  ys  ys  xs  lfinite ys  P ys)"
  shows "P xs"
proof -
  from step obtain zs
    where zs: "zs  xs" "lfinite zs"
    and ys: "ys.  zs  ys; ys  xs; lfinite ys   P ys" by blast
  let ?C = "{ys. ys  xs  zs  ys  lfinite ys}"
  from lprefixes_chain[of xs]
  have "Complete_Partial_Order.chain (⊑) ?C"
    by(auto dest: chain_compr)
  with adm have "P (lSup ?C)"
    by(rule ccpo.admissibleD)(auto intro: ys zs)
  also have "lSup ?C  = xs"
    using lSup_finite_gen_prefixes[OF zs] by simp
  finally show ?thesis .
qed

lemma llist_induct [case_names adm LNil LCons, induct type: llist]:
  assumes adm: "ccpo.admissible lSup (⊑) P"
  and LNil: "P LNil"
  and LCons: "x xs.  lfinite xs; P xs   P (LCons x xs)"
  shows "P xs"
proof -
  { fix ys :: "'a llist"
    assume "lfinite ys"
    hence "P ys" by(induct)(simp_all add: LNil LCons) }
  note [intro] = this
  show ?thesis using adm
    by(rule llist_gen_induct)(auto intro: exI[where x=LNil])
qed

lemma LCons_mono [partial_function_mono, cont_intro]:
  "mono_llist A  mono_llist (λf. LCons x (A f))"
by(rule monotoneI)(auto dest: monotoneD)

lemma mono2mono_LCons [THEN llist.mono2mono, simp, cont_intro]:
  shows monotone_LCons: "monotone (⊑) (⊑) (LCons x)"
by(auto intro: monotoneI)

lemma mcont2mcont_LCons [THEN llist.mcont2mcont, simp, cont_intro]:
  shows mcont_LCons: "mcont lSup (⊑) lSup (⊑) (LCons x)"
by(simp add: mcont_def monotone_LCons lSup_LCons[symmetric] contI)

lemma mono2mono_ltl[THEN llist.mono2mono, simp, cont_intro]:
  shows monotone_ltl: "monotone (⊑) (⊑) ltl"
by(auto intro: monotoneI lprefix_ltlI)

lemma cont_ltl: "cont lSup (⊑) lSup (⊑) ltl"
proof(rule contI)
  fix Y :: "'a llist set"
  assume "Y  {}"
  have "ltl (lSup Y) = lSup (insert LNil (ltl ` (Y  {xs. ¬ lnull xs})))"
    by(simp add: lSup_insert_LNil)
  also have "insert LNil (ltl ` (Y  {xs. ¬ lnull xs})) = insert LNil (ltl ` Y)" by auto
  also have "lSup  = lSup (ltl ` Y)" by(simp add: lSup_insert_LNil)
  finally show "ltl (lSup Y) = lSup (ltl ` Y)" .
qed

lemma mcont2mcont_ltl [THEN llist.mcont2mcont, simp, cont_intro]:
  shows mcont_ltl: "mcont lSup (⊑) lSup (⊑) ltl"
by(simp add: mcont_def monotone_ltl cont_ltl)

lemma llist_case_mono [partial_function_mono, cont_intro]:
  assumes lnil: "monotone orda ordb lnil"
  and lcons: "x xs. monotone orda ordb (λf. lcons f x xs)"
  shows "monotone orda ordb (λf. case_llist (lnil f) (lcons f) x)"
by(rule monotoneI)(auto split: llist.split dest: monotoneD[OF lnil] monotoneD[OF lcons])

lemma mcont_llist_case [cont_intro, simp]:
  " mcont luba orda lubb ordb (λx. f x); x xs. mcont luba orda lubb ordb (λy. g x xs y) 
   mcont luba orda lubb ordb (λy. case xs of LNil  f y | LCons x xs'  g x xs' y)"
by(cases xs) simp_all

lemma monotone_lprefix_case [cont_intro, simp]:
  assumes mono: "x. monotone (⊑) (⊑) (λxs. f x xs (LCons x xs))"
  shows "monotone (⊑) (⊑) (λxs. case xs of LNil  LNil | LCons x xs'  f x xs' xs)"
by(rule llist.monotone_if_bot[where f="λxs. f (lhd xs) (ltl xs) xs" and bound=LNil])(auto 4 3 split: llist.split simp add: not_lnull_conv LCons_lprefix_conv dest: monotoneD[OF mono])

lemma mcont_lprefix_case_aux:
  fixes f bot
  defines "g  λxs. f (lhd xs) (ltl xs) (LCons (lhd xs) (ltl xs))"
  assumes mcont: "x. mcont lSup (⊑) lub ord (λxs. f x xs (LCons x xs))"
  and ccpo: "class.ccpo lub ord (mk_less ord)"
  and bot: "x. ord bot x"
  shows "mcont lSup (⊑) lub ord (λxs. case xs of LNil  bot | LCons x xs'  f x xs' xs)"
proof(rule llist.mcont_if_bot[where f=g and bound=LNil and bot=bot, OF ccpo bot])
  fix Y :: "'a llist set"
  assume chain: "Complete_Partial_Order.chain (⊑) Y"
    and Y: "Y  {}" "x. x  Y  ¬ x  LNil"
  from Y have Y': "Y  {xs. ¬ lnull xs}  {}" by auto
  from Y obtain x xs where "LCons x xs  Y" by(fastforce simp add: not_lnull_conv)
  with Y(2) have eq: "Y = LCons x ` (ltl ` (Y  {xs. ¬ lnull xs}))"
    by(force dest: chainD[OF chain] simp add: LCons_lprefix_conv lprefix_LCons_conv intro: imageI rev_image_eqI)
  show "g (lSup Y) = lub (g ` Y)"
    by(subst (1 2) eq)(simp add: lSup_LCons Y' g_def mcont_contD[OF mcont] chain chain_lprefix_ltl, simp add: image_image)
qed(auto 4 3 split: llist.split simp add: not_lnull_conv LCons_lprefix_conv g_def intro: mcont_monoD[OF mcont])

lemma mcont_lprefix_case [cont_intro, simp]:
  assumes "x. mcont lSup (⊑) lSup (⊑) (λxs. f x xs (LCons x xs))"
  shows "mcont lSup (⊑) lSup (⊑) (λxs. case xs of LNil  LNil | LCons x xs'  f x xs' xs)"
using assms by(rule mcont_lprefix_case_aux)(simp_all add: llist_ccpo)

lemma monotone_lprefix_case_lfp [cont_intro, simp]:
  fixes f :: "_  _ :: order_bot"
  assumes mono: "x. monotone (⊑) (≤) (λxs. f x xs (LCons x xs))"
  shows "monotone (⊑) (≤) (λxs. case xs of LNil   | LCons x xs  f x xs (LCons x xs))"
by(rule llist.monotone_if_bot[where bound=LNil and bot= and f="λxs. f (lhd xs) (ltl xs) xs"])(auto 4 3 simp add: not_lnull_conv LCons_lprefix_conv dest: monotoneD[OF mono] split: llist.split)

lemma mcont_lprefix_case_lfp [cont_intro, simp]:
  fixes f :: "_ => _ :: complete_lattice"
  assumes "x. mcont lSup (⊑) Sup (≤) (λxs. f x xs (LCons x xs))"
  shows "mcont lSup (⊑) Sup (≤) (λxs. case xs of LNil   | LCons x xs  f x xs (LCons x xs))"
using assms by(rule mcont_lprefix_case_aux)(rule complete_lattice_ccpo', simp)

declaration Partial_Function.init "llist" @{term llist.fixp_fun}
  @{term llist.mono_body} @{thm llist.fixp_rule_uc} @{thm llist.fixp_strong_induct_uc} NONE›

subsection ‹Monotonicity and continuity of already defined functions›

lemma fixes f F
  defines "F  λlmap xs. case xs of LNil  LNil | LCons x xs  LCons (f x) (lmap xs)"
  shows lmap_conv_fixp: "lmap f  ccpo.fixp (fun_lub lSup) (fun_ord (⊑)) F" (is "?lhs  ?rhs")
  and lmap_mono: "xs. mono_llist (λlmap. F lmap xs)" (is "PROP ?mono")
proof(intro eq_reflection ext)
  show mono: "PROP ?mono" unfolding F_def by(tactic Partial_Function.mono_tac @{context} 1)
  fix xs
  show "?lhs xs = ?rhs xs"
  proof(coinduction arbitrary: xs)
    case Eq_llist
    show ?case by(subst (1 3 4) llist.mono_body_fixp[OF mono])(auto simp add: F_def split: llist.split)
  qed
qed

lemma mono2mono_lmap[THEN llist.mono2mono, simp, cont_intro]:
  shows monotone_lmap: "monotone (⊑) (⊑) (lmap f)"
by(rule llist.fixp_preserves_mono1[OF lmap_mono lmap_conv_fixp]) simp

lemma mcont2mcont_lmap[THEN llist.mcont2mcont, simp, cont_intro]:
  shows mcont_lmap: "mcont lSup (⊑) lSup (⊑) (lmap f)"
by(rule llist.fixp_preserves_mcont1[OF lmap_mono lmap_conv_fixp]) simp

lemma [partial_function_mono]: "mono_llist F  mono_llist (λf. lmap g (F f))"
by(rule mono2mono_lmap)


lemma mono_llist_lappend2 [partial_function_mono]:
  "mono_llist A  mono_llist (λf. lappend xs (A f))"
by(auto intro!: monotoneI lprefix_lappend_sameI simp add: fun_ord_def dest: monotoneD)

lemma mono2mono_lappend2 [THEN llist.mono2mono, cont_intro, simp]:
  shows monotone_lappend2: "monotone (⊑) (⊑) (lappend xs)"
by(rule monotoneI)(rule lprefix_lappend_sameI)

lemma mcont2mcont_lappend2 [THEN llist.mcont2mcont, cont_intro, simp]:
  shows mcont_lappend2: "mcont lSup (⊑) lSup (⊑) (lappend xs)"
proof(cases "lfinite xs")
  case True
  thus ?thesis by induct(simp_all add: monotone_lappend2)
next
  case False
  hence "lappend xs = (λ_. xs)" by(simp add: fun_eq_iff lappend_inf)
  thus ?thesis by(simp add: ccpo.cont_const[OF llist_ccpo])
qed

lemma fixes f F
  defines "F  λlset xs. case xs of LNil  {} | LCons x xs  insert x (lset xs)"
  shows lset_conv_fixp: "lset  ccpo.fixp (fun_lub Union) (fun_ord (⊆)) F" (is "_  ?fixp")
  and lset_mono: "x. monotone (fun_ord (⊆)) (⊆) (λf. F f x)" (is "PROP ?mono")
proof(rule eq_reflection ext antisym subsetI)+
  show mono: "PROP ?mono" unfolding F_def by(tactic Partial_Function.mono_tac @{context} 1)
  fix x xs
  show "?fixp xs  lset xs"
    by(induct arbitrary: xs rule: lfp.fixp_induct_uc[of "λx. x" F "λx. x", OF mono reflexive refl])(auto simp add: F_def split: llist.split)

  assume "x  lset xs"
  thus "x  ?fixp xs" by induct(subst lfp.mono_body_fixp[OF mono], simp add: F_def)+
qed

lemma mono2mono_lset [THEN lfp.mono2mono, cont_intro, simp]:
  shows monotone_lset: "monotone (⊑) (⊆) lset"
by(rule lfp.fixp_preserves_mono1[OF lset_mono lset_conv_fixp]) simp

lemma mcont2mcont_lset[THEN mcont2mcont, cont_intro, simp]:
  shows mcont_lset: "mcont lSup (⊑) Union (⊆) lset"
by(rule lfp.fixp_preserves_mcont1[OF lset_mono lset_conv_fixp]) simp

lemma lset_lSup: "Complete_Partial_Order.chain (⊑) Y  lset (lSup Y) = (lset ` Y)"
by(cases "Y = {}")(simp_all add: mcont_lset[THEN mcont_contD])

lemma lfinite_lSupD: "lfinite (lSup A)  xs  A. lfinite xs"
by(induct ys"lSup A" arbitrary: A rule: lfinite_induct) fastforce+

lemma monotone_enat_le_lprefix_case [cont_intro, simp]:
  "monotone (≤) (⊑) (λx. f x (eSuc x))  monotone (≤) (⊑) (λx. case x of 0  LNil | eSuc x'  f x' x)"
by(erule monotone_enat_le_case) simp_all

lemma mcont_enat_le_lprefix_case [cont_intro, simp]:
  assumes "mcont Sup (≤) lSup (⊑) (λx. f x (eSuc x))"
  shows "mcont Sup (≤) lSup (⊑) (λx. case x of 0  LNil | eSuc x'  f x' x)"
using llist_ccpo assms by(rule mcont_enat_le_case) simp

lemma compact_LConsI:
  assumes "ccpo.compact lSup (⊑) xs"
  shows "ccpo.compact lSup (⊑) (LCons x xs)"
using llist_ccpo
proof(rule ccpo.compactI)
  from assms have "ccpo.admissible lSup (⊑) (λys. ¬ xs  ys)" by cases
  hence [cont_intro]: "ccpo.admissible lSup (⊑) (λys. ¬ xs  ltl ys)"
    using mcont_ltl by(rule admissible_subst)
  have [cont_intro]: "ccpo.admissible lSup (⊑) (λys. ¬ lnull ys  lhd ys  x)"
  proof(rule ccpo.admissibleI)
    fix Y
    assume chain: "Complete_Partial_Order.chain (⊑) Y"
      and *: "Y  {}" "ysY. ¬ lnull ys  lhd ys  x"
    from * show "¬ lnull (lSup Y)  lhd (lSup Y)  x"
      by(subst lhd_lSup)(auto 4 4 dest: chainD[OF chain] intro!: the_equality[symmetric] dest: lprefix_lhdD)
  qed

  have eq: "(λys. ¬ LCons x xs  ys) = (λys. ¬ xs  ltl ys  ys = LNil  ¬ lnull ys  lhd ys  x)"
    by(auto simp add: fun_eq_iff LCons_lprefix_conv neq_LNil_conv)
  show "ccpo.admissible lSup (⊑) (λys. ¬ LCons x xs  ys)"
    by(simp add: eq)
qed

lemma compact_LConsD:
  assumes "ccpo.compact lSup (⊑) (LCons x xs)"
  shows "ccpo.compact lSup (⊑) xs"
using llist_ccpo
proof(rule ccpo.compactI)
  from assms have "ccpo.admissible lSup (⊑) (λys. ¬ LCons x xs  ys)" by cases
  hence "ccpo.admissible lSup (⊑) (λys. ¬ LCons x xs  LCons x ys)"
    by(rule admissible_subst)(rule mcont_LCons)
  thus "ccpo.admissible lSup (⊑) (λys. ¬ xs  ys)" by simp
qed

lemma compact_LCons_iff [simp]:
  "ccpo.compact lSup (⊑) (LCons x xs)  ccpo.compact lSup (⊑) xs"
by(blast intro: compact_LConsI compact_LConsD)

lemma compact_lfiniteI:
  "lfinite xs  ccpo.compact lSup (⊑) xs"
by(induction rule: lfinite.induct) simp_all

lemma compact_lfiniteD:
  assumes "ccpo.compact lSup (⊑) xs"
  shows "lfinite xs"
proof(rule ccontr)
  assume inf: "¬ lfinite xs"

  from assms have "ccpo.admissible lSup (⊑) (λys. ¬ xs  ys)" by cases
  moreover let ?C = "{ys. ys  xs  ys  xs}"
  have "Complete_Partial_Order.chain (⊑) ?C"
    using lprefixes_chain[of xs] by(auto dest: chain_compr)
  moreover have "?C  {}" using inf by(cases xs) auto
  ultimately have "¬ xs  lSup ?C"
    by(rule ccpo.admissibleD)(auto dest: lprefix_antisym)
  also have "lSup ?C = xs" using inf by(rule lSup_strict_prefixes)
  finally show False by simp
qed

lemma compact_eq_lfinite [simp]: "ccpo.compact lSup (⊑) = lfinite"
by(blast intro: compact_lfiniteI compact_lfiniteD)

subsection ‹More function definitions›

primcorec iterates :: "('a  'a)  'a  'a llist"
where "iterates f x = LCons x (iterates f (f x))"

primrec llist_of :: "'a list  'a llist"
where
  "llist_of [] = LNil"
| "llist_of (x#xs) = LCons x (llist_of xs)"

definition list_of :: "'a llist  'a list"
where [code del]: "list_of xs = (if lfinite xs then inv llist_of xs else undefined)"

definition llength :: "'a llist  enat"
where [code del]:
  "llength = enat_unfold lnull ltl"

primcorec ltake :: "enat  'a llist  'a llist"
where
  "n = 0  lnull xs  lnull (ltake n xs)"
| "lhd (ltake n xs) = lhd xs"
| "ltl (ltake n xs) = ltake (epred n) (ltl xs)"

definition ldropn :: "nat  'a llist  'a llist"
where "ldropn n xs = (ltl ^^ n) xs"

context notes [[function_internals]]
begin

partial_function (llist) ldrop :: "enat  'a llist  'a llist"
where
  "ldrop n xs = (case n of 0  xs | eSuc n'  case xs of LNil  LNil | LCons x xs'  ldrop n' xs')"

end

primcorec ltakeWhile :: "('a  bool)  'a llist  'a llist"
where
  "lnull xs  ¬ P (lhd xs)  lnull (ltakeWhile P xs)"
| "lhd (ltakeWhile P xs) = lhd xs"
| "ltl (ltakeWhile P xs) = ltakeWhile P (ltl xs)"

context fixes P :: "'a  bool"
  notes [[function_internals]]
begin

partial_function (llist) ldropWhile :: "'a llist  'a llist"
where "ldropWhile xs = (case xs of LNil  LNil | LCons x xs'  if P x then ldropWhile xs' else xs)"

partial_function (llist) lfilter :: "'a llist  'a llist"
where "lfilter xs = (case xs of LNil  LNil | LCons x xs'  if P x then LCons x (lfilter xs') else lfilter xs')"

end

primrec lnth :: "'a llist  nat  'a"
where
  "lnth xs 0 = (case xs of LNil  undefined (0 :: nat) | LCons x xs'  x)"
| "lnth xs (Suc n) = (case xs of LNil  undefined (Suc n) | LCons x xs'  lnth xs' n)"

declare lnth.simps [simp del]

primcorec lzip :: "'a llist  'b llist  ('a × 'b) llist"
where
  "lnull xs  lnull ys  lnull (lzip xs ys)"
| "lhd (lzip xs ys) = (lhd xs, lhd ys)"
| "ltl (lzip xs ys) = lzip (ltl xs) (ltl ys)"

definition llast :: "'a llist  'a"
where [nitpick_simp]:
  "llast xs = (case llength xs of enat n  (case n of 0  undefined | Suc n'  lnth xs n') |   undefined)"

coinductive ldistinct :: "'a llist  bool"
where
  LNil [simp]: "ldistinct LNil"
| LCons: " x  lset xs; ldistinct xs   ldistinct (LCons x xs)"

hide_fact (open) LNil LCons

definition inf_llist :: "(nat  'a)  'a llist"
where [code del]: "inf_llist f = lmap f (iterates Suc 0)"

abbreviation repeat :: "'a  'a llist"
where "repeat  iterates (λx. x)"

definition lstrict_prefix :: "'a llist  'a llist  bool"
where [code del]: "lstrict_prefix xs ys  xs  ys  xs  ys"

text ‹longest common prefix›
definition llcp :: "'a llist  'a llist  enat"
where [code del]:
  "llcp xs ys =
   enat_unfold (λ(xs, ys). lnull xs  lnull ys  lhd xs  lhd ys) (map_prod ltl ltl) (xs, ys)"

coinductive llexord :: "('a  'a  bool)  'a llist  'a llist  bool"
for r :: "'a  'a  bool"
where
  llexord_LCons_eq: "llexord r xs ys  llexord r (LCons x xs) (LCons x ys)"
| llexord_LCons_less: "r x y  llexord r (LCons x xs) (LCons y ys)"
| llexord_LNil [simp, intro!]: "llexord r LNil ys"

context notes [[function_internals]]
begin

partial_function (llist) lconcat :: "'a llist llist  'a llist"
where "lconcat xss = (case xss of LNil  LNil | LCons xs xss'  lappend xs (lconcat xss'))"

end

definition lhd' :: "'a llist  'a option" where
"lhd' xs = (if lnull xs then None else Some (lhd xs))"

lemma lhd'_simps[simp]:
  "lhd' LNil = None"
  "lhd' (LCons x xs) = Some x"
unfolding lhd'_def by auto

definition ltl' :: "'a llist  'a llist option" where
"ltl' xs = (if lnull xs then None else Some (ltl xs))"

lemma ltl'_simps[simp]:
  "ltl' LNil = None"
  "ltl' (LCons x xs) = Some xs"
unfolding ltl'_def by auto

definition lnths :: "'a llist  nat set  'a llist"
where "lnths xs A = lmap fst (lfilter (λ(x, y). y  A) (lzip xs (iterates Suc 0)))"

definition (in monoid_add) lsum_list :: "'a llist  'a"
where "lsum_list xs = (if lfinite xs then sum_list (list_of xs) else 0)"

subsection ‹Converting ordinary lists to lazy lists: @{term "llist_of"}

lemma lhd_llist_of [simp]: "lhd (llist_of xs) = hd xs"
by(cases xs)(simp_all add: hd_def lhd_def)

lemma ltl_llist_of [simp]: "ltl (llist_of xs) = llist_of (tl xs)"
by(cases xs) simp_all

lemma lfinite_llist_of [simp]: "lfinite (llist_of xs)"
by(induct xs) auto

lemma lfinite_eq_range_llist_of: "lfinite xs  xs  range llist_of"
proof
  assume "lfinite xs"
  thus "xs  range llist_of"
    by(induct rule: lfinite.induct)(auto intro: llist_of.simps[symmetric])
next
  assume "xs  range llist_of"
  thus "lfinite xs" by(auto intro: lfinite_llist_of)
qed

lemma lnull_llist_of [simp]: "lnull (llist_of xs)  xs = []"
by(cases xs) simp_all

lemma llist_of_eq_LNil_conv:
  "llist_of xs = LNil  xs = []"
by(cases xs) simp_all

lemma llist_of_eq_LCons_conv:
  "llist_of xs = LCons y ys  (xs'. xs = y # xs'  ys = llist_of xs')"
by(cases xs) auto

lemma lappend_llist_of_llist_of:
  "lappend (llist_of xs) (llist_of ys) = llist_of (xs @ ys)"
by(induct xs) simp_all

lemma lfinite_rev_induct [consumes 1, case_names Nil snoc]:
  assumes fin: "lfinite xs"
  and Nil: "P LNil"
  and snoc: "x xs.  lfinite xs; P xs   P (lappend xs (LCons x LNil))"
  shows "P xs"
proof -
  from fin obtain xs' where xs: "xs = llist_of xs'"
    unfolding lfinite_eq_range_llist_of by blast
  show ?thesis unfolding xs
    by(induct xs' rule: rev_induct)(auto simp add: Nil lappend_llist_of_llist_of[symmetric] dest: snoc[rotated])
qed

lemma lappend_llist_of_LCons:
  "lappend (llist_of xs) (LCons y ys) = lappend (llist_of (xs @ [y])) ys"
by(induct xs) simp_all

lemma lmap_llist_of [simp]:
  "lmap f (llist_of xs) = llist_of (map f xs)"
by(induct xs) simp_all

lemma lset_llist_of [simp]: "lset (llist_of xs) = set xs"
by(induct xs) simp_all

lemma llist_of_inject [simp]: "llist_of xs = llist_of ys  xs = ys"
proof
  assume "llist_of xs = llist_of ys"
  thus "xs = ys"
  proof(induct xs arbitrary: ys)
    case Nil thus ?case by(cases ys) auto
  next
    case Cons thus ?case by(cases ys) auto
  qed
qed simp

lemma inj_llist_of [simp]: "inj llist_of"
by(rule inj_onI) simp

subsection ‹Converting finite lazy lists to ordinary lists: @{term "list_of"}

lemma list_of_llist_of [simp]: "list_of (llist_of xs) = xs"
by(fastforce simp add: list_of_def intro: inv_f_f inj_onI)

lemma llist_of_list_of [simp]: "lfinite xs  llist_of (list_of xs) = xs"
unfolding lfinite_eq_range_llist_of by auto

lemma list_of_LNil [simp, nitpick_simp]: "list_of LNil = []"
using list_of_llist_of[of "[]"] by simp

lemma list_of_LCons [simp]: "lfinite xs  list_of (LCons x xs) = x # list_of xs"
proof(induct arbitrary: x rule: lfinite.induct)
  case lfinite_LNil
  show ?case using list_of_llist_of[of "[x]"] by simp
next
  case (lfinite_LConsI xs' x')
  from ‹list_of (LCons x' xs') = x' # list_of xs' show ?case
    using list_of_llist_of[of "x # x' # list_of xs'"]
      llist_of_list_of[OF ‹lfinite xs'] by simp
qed

lemma list_of_LCons_conv [nitpick_simp]:
  "list_of (LCons x xs) = (if lfinite xs then x # list_of xs else undefined)"
by(auto)(auto simp add: list_of_def)

lemma list_of_lappend:
  assumes "lfinite xs" "lfinite ys"
  shows "list_of (lappend xs ys) = list_of xs @ list_of ys"
using ‹lfinite xs by induct(simp_all add: ‹lfinite ys)

lemma list_of_lmap [simp]:
  assumes "lfinite xs"
  shows "list_of (lmap f xs) = map f (list_of xs)"
using assms by induct simp_all

lemma set_list_of [simp]:
  assumes "lfinite xs"
  shows "set (list_of xs) = lset xs"
using assms by(induct)(simp_all)

lemma hd_list_of [simp]: "lfinite xs  hd (list_of xs) = lhd xs"
by(clarsimp simp add: lfinite_eq_range_llist_of)

lemma tl_list_of: "lfinite xs  tl (list_of xs) = list_of (ltl xs)"
by(auto simp add: lfinite_eq_range_llist_of)

text ‹Efficient implementation via tail recursion suggested by Brian Huffman›

definition list_of_aux :: "'a list  'a llist  'a list"
where "list_of_aux xs ys = (if lfinite ys then rev xs @ list_of ys else undefined)"

lemma list_of_code [code]: "list_of = list_of_aux []"
by(simp add: fun_eq_iff list_of_def list_of_aux_def)

lemma list_of_aux_code [code]:
  "list_of_aux xs LNil = rev xs"
  "list_of_aux xs (LCons y ys) = list_of_aux (y # xs) ys"
by(simp_all add: list_of_aux_def)

subsection ‹The length of a lazy list: @{term "llength"}

lemma [simp, nitpick_simp]:
  shows llength_LNil: "llength LNil = 0"
  and llength_LCons: "llength (LCons x xs) = eSuc (llength xs)"
by(simp_all add: llength_def enat_unfold)

lemma llength_eq_0 [simp]: "llength xs = 0  lnull xs"
by(cases xs) simp_all

lemma llength_lnull [simp]: "lnull xs  llength xs = 0"
by simp

lemma epred_llength:
  "epred (llength xs) = llength (ltl xs)"
by(cases xs) simp_all

lemmas llength_ltl = epred_llength[symmetric]

lemma llength_lmap [simp]: "llength (lmap f xs) = llength xs"
by(coinduction arbitrary: xs rule: enat_coinduct)(auto simp add: epred_llength)

lemma llength_lappend [simp]: "llength (lappend xs ys) = llength xs + llength ys"
by(coinduction arbitrary: xs ys rule: enat_coinduct)(simp_all add: iadd_is_0 epred_iadd1 split_paired_all epred_llength, auto)

lemma llength_llist_of [simp]:
  "llength (llist_of xs) = enat (length xs)"
by(induct xs)(simp_all add: zero_enat_def eSuc_def)

lemma length_list_of:
  "lfinite xs  enat (length (list_of xs)) = llength xs"
apply(rule sym)
by(induct rule: lfinite.induct)(auto simp add: eSuc_enat zero_enat_def)

lemma length_list_of_conv_the_enat:
  "lfinite xs  length (list_of xs) = the_enat (llength xs)"
unfolding lfinite_eq_range_llist_of by auto

lemma llength_eq_enat_lfiniteD: "llength xs = enat n  lfinite xs"
proof(induct n arbitrary: xs)
  case [folded zero_enat_def]: 0
  thus ?case by simp
next
  case (Suc n)
  note len = ‹llength xs = enat (Suc n)
  then obtain x xs' where "xs = LCons x xs'"
    by(cases xs)(auto simp add: zero_enat_def)
  moreover with len have "llength xs' = enat n"
    by(simp add: eSuc_def split: enat.split_asm)
  hence "lfinite xs'" by(rule Suc)
  ultimately show ?case by simp
qed

lemma lfinite_llength_enat:
  assumes "lfinite xs"
  shows "n. llength xs = enat n"
using assms
by induct(auto simp add: eSuc_def zero_enat_def)

lemma lfinite_conv_llength_enat:
  "lfinite xs  (n. llength xs = enat n)"
by(blast dest: llength_eq_enat_lfiniteD lfinite_llength_enat)

lemma not_lfinite_llength:
  "¬ lfinite xs  llength xs = "
by(simp add: lfinite_conv_llength_enat)

lemma llength_eq_infty_conv_lfinite:
  "llength xs =   ¬ lfinite xs"
by(simp add: lfinite_conv_llength_enat)

lemma lfinite_finite_index: "lfinite xs  finite {n. enat n < llength xs}"
by(auto dest: lfinite_llength_enat)

text ‹tail-recursive implementation for @{term llength}

definition gen_llength :: "nat  'a llist  enat"
where "gen_llength n xs = enat n + llength xs"

lemma gen_llength_code [code]:
  "gen_llength n LNil = enat n"
  "gen_llength n (LCons x xs) = gen_llength (n + 1) xs"
by(simp_all add: gen_llength_def iadd_Suc eSuc_enat[symmetric] iadd_Suc_right)

lemma llength_code [code]: "llength = gen_llength 0"
by(simp add: gen_llength_def fun_eq_iff zero_enat_def)

lemma fixes F
  defines "F  λllength xs. case xs of LNil  0 | LCons x xs  eSuc (llength xs)"
  shows llength_conv_fixp: "llength  ccpo.fixp (fun_lub Sup) (fun_ord (≤)) F" (is "_  ?fixp")
  and llength_mono: "xs. monotone (fun_ord (≤)) (≤) (λllength. F llength xs)" (is "PROP ?mono")
proof(intro eq_reflection ext)
  show mono: "PROP ?mono" unfolding F_def by(tactic Partial_Function.mono_tac @{context} 1)
  fix xs
  show "llength xs = ?fixp xs"
    by(coinduction arbitrary: xs rule: enat_coinduct)(subst (1 2 3) lfp.mono_body_fixp[OF mono], fastforce simp add: F_def split: llist.split del: iffI)+
qed

lemma mono2mono_llength[THEN lfp.mono2mono, simp, cont_intro]:
  shows monotone_llength: "monotone (⊑) (≤) llength"
by(rule lfp.fixp_preserves_mono1[OF llength_mono llength_conv_fixp])(fold bot_enat_def, simp)

lemma mcont2mcont_llength[THEN lfp.mcont2mcont, simp, cont_intro]:
  shows mcont_llength: "mcont lSup (⊑) Sup (≤) llength"
by(rule lfp.fixp_preserves_mcont1[OF llength_mono llength_conv_fixp])(fold bot_enat_def, simp)

subsection ‹Taking and dropping from lazy lists: @{term "ltake"}, @{term "ldropn"}, and @{term "ldrop"}

lemma ltake_LNil [simp, code, nitpick_simp]: "ltake n LNil = LNil"
by simp

lemma ltake_0 [simp]: "ltake 0 xs = LNil"
by(simp add: ltake_def)

lemma ltake_eSuc_LCons [simp]:
  "ltake (eSuc n) (LCons x xs) = LCons x (ltake n xs)"
by(rule llist.expand)(simp_all)

lemma ltake_eSuc:
  "ltake (eSuc n) xs =
  (case xs of LNil  LNil | LCons x xs'  LCons x (ltake n xs'))"
by(cases xs) simp_all

lemma lnull_ltake [simp]: "lnull (ltake n xs)  lnull xs  n = 0"
by(cases n xs rule: enat_coexhaust[case_product llist.exhaust]) simp_all

lemma ltake_eq_LNil_iff: "ltake n xs = LNil  xs = LNil  n = 0"
by(cases n xs rule: enat_coexhaust[case_product llist.exhaust]) simp_all

lemma LNil_eq_ltake_iff [simp]: "LNil = ltake n xs  xs = LNil  n = 0"
by(cases n xs rule: enat_coexhaust[case_product llist.exhaust]) simp_all

lemma ltake_LCons [code, nitpick_simp]:
  "ltake n (LCons x xs) =
  (case n of 0  LNil | eSuc n'  LCons x (ltake n' xs))"
by(rule llist.expand)(simp_all split: co.enat.split)

lemma lhd_ltake [simp]: "n  0  lhd (ltake n xs) = lhd xs"
by(cases n xs rule: enat_coexhaust[case_product llist.exhaust]) simp_all

lemma ltl_ltake: "ltl (ltake n xs) = ltake (epred n) (ltl xs)"
by(cases n xs rule: enat_coexhaust[case_product llist.exhaust]) simp_all

lemmas ltake_epred_ltl = ltl_ltake [symmetric]

declare ltake.sel(2) [simp del]

lemma ltake_ltl: "ltake n (ltl xs) = ltl (ltake (eSuc n) xs)"
by(cases xs) simp_all

lemma llength_ltake [simp]: "llength (ltake n xs) = min n (llength xs)"
by(coinduction arbitrary: n xs rule: enat_coinduct)(auto 4 3 simp add: enat_min_eq_0_iff epred_llength ltl_ltake)

lemma ltake_lmap [simp]: "ltake n (lmap f xs) = lmap f (ltake n xs)"
by(coinduction arbitrary: n xs)(auto 4 3 simp add: ltl_ltake)

lemma ltake_ltake [simp]: "ltake n (ltake m xs) = ltake (min n m) xs"
by(coinduction arbitrary: n m xs)(auto 4 4 simp add: enat_min_eq_0_iff ltl_ltake)

lemma lset_ltake: "lset (ltake n xs)  lset xs"
proof(rule subsetI)
  fix x
  assume "x  lset (ltake n xs)"
  thus "x  lset xs"
  proof(induct "ltake n xs" arbitrary: xs n rule: lset_induct)
    case find thus ?case
      by(cases xs)(simp, cases n rule: enat_coexhaust, simp_all)
  next
    case step thus ?case
      by(cases xs)(simp, cases n rule: enat_coexhaust, simp_all)
  qed
qed

lemma ltake_all: "llength xs  m  ltake m xs = xs"
by(coinduction arbitrary: m xs)(auto simp add: epred_llength[symmetric] ltl_ltake intro: epred_le_epredI)

lemma ltake_llist_of [simp]:
  "ltake (enat n) (llist_of xs) = llist_of (take n xs)"
proof(induct n arbitrary: xs)
  case 0
  thus ?case unfolding zero_enat_def[symmetric]
    by(cases xs) simp_all
next
  case (Suc n)
  thus ?case unfolding eSuc_enat[symmetric]
    by(cases xs) simp_all
qed

lemma lfinite_ltake [simp]:
  "lfinite (ltake n xs)  lfinite xs  n < "
  (is "?lhs  ?rhs")
proof
  assume ?lhs
  thus ?rhs
    by(induct ys"ltake n xs" arbitrary: n xs rule: lfinite_induct)(fastforce simp add: zero_enat_def ltl_ltake)+
next
  assume ?rhs (is "?xs  ?n")
  thus ?lhs
  proof
    assume ?xs thus ?thesis
      by(induct xs arbitrary: n)(simp_all add: ltake_LCons split: enat_cosplit)
  next
    assume ?n
    then obtain n' where "n = enat n'" by auto
    moreover have "lfinite (ltake (enat n') xs)"
      by(induct n' arbitrary: xs)
        (auto simp add: zero_enat_def[symmetric] eSuc_enat[symmetric] ltake_eSuc
              split: llist.split)
    ultimately show ?thesis by simp
  qed
qed

lemma ltake_lappend1:  "n  llength xs  ltake n (lappend xs ys) = ltake n xs"
by(coinduction arbitrary: n xs)(auto intro!: exI simp add: llength_ltl epred_le_epredI ltl_ltake)

lemma ltake_lappend2:
  "llength xs  n  ltake n (lappend xs ys) = lappend xs (ltake (n - llength xs) ys)"
by(coinduction arbitrary: n xs rule: llist.coinduct_strong)(auto intro!: exI simp add: llength_ltl epred_le_epredI ltl_ltake)

lemma ltake_lappend:
  "ltake n (lappend xs ys) = lappend (ltake n xs) (ltake (n - llength xs) ys)"
by(coinduction arbitrary: n xs ys rule: llist.coinduct_strong)(auto intro!: exI simp add: llength_ltl ltl_ltake)

lemma take_list_of:
  assumes "lfinite xs"
  shows "take n (list_of xs) = list_of (ltake (enat n) xs)"
using assms
by(induct arbitrary: n)
  (simp_all add: take_Cons zero_enat_def[symmetric] eSuc_enat[symmetric] split: nat.split)

lemma ltake_eq_ltake_antimono:
  " ltake n xs = ltake n ys; m  n   ltake m xs = ltake m ys"
by (metis ltake_ltake min_def)

lemma ltake_is_lprefix [simp, intro]: "ltake n xs  xs"
by(coinduction arbitrary: xs n)(auto simp add: ltl_ltake)

lemma lprefix_ltake_same [simp]:
  "ltake n xs  ltake m xs  n  m  llength xs  m"
  (is "?lhs  ?rhs")
proof(rule iffI disjCI)+
  assume ?lhs "¬ llength xs  m"
  thus "n  m"
  proof(coinduction arbitrary: n m xs rule: enat_le_coinduct)
    case (le n m xs)
    thus ?case by(cases xs)(auto 4 3 simp add: ltake_LCons split: co.enat.splits)
  qed
next
  assume ?rhs
  thus ?lhs
  proof
    assume "n  m"
    thus ?thesis
      by(coinduction arbitrary: n m xs)(auto 4 4 simp add: ltl_ltake epred_le_epredI)
  qed(simp add: ltake_all)
qed

lemma fixes f F
  defines "F  λltake n xs. case xs of LNil  LNil | LCons x xs  case n of 0  LNil | eSuc n  LCons x (ltake n xs)"
  shows ltake_conv_fixp: "ltake  curry (ccpo.fixp (fun_lub lSup) (fun_ord (⊑)) (λltake. case_prod (F (curry ltake))))" (is "?lhs  ?rhs")
  and ltake_mono: "nxs. mono_llist (λltake. case nxs of (n, xs)  F (curry ltake) n xs)" (is "PROP ?mono")
proof(intro eq_reflection ext)
  show mono: "PROP ?mono" unfolding F_def by(tactic Partial_Function.mono_tac @{context} 1)
  fix n xs
  show "?lhs n xs = ?rhs n xs"
  proof(coinduction arbitrary: n xs)
    case Eq_llist
    show ?case by(subst (1 3 4) llist.mono_body_fixp[OF mono])(auto simp add: F_def split: llist.split prod.split co.enat.split)
  qed
qed

lemma monotone_ltake: "monotone (rel_prod (≤) (⊑)) (⊑) (case_prod ltake)"
by(rule llist.fixp_preserves_mono2[OF ltake_mono ltake_conv_fixp]) simp

lemma mono2mono_ltake1[THEN llist.mono2mono, cont_intro, simp]:
  shows monotone_ltake1: "monotone (≤) (⊑) (λn. ltake n xs)"
using monotone_ltake by auto

lemma mono2mono_ltake2[THEN llist.mono2mono, cont_intro, simp]:
  shows monotone_ltake2: "monotone (⊑) (⊑) (ltake n)"
using monotone_ltake by auto

lemma mcont_ltake: "mcont (prod_lub Sup lSup) (rel_prod (≤) (⊑)) lSup (⊑) (case_prod ltake)"
by(rule llist.fixp_preserves_mcont2[OF ltake_mono ltake_conv_fixp]) simp

lemma mcont2mcont_ltake1 [THEN llist.mcont2mcont, cont_intro, simp]:
  shows mcont_ltake1: "mcont Sup (≤) lSup (⊑) (λn. ltake n xs)"
using mcont_ltake by auto

lemma mcont2mcont_ltake2 [THEN llist.mcont2mcont, cont_intro, simp]:
  shows mcont_ltake2: "mcont lSup (⊑) lSup (⊑) (ltake n)"
using mcont_ltake by auto

lemma [partial_function_mono]: "mono_llist F  mono_llist (λf. ltake n (F f))"
by(rule mono2mono_ltake2)

lemma llist_induct2:
  assumes adm: "ccpo.admissible (prod_lub lSup lSup) (rel_prod (⊑) (⊑)) (λx. P (fst x) (snd x))"
  and LNil: "P LNil LNil"
  and LCons1: "x xs.  lfinite xs; P xs LNil   P (LCons x xs) LNil"
  and LCons2: "y ys.  lfinite ys; P LNil ys   P LNil (LCons y ys)"
  and LCons: "x xs y ys.  lfinite xs; lfinite ys; P xs ys   P (LCons x xs) (LCons y ys)"
  shows "P xs ys"
proof -
  let ?C = "(λn. (ltake n xs, ltake n ys)) ` range enat"
  have "Complete_Partial_Order.chain (rel_prod (⊑) (⊑)) ?C"
    by(rule chainI) auto
  with adm have "P (fst (prod_lub lSup lSup ?C)) (snd (prod_lub lSup lSup ?C))"
  proof(rule ccpo.admissibleD)
    fix xsys
    assume "xsys  ?C"
    then obtain n where "xsys = (ltake (enat n) xs, ltake (enat n) ys)" by auto
    moreover {
      fix xs :: "'a llist"
      assume "lfinite xs"
      hence "P xs LNil" by induct(auto intro: LNil LCons1) }
    note 1 = this
    { fix ys :: "'b llist"
      assume "lfinite ys"
      hence "P LNil ys" by induct(auto intro: LNil LCons2) }
    note 2 = this
    have "P (ltake (enat n) xs) (ltake (enat n) ys)"
      by(induct n arbitrary: xs ys)(auto simp add: zero_enat_def[symmetric] LNil eSuc_enat[symmetric] ltake_eSuc split: llist.split intro: LNil LCons 1 2)
    ultimately show "P (fst xsys) (snd xsys)" by simp
  qed simp
  also have "fst (prod_lub lSup lSup ?C) = xs"
    unfolding prod_lub_def fst_conv
    by(subst image_image)(simp add: mcont_contD[OF mcont_ltake1, symmetric] ltake_all)
  also have "snd (prod_lub lSup lSup ?C) = ys"
    unfolding prod_lub_def snd_conv
    by(subst image_image)(simp add: mcont_contD[OF mcont_ltake1, symmetric] ltake_all)
  finally show ?thesis .
qed

lemma ldropn_0 [simp]: "ldropn 0 xs = xs"
by(simp add: ldropn_def)

lemma ldropn_LNil [code, simp]: "ldropn n LNil = LNil"
by(induct n)(simp_all add: ldropn_def)

lemma ldropn_lnull: "lnull xs  ldropn n xs = LNil"
by(simp add: lnull_def)

lemma ldropn_LCons [code]:
  "ldropn n (LCons x xs) = (case n of 0  LCons x xs | Suc n'  ldropn n' xs)"
by(cases n)(simp_all add: ldropn_def funpow_swap1)

lemma ldropn_Suc: "ldropn (Suc n) xs = (case xs of LNil  LNil | LCons x xs'  ldropn n xs')"
by(simp split: llist.split)(simp add: ldropn_def funpow_swap1)

lemma ldropn_Suc_LCons [simp]: "ldropn (Suc n) (LCons x xs) = ldropn n xs"
by(simp add: ldropn_LCons)

lemma ltl_ldropn: "ltl (ldropn n xs) = ldropn n (ltl xs)"
proof(induct n arbitrary: xs)
  case 0 thus ?case by simp
next
  case (Suc n)
  thus ?case
    by(cases xs)(simp_all add: ldropn_Suc split: llist.split)
qed

lemma ldrop_simps [simp]:
  shows ldrop_LNil: "ldrop n LNil = LNil"
  and ldrop_0: "ldrop 0 xs = xs"
  and ldrop_eSuc_LCons: "ldrop (eSuc n) (LCons x xs) = ldrop n xs"
by(simp_all add: ldrop.simps split: co.enat.split)

lemma ldrop_lnull: "lnull xs  ldrop n xs = LNil"
by(simp add: lnull_def)

lemma fixes f F
  defines "F  λldropn xs. case xs of LNil  λ_. LNil | LCons x xs  λn. if n = 0 then LCons x xs else ldropn xs (n - 1)"
  shows ldrop_conv_fixp: "(λxs n. ldropn n xs)  ccpo.fixp (fun_lub (fun_lub lSup)) (fun_ord (fun_ord lprefix)) (λldrop. F ldrop)" (is "?lhs  ?rhs")
  and ldrop_mono: "xs. mono_llist_lift (λldrop. F ldrop xs)" (is "PROP ?mono")
proof(intro eq_reflection ext)
  show mono: "PROP ?mono" unfolding F_def by(tactic Partial_Function.mono_tac @{context} 1)
  fix n xs
  show "?lhs xs n = ?rhs xs n"
    by(induction n arbitrary: xs)
      (subst llist_lift.mono_body_fixp[OF mono], simp add: F_def split: llist.split)+
qed

lemma ldropn_fixp_case_conv:
  "(λxs. case xs of LNil  λ_. LNil | LCons x xs  λn. if n = 0 then LCons x xs else f xs (n - 1)) =
   (λxs n. case xs of LNil  LNil | LCons x xs  if n = 0 then LCons x xs else f xs (n - 1))"
by(auto simp add: fun_eq_iff split: llist.split)

lemma monotone_ldropn_aux: "monotone lprefix (fun_ord lprefix) (λxs n. ldropn n xs)"
by(rule llist_lift.fixp_preserves_mono1[OF ldrop_mono ldrop_conv_fixp])
  (simp add: ldropn_fixp_case_conv monotone_fun_ord_apply)

lemma mono2mono_ldropn[THEN llist.mono2mono, cont_intro, simp]:
  shows monotone_ldropn': "monotone lprefix lprefix (λxs. ldropn n xs)"
using monotone_ldropn_aux by(auto simp add: monotone_def fun_ord_def)

lemma mcont_ldropn_aux: "mcont lSup lprefix (fun_lub lSup) (fun_ord lprefix) (λxs n. ldropn n xs)"
by(rule llist_lift.fixp_preserves_mcont1[OF ldrop_mono ldrop_conv_fixp])
  (simp add: ldropn_fixp_case_conv mcont_fun_lub_apply)

lemma mcont2mcont_ldropn [THEN llist.mcont2mcont, cont_intro, simp]:
  shows mcont_ldropn: "mcont lSup lprefix lSup lprefix (ldropn n)"
using mcont_ldropn_aux by(auto simp add: mcont_fun_lub_apply)

lemma monotone_enat_cocase [cont_intro, simp]:
  " n. monotone (≤) ord (λn. f n (eSuc n));
    n. ord a (f n (eSuc n)); ord a a 
   monotone (≤) ord (λn. case n of 0  a | eSuc n'  f n' n)"
by(rule monotone_enat_le_case)

lemma monotone_ldrop: "monotone (rel_prod (=) (⊑)) (⊑) (case_prod ldrop)"
by(rule llist.fixp_preserves_mono2[OF ldrop.mono ldrop_def]) simp

lemma mono2mono_ldrop2 [THEN llist.mono2mono, cont_intro, simp]:
  shows monotone_ldrop2: "monotone (⊑) (⊑) (ldrop n)"
by(simp add: monotone_ldrop[simplified])

lemma mcont_ldrop: "mcont (prod_lub the_Sup lSup) (rel_prod (=) (⊑)) lSup (⊑) (case_prod ldrop)"
by(rule llist.fixp_preserves_mcont2[OF ldrop.mono ldrop_def]) simp

lemma mcont2monct_ldrop2 [THEN llist.mcont2mcont, cont_intro, simp]:
  shows mcont_ldrop2: "mcont lSup (⊑) lSup (⊑) (ldrop n)"
by(simp add: mcont_ldrop[simplified])

lemma ldrop_eSuc_conv_ltl: "ldrop (eSuc n) xs = ltl (ldrop n xs)"
proof(induct xs arbitrary: n)
  case LCons thus ?case by(cases n rule: co.enat.exhaust) simp_all
qed simp_all

lemma ldrop_ltl: "ldrop n (ltl xs) = ldrop (eSuc n) xs"
proof(induct xs arbitrary: n)
  case LCons thus ?case by(cases n rule: co.enat.exhaust) simp_all
qed simp_all

lemma lnull_ldropn [simp]: "lnull (ldropn n xs)  llength xs  enat n"
proof(induction n arbitrary: xs)
  case (Suc n)
  from Suc.IH[of "ltl xs"] show ?case
    by(cases xs)(simp_all add: eSuc_enat[symmetric])
qed(simp add: zero_enat_def[symmetric])

lemma ldrop_eq_LNil [simp]: "ldrop n xs = LNil  llength xs  n"
proof(induction xs arbitrary: n)
  case (LCons x xs n)
  thus ?case by(cases n rule: co.enat.exhaust) simp_all
qed simp_all

lemma lnull_ldrop [simp]: "lnull (ldrop n xs)  llength xs  n"
unfolding lnull_def by(fact ldrop_eq_LNil)

lemma ldropn_eq_LNil: "(ldropn n xs = LNil) = (llength xs  enat n)"
using lnull_ldropn unfolding lnull_def .

lemma ldropn_all: "llength xs  enat m  ldropn m xs = LNil"
by(simp add: ldropn_eq_LNil)

lemma ldrop_all: "llength xs  m  ldrop m xs = LNil"
by(simp)

lemma ltl_ldrop: "ltl (ldrop n xs) = ldrop n (ltl xs)"
by(simp add: ldrop_eSuc_conv_ltl ldrop_ltl)

lemma ldrop_eSuc:
  "ldrop (eSuc n) xs = (case xs of LNil  LNil | LCons x xs'  ldrop n xs')"
by(cases xs) simp_all

lemma ldrop_LCons:
  "ldrop n (LCons x xs) = (case n of 0  LCons x xs | eSuc n'  ldrop n' xs)"
by(cases n rule: enat_coexhaust) simp_all

lemma ldrop_inf [code, simp]: "ldrop  xs = LNil"
by(induction xs)(simp_all add: ldrop_LCons enat_cocase_inf)

lemma ldrop_enat [code]: "ldrop (enat n) xs = ldropn n xs"
proof(induct n arbitrary: xs)
  case Suc thus ?case
    by(cases xs)(simp_all add: eSuc_enat[symmetric])
qed(simp add: zero_enat_def[symmetric])

lemma lfinite_ldropn [simp]: "lfinite (ldropn n xs) = lfinite xs"
by(induct n arbitrary: xs)(simp_all add: ldropn_Suc split: llist.split)

lemma lfinite_ldrop [simp]:
  "lfinite (ldrop n xs)  lfinite xs  n = "
by(cases n)(simp_all add: ldrop_enat)

lemma ldropn_ltl: "ldropn n (ltl xs) = ldropn (Suc n) xs"
by(simp add: ldropn_def funpow_swap1)

lemmas ldrop_eSuc_ltl = ldropn_ltl[symmetric]

lemma lset_ldropn_subset: "lset (ldropn n xs)  lset xs"
by(induct n arbitrary: xs)(fastforce simp add: ldropn_Suc split: llist.split_asm)+

lemma in_lset_ldropnD: "x  lset (ldropn n xs)  x  lset xs"
using lset_ldropn_subset[of n xs] by auto

lemma lset_ldrop_subset: "lset (ldrop n xs)  lset xs"
proof(induct xs arbitrary: n)
  case LCons thus ?case
    by(cases n rule: co.enat.exhaust) auto
qed simp_all

lemma in_lset_ldropD: "x  lset (ldrop n xs)  x  lset xs"
using lset_ldrop_subset[of n xs] by(auto)

lemma lappend_ltake_ldrop: "lappend (ltake n xs) (ldrop n xs) = xs"
by(coinduction arbitrary: n xs rule: llist.coinduct_strong)
  (auto simp add: ldrop_ltl ltl_ltake intro!: arg_cong2[where f=lappend])

lemma ldropn_lappend:
  "ldropn n (lappend xs ys) =
  (if enat n < llength xs then lappend (ldropn n xs) ys
   else ldropn (n - the_enat (llength xs)) ys)"
proof(induct n arbitrary: xs)
  case 0
  thus ?case by(simp add: zero_enat_def[symmetric] lappend_lnull1)
next
  case (Suc n)
  { fix zs
    assume "llength zs  enat n"
    hence "the_enat (eSuc (llength zs)) = Suc (the_enat (llength zs))"
      by(auto intro!: the_enat_eSuc iff del: not_infinity_eq) }
  note eq = this
  from Suc show ?case
    by(cases xs)(auto simp add: not_less not_le eSuc_enat[symmetric] eq)
qed

lemma ldropn_lappend2:
  "llength xs  enat n  ldropn n (lappend xs ys) = ldropn (n - the_enat (llength xs)) ys"
by(auto simp add: ldropn_lappend)

lemma lappend_ltake_enat_ldropn [simp]: "lappend (ltake (enat n) xs) (ldropn n xs) = xs"
by(fold ldrop_enat)(rule lappend_ltake_ldrop)

lemma ldrop_lappend:
  "ldrop n (lappend xs ys) =
  (if n < llength xs then lappend (ldrop n xs) ys
   else ldrop (n - llength xs) ys)"
  ― ‹cannot prove this directly using fixpoint induction,
     because @{term "(-) :: enat  enat  enat"} is not a least fixpoint›
by(cases n)(cases "llength xs", simp_all add: ldropn_lappend not_less ldrop_enat)

lemma ltake_plus_conv_lappend:
  "ltake (n + m) xs = lappend (ltake n xs) (ltake m (ldrop n xs))"
by(coinduction arbitrary: n m xs rule: llist.coinduct_strong)(auto intro!: exI simp add: iadd_is_0 ltl_ltake epred_iadd1 ldrop_ltl)

lemma ldropn_eq_LConsD:
  "ldropn n xs = LCons y ys  enat n < llength xs"
proof(induct n arbitrary: xs)
  case 0 thus ?case by(simp add: zero_enat_def[symmetric])
next
  case (Suc n) thus ?case by(cases xs)(simp_all add: Suc_ile_eq)
qed

lemma ldrop_eq_LConsD:
  "ldrop n xs = LCons y ys  n < llength xs"
by(rule ccontr)(simp add: not_less ldrop_all)

lemma ldropn_lmap [simp]: "ldropn n (lmap f xs) = lmap f (ldropn n xs)"
by(induct n arbitrary: xs)(simp_all add: ldropn_Suc split: llist.split)

lemma ldrop_lmap [simp]: "ldrop n (lmap f xs) = lmap f (ldrop n xs)"
proof(induct xs arbitrary: n)
  case LCons thus ?case by(cases n rule: co.enat.exhaust) simp_all
qed simp_all

lemma ldropn_ldropn [simp]:
  "ldropn n (ldropn m xs) = ldropn (n + m) xs"
by(induct m arbitrary: xs)(auto simp add: ldropn_Suc split: llist.split)

lemma ldrop_ldrop [simp]:
  "ldrop n (ldrop m xs) = ldrop (n + m) xs"
proof(induct xs arbitrary: m)
  case LCons thus ?case by(cases m rule: co.enat.exhaust)(simp_all add: iadd_Suc_right)
qed simp_all

lemma llength_ldropn [simp]: "llength (ldropn n xs) = llength xs - enat n"
proof(induct n arbitrary: xs)
  case 0 thus ?case by(simp add: zero_enat_def[symmetric])
next
  case (Suc n) thus ?case by(cases xs)(simp_all add: eSuc_enat[symmetric])
qed

lemma enat_llength_ldropn:
  "enat n  llength xs  enat (n - m)  llength (ldropn m xs)"
by(cases "llength xs") simp_all

lemma ldropn_llist_of [simp]: "ldropn n (llist_of xs) = llist_of (drop n xs)"
proof(induct n arbitrary: xs)
  case Suc thus ?case by(cases xs) simp_all
qed simp

lemma ldrop_llist_of: "ldrop (enat n) (llist_of xs) = llist_of (drop n xs)"
proof(induct xs arbitrary: n)
  case Cons thus ?case by(cases n)(simp_all add: zero_enat_def[symmetric] eSuc_enat[symmetric])
qed simp

lemma drop_list_of:
  "lfinite xs  drop n (list_of xs) = list_of (ldropn n xs)"
by (metis ldropn_llist_of list_of_llist_of llist_of_list_of)

lemma llength_ldrop: "llength (ldrop n xs) = (if n =  then 0 else llength xs - n)"
proof(induct xs arbitrary: n)
  case (LCons x xs)
  thus ?case by simp(cases n rule: co.enat.exhaust, simp_all)
qed simp_all

lemma ltake_ldropn: "ltake n (ldropn m xs) = ldropn m (ltake (n + enat m) xs)"
by(induct m arbitrary: n xs)(auto simp add: zero_enat_def[symmetric] ldropn_Suc eSuc_enat[symmetric] iadd_Suc_right split: llist.split)

lemma ldropn_ltake: "ldropn n (ltake m xs) = ltake (m - enat n) (ldropn n xs)"
by(induct n arbitrary: m xs)(auto simp add: zero_enat_def[symmetric] ltake_LCons ldropn_Suc eSuc_enat[symmetric] iadd_Suc_right split: llist.split co.enat.split_asm)

lemma ltake_ldrop: "ltake n (ldrop m xs) = ldrop m (ltake (n + m) xs)"
by(induct xs arbitrary: n m)(simp_all add: ldrop_LCons iadd_Suc_right split: co.enat.split)

lemma ldrop_ltake: "ldrop n (ltake m xs) = ltake (m - n) (ldrop n xs)"
by(induct xs arbitrary: n m)(simp_all add: ltake_LCons ldrop_LCons split: co.enat.split)

subsection ‹Taking the $n$-th element of a lazy list: @{term "lnth" }

lemma lnth_LNil:
  "lnth LNil n = undefined n"
by(cases n)(simp_all add: lnth.simps)

lemma lnth_0 [simp]:
  "lnth (LCons x xs) 0 = x"
by(simp add: lnth.simps)

lemma lnth_Suc_LCons [simp]:
  "lnth (LCons x xs) (Suc n) = lnth xs n"
by(simp add: lnth.simps)

lemma lnth_LCons:
  "lnth (LCons x xs) n = (case n of 0  x | Suc n'  lnth xs n')"
by(cases n) simp_all

lemma lnth_LCons': "lnth (LCons x xs) n = (if n = 0 then x else lnth xs (n - 1))"
by(simp add: lnth_LCons split: nat.split)

lemma lhd_conv_lnth:
  "¬ lnull xs  lhd xs = lnth xs 0"
by(auto simp add: lhd_def not_lnull_conv)

lemmas lnth_0_conv_lhd = lhd_conv_lnth[symmetric]

lemma lnth_ltl: "¬ lnull xs  lnth (ltl xs) n = lnth xs (Suc n)"
by(auto simp add: not_lnull_conv)

lemma lhd_ldropn:
  "enat n < llength xs  lhd (ldropn n xs) = lnth xs n"
proof(induct n arbitrary: xs)
  case 0 thus ?case by(cases xs) auto
next
  case (Suc n)
  from ‹enat (Suc n) < llength xs obtain x xs'
    where [simp]: "xs = LCons x xs'" by(cases xs) auto
  from ‹enat (Suc n) < llength xs
  have "enat n < llength xs'" by(simp add: Suc_ile_eq)
  hence "lhd (ldropn n xs') = lnth xs' n" by(rule Suc)
  thus ?case by simp
qed

lemma lhd_ldrop:
  assumes "n < llength xs"
  shows "lhd (ldrop n xs) = lnth xs (the_enat n)"
proof -
  from assms obtain n' where n: "n = enat n'" by(cases n) auto
  from assms show ?thesis unfolding n
  proof(induction n' arbitrary: xs)
    case 0 thus ?case
      by(simp add: zero_enat_def[symmetric] lhd_conv_lnth)
  next
    case (Suc n')
    thus ?case
      by(cases xs)(simp_all add: eSuc_enat[symmetric], simp add: eSuc_enat)
  qed
qed

lemma lnth_beyond:
  "llength xs  enat n  lnth xs n = undefined (n - (case llength xs of enat m  m))"
proof(induct n arbitrary: xs)
  case 0 thus ?case by(simp add: zero_enat_def[symmetric] lnth_def lnull_def)
next
  case Suc thus ?case
    by(cases xs)(simp_all add: zero_enat_def lnth_def eSuc_enat[symmetric] split: enat.split, auto simp add: eSuc_enat)
qed

lemma lnth_lmap [simp]:
  "enat n < llength xs  lnth (lmap f xs) n = f (lnth xs n)"
proof(induct n arbitrary: xs)
  case 0 thus ?case by(cases xs) simp_all
next
  case (Suc n)
  from ‹enat (Suc n) < llength xs obtain x xs'
    where xs: "xs = LCons x xs'" and len: "enat n < llength xs'"
    by(cases xs)(auto simp add: Suc_ile_eq)
  from len have "lnth (lmap f xs') n = f (lnth xs' n)" by(rule Suc)
  with xs show ?case by simp
qed

lemma lnth_ldropn [simp]:
  "enat (n + m) < llength xs  lnth (ldropn n xs) m = lnth xs (m + n)"
proof(induct n arbitrary: xs)
  case (Suc n)
  from ‹enat (Suc n + m) < llength xs
  obtain x xs' where "xs = LCons x xs'" by(cases xs) auto
  moreover with ‹enat (Suc n + m) < llength xs
  have "enat (n + m) < llength xs'" by(simp add: Suc_ile_eq)
  hence "lnth (ldropn n xs') m = lnth xs' (m + n)" by(rule Suc)
  ultimately show ?case by simp
qed simp

lemma lnth_ldrop [simp]:
  "n + enat m < llength xs  lnth (ldrop n xs) m = lnth xs (m + the_enat n)"
by(cases n)(simp_all add: ldrop_enat)

lemma in_lset_conv_lnth:
  "x  lset xs  (n. enat n < llength xs  lnth xs n = x)"
  (is "?lhs  ?rhs")
proof
  assume ?rhs
  then obtain n where "enat n < llength xs" "lnth xs n = x" by blast
  thus ?lhs
  proof(induct n arbitrary: xs)
    case 0
    thus ?case
      by(auto simp add: zero_enat_def[symmetric] not_lnull_conv)
  next
    case (Suc n)
    thus ?case
      by(cases xs)(auto simp add: eSuc_enat[symmetric])
  qed
next
  assume ?lhs
  thus ?rhs
  proof(induct)
    case (find xs)
    show ?case by(auto intro: exI[where x=0] simp add: zero_enat_def[symmetric])
  next
    case (step x' xs)
    thus ?case
      by(auto 4 4 intro: exI[where x="Suc n" for n] ileI1 simp add: eSuc_enat[symmetric])
  qed
qed

lemma lset_conv_lnth: "lset xs = {lnth xs n|n. enat n < llength xs}"
by(auto simp add: in_lset_conv_lnth)

lemma lnth_llist_of [simp]: "lnth (llist_of xs) = nth xs"
proof(rule ext)
  fix n
  show "lnth (llist_of xs) n = xs ! n"
  proof(induct xs arbitrary: n)
    case Nil thus ?case by(cases n)(simp_all add: nth_def lnth_def)
  next
    case Cons thus ?case by(simp add: lnth_LCons split: nat.split)
  qed
qed

lemma nth_list_of [simp]:
  assumes "lfinite xs"
  shows "nth (list_of xs) = lnth xs"
using assms
by induct(auto intro: simp add: nth_def lnth_LNil nth_Cons split: nat.split)

lemma lnth_lappend1:
  "enat n < llength xs  lnth (lappend xs ys) n = lnth xs n"
proof(induct n arbitrary: xs)
  case 0 thus ?case by(auto simp add: zero_enat_def[symmetric] not_lnull_conv)
next
  case (Suc n)
  from ‹enat (Suc n) < llength xs obtain x xs'
    where [simp]: "xs = LCons x xs'" and len: "enat n < llength xs'"
    by(cases xs)(auto simp add: Suc_ile_eq)
  from len have "lnth (lappend xs' ys) n = lnth xs' n" by(rule Suc)
  thus ?case by simp
qed

lemma lnth_lappend_llist_of:
  "lnth (lappend (llist_of xs) ys) n =
  (if n < length xs then xs ! n else lnth ys (n - length xs))"
proof(induct xs arbitrary: n)
  case (Cons x xs) thus ?case by(cases n) auto
qed simp

lemma lnth_lappend2:
  " llength xs = enat k; k  n   lnth (lappend xs ys) n = lnth ys (n - k)"
proof(induct n arbitrary: xs k)
  case 0 thus ?case by(simp add: zero_enat_def[symmetric] lappend_lnull1)
next
  case (Suc n) thus ?case
    by(cases xs)(auto simp add: eSuc_def zero_enat_def split: enat.split_asm)
qed

lemma lnth_lappend:
  "lnth (lappend xs ys) n = (if enat n < llength xs then lnth xs n else lnth ys (n - the_enat (llength xs)))"
by(cases "llength xs")(auto simp add: lnth_lappend1 lnth_lappend2)

lemma lnth_ltake:
  "enat m < n  lnth (ltake n xs) m = lnth xs m"
proof(induct m arbitrary: xs n)
  case 0 thus ?case
    by(cases n rule: enat_coexhaust)(auto, cases xs, auto)
next
  case (Suc m)
  from ‹enat (Suc m) < n obtain n' where "n = eSuc n'"
    by(cases n rule: enat_coexhaust) auto
  with ‹enat (Suc m) < n have "enat m < n'" by(simp add: eSuc_enat[symmetric])
  with Suc n = eSuc n' show ?case by(cases xs) auto
qed

lemma ldropn_Suc_conv_ldropn:
  "enat n < llength xs  LCons (lnth xs n) (ldropn (Suc n) xs) = ldropn n xs"
proof(induct n arbitrary: xs)
  case 0 thus ?case by(cases xs) auto
next
  case (Suc n)
  from ‹enat (Suc n) < llength xs obtain x xs'
    where [simp]: "xs = LCons x xs'" by(cases xs) auto
  from ‹enat (Suc n) < llength xs
  have "enat n < llength xs'" by(simp add: Suc_ile_eq)
  hence "LCons (lnth xs' n) (ldropn (Suc n) xs') = ldropn n xs'" by(rule Suc)
  thus ?case by simp
qed

lemma ltake_Suc_conv_snoc_lnth:
  "enat m < llength xs  ltake (enat (Suc m)) xs = lappend (ltake (enat m) xs) (LCons (lnth xs m) LNil)"
by(metis eSuc_enat eSuc_plus_1 ltake_plus_conv_lappend ldrop_enat ldropn_Suc_conv_ldropn ltake_0 ltake_eSuc_LCons one_eSuc)

lemma lappend_eq_lappend_conv:
  assumes len: "llength xs = llength us"
  shows "lappend xs ys = lappend us vs 
         xs = us  (lfinite xs  ys = vs)" (is "?lhs  ?rhs")
proof
  assume ?rhs
  thus ?lhs by(auto simp add: lappend_inf)
next
  assume eq: ?lhs
  show ?rhs
  proof(intro conjI impI)
    show "xs = us" using len eq
    proof(coinduction arbitrary: xs us)
      case (Eq_llist xs us)
      thus ?case
        by(cases xs us rule: llist.exhaust[case_product llist.exhaust]) auto
    qed
    assume "lfinite xs"
    then obtain xs' where "xs = llist_of xs'"
      by(auto simp add: lfinite_eq_range_llist_of)
    hence "lappend (llist_of xs') ys = lappend (llist_of xs') vs"
      using eq xs = us by blast
    thus "ys = vs"
      by (induct xs') simp_all
  qed
qed


subsection‹iterates›

lemmas iterates [code, nitpick_simp] = iterates.ctr
  and lnull_iterates = iterates.simps(1)
  and lhd_iterates = iterates.simps(2)
  and ltl_iterates = iterates.simps(3)

lemma lfinite_iterates [iff]: "¬ lfinite (iterates f x)"
proof
  assume "lfinite (iterates f x)"
  thus False
    by(induct zs"iterates f x" arbitrary: x rule: lfinite_induct) auto
qed

lemma lmap_iterates: "lmap f (iterates f x) = iterates f (f x)"
by(coinduction arbitrary: x) auto

lemma iterates_lmap: "iterates f x = LCons x (lmap f (iterates f x))"
by(simp add: lmap_iterates)(rule iterates)

lemma lappend_iterates: "lappend (iterates f x) xs = iterates f x"
by(coinduction arbitrary: x) auto

lemma [simp]:
  fixes f :: "'a  'a"
  shows lnull_funpow_lmap: "lnull ((lmap f ^^ n) xs)  lnull xs"
  and lhd_funpow_lmap: "¬ lnull xs  lhd ((lmap f ^^ n) xs) = (f ^^ n) (lhd xs)"
  and ltl_funpow_lmap: "¬ lnull xs  ltl ((lmap f ^^ n) xs) = (lmap f ^^ n) (ltl xs)"
by(induct n) simp_all

lemma iterates_equality:
  assumes h: "x. h x = LCons x (lmap f (h x))"
  shows "h = iterates f"
proof -
  { fix x
    have "¬ lnull (h x)" "lhd (h x) = x" "ltl (h x) = lmap f (h x)"
      by(subst h, simp)+ }
  note [simp] = this

  { fix x
    define n :: nat where "n = 0"
    have "(lmap f ^^ n) (h x) = (lmap f ^^ n) (iterates f x)"
      by(coinduction arbitrary: n)(auto simp add: funpow_swap1 lmap_iterates intro: exI[where x="Suc n" for n]) }
  thus ?thesis by auto
qed

lemma llength_iterates [simp]: "llength (iterates f x) = "
by(coinduction arbitrary: x rule: enat_coinduct)(auto simp add: epred_llength)

lemma ldropn_iterates: "ldropn n (iterates f x) = iterates f ((f ^^ n) x)"
proof(induct n arbitrary: x)
  case 0 thus ?case by simp
next
  case (Suc n)
  have "ldropn (Suc n) (iterates f x) = ldropn n (iterates f (f x))"
    by(subst iterates)simp
  also have " = iterates f ((f ^^ n) (f x))" by(rule Suc)
  finally show ?case by(simp add: funpow_swap1)
qed

lemma ldrop_iterates: "ldrop (enat n) (iterates f x) = iterates f ((f ^^ n) x)"
proof(induct n arbitrary: x)
  case Suc thus ?case
    by(subst iterates)(simp add: eSuc_enat[symmetric] funpow_swap1)
qed(simp add: zero_enat_def[symmetric])

lemma lnth_iterates [simp]: "lnth (iterates f x) n = (f ^^ n) x"
proof(induct n arbitrary: x)
  case 0 thus ?case by(subst iterates) simp
next
  case (Suc n)
  hence "lnth (iterates f (f x)) n = (f ^^ n) (f x)" .
  thus ?case by(subst iterates)(simp add: funpow_swap1)
qed

lemma lset_iterates:
  "lset (iterates f x) = {(f ^^ n) x|n. True}"
by(auto simp add: lset_conv_lnth)

lemma lset_repeat [simp]: "lset (repeat x) = {x}"
by(simp add: lset_iterates id_def[symmetric])

subsection ‹
  More on the prefix ordering on lazy lists: @{term "lprefix"} and @{term "lstrict_prefix"}

lemma lstrict_prefix_code [code, simp]:
  "lstrict_prefix LNil LNil  False"
  "lstrict_prefix LNil (LCons y ys)  True"
  "lstrict_prefix (LCons x xs) LNil  False"
  "lstrict_prefix (LCons x xs) (LCons y ys)  x = y  lstrict_prefix xs ys"
by(auto simp add: lstrict_prefix_def)

lemma lmap_lprefix: "xs  ys  lmap f xs  lmap f ys"
by(rule monotoneD[OF monotone_lmap])

lemma lprefix_llength_eq_imp_eq:
  " xs  ys; llength xs = llength ys   xs = ys"
by(coinduction arbitrary: xs ys)(auto simp add: not_lnull_conv)

lemma lprefix_llength_le: "xs  ys  llength xs  llength ys"
using monotone_llength by(rule monotoneD)

lemma lstrict_prefix_llength_less:
  assumes "lstrict_prefix xs ys"
  shows "llength xs < llength ys"
proof(rule ccontr)
  assume "¬ llength xs < llength ys"
  moreover from ‹lstrict_prefix xs ys have "xs  ys" "xs  ys"
    unfolding lstrict_prefix_def by simp_all
  from xs  ys have "llength xs  llength ys"
    by(rule lprefix_llength_le)
  ultimately have "llength xs = llength ys" by auto
  with xs  ys have "xs = ys"
    by(rule lprefix_llength_eq_imp_eq)
  with xs  ys show False by contradiction
qed

lemma lstrict_prefix_lfinite1: "lstrict_prefix xs ys  lfinite xs"
by (metis lstrict_prefix_def not_lfinite_lprefix_conv_eq)

lemma wfP_lstrict_prefix: "wfP lstrict_prefix"
proof(unfold wfP_def)
  have "wf {(x :: enat, y). x < y}"
    unfolding wf_def by(blast intro: less_induct)
  hence "wf (inv_image {(x, y). x < y} llength)" by(rule wf_inv_image)
  moreover have "{(xs, ys). lstrict_prefix xs ys}  inv_image {(x, y). x < y} llength"
    by(auto intro: lstrict_prefix_llength_less)
  ultimately show "wf {(xs, ys). lstrict_prefix xs ys}" by(rule wf_subset)
qed

lemma llist_less_induct[case_names less]:
  "(xs. (ys. lstrict_prefix ys xs  P ys)  P xs)  P xs"
by(rule wfP_induct[OF wfP_lstrict_prefix]) blast

lemma ltake_enat_eq_imp_eq: "(n. ltake (enat n) xs = ltake (enat n) ys)  xs = ys"
by(coinduction arbitrary: xs ys)(auto simp add: zero_enat_def lnull_def neq_LNil_conv ltake_eq_LNil_iff eSuc_enat[symmetric] elim: allE[where x="Suc n" for n])

lemma ltake_enat_lprefix_imp_lprefix:
  assumes "n. lprefix (ltake (enat n) xs) (ltake (enat n) ys)"
  shows "lprefix xs ys"
proof -
  have "ccpo.admissible Sup (≤) (λn. ltake n xs  ltake n ys)" by simp
  hence "ltake (Sup (range enat)) xs  ltake (Sup (range enat)) ys"
    by(rule ccpo.admissibleD)(auto intro: assms)
  thus ?thesis by(simp add: ltake_all)
qed

lemma lprefix_conv_lappend: "xs  ys  (zs. ys = lappend xs zs)" (is "?lhs  ?rhs")
proof(rule iffI)
  assume ?lhs
  hence "ys = lappend xs (ldrop (llength xs) ys)"
    by(coinduction arbitrary: xs ys)(auto dest: lprefix_lnullD lprefix_lhdD intro: lprefix_ltlI simp add: not_lnull_conv lprefix_LCons_conv intro: exI[where x=LNil])
  thus ?rhs ..
next
  assume ?rhs
  thus ?lhs by(coinduct rule: lprefix_coinduct) auto
qed

lemma lappend_lprefixE:
  assumes "lappend xs ys  zs"
  obtains zs' where "zs = lappend xs zs'"
using assms unfolding lprefix_conv_lappend by(auto simp add: lappend_assoc)

lemma lprefix_lfiniteD:
  " xs  ys; lfinite ys   lfinite xs"
unfolding lprefix_conv_lappend by auto

lemma lprefix_lappendD:
  assumes "xs  lappend ys zs"
  shows "xs  ys  ys  xs"
proof(rule ccontr)
  assume "¬ (xs  ys  ys  xs)"
  hence "¬ xs  ys" "¬ ys  xs" by simp_all
  from xs  lappend ys zs obtain xs'
    where "lappend xs xs' = lappend ys zs"
    unfolding lprefix_conv_lappend by auto
  hence eq: "lappend (ltake (llength ys) xs) (lappend (ldrop (llength ys) xs) xs') =
             lappend ys zs"
    unfolding lappend_assoc[symmetric] by(simp only: lappend_ltake_ldrop)
  moreover have "llength xs  llength ys"
  proof(rule ccontr)
    assume "¬ ?thesis"
    hence "llength xs < llength ys" by simp
    hence "ltake (llength ys) xs = xs" by(simp add: ltake_all)
    hence "lappend xs (lappend (ldrop (llength ys) xs) xs') =
           lappend (ltake (llength xs) ys) (lappend (ldrop (llength xs) ys) zs)"
      unfolding lappend_assoc[symmetric] lappend_ltake_ldrop
      using eq by(simp add: lappend_assoc)
    hence xs: "xs = ltake (llength xs) ys" using ‹llength xs < llength ys
      by(subst (asm) lappend_eq_lappend_conv)(auto simp add: min_def)
    have "xs  ys" by(subst xs) auto
    with ¬ xs  ys show False by contradiction
  qed
  ultimately have ys: "ys = ltake (llength ys) xs"
    by(subst (asm) lappend_eq_lappend_conv)(simp_all add: min_def)
  have "ys  xs" by(subst ys) auto
  with ¬ ys  xs show False by contradiction
qed

lemma lstrict_prefix_lappend_conv:
  "lstrict_prefix xs (lappend xs ys)  lfinite xs  ¬ lnull ys"
proof -
  { assume "lfinite xs" "xs = lappend xs ys"
    hence "lnull ys" by induct auto }
  thus ?thesis
    by(auto simp add: lstrict_prefix_def lprefix_lappend lappend_inf lappend_lnull2
            elim: contrapos_np)
qed

lemma lprefix_llist_ofI:
  "zs. ys = xs @ zs  llist_of xs  llist_of ys"
by(clarsimp simp add: lappend_llist_of_llist_of[symmetric] lprefix_lappend)

lemma lprefix_llist_of [simp]: "llist_of xs  llist_of ys  prefix xs ys"
by(auto simp add: prefix_def lprefix_conv_lappend)(metis lfinite_lappend lfinite_llist_of list_of_lappend list_of_llist_of lappend_llist_of_llist_of)+

lemma llimit_induct [case_names LNil LCons limit]:
  ― ‹The limit case is just an instance of admissibility›
  assumes LNil: "P LNil"
  and LCons: "x xs.  lfinite xs; P xs   P (LCons x xs)"
  and limit: "(ys. lstrict_prefix ys xs  P ys)  P xs"
  shows "P xs"
proof(rule limit)
  fix ys
  assume "lstrict_prefix ys xs"
  hence "lfinite ys" by(rule lstrict_prefix_lfinite1)
  thus "P ys" by(induct)(blast intro: LNil LCons)+
qed

lemma lmap_lstrict_prefix:
  "lstrict_prefix xs ys  lstrict_prefix (lmap f xs) (lmap f ys)"
by (metis llength_lmap lmap_lprefix lprefix_llength_eq_imp_eq lstrict_prefix_def)

lemma lprefix_lnthD:
  assumes "xs  ys" and "enat n < llength xs"
  shows "lnth xs n = lnth ys n"
using assms by (metis lnth_lappend1 lprefix_conv_lappend)

lemma lfinite_lSup_chain:
  assumes chain: "Complete_Partial_Order.chain (⊑) A"
  shows "lfinite (lSup A)  finite A  (xs  A. lfinite xs)" (is "?lhs  ?rhs")
proof(intro iffI conjI)
  assume ?lhs
  then obtain n where n: "llength (lSup A) = enat n" unfolding lfinite_conv_llength_enat ..
  have "llength ` A  {..<enat (Suc n)}"
    by(auto dest!: chain_lprefix_lSup[OF chain] lprefix_llength_le simp add: n intro: le_less_trans)
  hence "finite (llength ` A)" by(rule finite_subset)(simp add: finite_lessThan_enat_iff)
  moreover have "inj_on llength A" by(rule inj_onI)(auto 4 3 dest: chainD[OF chain] lprefix_llength_eq_imp_eq)
  ultimately show "finite A" by(rule finite_imageD)
next
  assume ?rhs
  hence "finite A" "xsA. lfinite xs" by simp_all
  show ?lhs
  proof(cases "A = {}")
    case False
    with chain ‹finite A
    have "lSup A  A" by(rule ccpo.in_chain_finite[OF llist_ccpo])
    with xsA. lfinite xs show ?thesis ..
  qed simp
qed(rule lfinite_lSupD)

text ‹Setup for @{term "lprefix"} for Nitpick›

definition finite_lprefix :: "'a llist  'a llist  bool"
where "finite_lprefix = (⊑)"

lemma finite_lprefix_nitpick_simps [nitpick_simp]:
  "finite_lprefix xs LNil  xs = LNil"
  "finite_lprefix LNil xs  True"
  "finite_lprefix xs (LCons y ys) 
   xs = LNil  (xs'. xs = LCons y xs'  finite_lprefix xs' ys)"
by(simp_all add: lprefix_LCons_conv finite_lprefix_def lnull_def)

lemma lprefix_nitpick_simps [nitpick_simp]:
  "xs  ys = (if lfinite xs then finite_lprefix xs ys else xs = ys)"
by(simp add: finite_lprefix_def not_lfinite_lprefix_conv_eq)

hide_const (open) finite_lprefix
hide_fact (open) finite_lprefix_def finite_lprefix_nitpick_simps lprefix_nitpick_simps

subsection ‹Length of the longest common prefix›

lemma llcp_simps [simp, code, nitpick_simp]:
  shows llcp_LNil1: "llcp LNil ys = 0"
  and llcp_LNil2: "llcp xs LNil = 0"
  and llcp_LCons: "llcp (LCons x xs) (LCons y ys) = (if x = y then eSuc (llcp xs ys) else 0)"
by(simp_all add: llcp_def enat_unfold split: llist.split)

lemma llcp_eq_0_iff:
  "llcp xs ys = 0  lnull xs  lnull ys  lhd xs  lhd ys"
by(simp add: llcp_def)

lemma epred_llcp:
  " ¬ lnull xs; ¬ lnull ys; lhd xs = lhd ys 
    epred (llcp xs ys) = llcp (ltl xs) (ltl ys)"
by(simp add: llcp_def)

lemma llcp_commute: "llcp xs ys = llcp ys xs"
by(coinduction arbitrary: xs ys rule: enat_coinduct)(auto simp add: llcp_eq_0_iff epred_llcp)

lemma llcp_same_conv_length [simp]: "llcp xs xs = llength xs"
by(coinduction arbitrary: xs rule: enat_coinduct)(auto simp add: llcp_eq_0_iff epred_llcp epred_llength)

lemma llcp_lappend_same [simp]:
  "llcp (lappend xs ys) (lappend xs zs) = llength xs + llcp ys zs"
by(coinduction arbitrary: xs rule: enat_coinduct)(auto simp add: iadd_is_0 llcp_eq_0_iff epred_iadd1 epred_llcp epred_llength)

lemma llcp_lprefix1 [simp]: "xs  ys  llcp xs ys = llength xs"
by (metis add_0_right lappend_LNil2 llcp_LNil1 llcp_lappend_same lprefix_conv_lappend)

lemma llcp_lprefix2 [simp]: "ys  xs  llcp xs ys = llength ys"
by (metis llcp_commute llcp_lprefix1)

lemma llcp_le_length: "llcp xs ys  min (llength xs) (llength ys)"
proof -
  define m n where "m = llcp xs ys" and "n = min (llength xs) (llength ys)"
  hence "(m, n)  {(llcp xs ys, min (llength xs) (llength ys)) |xs ys :: 'a llist. True}" by blast
  thus "m  n"
  proof(coinduct rule: enat_leI)
    case (Leenat m n)
    then obtain xs ys :: "'a llist" where "m = llcp xs ys" "n = min (llength xs) (llength ys)" by blast
    thus ?case
      by(cases xs ys rule: llist.exhaust[case_product llist.exhaust])(auto 4 3 intro!: exI[where x="Suc 0"] simp add: eSuc_enat[symmetric] iadd_Suc_right zero_enat_def[symmetric])
  qed
qed

lemma llcp_ltake1: "llcp (ltake n xs) ys = min n (llcp xs ys)"
by(coinduction arbitrary: n xs ys rule: enat_coinduct)(auto simp add: llcp_eq_0_iff enat_min_eq_0_iff epred_llcp ltl_ltake)

lemma llcp_ltake2: "llcp xs (ltake n ys) = min n (llcp xs ys)"
by(metis llcp_commute llcp_ltake1)

lemma llcp_ltake [simp]: "llcp (ltake n xs) (ltake m ys) = min (min n m) (llcp xs ys)"
by(metis llcp_ltake1 llcp_ltake2 min.assoc)

subsection ‹Zipping two lazy lists to a lazy list of pairs @{term "lzip" }

lemma lzip_simps [simp, code, nitpick_simp]:
  "lzip LNil ys = LNil"
  "lzip xs LNil = LNil"
  "lzip (LCons x xs) (LCons y ys) = LCons (x, y) (lzip xs ys)"
by(auto intro: llist.expand)

lemma lnull_lzip [simp]: "lnull (lzip xs ys)  lnull xs  lnull ys"
by(simp add: lzip_def)

lemma lzip_eq_LNil_conv: "lzip xs ys = LNil  xs = LNil  ys = LNil"
using lnull_lzip unfolding lnull_def .

lemmas lhd_lzip = lzip.sel(1)
  and ltl_lzip = lzip.sel(2)

lemma lzip_eq_LCons_conv:
  "lzip xs ys = LCons z zs 
   (x xs' y ys'. xs = LCons x xs'  ys = LCons y ys'  z = (x, y)  zs = lzip xs' ys')"
by(cases xs ys rule: llist.exhaust[case_product llist.exhaust]) auto

lemma lzip_lappend:
  "llength xs = llength us
   lzip (lappend xs ys) (lappend us vs) = lappend (lzip xs us) (lzip ys vs)"
by(coinduction arbitrary: xs ys us vs rule: llist.coinduct_strong)(auto 4 6 simp add: llength_ltl)

lemma llength_lzip [simp]:
  "llength (lzip xs ys) = min (llength xs) (llength ys)"
by(coinduction arbitrary: xs ys rule: enat_coinduct)(auto simp add: enat_min_eq_0_iff epred_llength)

lemma ltake_lzip: "ltake n (lzip xs ys) = lzip (ltake n xs) (ltake n ys)"
by(coinduction arbitrary: xs ys n)(auto simp add: ltl_ltake)

lemma ldropn_lzip [simp]:
  "ldropn n (lzip xs ys) = lzip (ldropn n xs) (ldropn n ys)"
by(induct n arbitrary: xs ys)(simp_all add: ldropn_Suc split: llist.split)

lemma
  fixes F
  defines "F  λlzip (xs, ys). case xs of LNil  LNil | LCons x xs'  case ys of LNil  LNil | LCons y ys'  LCons (x, y) (curry lzip xs' ys')"
  shows lzip_conv_fixp: "lzip  curry (ccpo.fixp (fun_lub lSup) (fun_ord (⊑)) F)" (is "?lhs  ?rhs")
  and lzip_mono: "mono_llist (λlzip. F lzip xs)" (is "?mono xs")
proof(intro eq_reflection ext)
  show mono: "xs. ?mono xs" unfolding F_def by(tactic Partial_Function.mono_tac @{context} 1)
  fix xs ys
  show "lzip xs ys = ?rhs xs ys"
  proof(coinduction arbitrary: xs ys)
    case Eq_llist show ?case
      by(subst (1 3 4) llist.mono_body_fixp[OF mono])(auto simp add: F_def split: llist.split)
  qed
qed

lemma monotone_lzip: "monotone (rel_prod (⊑) (⊑)) (⊑) (case_prod lzip)"
by(rule llist.fixp_preserves_mono2[OF lzip_mono lzip_conv_fixp]) simp

lemma mono2mono_lzip1 [THEN llist.mono2mono, cont_intro, simp]:
  shows monotone_lzip1: "monotone (⊑) (⊑) (λxs. lzip xs ys)"
by(simp add: monotone_lzip[simplified])

lemma mono2mono_lzip2 [THEN llist.mono2mono, cont_intro, simp]:
  shows monotone_lzip2: "monotone (⊑) (⊑) (λys. lzip xs ys)"
by(simp add: monotone_lzip[simplified])

lemma mcont_lzip: "mcont (prod_lub lSup lSup) (rel_prod (⊑) (⊑)) lSup (⊑) (case_prod lzip)"
by(rule llist.fixp_preserves_mcont2[OF lzip_mono lzip_conv_fixp]) simp

lemma mcont2mcont_lzip1 [THEN llist.mcont2mcont, cont_intro, simp]:
  shows mcont_lzip1: "mcont lSup (⊑) lSup (⊑) (λxs. lzip xs ys)"
by(simp add: mcont_lzip[simplified])

lemma mcont2mcont_lzip2 [THEN llist.mcont2mcont, cont_intro, simp]:
  shows mcont_lzip2: "mcont lSup (⊑) lSup (⊑) (λys. lzip xs ys)"
by(simp add: mcont_lzip[simplified])

lemma ldrop_lzip [simp]: "ldrop n (lzip xs ys) = lzip (ldrop n xs) (ldrop n ys)"
proof(induct xs arbitrary: ys n)
  case LCons
  thus ?case by(cases ys n rule: llist.exhaust[case_product co.enat.exhaust]) simp_all
qed simp_all

lemma lzip_iterates:
  "lzip (iterates f x) (iterates g y) = iterates (λ(x, y). (f x, g y)) (x, y)"
by(coinduction arbitrary: x y) auto

lemma lzip_llist_of [simp]:
  "lzip (llist_of xs) (llist_of ys) = llist_of (zip xs ys)"
proof(induct xs arbitrary: ys)
  case (Cons x xs')
  thus ?case by(cases ys) simp_all
qed simp

lemma lnth_lzip:
  " enat n < llength xs; enat n < llength ys 
   lnth (lzip xs ys) n = (lnth xs n, lnth ys n)"
proof(induct n arbitrary: xs ys)
  case 0 thus ?case
    by(simp add: zero_enat_def[symmetric] lnth_0_conv_lhd)
next
  case (Suc n)
  thus ?case
    by(cases xs ys rule: llist.exhaust[case_product llist.exhaust])(auto simp add: eSuc_enat[symmetric])
qed

lemma lset_lzip:
  "lset (lzip xs ys) =
   {(lnth xs n, lnth ys n)|n. enat n < min (llength xs) (llength ys)}"
by(auto simp add: lset_conv_lnth lnth_lzip)(auto intro!: exI simp add: lnth_lzip)

lemma lset_lzipD1: "(x, y)  lset (lzip xs ys)  x  lset xs"
proof(induct "lzip xs ys" arbitrary: xs ys rule: lset_induct)
  case [symmetric]: find
  thus ?case by(auto simp add: lzip_eq_LCons_conv)
next
  case (step z zs)
  thus ?case by -(drule sym, auto simp add: lzip_eq_LCons_conv)
qed

lemma lset_lzipD2: "(x, y)  lset (lzip xs ys)  y  lset ys"
proof(induct "lzip xs ys" arbitrary: xs ys rule: lset_induct)
  case [symmetric]: find
  thus ?case by(auto simp add: lzip_eq_LCons_conv)
next
  case (step z zs)
  thus ?case by -(drule sym, auto simp add: lzip_eq_LCons_conv)
qed

lemma lset_lzip_same [simp]: "lset (lzip xs xs) = (λx. (x, x)) ` lset xs"
by(auto 4 3 simp add: lset_lzip in_lset_conv_lnth)

lemma lfinite_lzip [simp]:
  "lfinite (lzip xs ys)  lfinite xs  lfinite ys" (is "?lhs  ?rhs")
proof
  assume ?lhs
  thus ?rhs
    by(induct zs"lzip xs ys" arbitrary: xs ys rule: lfinite_induct) fastforce+
next
  assume ?rhs (is "?xs  ?ys")
  thus ?lhs
  proof
    assume ?xs
    thus ?thesis
    proof(induct arbitrary: ys)
      case (lfinite_LConsI xs x)
      thus ?case by(cases ys) simp_all
    qed simp
  next
    assume ?ys
    thus ?thesis
    proof(induct arbitrary: xs)
      case (lfinite_LConsI ys y)
      thus ?case by(cases xs) simp_all
    qed simp
  qed
qed

lemma lzip_eq_lappend_conv:
  assumes eq: "lzip xs ys = lappend us vs"
  shows "xs' xs'' ys' ys''. xs = lappend xs' xs''  ys = lappend ys' ys'' 
                             llength xs' = llength ys'  us = lzip xs' ys' 
                             vs = lzip xs'' ys''"
proof -
  let ?xs' = "ltake (llength us) xs"
  let ?xs'' = "ldrop (llength us) xs"
  let ?ys' = "ltake (llength us) ys"
  let ?ys'' = "ldrop (llength us) ys"

  from eq have "llength (lzip xs ys) = llength (lappend us vs)" by simp
  hence "min (llength xs) (llength ys)  llength us"
    by(auto simp add: enat_le_plus_same)
  hence len: "llength xs  llength us" "llength ys  llength us" by(auto)

  hence leneq: "llength ?xs' = llength ?ys'" by(simp add: min_def)
  have xs: "xs = lappend ?xs' ?xs''" and ys: "ys = lappend ?ys' ?ys''"
    by(simp_all add: lappend_ltake_ldrop)
  hence "lappend us vs = lzip (lappend ?xs' ?xs'') (lappend ?ys' ?ys'')"
    using eq by simp
  with len have "lappend us vs = lappend (lzip ?xs' ?ys') (lzip ?xs'' ?ys'')"
    by(simp add: lzip_lappend min_def)
  hence us: "us = lzip ?xs' ?ys'"
    and vs: "lfinite us  vs = lzip ?xs'' ?ys''" using len
    by(simp_all add: min_def lappend_eq_lappend_conv)
  show ?thesis
  proof(cases "lfinite us")
    case True
    with leneq xs ys us vs len show ?thesis by fastforce
  next
    case False
    let ?xs'' = "lmap fst vs"
    let ?ys'' = "lmap snd vs"
    from False have "lappend us vs = us" by(simp add: lappend_inf)
    moreover from False have "llength us = "
      by(rule not_lfinite_llength)
    moreover with len
    have "llength xs = " "llength ys = " by auto
    moreover with ‹llength us = 
    have "xs = ?xs'" "ys = ?ys'" by(simp_all add: ltake_all)
    from ‹llength us =  len
    have "¬ lfinite ?xs'" "¬ lfinite ?ys'"
      by(auto simp del: llength_ltake lfinite_ltake
             simp add: ltake_all dest: lfinite_llength_enat)
    with xs = ?xs' ys = ?ys'
    have "xs = lappend ?xs' ?xs''" "ys = lappend ?ys' ?ys''"
      by(simp_all add: lappend_inf)
    moreover have "vs = lzip ?xs'' ?ys''"
      by(coinduction arbitrary: vs) auto
    ultimately show ?thesis using eq by(fastforce simp add: ltake_all)
  qed
qed

lemma lzip_lmap [simp]:
  "lzip (lmap f xs) (lmap g ys) = lmap (λ(x, y). (f x, g y)) (lzip xs ys)"
by(coinduction arbitrary: xs ys) auto

lemma lzip_lmap1:
  "lzip (lmap f xs) ys = lmap (λ(x, y). (f x, y)) (lzip xs ys)"
by(subst (4) llist.map_ident[symmetric])(simp only: lzip_lmap)

lemma lzip_lmap2:
  "lzip xs (lmap f ys) = lmap (λ(x, y). (x, f y)) (lzip xs ys)"
by(subst (1) llist.map_ident[symmetric])(simp only: lzip_lmap)

lemma lmap_fst_lzip_conv_ltake:
  "lmap fst (lzip xs ys) = ltake (min (llength xs) (llength ys)) xs"
by(coinduction arbitrary: xs ys)(auto simp add: enat_min_eq_0_iff ltl_ltake epred_llength)

lemma lmap_snd_lzip_conv_ltake:
  "lmap snd (lzip xs ys) = ltake (min (llength xs) (llength ys)) ys"
by(coinduction arbitrary: xs ys)(auto simp add: enat_min_eq_0_iff ltl_ltake epred_llength)

lemma lzip_conv_lzip_ltake_min_llength:
  "lzip xs ys =
  lzip (ltake (min (llength xs) (llength ys)) xs)
       (ltake (min (llength xs) (llength ys)) ys)"
by(coinduction arbitrary: xs ys)(auto simp add: enat_min_eq_0_iff ltl_ltake epred_llength)

subsection ‹Taking and dropping from a lazy list: @{term "ltakeWhile"} and @{term "ldropWhile"}

lemma ltakeWhile_simps [simp, code, nitpick_simp]:
  shows ltakeWhile_LNil: "ltakeWhile P LNil = LNil"
  and ltakeWhile_LCons: "ltakeWhile P (LCons x xs) = (if P x then LCons x (ltakeWhile P xs) else LNil)"
by(auto simp add: ltakeWhile_def intro: llist.expand)

lemma ldropWhile_simps [simp, code]:
  shows ldropWhile_LNil: "ldropWhile P LNil = LNil"
  and ldropWhile_LCons: "ldropWhile P (LCons x xs) = (if P x then ldropWhile P xs else LCons x xs)"
by(simp_all add: ldropWhile.simps)

lemma fixes f F P
  defines "F  λltakeWhile xs. case xs of LNil  LNil | LCons x xs  if P x then LCons x (ltakeWhile xs) else LNil"
  shows ltakeWhile_conv_fixp: "ltakeWhile P  ccpo.fixp (fun_lub lSup) (fun_ord lprefix) F" (is "?lhs  ?rhs")
  and ltakeWhile_mono: "xs. mono_llist (λltakeWhile. F ltakeWhile xs)" (is "PROP ?mono")
proof(intro eq_reflection ext)
  show mono: "PROP ?mono" unfolding F_def by(tactic Partial_Function.mono_tac @{context} 1)
  fix xs
  show "?lhs xs = ?rhs xs"
  proof(coinduction arbitrary: xs)
    case Eq_llist
    show ?case by(subst (1 3 4) llist.mono_body_fixp[OF mono])(auto simp add: F_def split: llist.split prod.split co.enat.split)
  qed
qed

lemma mono2mono_ltakeWhile[THEN llist.mono2mono, cont_intro, simp]:
  shows monotone_ltakeWhile: "monotone lprefix lprefix (ltakeWhile P)"
by(rule llist.fixp_preserves_mono1[OF ltakeWhile_mono ltakeWhile_conv_fixp]) simp

lemma mcont2mcont_ltakeWhile [THEN llist.mcont2mcont, cont_intro, simp]:
  shows mcont_ltakeWhile: "mcont lSup lprefix lSup lprefix (ltakeWhile P)"
by(rule llist.fixp_preserves_mcont1[OF ltakeWhile_mono ltakeWhile_conv_fixp]) simp

lemma mono_llist_ltakeWhile [partial_function_mono]:
  "mono_llist F  mono_llist (λf. ltakeWhile P (F f))"
by(rule mono2mono_ltakeWhile)

lemma mono2mono_ldropWhile [THEN llist.mono2mono, cont_intro, simp]:
  shows monotone_ldropWhile: "monotone