Theory Coinductive.Coinductive_List
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›