# Theory TLList

```(*  Title:       Terminated coinductive list
Author:      Andreas Lochbihler
Maintainer:  Andreas Lochbihler
*)

section ‹Terminated coinductive lists and their operations›

theory TLList imports
Coinductive_List
begin

text ‹
Terminated coinductive lists ‹('a, 'b) tllist› are the codatatype defined by the construtors
‹TNil› of type ‹'b ⇒ ('a, 'b) tllist› and
‹TCons› of type ‹'a ⇒ ('a, 'b) tllist ⇒ ('a, 'b) tllist›.
›

subsection ‹Auxiliary lemmas›

lemma split_fst: "R (fst p) = (∀x y. p = (x, y) ⟶ R x)"
by(cases p) simp

lemma split_fst_asm: "R (fst p) ⟷ (¬ (∃x y. p = (x, y) ∧ ¬ R x))"
by(cases p) simp

subsection ‹Type definition›

consts terminal0 :: "'a"

codatatype (tset: 'a, 'b) tllist =
TNil (terminal : 'b)
| TCons (thd : 'a) (ttl : "('a, 'b) tllist")
for
map: tmap
rel: tllist_all2
where
"thd (TNil _) = undefined"
| "ttl (TNil b) = TNil b"
| "terminal (TCons _ xs) = terminal0 xs"

terminal0 == "terminal0::('a, 'b) tllist ⇒ 'b"
begin

partial_function (tailrec) terminal0
where "terminal0 xs = (if is_TNil xs then case_tllist id undefined xs else terminal0 (ttl xs))"

end

lemma terminal0_terminal [simp]: "terminal0 = terminal"
apply(rule ext)
apply(subst terminal0.simps)
apply(case_tac x)
done

lemmas terminal_TNil [code, nitpick_simp] = tllist.sel(1)

lemma terminal_TCons [simp, code, nitpick_simp]: "terminal (TCons x xs) = terminal xs"
by simp

declare tllist.sel(2) [simp del]

primcorec unfold_tllist :: "('a ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ ('a ⇒ 'c) ⇒ ('a ⇒ 'a) ⇒ 'a ⇒ ('c, 'b) tllist" where
"p a ⟹ unfold_tllist p g1 g21 g22 a = TNil (g1 a)" |
"_ ⟹ unfold_tllist p g1 g21 g22 a =
TCons (g21 a) (unfold_tllist p g1 g21 g22 (g22 a))"

declare
unfold_tllist.ctr(1) [simp]
tllist.corec(1) [simp]

subsection ‹Code generator setup›

text ‹Test quickcheck setup›

lemma "xs = TNil x"
quickcheck[random, expect=counterexample]
quickcheck[exhaustive, expect=counterexample]
oops

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

text ‹More lemmas about generated constants›

lemma ttl_unfold_tllist:
"ttl (unfold_tllist IS_TNIL TNIL THD TTL a) =
(if IS_TNIL a then TNil (TNIL a) else unfold_tllist IS_TNIL TNIL THD TTL (TTL a))"
by(simp)

lemma is_TNil_ttl [simp]: "is_TNil xs ⟹ is_TNil (ttl xs)"
by(cases xs) simp_all

lemma terminal_ttl [simp]: "terminal (ttl xs) = terminal xs"
by(cases xs) simp_all

lemma unfold_tllist_eq_TNil [simp]:
"unfold_tllist IS_TNIL TNIL THD TTL a = TNil b ⟷ IS_TNIL a ∧ b = TNIL a"

lemma TNil_eq_unfold_tllist [simp]:
"TNil b = unfold_tllist IS_TNIL TNIL THD TTL a ⟷ IS_TNIL a ∧ b = TNIL a"

lemma tmap_is_TNil: "is_TNil xs ⟹ tmap f g xs = TNil (g (terminal xs))"

declare tllist.map_sel(2)[simp]

lemma ttl_tmap [simp]: "ttl (tmap f g xs) = tmap f g (ttl xs)"
by(cases xs) simp_all

lemma tmap_eq_TNil_conv:
"tmap f g xs = TNil y ⟷ (∃y'. xs = TNil y' ∧ g y' = y)"
by(cases xs) simp_all

lemma TNil_eq_tmap_conv:
"TNil y = tmap f g xs ⟷ (∃y'. xs = TNil y' ∧ g y' = y)"
by(cases xs) auto

declare tllist.set_sel(1)[simp]

lemma tset_ttl: "tset (ttl xs) ⊆ tset xs"
by(cases xs) auto

lemma in_tset_ttlD: "x ∈ tset (ttl xs) ⟹ x ∈ tset xs"
using tset_ttl[of xs] by auto

theorem tllist_set_induct[consumes 1, case_names find step]:
assumes "x ∈ tset xs" and "⋀xs. ¬ is_TNil xs ⟹ P (thd xs) xs"
and "⋀xs y. ⟦¬ is_TNil xs; y ∈ tset (ttl xs); P y (ttl xs)⟧ ⟹ P y xs"
shows "P x xs"
using assms by(induct)(fastforce simp del: tllist.disc(2) iff: tllist.disc(2), auto)

theorem set2_tllist_induct[consumes 1, case_names find step]:
assumes "x ∈ set2_tllist xs" and "⋀xs. is_TNil xs ⟹ P (terminal xs) xs"
and "⋀xs y. ⟦¬ is_TNil xs; y ∈ set2_tllist (ttl xs); P y (ttl xs)⟧ ⟹ P y xs"
shows "P x xs"
using assms by(induct)(fastforce simp del: tllist.disc(1) iff: tllist.disc(1), auto)

subsection ‹Connection with @{typ "'a llist"}›

context fixes b :: 'b begin
primcorec tllist_of_llist :: "'a llist ⇒ ('a, 'b) tllist" where
"tllist_of_llist xs = (case xs of LNil ⇒ TNil b | LCons x xs' ⇒ TCons x (tllist_of_llist xs'))"
end

primcorec llist_of_tllist :: "('a, 'b) tllist ⇒ 'a llist"
where "llist_of_tllist xs = (case xs of TNil _ ⇒ LNil | TCons x xs' ⇒ LCons x (llist_of_tllist xs'))"

simps_of_case tllist_of_llist_simps [simp, code, nitpick_simp]: tllist_of_llist.code

lemmas tllist_of_llist_LNil = tllist_of_llist_simps(1)
and tllist_of_llist_LCons = tllist_of_llist_simps(2)

lemma terminal_tllist_of_llist_lnull [simp]:
"lnull xs ⟹ terminal (tllist_of_llist b xs) = b"
unfolding lnull_def by simp

declare tllist_of_llist.sel(1)[simp del]

lemma lhd_LNil: "lhd LNil = undefined"

lemma thd_TNil: "thd (TNil b) = undefined"

lemma thd_tllist_of_llist [simp]: "thd (tllist_of_llist b xs) = lhd xs"

lemma ttl_tllist_of_llist [simp]: "ttl (tllist_of_llist b xs) = tllist_of_llist b (ltl xs)"
by(cases xs) simp_all

lemma llist_of_tllist_eq_LNil:
"llist_of_tllist xs = LNil ⟷ is_TNil xs"
using llist_of_tllist.disc_iff(1) unfolding lnull_def .

simps_of_case llist_of_tllist_simps [simp, code, nitpick_simp]: llist_of_tllist.code

lemmas llist_of_tllist_TNil = llist_of_tllist_simps(1)
and llist_of_tllist_TCons = llist_of_tllist_simps(2)

declare llist_of_tllist.sel [simp del]

lemma lhd_llist_of_tllist [simp]: "¬ is_TNil xs ⟹ lhd (llist_of_tllist xs) = thd xs"
by(cases xs) simp_all

lemma ltl_llist_of_tllist [simp]:
"ltl (llist_of_tllist xs) = llist_of_tllist (ttl xs)"
by(cases xs) simp_all

lemma tllist_of_llist_cong [cong]:
assumes "xs = xs'" "lfinite xs' ⟹ b = b'"
shows "tllist_of_llist b xs = tllist_of_llist b' xs'"
proof(unfold ‹xs = xs'›)
from assms have "lfinite xs' ⟶ b = b'" by simp
thus "tllist_of_llist b xs' = tllist_of_llist b' xs'"
by(coinduction arbitrary: xs') auto
qed

lemma llist_of_tllist_inverse [simp]:
"tllist_of_llist (terminal b) (llist_of_tllist b) = b"
by(coinduction arbitrary: b) simp_all

lemma tllist_of_llist_eq [simp]: "tllist_of_llist b' xs = TNil b ⟷ b = b' ∧ xs = LNil"
by(cases xs) auto

lemma TNil_eq_tllist_of_llist [simp]: "TNil b = tllist_of_llist b' xs ⟷ b = b' ∧ xs = LNil"
by(cases xs) auto

lemma tllist_of_llist_inject [simp]:
"tllist_of_llist b xs = tllist_of_llist c ys ⟷ xs = ys ∧ (lfinite ys ⟶ b = c)"
(is "?lhs ⟷ ?rhs")
proof(intro iffI conjI impI)
assume ?rhs
thus ?lhs by(auto intro: tllist_of_llist_cong)
next
assume ?lhs
thus "xs = ys"
by(coinduction arbitrary: xs ys)(auto simp add: lnull_def neq_LNil_conv)
assume "lfinite ys"
thus "b = c" using ‹?lhs›
unfolding ‹xs = ys› by(induct) simp_all
qed

lemma tllist_of_llist_inverse [simp]:
"llist_of_tllist (tllist_of_llist b xs) = xs"
by(coinduction arbitrary: xs) auto

definition cr_tllist :: "('a llist × 'b) ⇒ ('a, 'b) tllist ⇒ bool"
where "cr_tllist ≡ (λ(xs, b) ys. tllist_of_llist b xs = ys)"

lemma Quotient_tllist:
"Quotient (λ(xs, a) (ys, b). xs = ys ∧ (lfinite ys ⟶ a = b))
(λ(xs, a). tllist_of_llist a xs) (λys. (llist_of_tllist ys, terminal ys)) cr_tllist"
unfolding Quotient_alt_def cr_tllist_def by(auto intro: tllist_of_llist_cong)

lemma reflp_tllist: "reflp (λ(xs, a) (ys, b). xs = ys ∧ (lfinite ys ⟶ a = b))"

setup_lifting Quotient_tllist reflp_tllist

context includes lifting_syntax
begin

lemma TNil_transfer [transfer_rule]:
"(B ===> pcr_tllist A B) (Pair LNil) TNil"

lemma TCons_transfer [transfer_rule]:
"(A ===> pcr_tllist A B ===> pcr_tllist A B) (apfst ∘ LCons) TCons"
by(force simp add: pcr_tllist_def llist_all2_LCons1 cr_tllist_def)

lemma tmap_tllist_of_llist:
"tmap f g (tllist_of_llist b xs) = tllist_of_llist (g b) (lmap f xs)"
by(coinduction arbitrary: xs)(auto simp add: tmap_is_TNil)

lemma tmap_transfer [transfer_rule]:
"((=) ===> (=) ===> pcr_tllist (=) (=) ===> pcr_tllist (=) (=)) (map_prod ∘ lmap) tmap"
by(force simp add: cr_tllist_def tllist.pcr_cr_eq tmap_tllist_of_llist)

lemma lset_llist_of_tllist [simp]:
"lset (llist_of_tllist xs) = tset xs" (is "?lhs = ?rhs")
proof(intro set_eqI iffI)
fix x
assume "x ∈ ?lhs"
thus "x ∈ ?rhs"
by(induct "llist_of_tllist xs" arbitrary: xs rule: llist_set_induct)(auto simp: tllist.set_sel(2))
next
fix x
assume "x ∈ ?rhs"
thus "x ∈ ?lhs"
proof(induct rule: tllist_set_induct)
case (find xs)
thus ?case by(cases xs) auto
next
case step
thus ?case
by(auto simp add: ltl_llist_of_tllist[symmetric] simp del: ltl_llist_of_tllist dest: in_lset_ltlD)
qed
qed

lemma tset_tllist_of_llist [simp]:
"tset (tllist_of_llist b xs) = lset xs"

lemma tset_transfer [transfer_rule]:
"(pcr_tllist (=) (=) ===> (=)) (lset ∘ fst) tset"

lemma is_TNil_transfer [transfer_rule]:
"(pcr_tllist (=) (=) ===> (=)) (λ(xs, b). lnull xs) is_TNil"

lemma thd_transfer [transfer_rule]:
"(pcr_tllist (=) (=) ===> (=)) (lhd ∘ fst) thd"

lemma ttl_transfer [transfer_rule]:
"(pcr_tllist A B ===> pcr_tllist A B) (apfst ltl) ttl"
by(force simp add: pcr_tllist_def cr_tllist_def intro: llist_all2_ltlI)

lemma llist_of_tllist_transfer [transfer_rule]:
"(pcr_tllist (=) B ===> (=)) fst llist_of_tllist"
by(auto simp add: pcr_tllist_def cr_tllist_def llist.rel_eq)

lemma tllist_of_llist_transfer [transfer_rule]:
"((=) ===> (=) ===> pcr_tllist (=) (=)) (λb xs. (xs, b)) tllist_of_llist"

lemma terminal_tllist_of_llist_lfinite [simp]:
"lfinite xs ⟹ terminal (tllist_of_llist b xs) = b"
by(induct rule: lfinite.induct) simp_all

lemma set2_tllist_tllist_of_llist [simp]:
"set2_tllist (tllist_of_llist b xs) = (if lfinite xs then {b} else {})"
proof(cases "lfinite xs")
case True
thus ?thesis by(induct) auto
next
case False
{ fix x
assume "x ∈ set2_tllist (tllist_of_llist b xs)"
hence False using False
by(induct "tllist_of_llist b xs" arbitrary: xs rule: set2_tllist_induct) fastforce+ }
thus ?thesis using False by auto
qed

lemma set2_tllist_transfer [transfer_rule]:
"(pcr_tllist A B ===> rel_set B) (λ(xs, b). if lfinite xs then {b} else {}) set2_tllist"
by(auto 4 4 simp add: pcr_tllist_def cr_tllist_def dest: llist_all2_lfiniteD intro: rel_setI)

lemma tllist_all2_transfer [transfer_rule]:
"((=) ===> (=) ===> pcr_tllist (=) (=) ===> pcr_tllist (=) (=) ===> (=))
(λP Q (xs, b) (ys, b'). llist_all2 P xs ys ∧ (lfinite xs ⟶ Q b b')) tllist_all2"
unfolding tllist.pcr_cr_eq
apply(rule rel_funI)+
apply(clarsimp simp add: cr_tllist_def llist_all2_def tllist_all2_def)
apply(safe elim!: GrpE)
apply simp_all
apply(rule_tac b="tllist_of_llist (b, ba) bb" in relcomppI)
apply(auto intro!: GrpI simp add: tmap_tllist_of_llist)[2]
apply(rule_tac b="tllist_of_llist (b, ba) bb" in relcomppI)
apply(auto simp add: tmap_tllist_of_llist intro!: GrpI split: if_split_asm)[2]
apply(rule_tac b="llist_of_tllist bb" in relcomppI)
apply(auto intro!: GrpI)
apply(transfer, auto intro: GrpI split: if_split_asm)+
done

subsection ‹Library function definitions›

text ‹
We lift the constants from @{typ "'a llist"} to @{typ "('a, 'b) tllist"} using the lifting package.
This way, many results are transferred easily.
›

lift_definition tappend :: "('a, 'b) tllist ⇒ ('b ⇒ ('a, 'c) tllist) ⇒ ('a, 'c) tllist"
is "λ(xs, b) f. apfst (lappend xs) (f b)"

lift_definition lappendt :: "'a llist ⇒ ('a, 'b) tllist ⇒ ('a, 'b) tllist"
is "apfst ∘ lappend"

lift_definition tfilter :: "'b ⇒ ('a ⇒ bool) ⇒ ('a, 'b) tllist ⇒ ('a, 'b) tllist"
is "λb P (xs, b'). (lfilter P xs, if lfinite xs then b' else b)"

lift_definition tconcat :: "'b ⇒ ('a llist, 'b) tllist ⇒ ('a, 'b) tllist"
is "λb (xss, b'). (lconcat xss, if lfinite xss then b' else b)"

lift_definition tnth :: "('a, 'b) tllist ⇒ nat ⇒ 'a"
is "lnth ∘ fst" by(auto)

lift_definition tlength :: "('a, 'b) tllist ⇒ enat"
is "llength ∘ fst" by auto

lift_definition tdropn :: "nat ⇒ ('a, 'b) tllist ⇒ ('a, 'b) tllist"
is "apfst ∘ ldropn" by auto

abbreviation tfinite :: "('a, 'b) tllist ⇒ bool"
where "tfinite xs ≡ lfinite (llist_of_tllist xs)"

subsection ‹@{term "tfinite"}›

lemma tfinite_induct [consumes 1, case_names TNil TCons]:
assumes "tfinite xs"
and "⋀y. P (TNil y)"
and "⋀x xs. ⟦tfinite xs; P xs⟧ ⟹ P (TCons x xs)"
shows "P xs"
using assms
by transfer (clarsimp, erule lfinite.induct)

lemma is_TNil_tfinite [simp]: "is_TNil xs ⟹ tfinite xs"
by transfer clarsimp

subsection ‹The terminal element @{term "terminal"}›

lemma terminal_tinfinite:
assumes "¬ tfinite xs"
shows "terminal xs = undefined"
unfolding terminal0_terminal[symmetric]
using assms
apply(rule contrapos_np)
by(induct xs rule: terminal0.raw_induct[rotated 1, OF refl, consumes 1])(auto split: tllist.split_asm)

lemma terminal_tllist_of_llist:
"terminal (tllist_of_llist y xs) = (if lfinite xs then y else undefined)"

lemma terminal_transfer [transfer_rule]:
"(pcr_tllist A (=) ===> (=)) (λ(xs, b). if lfinite xs then b else undefined) terminal"
by(force simp add: cr_tllist_def pcr_tllist_def terminal_tllist_of_llist dest: llist_all2_lfiniteD)

lemma terminal_tmap [simp]: "tfinite xs ⟹ terminal (tmap f g xs) = g (terminal xs)"
by(induct rule: tfinite_induct) simp_all

subsection ‹@{term "tmap"}›

lemma tmap_eq_TCons_conv:
"tmap f g xs = TCons y ys ⟷
(∃z zs. xs = TCons z zs ∧ f z = y ∧ tmap f g zs = ys)"
by(cases xs) simp_all

lemma TCons_eq_tmap_conv:
"TCons y ys = tmap f g xs ⟷
(∃z zs. xs = TCons z zs ∧ f z = y ∧ tmap f g zs = ys)"
by(cases xs) auto

subsection ‹Appending two terminated lazy lists @{term "tappend" }›

lemma tappend_TNil [simp, code, nitpick_simp]:
"tappend (TNil b) f = f b"
by transfer auto

lemma tappend_TCons [simp, code, nitpick_simp]:
"tappend (TCons a tr) f = TCons a (tappend tr f)"
by transfer(auto simp add: apfst_def map_prod_def split: prod.splits)

lemma tappend_TNil2 [simp]:
"tappend xs TNil = xs"
by transfer auto

lemma tappend_assoc: "tappend (tappend xs f) g = tappend xs (λb. tappend (f b) g)"
by transfer(auto simp add: split_beta lappend_assoc)

lemma terminal_tappend:
"terminal (tappend xs f) = (if tfinite xs then terminal (f (terminal xs)) else terminal xs)"

lemma tfinite_tappend: "tfinite (tappend xs f) ⟷ tfinite xs ∧ tfinite (f (terminal xs))"
by transfer auto

lift_definition tcast :: "('a, 'b) tllist ⇒ ('a, 'c) tllist"
is "λ(xs, a). (xs, undefined)" by clarsimp

lemma tappend_inf: "¬ tfinite xs ⟹ tappend xs f = tcast xs"
by(transfer)(auto simp add: apfst_def map_prod_def split_beta lappend_inf)

text ‹@{term tappend} is the monadic bind on @{typ "('a, 'b) tllist"}›

lemmas tllist_monad = tappend_TNil tappend_TNil2 tappend_assoc

subsection ‹Appending a terminated lazy list to a lazy list @{term "lappendt"}›

lemma lappendt_LNil [simp, code, nitpick_simp]: "lappendt LNil tr = tr"
by transfer auto

lemma lappendt_LCons [simp, code, nitpick_simp]:
"lappendt (LCons x xs) tr = TCons x (lappendt xs tr)"
by transfer auto

lemma terminal_lappendt_lfinite [simp]:
"lfinite xs ⟹ terminal (lappendt xs ys) = terminal ys"
by transfer auto

lemma tllist_of_llist_eq_lappendt_conv:
"tllist_of_llist a xs = lappendt ys zs ⟷
(∃xs' a'. xs = lappend ys xs' ∧ zs = tllist_of_llist a' xs' ∧ (lfinite ys ⟶ a = a'))"
by transfer auto

lemma tset_lappendt_lfinite [simp]:
"lfinite xs ⟹ tset (lappendt xs ys) = lset xs ∪ tset ys"
by transfer auto

subsection ‹Filtering terminated lazy lists @{term tfilter}›

lemma tfilter_TNil [simp]:
"tfilter b' P (TNil b) = TNil b"
by transfer auto

lemma tfilter_TCons [simp]:
"tfilter b P (TCons a tr) = (if P a then TCons a (tfilter b P tr) else tfilter b P tr)"
by transfer auto

lemma is_TNil_tfilter[simp]:
"is_TNil (tfilter y P xs) ⟷ (∀x ∈ tset xs. ¬ P x)"
by transfer auto

lemma tfilter_empty_conv:
"tfilter y P xs = TNil y' ⟷ (∀x ∈ tset xs. ¬ P x) ∧ (if tfinite xs then terminal xs = y' else y = y')"

lemma tfilter_eq_TConsD:
"tfilter a P ys = TCons x xs ⟹
∃us vs. ys = lappendt us (TCons x vs) ∧ lfinite us ∧ (∀u∈lset us. ¬ P u) ∧ P x ∧ xs = tfilter a P vs"
by transfer(fastforce dest: lfilter_eq_LConsD[OF sym])

text ‹Use a version of @{term "tfilter"} for code generation that does not evaluate the first argument›

definition tfilter' :: "(unit ⇒ 'b) ⇒ ('a ⇒ bool) ⇒ ('a, 'b) tllist ⇒ ('a, 'b) tllist"
where [simp, code del]: "tfilter' b = tfilter (b ())"

lemma tfilter_code [code, code_unfold]:
"tfilter = (λb. tfilter' (λ_. b))"
by simp

lemma tfilter'_code [code]:
"tfilter' b' P (TNil b) = TNil b"
"tfilter' b' P (TCons a tr) = (if P a then TCons a (tfilter' b' P tr) else tfilter' b' P tr)"
by simp_all

end

hide_const (open) tfilter'

subsection ‹Concatenating a terminated lazy list of lazy lists @{term tconcat}›

lemma tconcat_TNil [simp]: "tconcat b (TNil b') = TNil b'"
by transfer auto

lemma tconcat_TCons [simp]: "tconcat b (TCons a tr) = lappendt a (tconcat b tr)"
by transfer auto

text ‹Use a version of @{term "tconcat"} for code generation that does not evaluate the first argument›

definition tconcat' :: "(unit ⇒ 'b) ⇒ ('a llist, 'b) tllist ⇒ ('a, 'b) tllist"
where [simp, code del]: "tconcat' b = tconcat (b ())"

lemma tconcat_code [code, code_unfold]: "tconcat = (λb. tconcat' (λ_. b))"
by simp

lemma tconcat'_code [code]:
"tconcat' b (TNil b') = TNil b'"
"tconcat' b (TCons a tr) = lappendt a (tconcat' b tr)"
by simp_all

hide_const (open) tconcat'

subsection ‹@{term tllist_all2}›

lemmas tllist_all2_TNil = tllist.rel_inject(1)
lemmas tllist_all2_TCons = tllist.rel_inject(2)

lemma tllist_all2_TNil1: "tllist_all2 P Q (TNil b) ts ⟷ (∃b'. ts = TNil b' ∧ Q b b')"
by transfer auto

lemma tllist_all2_TNil2: "tllist_all2 P Q ts (TNil b') ⟷ (∃b. ts = TNil b ∧ Q b b')"
by transfer auto

lemma tllist_all2_TCons1:
"tllist_all2 P Q (TCons x ts) ts' ⟷ (∃x' ts''. ts' = TCons x' ts'' ∧ P x x' ∧ tllist_all2 P Q ts ts'')"
by transfer(fastforce simp add: llist_all2_LCons1 dest: llist_all2_lfiniteD)

lemma tllist_all2_TCons2:
"tllist_all2 P Q ts' (TCons x ts) ⟷ (∃x' ts''. ts' = TCons x' ts'' ∧ P x' x ∧ tllist_all2 P Q ts'' ts)"
by transfer(fastforce simp add: llist_all2_LCons2 dest: llist_all2_lfiniteD)

lemma tllist_all2_coinduct [consumes 1, case_names tllist_all2, case_conclusion tllist_all2 is_TNil TNil TCons, coinduct pred: tllist_all2]:
assumes "X xs ys"
and "⋀xs ys. X xs ys ⟹
(is_TNil xs ⟷ is_TNil ys) ∧
(is_TNil xs ⟶ is_TNil ys ⟶ R (terminal xs) (terminal ys)) ∧
(¬ is_TNil xs ⟶ ¬ is_TNil ys ⟶ P (thd xs) (thd ys) ∧ (X (ttl xs) (ttl ys) ∨ tllist_all2 P R (ttl xs) (ttl ys)))"
shows "tllist_all2 P R xs ys"
using assms
apply(transfer fixing: P R)
apply clarsimp
apply(rule conjI)
apply(erule llist_all2_coinduct, blast, blast)
apply (rule impI)
subgoal premises prems for X xs b ys c
proof -
from ‹lfinite xs› ‹X (xs, b) (ys, c)›
show "R b c"
by(induct arbitrary: ys rule: lfinite_induct)(auto dest: prems(2))
qed
done

lemma tllist_all2_cases[consumes 1, case_names TNil TCons, cases pred]:
assumes "tllist_all2 P Q xs ys"
obtains (TNil) b b' where "xs = TNil b" "ys = TNil b'" "Q b b'"
| (TCons) x xs' y ys'
where "xs = TCons x xs'" and "ys = TCons y ys'"
and "P x y" and "tllist_all2 P Q xs' ys'"
using assms
by(cases xs)(fastforce simp add: tllist_all2_TCons1 tllist_all2_TNil1)+

lemma tllist_all2_tmap1:
"tllist_all2 P Q (tmap f g xs) ys ⟷ tllist_all2 (λx. P (f x)) (λx. Q (g x)) xs ys"

lemma tllist_all2_tmap2:
"tllist_all2 P Q xs (tmap f g ys) ⟷ tllist_all2 (λx y. P x (f y)) (λx y. Q x (g y)) xs ys"

lemma tllist_all2_mono:
"⟦ tllist_all2 P Q xs ys; ⋀x y. P x y ⟹ P' x y; ⋀x y. Q x y ⟹ Q' x y ⟧
⟹ tllist_all2 P' Q' xs ys"
by transfer(auto elim!: llist_all2_mono)

lemma tllist_all2_tlengthD: "tllist_all2 P Q xs ys ⟹ tlength xs = tlength ys"
by(transfer)(auto dest: llist_all2_llengthD)

lemma tllist_all2_tfiniteD: "tllist_all2 P Q xs ys ⟹ tfinite xs = tfinite ys"
by(transfer)(auto dest: llist_all2_lfiniteD)

lemma tllist_all2_tfinite1_terminalD:
"⟦ tllist_all2 P Q xs ys; tfinite xs ⟧ ⟹ Q (terminal xs) (terminal ys)"
by(frule tllist_all2_tfiniteD)(transfer, auto)

lemma tllist_all2_tfinite2_terminalD:
"⟦ tllist_all2 P Q xs ys; tfinite ys ⟧ ⟹ Q (terminal xs) (terminal ys)"
by(metis tllist_all2_tfinite1_terminalD tllist_all2_tfiniteD)

lemma tllist_all2D_llist_all2_llist_of_tllist:
"tllist_all2 P Q xs ys ⟹ llist_all2 P (llist_of_tllist xs) (llist_of_tllist ys)"
by(transfer) auto

lemma tllist_all2_is_TNilD:
"tllist_all2 P Q xs ys ⟹ is_TNil xs ⟷ is_TNil ys"
by(cases xs)(auto simp add: tllist_all2_TNil1 tllist_all2_TCons1)

lemma tllist_all2_thdD:
"⟦ tllist_all2 P Q xs ys; ¬ is_TNil xs ∨ ¬ is_TNil ys ⟧ ⟹ P (thd xs) (thd ys)"
by(cases xs)(auto simp add: tllist_all2_TNil1 tllist_all2_TCons1)

lemma tllist_all2_ttlI:
"⟦ tllist_all2 P Q xs ys; ¬ is_TNil xs ∨ ¬ is_TNil ys ⟧ ⟹ tllist_all2 P Q (ttl xs) (ttl ys)"
by(cases xs)(auto simp add: tllist_all2_TNil1 tllist_all2_TCons1)

lemma tllist_all2_refl:
"tllist_all2 P Q xs xs ⟷ (∀x ∈ tset xs. P x x) ∧ (tfinite xs ⟶ Q (terminal xs) (terminal xs))"
by transfer(auto)

lemma tllist_all2_reflI:
"⟦ ⋀x. x ∈ tset xs ⟹ P x x; tfinite xs ⟹ Q (terminal xs) (terminal xs) ⟧
⟹ tllist_all2 P Q xs xs"

lemma tllist_all2_conv_all_tnth:
"tllist_all2 P Q xs ys ⟷
tlength xs = tlength ys ∧
(∀n. enat n < tlength xs ⟶ P (tnth xs n) (tnth ys n)) ∧
(tfinite xs ⟶ Q (terminal xs) (terminal ys))"
by transfer(auto 4 4 simp add: llist_all2_conv_all_lnth split: if_split_asm dest: lfinite_llength_enat not_lfinite_llength)

lemma tllist_all2_tnthD:
"⟦ tllist_all2 P Q xs ys; enat n < tlength xs ⟧
⟹ P (tnth xs n) (tnth ys n)"

lemma tllist_all2_tnthD2:
"⟦ tllist_all2 P Q xs ys; enat n < tlength ys ⟧
⟹ P (tnth xs n) (tnth ys n)"

lemmas tllist_all2_eq = tllist.rel_eq

lemma tmap_eq_tmap_conv_tllist_all2:
"tmap f g xs = tmap f' g' ys ⟷
tllist_all2 (λx y. f x = f' y) (λx y. g x = g' y) xs ys"
apply transfer
apply(auto dest: llist_all2_lfiniteD)
done

lemma tllist_all2_trans:
"⟦ tllist_all2 P Q xs ys; tllist_all2 P Q ys zs; transp P; transp Q ⟧
⟹ tllist_all2 P Q xs zs"
by transfer(auto elim: llist_all2_trans dest: llist_all2_lfiniteD transpD)

lemma tllist_all2_tappendI:
"⟦ tllist_all2 P Q xs ys;
⟦ tfinite xs; tfinite ys; Q (terminal xs) (terminal ys) ⟧
⟹ tllist_all2 P R (xs' (terminal xs)) (ys' (terminal ys)) ⟧
⟹ tllist_all2 P R (tappend xs xs') (tappend ys ys')"
apply transfer
apply(auto 4 3 simp add: apfst_def map_prod_def lappend_inf split: prod.split_asm dest: llist_all2_lfiniteD intro: llist_all2_lappendI)
done

lemma llist_all2_tllist_of_llistI:
"tllist_all2 A B xs ys ⟹ llist_all2 A (llist_of_tllist xs) (llist_of_tllist ys)"
by(coinduction arbitrary: xs ys)(auto dest: tllist_all2_is_TNilD tllist_all2_thdD intro: tllist_all2_ttlI)

lemma tllist_all2_tllist_of_llist [simp]:
"tllist_all2 A B (tllist_of_llist b xs) (tllist_of_llist c ys) ⟷
llist_all2 A xs ys ∧ (lfinite xs ⟶ B b c)"
by transfer auto

subsection ‹From a terminated lazy list to a lazy list @{term llist_of_tllist}›

lemma llist_of_tllist_tmap [simp]:
"llist_of_tllist (tmap f g xs) = lmap f (llist_of_tllist xs)"
by transfer auto

lemma llist_of_tllist_tappend:
"llist_of_tllist (tappend xs f) = lappend (llist_of_tllist xs) (llist_of_tllist (f (terminal xs)))"

lemma llist_of_tllist_lappendt [simp]:
"llist_of_tllist (lappendt xs tr) = lappend xs (llist_of_tllist tr)"
by transfer auto

lemma llist_of_tllist_tfilter [simp]:
"llist_of_tllist (tfilter b P tr) = lfilter P (llist_of_tllist tr)"
by transfer auto

lemma llist_of_tllist_tconcat:
"llist_of_tllist (tconcat b trs) = lconcat (llist_of_tllist trs)"
by transfer auto

lemma llist_of_tllist_eq_lappend_conv:
"llist_of_tllist xs = lappend us vs ⟷
(∃ys. xs = lappendt us ys ∧ vs = llist_of_tllist ys ∧ terminal xs = terminal ys)"
by transfer auto

subsection ‹The nth element of a terminated lazy list @{term "tnth"}›

lemma tnth_TNil [nitpick_simp]:
"tnth (TNil b) n = undefined n"

lemma tnth_TCons:
"tnth (TCons x xs) n = (case n of 0 ⇒ x | Suc n' ⇒ tnth xs n')"
by(transfer)(auto simp add: lnth_LCons split: nat.split)

lemma tnth_code [simp, nitpick_simp, code]:
shows tnth_0: "tnth (TCons x xs) 0 = x"
and tnth_Suc_TCons: "tnth (TCons x xs) (Suc n) = tnth xs n"

lemma lnth_llist_of_tllist [simp]:
"lnth (llist_of_tllist xs) = tnth xs"
by(transfer)(auto)

lemma tnth_tmap [simp]: "enat n < tlength xs ⟹ tnth (tmap f g xs) n = f (tnth xs n)"
by transfer simp

subsection ‹The length of a terminated lazy list @{term "tlength"}›

lemma [simp, nitpick_simp]:
shows tlength_TNil: "tlength (TNil b) = 0"
and tlength_TCons: "tlength (TCons x xs) = eSuc (tlength xs)"
apply(transfer, simp)
apply(transfer, auto)
done

lemma llength_llist_of_tllist [simp]: "llength (llist_of_tllist xs) = tlength xs"
by transfer auto

lemma tlength_tmap [simp]: "tlength (tmap f g xs) = tlength xs"
by transfer simp

definition gen_tlength :: "nat ⇒ ('a, 'b) tllist ⇒ enat"
where "gen_tlength n xs = enat n + tlength xs"

lemma gen_tlength_code [code]:
"gen_tlength n (TNil b) = enat n"
"gen_tlength n (TCons x xs) = gen_tlength (n + 1) xs"

lemma tlength_code [code]: "tlength = gen_tlength 0"

subsection ‹@{term "tdropn"}›

lemma tdropn_0 [simp, code, nitpick_simp]: "tdropn 0 xs = xs"
by transfer auto

lemma tdropn_TNil [simp, code]: "tdropn n (TNil b) = (TNil b)"
by transfer(auto)

lemma tdropn_Suc_TCons [simp, code]: "tdropn (Suc n) (TCons x xs) = tdropn n xs"
by transfer(auto)

lemma tdropn_Suc [nitpick_simp]: "tdropn (Suc n) xs = (case xs of TNil b ⇒ TNil b | TCons x xs' ⇒ tdropn n xs')"
by(cases xs) simp_all

lemma lappendt_ltake_tdropn:
"lappendt (ltake (enat n) (llist_of_tllist xs)) (tdropn n xs) = xs"
by transfer (auto)

lemma llist_of_tllist_tdropn [simp]:
"llist_of_tllist (tdropn n xs) = ldropn n (llist_of_tllist xs)"
by transfer auto

lemma tdropn_Suc_conv_tdropn:
"enat n < tlength xs ⟹ TCons (tnth xs n) (tdropn (Suc n) xs) = tdropn n xs"

lemma tlength_tdropn [simp]: "tlength (tdropn n xs) = tlength xs - enat n"
by transfer auto

lemma tnth_tdropn [simp]: "enat (n + m) < tlength xs ⟹ tnth (tdropn n xs) m = tnth xs (m + n)"
by transfer auto

subsection ‹@{term "tset"}›

lemma tset_induct [consumes 1, case_names find step]:
assumes "x ∈ tset xs"
and "⋀xs. P (TCons x xs)"
and "⋀x' xs. ⟦ x ∈ tset xs; x ≠ x'; P xs ⟧ ⟹ P (TCons x' xs)"
shows "P xs"
using assms
by transfer(clarsimp, erule lset_induct)

lemma tset_conv_tnth: "tset xs = {tnth xs n|n . enat n < tlength xs}"

lemma in_tset_conv_tnth: "x ∈ tset xs ⟷ (∃n. enat n < tlength xs ∧ tnth xs n = x)"
using tset_conv_tnth[of xs] by auto

subsection ‹Setup for Lifting/Transfer›

subsubsection ‹Relator and predicator properties›

abbreviation "tllist_all == pred_tllist"

subsubsection ‹Transfer rules for the Transfer package›

context includes lifting_syntax
begin

lemma set1_pre_tllist_transfer [transfer_rule]:
"(rel_pre_tllist A B C ===> rel_set A) set1_pre_tllist set1_pre_tllist"
by(auto simp add: rel_pre_tllist_def vimage2p_def rel_fun_def set1_pre_tllist_def rel_set_def collect_def sum_set_defs prod_set_defs elim: rel_sum.cases split: sum.split_asm)

lemma set2_pre_tllist_transfer [transfer_rule]:
"(rel_pre_tllist A B C ===> rel_set B) set2_pre_tllist set2_pre_tllist"
by(auto simp add: rel_pre_tllist_def vimage2p_def rel_fun_def set2_pre_tllist_def rel_set_def collect_def sum_set_defs prod_set_defs elim: rel_sum.cases split: sum.split_asm)

lemma set3_pre_tllist_transfer [transfer_rule]:
"(rel_pre_tllist A B C ===> rel_set C) set3_pre_tllist set3_pre_tllist"
by(auto simp add: rel_pre_tllist_def vimage2p_def rel_fun_def set3_pre_tllist_def rel_set_def collect_def sum_set_defs prod_set_defs elim: rel_sum.cases split: sum.split_asm)

lemma TNil_transfer2 [transfer_rule]: "(B ===> tllist_all2 A B) TNil TNil"
by auto
declare TNil_transfer [transfer_rule]

lemma TCons_transfer2 [transfer_rule]:
"(A ===> tllist_all2 A B ===> tllist_all2 A B) TCons TCons"
unfolding rel_fun_def by simp
declare TCons_transfer [transfer_rule]

lemma case_tllist_transfer [transfer_rule]:
"((B ===> C) ===> (A ===> tllist_all2 A B ===> C) ===> tllist_all2 A B ===> C)
case_tllist case_tllist"
unfolding rel_fun_def
by (simp add: tllist_all2_TNil1 tllist_all2_TNil2 split: tllist.split)

lemma unfold_tllist_transfer [transfer_rule]:
"((A ===> (=)) ===> (A ===> B) ===> (A ===> C) ===> (A ===> A) ===> A ===> tllist_all2 C B) unfold_tllist unfold_tllist"
proof(rule rel_funI)+
fix IS_TNIL1 :: "'a ⇒ bool" and IS_TNIL2
TERMINAL1 TERMINAL2 THD1 THD2 TTL1 TTL2 x y
assume rel: "(A ===> (=)) IS_TNIL1 IS_TNIL2" "(A ===> B) TERMINAL1 TERMINAL2"
"(A ===> C) THD1 THD2" "(A ===> A) TTL1 TTL2"
and "A x y"
show "tllist_all2 C B (unfold_tllist IS_TNIL1 TERMINAL1 THD1 TTL1 x) (unfold_tllist IS_TNIL2 TERMINAL2 THD2 TTL2 y)"
using ‹A x y›
apply(coinduction arbitrary: x y)
using rel by(auto 4 4 elim: rel_funE)
qed

lemma corec_tllist_transfer [transfer_rule]:
"((A ===> (=)) ===> (A ===> B) ===> (A ===> C) ===> (A ===> (=)) ===> (A ===> tllist_all2 C B) ===> (A ===> A) ===> A ===> tllist_all2 C B) corec_tllist corec_tllist"
proof(rule rel_funI)+
fix IS_TNIL1 MORE1 :: "'a ⇒ bool" and IS_TNIL2
TERMINAL1 TERMINAL2 THD1 THD2 MORE2 STOP1 STOP2 TTL1 TTL2 x y
assume rel: "(A ===> (=)) IS_TNIL1 IS_TNIL2" "(A ===> B) TERMINAL1 TERMINAL2"
"(A ===> C) THD1 THD2" "(A ===> (=)) MORE1 MORE2"
"(A ===> tllist_all2 C B) STOP1 STOP2" "(A ===> A) TTL1 TTL2"
and "A x y"
show "tllist_all2 C B (corec_tllist IS_TNIL1 TERMINAL1 THD1 MORE1 STOP1 TTL1 x) (corec_tllist IS_TNIL2 TERMINAL2 THD2 MORE2 STOP2 TTL2 y)"
using ‹A x y›
apply(coinduction arbitrary: x y)
using rel by(auto 4 4 elim: rel_funE)
qed

lemma ttl_transfer2 [transfer_rule]:
"(tllist_all2 A B ===> tllist_all2 A B) ttl ttl"
unfolding ttl_def[abs_def] by transfer_prover
declare ttl_transfer [transfer_rule]

lemma tset_transfer2 [transfer_rule]:
"(tllist_all2 A B ===> rel_set A) tset tset"
by (intro rel_funI rel_setI) (auto simp only: in_tset_conv_tnth tllist_all2_conv_all_tnth Bex_def)

lemma tmap_transfer2 [transfer_rule]:
"((A ===> B) ===> (C ===> D) ===> tllist_all2 A C ===> tllist_all2 B D) tmap tmap"
by(auto simp add: rel_fun_def tllist_all2_tmap1 tllist_all2_tmap2 elim: tllist_all2_mono)
declare tmap_transfer [transfer_rule]

lemma is_TNil_transfer2 [transfer_rule]:
"(tllist_all2 A B ===> (=)) is_TNil is_TNil"
by(auto dest: tllist_all2_is_TNilD)
declare is_TNil_transfer [transfer_rule]

lemma tappend_transfer [transfer_rule]:
"(tllist_all2 A B ===> (B ===> tllist_all2 A C) ===> tllist_all2 A C) tappend tappend"
by(auto intro: tllist_all2_tappendI elim: rel_funE)
declare tappend.transfer [transfer_rule]

lemma lappendt_transfer [transfer_rule]:
"(llist_all2 A ===> tllist_all2 A B ===> tllist_all2 A B) lappendt lappendt"
unfolding rel_fun_def
by transfer(auto intro: llist_all2_lappendI)
declare lappendt.transfer [transfer_rule]

lemma llist_of_tllist_transfer2 [transfer_rule]:
"(tllist_all2 A B ===> llist_all2 A) llist_of_tllist llist_of_tllist"
by(auto intro: llist_all2_tllist_of_llistI)
declare llist_of_tllist_transfer [transfer_rule]

lemma tllist_of_llist_transfer2 [transfer_rule]:
"(B ===> llist_all2 A ===> tllist_all2 A B) tllist_of_llist tllist_of_llist"
by(auto intro!: rel_funI)
declare tllist_of_llist_transfer [transfer_rule]

lemma tlength_transfer [transfer_rule]:
"(tllist_all2 A B ===> (=)) tlength tlength"
by(auto dest: tllist_all2_tlengthD)
declare tlength.transfer [transfer_rule]

lemma tdropn_transfer [transfer_rule]:
"((=) ===> tllist_all2 A B ===> tllist_all2 A B) tdropn tdropn"
unfolding rel_fun_def
by transfer(auto intro: llist_all2_ldropnI)
declare tdropn.transfer [transfer_rule]

lemma tfilter_transfer [transfer_rule]:
"(B ===> (A ===> (=)) ===> tllist_all2 A B ===> tllist_all2 A B) tfilter tfilter"
unfolding rel_fun_def
by transfer(auto intro: llist_all2_lfilterI dest: llist_all2_lfiniteD)
declare tfilter.transfer [transfer_rule]

lemma tconcat_transfer [transfer_rule]:
"(B ===> tllist_all2 (llist_all2 A) B ===> tllist_all2 A B) tconcat tconcat"
unfolding rel_fun_def
by transfer(auto intro: llist_all2_lconcatI dest: llist_all2_lfiniteD)
declare tconcat.transfer [transfer_rule]

lemma tllist_all2_rsp:
assumes R1: "∀x y. R1 x y ⟶ (∀a b. R1 a b ⟶ S x a = T y b)"
and R2: "∀x y. R2 x y ⟶ (∀a b. R2 a b ⟶ S' x a = T' y b)"
and xsys: "tllist_all2 R1 R2 xs ys"
and xs'ys': "tllist_all2 R1 R2 xs' ys'"
shows "tllist_all2 S S' xs xs' = tllist_all2 T T' ys ys'"
proof
assume "tllist_all2 S S' xs xs'"
with xsys xs'ys' show "tllist_all2 T T' ys ys'"
proof(coinduction arbitrary: ys ys' xs xs')
case (tllist_all2 ys ys' xs xs')
thus ?case
by cases (auto 4 4 simp add: tllist_all2_TCons1 tllist_all2_TCons2 tllist_all2_TNil1 tllist_all2_TNil2 dest: R1[rule_format] R2[rule_format])
qed
next
assume "tllist_all2 T T' ys ys'"
with xsys xs'ys' show "tllist_all2 S S' xs xs'"
proof(coinduction arbitrary: xs xs' ys ys')
case (tllist_all2 xs xs' ys ys')
thus ?case
by cases(auto 4 4 simp add: tllist_all2_TCons1 tllist_all2_TCons2 tllist_all2_TNil1 tllist_all2_TNil2 dest: R1[rule_format] R2[rule_format])
qed
qed

lemma tllist_all2_transfer2 [transfer_rule]:
"((R1 ===> R1 ===> (=)) ===> (R2 ===> R2 ===> (=)) ===>
tllist_all2 R1 R2 ===> tllist_all2 R1 R2 ===> (=)) tllist_all2 tllist_all2"
declare tllist_all2_transfer [transfer_rule]

end

text ‹
Delete lifting rules for @{typ "('a, 'b) tllist"}
because the parametricity rules take precedence over
most of the transfer rules. They can be restored by
including the bundle ‹tllist.lifting›.
›

lifting_update tllist.lifting
lifting_forget tllist.lifting

end
```