Theory Ordered_Resolution_Prover.Lazy_List_Chain

(*  Title:       Relational Chains over Lazy Lists
    Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2014, 2017
    Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2017
    Author:      Anders Schlichtkrull <andschl at dtu.dk>, 2017
    Maintainer:  Anders Schlichtkrull <andschl at dtu.dk>
*)

section ‹Relational Chains over Lazy Lists›

theory Lazy_List_Chain
  imports
    "HOL-Library.BNF_Corec"
    Lazy_List_Liminf
begin

text ‹
A chain is a lazy list of elements such that all pairs of consecutive elements are related by a
given relation. A full chain is either an infinite chain or a finite chain that cannot be extended.
The inspiration for this theory is Section 4.1 (``Theorem Proving Processes'') of Bachmair and
Ganzinger's chapter.
›


subsection ‹Chains›

coinductive chain :: "('a  'a  bool)  'a llist  bool" for R :: "'a  'a  bool" where
  chain_singleton: "chain R (LCons x LNil)"
| chain_cons: "chain R xs  R x (lhd xs)  chain R (LCons x xs)"

lemma
  chain_LNil[simp]: "¬ chain R LNil" and
  chain_not_lnull: "chain R xs  ¬ lnull xs"
  by (auto elim: chain.cases)

lemma chain_lappend:
  assumes
    r_xs: "chain R xs" and
    r_ys: "chain R ys" and
    mid: "R (llast xs) (lhd ys)"
  shows "chain R (lappend xs ys)"
proof (cases "lfinite xs")
  case True
  then show ?thesis
    using r_xs mid
  proof (induct rule: lfinite.induct)
    case (lfinite_LConsI xs x)
    note fin = this(1) and ih = this(2) and r_xxs = this(3) and mid = this(4)
    show ?case
    proof (cases "xs = LNil")
      case True
      then show ?thesis
        using r_ys mid by simp (rule chain_cons)
    next
      case xs_nnil: False
      have r_xs: "chain R xs"
        by (metis chain.simps ltl_simps(2) r_xxs xs_nnil)
      have mid': "R (llast xs) (lhd ys)"
        by (metis llast_LCons lnull_def mid xs_nnil)
      have start: "R x (lhd (lappend xs ys))"
        by (metis (no_types) chain.simps lhd_LCons lhd_lappend chain_not_lnull ltl_simps(2) r_xxs
            xs_nnil)
      show ?thesis
        unfolding lappend_code(2) using ih[OF r_xs mid'] start by (rule chain_cons)
    qed
  qed simp
qed (simp add: r_xs lappend_inf)

lemma chain_length_pos: "chain R xs  llength xs > 0"
  by (cases xs) simp+

lemma chain_ldropn:
  assumes "chain R xs" and "enat n < llength xs"
  shows "chain R (ldropn n xs)"
  using assms
  by (induct n arbitrary: xs, simp,
      metis chain.cases ldrop_eSuc_ltl ldropn_LNil ldropn_eq_LNil ltl_simps(2) not_less)

lemma inf_chain_ldropn_chain: "chain R xs  ¬ lfinite xs  chain R (ldropn n xs)"
  using chain.simps[of R xs] by (simp add: chain_ldropn not_lfinite_llength)

lemma inf_chain_ltl_chain: "chain R xs  ¬ lfinite xs  chain R (ltl xs)"
  by (metis inf_chain_ldropn_chain ldropn_0 ldropn_ltl)

lemma chain_lnth_rel:
  assumes
    chain: "chain R xs" and
    len: "enat (Suc j) < llength xs"
  shows "R (lnth xs j) (lnth xs (Suc j))"
proof -
  define ys where "ys = ldropn j xs"
  have "llength ys > 1"
    unfolding ys_def using len
    by (metis One_nat_def funpow_swap1 ldropn_0 ldropn_def ldropn_eq_LNil ldropn_ltl not_less
        one_enat_def)
  obtain y0 y1 ys' where
    ys: "ys = LCons y0 (LCons y1 ys')"
    unfolding ys_def by (metis Suc_ile_eq ldropn_Suc_conv_ldropn len less_imp_not_less not_less)
  have "chain R ys"
    unfolding ys_def using Suc_ile_eq chain chain_ldropn len less_imp_le by blast
  then have "R y0 y1"
    unfolding ys by (auto elim: chain.cases)
  then show ?thesis
    using ys_def unfolding ys by (metis ldropn_Suc_conv_ldropn ldropn_eq_LConsD llist.inject)
qed

lemma infinite_chain_lnth_rel:
  assumes "¬ lfinite c" and "chain r c"
  shows "r (lnth c i) (lnth c (Suc i))"
  using assms chain_lnth_rel lfinite_conv_llength_enat by force

lemma lnth_rel_chain:
  assumes
    "¬ lnull xs" and
    "j. enat (j + 1) < llength xs  R (lnth xs j) (lnth xs (j + 1))"
  shows "chain R xs"
  using assms
proof (coinduction arbitrary: xs rule: chain.coinduct)
  case chain
  note nnul = this(1) and nth_chain = this(2)

  show ?case
  proof (cases "lnull (ltl xs)")
    case True
    have "xs = LCons (lhd xs) LNil"
      using nnul True by (simp add: llist.expand)
    then show ?thesis
      by blast
  next
    case nnul': False
    moreover have "xs = LCons (lhd xs) (ltl xs)"
      using nnul by simp
    moreover have
      "j. enat (j + 1) < llength (ltl xs)  R (lnth (ltl xs) j) (lnth (ltl xs) (j + 1))"
      using nnul nth_chain
      by (metis Suc_eq_plus1 ldrop_eSuc_ltl ldropn_Suc_conv_ldropn ldropn_eq_LConsD lnth_ltl)
    moreover have "R (lhd xs) (lhd (ltl xs))"
      using nnul' nnul nth_chain[rule_format, of 0, simplified]
      by (metis ldropn_0 ldropn_Suc_conv_ldropn ldropn_eq_LConsD lhd_LCons_ltl lhd_conv_lnth
          lnth_Suc_LCons ltl_simps(2))
    ultimately show ?thesis
      by blast
  qed
qed

lemma chain_lmap:
  assumes "x y. R x y  R' (f x) (f y)" and "chain R xs"
  shows "chain R' (lmap f xs)"
  using assms
proof (coinduction arbitrary: xs)
  case chain
  then have "(y. xs = LCons y LNil)  (ys x. xs = LCons x ys  chain R ys  R x (lhd ys))"
    using chain.simps[of R xs] by auto
  then show ?case
  proof
    assume "ys x. xs = LCons x ys  chain R ys  R x (lhd ys)"
    then have "ys x. lmap f xs = LCons x ys 
      (xs. ys = lmap f xs  (x y. R x y  R' (f x) (f y))  chain R xs)  R' x (lhd ys)"
      using chain
      by (metis (no_types) lhd_LCons llist.distinct(1) llist.exhaust_sel llist.map_sel(1)
          lmap_eq_LNil chain_not_lnull ltl_lmap ltl_simps(2))
    then show ?thesis
      by auto
  qed auto
qed

lemma chain_mono:
  assumes "x y. R x y  R' x y" and "chain R xs"
  shows "chain R' xs"
  using assms by (rule chain_lmap[of _ _ "λx. x", unfolded llist.map_ident])

lemma chain_ldropnI:
  assumes
    rel: "j. j  i  enat (Suc j) < llength xs  R (lnth xs j) (lnth xs (Suc j))" and
    si_lt: "enat (Suc i) < llength xs"
  shows "chain R (ldropn i xs)"
proof (rule lnth_rel_chain)
  show "¬ lnull (ldropn i xs)"
    using si_lt by (simp add: Suc_ile_eq less_le_not_le)
next
  show "j. enat (j + 1) < llength (ldropn i xs) 
    R (lnth (ldropn i xs) j) (lnth (ldropn i xs) (j + 1))"
    using rel
    by (smt (verit, best) Suc_ile_eq add.commute ldropn_eq_LNil ldropn_ldropn leD
        le_add1 linorder_le_less_linear lnth_ldropn order_less_imp_le plus_1_eq_Suc)
qed

lemma chain_ldropn_lmapI:
  assumes
    rel: "j. j  i  enat (Suc j) < llength xs  R (f (lnth xs j)) (f (lnth xs (Suc j)))" and
    si_lt: "enat (Suc i) < llength xs"
  shows "chain R (ldropn i (lmap f xs))"
proof -
  have "chain R (lmap f (ldropn i xs))"
    using chain_lmap[of "λx y. R (f x) (f y)" R f, of "ldropn i xs"] chain_ldropnI[OF rel si_lt]
    by auto
  thus ?thesis
    by auto
qed

lemma lfinite_chain_imp_rtranclp_lhd_llast: "lfinite xs  chain R xs  R** (lhd xs) (llast xs)"
proof (induct rule: lfinite.induct)
  case (lfinite_LConsI xs x)
  note fin_xs = this(1) and ih = this(2) and r_x_xs = this(3)
  show ?case
  proof (cases "xs = LNil")
    case xs_nnil: False
    then have r_xs: "chain R xs"
      using r_x_xs by (blast elim: chain.cases)
    then show ?thesis
      using ih[OF r_xs] xs_nnil r_x_xs
      by (metis chain.cases converse_rtranclp_into_rtranclp lhd_LCons llast_LCons chain_not_lnull
          ltl_simps(2))
  qed simp
qed simp

lemma tranclp_imp_exists_finite_chain_list:
  "R++ x y  xs. chain R (llist_of (x # xs @ [y]))"
proof (induct rule: tranclp.induct)
  case (r_into_trancl x y)
  then have "chain R (llist_of (x # [] @ [y]))"
    by (auto intro: chain.intros)
  then show ?case
    by blast
next
  case (trancl_into_trancl x y z)
  note rstar_xy = this(1) and ih = this(2) and r_yz = this(3)

  obtain xs where
    xs: "chain R (llist_of (x # xs @ [y]))"
    using ih by blast
  define ys where
    "ys = xs @ [y]"

  have "chain R (llist_of (x # ys @ [z]))"
    unfolding ys_def using r_yz chain_lappend[OF xs chain_singleton, of z]
    by (auto simp: lappend_llist_of_LCons llast_LCons)
  then show ?case
    by blast
qed

inductive_cases chain_consE: "chain R (LCons x xs)"
inductive_cases chain_nontrivE: "chain R (LCons x (LCons y xs))"


subsection ‹A Coinductive Puzzle›

primrec prepend where
  "prepend [] ys = ys"
| "prepend (x # xs) ys = LCons x (prepend xs ys)"

lemma lnull_prepend[simp]: "lnull (prepend xs ys) = (xs = []  lnull ys)"
  by (induct xs) auto

lemma lhd_prepend[simp]: "lhd (prepend xs ys) = (if xs  [] then hd xs else lhd ys)"
  by (induct xs) auto

lemma prepend_LNil[simp]: "prepend xs LNil = llist_of xs"
  by (induct xs) auto

lemma lfinite_prepend[simp]: "lfinite (prepend xs ys)  lfinite ys"
  by (induct xs) auto

lemma llength_prepend[simp]: "llength (prepend xs ys) = length xs + llength ys"
  by (induct xs) (auto simp: enat_0 iadd_Suc eSuc_enat[symmetric])

lemma llast_prepend[simp]: "¬ lnull ys  llast (prepend xs ys) = llast ys"
  by (induct xs) (auto simp: llast_LCons)

lemma prepend_prepend: "prepend xs (prepend ys zs) = prepend (xs @ ys) zs"
  by (induct xs) auto

lemma chain_prepend:
  "chain R (llist_of zs)  last zs = lhd xs  chain R xs  chain R (prepend zs (ltl xs))"
  by (induct zs; cases xs)
    (auto split: if_splits simp: lnull_def[symmetric] intro!: chain_cons elim!: chain_consE)

lemma lmap_prepend[simp]: "lmap f (prepend xs ys) = prepend (map f xs) (lmap f ys)"
  by (induct xs) auto

lemma lset_prepend[simp]: "lset (prepend xs ys) = set xs  lset ys"
  by (induct xs) auto

lemma prepend_LCons: "prepend xs (LCons y ys) = prepend (xs @ [y]) ys"
  by (induct xs) auto

lemma lnth_prepend:
  "lnth (prepend xs ys) i = (if i < length xs then nth xs i else lnth ys (i - length xs))"
  by (induct xs arbitrary: i) (auto simp: lnth_LCons' nth_Cons')

theorem lfinite_less_induct[consumes 1, case_names less]:
  assumes fin: "lfinite xs"
    and step: "xs. lfinite xs  (zs. llength zs < llength xs  P zs)  P xs"
  shows "P xs"
using fin proof (induct "the_enat (llength xs)" arbitrary: xs rule: less_induct)
  case (less xs)
  show ?case
    using less(2) by (intro step[OF less(2)] less(1))
      (auto dest!: lfinite_llength_enat simp: eSuc_enat elim!: less_enatE llength_eq_enat_lfiniteD)
qed

theorem lfinite_prepend_induct[consumes 1, case_names LNil prepend]:
  assumes "lfinite xs"
    and LNil: "P LNil"
    and prepend: "xs. lfinite xs  (zs. (ys. xs = prepend ys zs  ys  [])  P zs)  P xs"
  shows "P xs"
using assms(1) proof (induct xs rule: lfinite_less_induct)
  case (less xs)
  from less(1) show ?case
    by (cases xs)
      (force simp: LNil neq_Nil_conv dest: lfinite_llength_enat intro!: prepend[of "LCons _ _"] intro: less)+
qed

coinductive emb :: "'a llist  'a llist  bool" where
  "lfinite xs  emb LNil xs"
| "emb xs ys  emb (LCons x xs) (prepend zs (LCons x ys))"

inductive_cases emb_LConsE: "emb (LCons z zs) ys"
inductive_cases emb_LNil1E: "emb LNil ys"
inductive_cases emb_LNil2E: "emb xs LNil"

lemma emb_lfinite:
  assumes "emb xs ys"
  shows "lfinite ys  lfinite xs"
proof
  assume "lfinite xs"
  then show "lfinite ys" using assms
    by (induct xs arbitrary: ys rule: lfinite_induct)
      (auto simp: lnull_def neq_LNil_conv elim!: emb_LNil1E emb_LConsE)
next
  assume "lfinite ys"
  then show "lfinite xs" using assms
  proof (induction ys arbitrary: xs rule: lfinite_less_induct)
    case (less ys)
    from less.prems lfinite ys show ?case
      by (cases xs)
        (auto simp: eSuc_enat elim!: emb_LNil1E emb_LConsE less.IH[rotated]
          dest!: lfinite_llength_enat)
  qed
qed

inductive prepend_cong1 for X where
  prepend_cong1_base: "X xs  prepend_cong1 X xs"
| prepend_cong1_prepend: "prepend_cong1 X ys  prepend_cong1 X (prepend xs ys)"

lemma prepend_cong1_alt: "prepend_cong1 X xs  (ys zs. xs = prepend ys zs  X zs)"
  by (rule iffI, induct xs rule: prepend_cong1.induct)
    (force simp: prepend_prepend intro: prepend_cong1.intros exI[of _ "[]"])+

lemma emb_prepend_coinduct_cong[rotated, case_names emb]:
  assumes "(x1 x2. X x1 x2 
    (xs. x1 = LNil  x2 = xs  lfinite xs)
      (xs ys x zs. x1 = LCons x xs  x2 = prepend zs (LCons x ys)
        (prepend_cong1 (X xs) ys  emb xs ys)))" (is "x1 x2. X x1 x2  ?bisim x1 x2")
  shows "X x1 x2  emb x1 x2"
proof (erule emb.coinduct[OF prepend_cong1_base])
  fix xs zs
  assume "prepend_cong1 (X xs) zs"
  then show "?bisim xs zs"
    by (induct zs rule: prepend_cong1.induct) (erule assms, force simp: prepend_prepend)
qed

lemma emb_prepend: "emb xs ys  emb xs (prepend zs ys)"
  by (coinduction arbitrary: xs zs ys rule: emb_prepend_coinduct_cong)
    (force elim: emb.cases simp: prepend_prepend)

lemma prepend_cong1_emb: "prepend_cong1 (emb xs) ys = emb xs ys"
  by (rule iffI, induct ys rule: prepend_cong1.induct)
    (simp_all add: emb_prepend prepend_cong1_base)

lemma prepend_cong_distrib:
  "prepend_cong1 (P  Q) xs  prepend_cong1 P xs  prepend_cong1 Q xs"
  unfolding prepend_cong1_alt by auto

lemma emb_prepend_coinduct_aux[case_names emb]:
  assumes "X x1 x2 " "(x1 x2. X x1 x2 
    (xs. x1 = LNil  x2 = xs  lfinite xs)
      (xs ys x zs. x1 = LCons x xs  x2 = prepend zs (LCons x ys)
        (prepend_cong1 (X xs  emb xs) ys)))"
  shows "emb x1 x2"
  using assms unfolding prepend_cong_distrib prepend_cong1_emb
  by (rule emb_prepend_coinduct_cong)

lemma emb_prepend_coinduct[rotated, case_names emb]:
  assumes "(x1 x2. X x1 x2 
    (xs. x1 = LNil  x2 = xs  lfinite xs)
      (xs ys x zs zs'. x1 = LCons x xs  x2 = prepend zs (LCons x (prepend zs' ys))
        (X xs ys  emb xs ys)))"
  shows "X x1 x2  emb x1 x2"
  by (erule emb_prepend_coinduct_aux[of X]) (force simp: prepend_cong1_alt dest: assms)


context
begin

private coinductive chain' for R where
  "chain' R (LCons x LNil)"
| "chain R (llist_of (x # zs @ [lhd xs])) 
   chain' R xs  chain' R (LCons x (prepend zs xs))"

private lemma chain_imp_chain': "chain R xs  chain' R xs"
proof (coinduction arbitrary: xs rule: chain'.coinduct)
  case chain'
  then show ?case
  proof (cases rule: chain.cases)
    case (chain_cons zs z)
    then show ?thesis
      by (intro disjI2 exI[of _ z] exI[of _ "[]"] exI[of _ "zs"])
        (auto intro: chain.intros)
  qed simp
qed

private lemma chain'_imp_chain: "chain' R xs  chain R xs"
proof (coinduction arbitrary: xs rule: chain.coinduct)
  case chain
  then show ?case
  proof (cases rule: chain'.cases)
    case (2 y zs ys)
    then show ?thesis
      by (intro disjI2 exI[of _ "prepend zs ys"] exI[of _ y])
        (force dest!: neq_Nil_conv[THEN iffD1] elim: chain.cases chain_nontrivE
          intro: chain'.intros)
  qed simp
qed

private lemma chain_chain': "chain = chain'"
  unfolding fun_eq_iff by (metis chain_imp_chain' chain'_imp_chain)

lemma chain_prepend_coinduct[case_names chain]:
  "X x  (x. X x 
    (z. x = LCons z LNil) 
    (y xs zs. x = LCons y (prepend zs xs) 
      (X xs  chain R xs)  chain R (llist_of (y # zs @ [lhd xs]))))  chain R x"
  by (subst chain_chain', erule chain'.coinduct) (force simp: chain_chain')

end

context
  fixes R :: "'a  'a  bool"
begin

private definition pick where
  "pick x y = (SOME xs. chain R (llist_of (x # xs @ [y])))"

private lemma pick[simp]:
  assumes "R++ x y"
  shows "chain R (llist_of (x # pick x y @ [y]))"
  unfolding pick_def using tranclp_imp_exists_finite_chain_list[THEN someI_ex, OF assms] by auto

private friend_of_corec prepend where
  "prepend xs ys = (case xs of [] 
    (case ys of LNil  LNil | LCons x xs  LCons x xs) | x # xs'  LCons x (prepend xs' ys))"
  by (simp split: list.splits llist.splits) transfer_prover

private corec wit where
  "wit xs = (case xs of LCons x (LCons y xs) 
     LCons x (prepend (pick x y) (wit (LCons y xs))) | _  xs)"

private lemma
  wit_LNil[simp]: "wit LNil = LNil" and
  wit_lsingleton[simp]: "wit (LCons x LNil) = LCons x LNil" and
  wit_LCons2: "wit (LCons x (LCons y xs)) =
     (LCons x (prepend (pick x y) (wit (LCons y xs))))"
  by (subst wit.code; auto)+

private lemma lnull_wit[simp]: "lnull (wit xs)  lnull xs"
  by (subst wit.code) (auto split: llist.splits simp: Let_def)

private lemma lhd_wit[simp]: "chain R++ xs  lhd (wit xs) = lhd xs"
  by (erule chain.cases; subst wit.code) (auto split: llist.splits simp: Let_def)

private lemma LNil_eq_iff_lnull: "LNil = xs  lnull xs"
  by (cases xs) auto

lemma emb_wit[simp]: "chain R++ xs  emb xs (wit xs)"
proof (coinduction arbitrary: xs rule: emb_prepend_coinduct)
  case (emb xs)
  then show ?case
  proof (cases rule: chain.cases)
    case (chain_cons zs z)
    then show ?thesis
      by (subst (2) wit.code)
        (auto 0 3 split: llist.splits intro: exI[of _ "[]"] exI[of _ "pick z _"]
           intro!: exI[of _ "_ :: _ llist"])
  qed (auto intro!: exI[of _ LNil] exI[of _ "[]"] emb.intros)
qed

private lemma lfinite_wit[simp]:
  assumes "chain R++ xs"
  shows "lfinite (wit xs)  lfinite xs"
  using emb_wit emb_lfinite assms by blast

private lemma llast_wit[simp]:
  assumes "chain R++ xs"
  shows "llast (wit xs) = llast xs"
proof (cases "lfinite xs")
  case True
  from this assms show ?thesis
  proof (induct rule: lfinite.induct)
    case (lfinite_LConsI xs x)
    then show ?case
      by (cases xs) (auto simp: wit_LCons2 llast_LCons elim: chain_nontrivE)
  qed auto
qed (auto simp: llast_linfinite assms)

lemma chain_tranclp_imp_exists_chain:
  "chain R++ xs 
   ys. chain R ys  emb xs ys  lhd ys = lhd xs  llast ys = llast xs"
proof (intro exI[of _ "wit xs"] conjI, coinduction arbitrary: xs rule: chain_prepend_coinduct)
  case chain
  then show ?case
    by (subst (1 2) wit.code) (erule chain.cases; force split: llist.splits dest: pick)
qed auto

lemma emb_lset_mono[rotated]: "x  lset xs  emb xs ys  x  lset ys"
  by (induct x xs arbitrary: ys rule: llist.set_induct) (auto elim!: emb_LConsE)

lemma emb_Ball_lset_antimono:
  assumes "emb Xs Ys"
  shows "Y  lset Ys. x  Y  X  lset Xs. x  X"
  using emb_lset_mono[OF assms] by blast

lemma emb_lfinite_antimono[rotated]: "lfinite ys  emb xs ys  lfinite xs"
  by (induct ys arbitrary: xs rule: lfinite_prepend_induct)
    (force elim!: emb_LNil2E simp: LNil_eq_iff_lnull prepend_LCons elim: emb.cases)+

lemma emb_Liminf_llist_mono_aux:
  assumes "emb Xs Ys" and "¬ lfinite Xs" and "¬ lfinite Ys" and "ji. x  lnth Ys j"
  shows "ji. x  lnth Xs j"
using assms proof (induct i arbitrary: Xs Ys rule: less_induct)
  case (less i)
  then show ?case
  proof (cases i)
    case 0
    then show ?thesis
      using emb_Ball_lset_antimono[OF less(2), of x] less(5)
      unfolding Ball_def in_lset_conv_lnth simp_thms
        not_lfinite_llength[OF less(3)] not_lfinite_llength[OF less(4)] enat_ord_code subset_eq
      by blast
  next
    case [simp]: (Suc nat)
    from less(2,3) obtain xs as b bs where
      [simp]: "Xs = LCons b xs" "Ys = prepend as (LCons b bs)" and "emb xs bs"
      by (auto elim: emb.cases)
    have IH: "kj. x  lnth xs k" if "kj. x  lnth bs k" "j < i" for j
      using that less(1)[OF _ emb xs bs] less(3,4) by auto
    from less(5) have "ki - length as - 1. x  lnth xs k"
      by (intro IH allI)
        (drule spec[of _ "_ + length as + 1"], auto simp: lnth_prepend lnth_LCons')
    then show ?thesis
      by (auto simp: lnth_LCons')
  qed
qed

lemma emb_Liminf_llist_infinite:
  assumes "emb Xs Ys" and "¬ lfinite Xs"
  shows "Liminf_llist Ys  Liminf_llist Xs"
proof -
  from assms have "¬ lfinite Ys"
    using emb_lfinite_antimono by blast
  with assms show ?thesis
    unfolding Liminf_llist_def by (auto simp: not_lfinite_llength dest: emb_Liminf_llist_mono_aux)
qed

lemma emb_lmap: "emb xs ys  emb (lmap f xs) (lmap f ys)"
proof (coinduction arbitrary: xs ys rule: emb.coinduct)
  case emb
  show ?case
  proof (cases xs)
    case xs: (LCons x xs')

    obtain ysa0 and zs0 where
      ys: "ys = prepend zs0 (LCons x ysa0)" and
      emb': "emb xs' ysa0"
      using emb_LConsE[OF emb[unfolded xs]] by metis

    let ?xa = "f x"
    let ?xsa = "lmap f xs'"
    let ?zs = "map f zs0"
    let ?ysa = "lmap f ysa0"

    have "lmap f xs = LCons ?xa ?xsa"
      unfolding xs by simp
    moreover have "lmap f ys = prepend ?zs (LCons ?xa ?ysa)"
      unfolding ys by simp
    moreover have "xsa ysa. ?xsa = lmap f xsa  ?ysa = lmap f ysa  emb xsa ysa"
      using emb' by blast
    ultimately show ?thesis
      by blast
  qed (simp add: emb_lfinite[OF emb])
qed

end

lemma chain_inf_llist_if_infinite_chain_function:
  assumes "i. r (f (Suc i)) (f i)"
  shows "¬ lfinite (inf_llist f)  chain r¯¯ (inf_llist f)"
  using assms by (simp add: lnth_rel_chain)

lemma infinite_chain_function_iff_infinite_chain_llist:
  "(f. i. r (f (Suc i)) (f i))  (c. ¬ lfinite c  chain r¯¯ c)"
  using chain_inf_llist_if_infinite_chain_function infinite_chain_lnth_rel by blast

lemma wfP_iff_no_infinite_down_chain_llist: "wfP r  (c. ¬ lfinite c  chain r¯¯ c)"
proof -
  have "wfP r   wf {(x, y). r x y}"
    unfolding wfp_def by auto
  also have "  (f. i. (f (Suc i), f i)  {(x, y). r x y})"
    using wf_iff_no_infinite_down_chain by blast
  also have "  (f. i. r (f (Suc i)) (f i))"
    by auto
  also have "  (c. ¬lfinite c  chain r¯¯ c)"
    using infinite_chain_function_iff_infinite_chain_llist by blast
  finally show ?thesis
    by auto
qed


subsection ‹Full Chains›

coinductive full_chain :: "('a  'a  bool)  'a llist  bool" for R :: "'a  'a  bool" where
  full_chain_singleton: "(y. ¬ R x y)  full_chain R (LCons x LNil)"
| full_chain_cons: "full_chain R xs  R x (lhd xs)  full_chain R (LCons x xs)"

lemma
  full_chain_LNil[simp]: "¬ full_chain R LNil" and
  full_chain_not_lnull: "full_chain R xs  ¬ lnull xs"
  by (auto elim: full_chain.cases)

lemma full_chain_ldropn:
  assumes full: "full_chain R xs" and "enat n < llength xs"
  shows "full_chain R (ldropn n xs)"
  using assms
  by (induct n arbitrary: xs, simp,
      metis full_chain.cases ldrop_eSuc_ltl ldropn_LNil ldropn_eq_LNil ltl_simps(2) not_less)

lemma full_chain_iff_chain:
  "full_chain R xs  chain R xs  (lfinite xs  (y. ¬ R (llast xs) y))"
proof (intro iffI conjI impI allI; (elim conjE)?)
  assume full: "full_chain R xs"

  show chain: "chain R xs"
    using full by (coinduction arbitrary: xs) (auto elim: full_chain.cases)

  {
    fix y
    assume "lfinite xs"
    then obtain n where
      suc_n: "Suc n = llength xs"
      by (metis chain chain_length_pos lessE less_enatE lfinite_conv_llength_enat)

    have "full_chain R (ldropn n xs)"
      by (rule full_chain_ldropn[OF full]) (use suc_n Suc_ile_eq in force)
    moreover have "ldropn n xs = LCons (llast xs) LNil"
      using suc_n by (metis enat_le_plus_same(2) enat_ord_simps(2) gen_llength_def
          ldropn_Suc_conv_ldropn ldropn_all lessI llast_ldropn llast_singleton llength_code)
    ultimately show "¬ R (llast xs) y"
      by (auto elim: full_chain.cases)
  }
next
  assume
    "chain R xs" and
    "lfinite xs  (y. ¬ R (llast xs) y)"
  then show "full_chain R xs"
    by (coinduction arbitrary: xs) (erule chain.cases, simp, metis lfinite_LConsI llast_LCons)
qed

lemma full_chain_imp_chain: "full_chain R xs  chain R xs"
  using full_chain_iff_chain by blast

lemma full_chain_length_pos: "full_chain R xs  llength xs > 0"
  by (fact chain_length_pos[OF full_chain_imp_chain])

lemma full_chain_lnth_rel:
  "full_chain R xs  enat (Suc j) < llength xs  R (lnth xs j) (lnth xs (Suc j))"
  by (fact chain_lnth_rel[OF full_chain_imp_chain])

lemma full_chain_lnth_not_rel:
  assumes
    full: "full_chain R xs" and
    sj: "enat (Suc j) = llength xs"
  shows "¬ R (lnth xs j) y"
proof -
  have "lfinite xs"
    by (metis llength_eq_enat_lfiniteD sj)
  hence "¬ R (llast xs) y"
    using full_chain_iff_chain full by metis
  thus ?thesis
    by (metis eSuc_enat llast_conv_lnth sj)
qed

inductive_cases full_chain_consE: "full_chain R (LCons x xs)"
inductive_cases full_chain_nontrivE: "full_chain R (LCons x (LCons y xs))"

lemma full_chain_tranclp_imp_exists_full_chain:
  assumes full: "full_chain R++ xs"
  shows "ys. full_chain R ys  emb xs ys  lhd ys = lhd xs  llast ys = llast xs"
proof -
  obtain ys where ys:
    "chain R ys" "emb xs ys" "lhd ys = lhd xs" "llast ys = llast xs"
    using full_chain_imp_chain[OF full] chain_tranclp_imp_exists_chain by blast
  have "full_chain R ys"
    using ys(1,4) emb_lfinite[OF ys(2)] full unfolding full_chain_iff_chain by auto
  then show ?thesis
    using ys(2-4) by auto
qed

end