Theory TLList
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"