continuation of Nitpick's integration into Isabelle;
added examples, and integrated non-Main theories better.
(* Title: HOL/Library/Coinductive_Lists.thy
Author: Lawrence C Paulson and Makarius
*)
header {* Potentially infinite lists as greatest fixed-point *}
theory Coinductive_List
imports List Main
begin
subsection {* List constructors over the datatype universe *}
definition "NIL = Datatype.In0 (Datatype.Numb 0)"
definition "CONS M N = Datatype.In1 (Datatype.Scons M N)"
lemma CONS_not_NIL [iff]: "CONS M N \<noteq> NIL"
and NIL_not_CONS [iff]: "NIL \<noteq> CONS M N"
and CONS_inject [iff]: "(CONS K M) = (CONS L N) = (K = L \<and> M = N)"
by (simp_all add: NIL_def CONS_def)
lemma CONS_mono: "M \<subseteq> M' \<Longrightarrow> N \<subseteq> N' \<Longrightarrow> CONS M N \<subseteq> CONS M' N'"
by (simp add: CONS_def In1_mono Scons_mono)
lemma CONS_UN1: "CONS M (\<Union>x. f x) = (\<Union>x. CONS M (f x))"
-- {* A continuity result? *}
by (simp add: CONS_def In1_UN1 Scons_UN1_y)
definition "List_case c h = Datatype.Case (\<lambda>_. c) (Datatype.Split h)"
lemma List_case_NIL [simp]: "List_case c h NIL = c"
and List_case_CONS [simp]: "List_case c h (CONS M N) = h M N"
by (simp_all add: List_case_def NIL_def CONS_def)
subsection {* Corecursive lists *}
coinductive_set LList for A
where NIL [intro]: "NIL \<in> LList A"
| CONS [intro]: "a \<in> A \<Longrightarrow> M \<in> LList A \<Longrightarrow> CONS a M \<in> LList A"
lemma LList_mono:
assumes subset: "A \<subseteq> B"
shows "LList A \<subseteq> LList B"
-- {* This justifies using @{text LList} in other recursive type definitions. *}
proof
fix x
assume "x \<in> LList A"
then show "x \<in> LList B"
proof coinduct
case LList
then show ?case using subset
by cases blast+
qed
qed
consts
LList_corec_aux :: "nat \<Rightarrow> ('a \<Rightarrow> ('b Datatype.item \<times> 'a) option) \<Rightarrow>
'a \<Rightarrow> 'b Datatype.item"
primrec
"LList_corec_aux 0 f x = {}"
"LList_corec_aux (Suc k) f x =
(case f x of
None \<Rightarrow> NIL
| Some (z, w) \<Rightarrow> CONS z (LList_corec_aux k f w))"
definition "LList_corec a f = (\<Union>k. LList_corec_aux k f a)"
text {*
Note: the subsequent recursion equation for @{text LList_corec} may
be used with the Simplifier, provided it operates in a non-strict
fashion for case expressions (i.e.\ the usual @{text case}
congruence rule needs to be present).
*}
lemma LList_corec:
"LList_corec a f =
(case f a of None \<Rightarrow> NIL | Some (z, w) \<Rightarrow> CONS z (LList_corec w f))"
(is "?lhs = ?rhs")
proof
show "?lhs \<subseteq> ?rhs"
apply (unfold LList_corec_def)
apply (rule UN_least)
apply (case_tac k)
apply (simp_all (no_asm_simp) split: option.splits)
apply (rule allI impI subset_refl [THEN CONS_mono] UNIV_I [THEN UN_upper])+
done
show "?rhs \<subseteq> ?lhs"
apply (simp add: LList_corec_def split: option.splits)
apply (simp add: CONS_UN1)
apply safe
apply (rule_tac a = "Suc ?k" in UN_I, simp, simp)+
done
qed
lemma LList_corec_type: "LList_corec a f \<in> LList UNIV"
proof -
have "\<exists>x. LList_corec a f = LList_corec x f" by blast
then show ?thesis
proof coinduct
case (LList L)
then obtain x where L: "L = LList_corec x f" by blast
show ?case
proof (cases "f x")
case None
then have "LList_corec x f = NIL"
by (simp add: LList_corec)
with L have ?NIL by simp
then show ?thesis ..
next
case (Some p)
then have "LList_corec x f = CONS (fst p) (LList_corec (snd p) f)"
by (simp add: LList_corec split: prod.split)
with L have ?CONS by auto
then show ?thesis ..
qed
qed
qed
subsection {* Abstract type definition *}
typedef 'a llist = "LList (range Datatype.Leaf) :: 'a Datatype.item set"
proof
show "NIL \<in> ?llist" ..
qed
lemma NIL_type: "NIL \<in> llist"
unfolding llist_def by (rule LList.NIL)
lemma CONS_type: "a \<in> range Datatype.Leaf \<Longrightarrow>
M \<in> llist \<Longrightarrow> CONS a M \<in> llist"
unfolding llist_def by (rule LList.CONS)
lemma llistI: "x \<in> LList (range Datatype.Leaf) \<Longrightarrow> x \<in> llist"
by (simp add: llist_def)
lemma llistD: "x \<in> llist \<Longrightarrow> x \<in> LList (range Datatype.Leaf)"
by (simp add: llist_def)
lemma Rep_llist_UNIV: "Rep_llist x \<in> LList UNIV"
proof -
have "Rep_llist x \<in> llist" by (rule Rep_llist)
then have "Rep_llist x \<in> LList (range Datatype.Leaf)"
by (simp add: llist_def)
also have "\<dots> \<subseteq> LList UNIV" by (rule LList_mono) simp
finally show ?thesis .
qed
definition "LNil = Abs_llist NIL"
definition "LCons x xs = Abs_llist (CONS (Datatype.Leaf x) (Rep_llist xs))"
code_datatype LNil LCons
lemma LCons_not_LNil [iff]: "LCons x xs \<noteq> LNil"
apply (simp add: LNil_def LCons_def)
apply (subst Abs_llist_inject)
apply (auto intro: NIL_type CONS_type Rep_llist)
done
lemma LNil_not_LCons [iff]: "LNil \<noteq> LCons x xs"
by (rule LCons_not_LNil [symmetric])
lemma LCons_inject [iff]: "(LCons x xs = LCons y ys) = (x = y \<and> xs = ys)"
apply (simp add: LCons_def)
apply (subst Abs_llist_inject)
apply (auto simp add: Rep_llist_inject intro: CONS_type Rep_llist)
done
lemma Rep_llist_LNil: "Rep_llist LNil = NIL"
by (simp add: LNil_def add: Abs_llist_inverse NIL_type)
lemma Rep_llist_LCons: "Rep_llist (LCons x l) =
CONS (Datatype.Leaf x) (Rep_llist l)"
by (simp add: LCons_def Abs_llist_inverse CONS_type Rep_llist)
lemma llist_cases [cases type: llist]:
obtains
(LNil) "l = LNil"
| (LCons) x l' where "l = LCons x l'"
proof (cases l)
case (Abs_llist L)
from `L \<in> llist` have "L \<in> LList (range Datatype.Leaf)" by (rule llistD)
then show ?thesis
proof cases
case NIL
with Abs_llist have "l = LNil" by (simp add: LNil_def)
with LNil show ?thesis .
next
case (CONS a K)
then have "K \<in> llist" by (blast intro: llistI)
then obtain l' where "K = Rep_llist l'" by cases
with CONS and Abs_llist obtain x where "l = LCons x l'"
by (auto simp add: LCons_def Abs_llist_inject)
with LCons show ?thesis .
qed
qed
definition
[code del]: "llist_case c d l =
List_case c (\<lambda>x y. d (inv Datatype.Leaf x) (Abs_llist y)) (Rep_llist l)"
syntax (* FIXME? *)
LNil :: logic
LCons :: logic
translations
"case p of LNil \<Rightarrow> a | LCons x l \<Rightarrow> b" \<rightleftharpoons> "CONST llist_case a (\<lambda>x l. b) p"
lemma llist_case_LNil [simp, code]: "llist_case c d LNil = c"
by (simp add: llist_case_def LNil_def
NIL_type Abs_llist_inverse)
lemma llist_case_LCons [simp, code]: "llist_case c d (LCons M N) = d M N"
by (simp add: llist_case_def LCons_def
CONS_type Abs_llist_inverse Rep_llist Rep_llist_inverse inj_Leaf)
lemma llist_case_cert:
assumes "CASE \<equiv> llist_case c d"
shows "(CASE LNil \<equiv> c) &&& (CASE (LCons M N) \<equiv> d M N)"
using assms by simp_all
setup {*
Code.add_case @{thm llist_case_cert}
*}
definition
[code del]: "llist_corec a f =
Abs_llist (LList_corec a
(\<lambda>z.
case f z of None \<Rightarrow> None
| Some (v, w) \<Rightarrow> Some (Datatype.Leaf v, w)))"
lemma LList_corec_type2:
"LList_corec a
(\<lambda>z. case f z of None \<Rightarrow> None
| Some (v, w) \<Rightarrow> Some (Datatype.Leaf v, w)) \<in> llist"
(is "?corec a \<in> _")
proof (unfold llist_def)
let "LList_corec a ?g" = "?corec a"
have "\<exists>x. ?corec a = ?corec x" by blast
then show "?corec a \<in> LList (range Datatype.Leaf)"
proof coinduct
case (LList L)
then obtain x where L: "L = ?corec x" by blast
show ?case
proof (cases "f x")
case None
then have "?corec x = NIL"
by (simp add: LList_corec)
with L have ?NIL by simp
then show ?thesis ..
next
case (Some p)
then have "?corec x =
CONS (Datatype.Leaf (fst p)) (?corec (snd p))"
by (simp add: LList_corec split: prod.split)
with L have ?CONS by auto
then show ?thesis ..
qed
qed
qed
lemma llist_corec [code, nitpick_simp]:
"llist_corec a f =
(case f a of None \<Rightarrow> LNil | Some (z, w) \<Rightarrow> LCons z (llist_corec w f))"
proof (cases "f a")
case None
then show ?thesis
by (simp add: llist_corec_def LList_corec LNil_def)
next
case (Some p)
let "?corec a" = "llist_corec a f"
let "?rep_corec a" =
"LList_corec a
(\<lambda>z. case f z of None \<Rightarrow> None
| Some (v, w) \<Rightarrow> Some (Datatype.Leaf v, w))"
have "?corec a = Abs_llist (?rep_corec a)"
by (simp only: llist_corec_def)
also from Some have "?rep_corec a =
CONS (Datatype.Leaf (fst p)) (?rep_corec (snd p))"
by (simp add: LList_corec split: prod.split)
also have "?rep_corec (snd p) = Rep_llist (?corec (snd p))"
by (simp only: llist_corec_def Abs_llist_inverse LList_corec_type2)
finally have "?corec a = LCons (fst p) (?corec (snd p))"
by (simp only: LCons_def)
with Some show ?thesis by (simp split: prod.split)
qed
subsection {* Equality as greatest fixed-point -- the bisimulation principle *}
coinductive_set EqLList for r
where EqNIL: "(NIL, NIL) \<in> EqLList r"
| EqCONS: "(a, b) \<in> r \<Longrightarrow> (M, N) \<in> EqLList r \<Longrightarrow>
(CONS a M, CONS b N) \<in> EqLList r"
lemma EqLList_unfold:
"EqLList r = dsum (Id_on {Datatype.Numb 0}) (dprod r (EqLList r))"
by (fast intro!: EqLList.intros [unfolded NIL_def CONS_def]
elim: EqLList.cases [unfolded NIL_def CONS_def])
lemma EqLList_implies_ntrunc_equality:
"(M, N) \<in> EqLList (Id_on A) \<Longrightarrow> ntrunc k M = ntrunc k N"
apply (induct k arbitrary: M N rule: nat_less_induct)
apply (erule EqLList.cases)
apply (safe del: equalityI)
apply (case_tac n)
apply simp
apply (rename_tac n')
apply (case_tac n')
apply (simp_all add: CONS_def less_Suc_eq)
done
lemma Domain_EqLList: "Domain (EqLList (Id_on A)) \<subseteq> LList A"
apply (rule subsetI)
apply (erule LList.coinduct)
apply (subst (asm) EqLList_unfold)
apply (auto simp add: NIL_def CONS_def)
done
lemma EqLList_Id_on: "EqLList (Id_on A) = Id_on (LList A)"
(is "?lhs = ?rhs")
proof
show "?lhs \<subseteq> ?rhs"
apply (rule subsetI)
apply (rule_tac p = x in PairE)
apply clarify
apply (rule Id_on_eqI)
apply (rule EqLList_implies_ntrunc_equality [THEN ntrunc_equality],
assumption)
apply (erule DomainI [THEN Domain_EqLList [THEN subsetD]])
done
{
fix M N assume "(M, N) \<in> Id_on (LList A)"
then have "(M, N) \<in> EqLList (Id_on A)"
proof coinduct
case (EqLList M N)
then obtain L where L: "L \<in> LList A" and MN: "M = L" "N = L" by blast
from L show ?case
proof cases
case NIL with MN have ?EqNIL by simp
then show ?thesis ..
next
case CONS with MN have ?EqCONS by (simp add: Id_onI)
then show ?thesis ..
qed
qed
}
then show "?rhs \<subseteq> ?lhs" by auto
qed
lemma EqLList_Id_on_iff [iff]: "(p \<in> EqLList (Id_on A)) = (p \<in> Id_on (LList A))"
by (simp only: EqLList_Id_on)
text {*
To show two LLists are equal, exhibit a bisimulation! (Also admits
true equality.)
*}
lemma LList_equalityI
[consumes 1, case_names EqLList, case_conclusion EqLList EqNIL EqCONS]:
assumes r: "(M, N) \<in> r"
and step: "\<And>M N. (M, N) \<in> r \<Longrightarrow>
M = NIL \<and> N = NIL \<or>
(\<exists>a b M' N'.
M = CONS a M' \<and> N = CONS b N' \<and> (a, b) \<in> Id_on A \<and>
((M', N') \<in> r \<or> (M', N') \<in> EqLList (Id_on A)))"
shows "M = N"
proof -
from r have "(M, N) \<in> EqLList (Id_on A)"
proof coinduct
case EqLList
then show ?case by (rule step)
qed
then show ?thesis by auto
qed
lemma LList_fun_equalityI
[consumes 1, case_names NIL_type NIL CONS, case_conclusion CONS EqNIL EqCONS]:
assumes M: "M \<in> LList A"
and fun_NIL: "g NIL \<in> LList A" "f NIL = g NIL"
and fun_CONS: "\<And>x l. x \<in> A \<Longrightarrow> l \<in> LList A \<Longrightarrow>
(f (CONS x l), g (CONS x l)) = (NIL, NIL) \<or>
(\<exists>M N a b.
(f (CONS x l), g (CONS x l)) = (CONS a M, CONS b N) \<and>
(a, b) \<in> Id_on A \<and>
(M, N) \<in> {(f u, g u) | u. u \<in> LList A} \<union> Id_on (LList A))"
(is "\<And>x l. _ \<Longrightarrow> _ \<Longrightarrow> ?fun_CONS x l")
shows "f M = g M"
proof -
let ?bisim = "{(f L, g L) | L. L \<in> LList A}"
have "(f M, g M) \<in> ?bisim" using M by blast
then show ?thesis
proof (coinduct taking: A rule: LList_equalityI)
case (EqLList M N)
then obtain L where MN: "M = f L" "N = g L" and L: "L \<in> LList A" by blast
from L show ?case
proof (cases L)
case NIL
with fun_NIL and MN have "(M, N) \<in> Id_on (LList A)" by auto
then have "(M, N) \<in> EqLList (Id_on A)" ..
then show ?thesis by cases simp_all
next
case (CONS a K)
from fun_CONS and `a \<in> A` `K \<in> LList A`
have "?fun_CONS a K" (is "?NIL \<or> ?CONS") .
then show ?thesis
proof
assume ?NIL
with MN CONS have "(M, N) \<in> Id_on (LList A)" by auto
then have "(M, N) \<in> EqLList (Id_on A)" ..
then show ?thesis by cases simp_all
next
assume ?CONS
with CONS obtain a b M' N' where
fg: "(f L, g L) = (CONS a M', CONS b N')"
and ab: "(a, b) \<in> Id_on A"
and M'N': "(M', N') \<in> ?bisim \<union> Id_on (LList A)"
by blast
from M'N' show ?thesis
proof
assume "(M', N') \<in> ?bisim"
with MN fg ab show ?thesis by simp
next
assume "(M', N') \<in> Id_on (LList A)"
then have "(M', N') \<in> EqLList (Id_on A)" ..
with MN fg ab show ?thesis by simp
qed
qed
qed
qed
qed
text {*
Finality of @{text "llist A"}: Uniqueness of functions defined by corecursion.
*}
lemma equals_LList_corec:
assumes h: "\<And>x. h x =
(case f x of None \<Rightarrow> NIL | Some (z, w) \<Rightarrow> CONS z (h w))"
shows "h x = (\<lambda>x. LList_corec x f) x"
proof -
def h' \<equiv> "\<lambda>x. LList_corec x f"
then have h': "\<And>x. h' x =
(case f x of None \<Rightarrow> NIL | Some (z, w) \<Rightarrow> CONS z (h' w))"
unfolding h'_def by (simp add: LList_corec)
have "(h x, h' x) \<in> {(h u, h' u) | u. True}" by blast
then show "h x = h' x"
proof (coinduct taking: UNIV rule: LList_equalityI)
case (EqLList M N)
then obtain x where MN: "M = h x" "N = h' x" by blast
show ?case
proof (cases "f x")
case None
with h h' MN have ?EqNIL by simp
then show ?thesis ..
next
case (Some p)
with h h' MN have "M = CONS (fst p) (h (snd p))"
and "N = CONS (fst p) (h' (snd p))"
by (simp_all split: prod.split)
then have ?EqCONS by (auto iff: Id_on_iff)
then show ?thesis ..
qed
qed
qed
lemma llist_equalityI
[consumes 1, case_names Eqllist, case_conclusion Eqllist EqLNil EqLCons]:
assumes r: "(l1, l2) \<in> r"
and step: "\<And>q. q \<in> r \<Longrightarrow>
q = (LNil, LNil) \<or>
(\<exists>l1 l2 a b.
q = (LCons a l1, LCons b l2) \<and> a = b \<and>
((l1, l2) \<in> r \<or> l1 = l2))"
(is "\<And>q. _ \<Longrightarrow> ?EqLNil q \<or> ?EqLCons q")
shows "l1 = l2"
proof -
def M \<equiv> "Rep_llist l1" and N \<equiv> "Rep_llist l2"
with r have "(M, N) \<in> {(Rep_llist l1, Rep_llist l2) | l1 l2. (l1, l2) \<in> r}"
by blast
then have "M = N"
proof (coinduct taking: UNIV rule: LList_equalityI)
case (EqLList M N)
then obtain l1 l2 where
MN: "M = Rep_llist l1" "N = Rep_llist l2" and r: "(l1, l2) \<in> r"
by auto
from step [OF r] show ?case
proof
assume "?EqLNil (l1, l2)"
with MN have ?EqNIL by (simp add: Rep_llist_LNil)
then show ?thesis ..
next
assume "?EqLCons (l1, l2)"
with MN have ?EqCONS
by (force simp add: Rep_llist_LCons EqLList_Id_on intro: Rep_llist_UNIV)
then show ?thesis ..
qed
qed
then show ?thesis by (simp add: M_def N_def Rep_llist_inject)
qed
lemma llist_fun_equalityI
[case_names LNil LCons, case_conclusion LCons EqLNil EqLCons]:
assumes fun_LNil: "f LNil = g LNil"
and fun_LCons: "\<And>x l.
(f (LCons x l), g (LCons x l)) = (LNil, LNil) \<or>
(\<exists>l1 l2 a b.
(f (LCons x l), g (LCons x l)) = (LCons a l1, LCons b l2) \<and>
a = b \<and> ((l1, l2) \<in> {(f u, g u) | u. True} \<or> l1 = l2))"
(is "\<And>x l. ?fun_LCons x l")
shows "f l = g l"
proof -
have "(f l, g l) \<in> {(f l, g l) | l. True}" by blast
then show ?thesis
proof (coinduct rule: llist_equalityI)
case (Eqllist q)
then obtain l where q: "q = (f l, g l)" by blast
show ?case
proof (cases l)
case LNil
with fun_LNil and q have "q = (g LNil, g LNil)" by simp
then show ?thesis by (cases "g LNil") simp_all
next
case (LCons x l')
with `?fun_LCons x l'` q LCons show ?thesis by blast
qed
qed
qed
subsection {* Derived operations -- both on the set and abstract type *}
subsubsection {* @{text Lconst} *}
definition "Lconst M \<equiv> lfp (\<lambda>N. CONS M N)"
lemma Lconst_fun_mono: "mono (CONS M)"
by (simp add: monoI CONS_mono)
lemma Lconst: "Lconst M = CONS M (Lconst M)"
by (rule Lconst_def [THEN def_lfp_unfold]) (rule Lconst_fun_mono)
lemma Lconst_type:
assumes "M \<in> A"
shows "Lconst M \<in> LList A"
proof -
have "Lconst M \<in> {Lconst (id M)}" by simp
then show ?thesis
proof coinduct
case (LList N)
then have "N = Lconst M" by simp
also have "\<dots> = CONS M (Lconst M)" by (rule Lconst)
finally have ?CONS using `M \<in> A` by simp
then show ?case ..
qed
qed
lemma Lconst_eq_LList_corec: "Lconst M = LList_corec M (\<lambda>x. Some (x, x))"
apply (rule equals_LList_corec)
apply simp
apply (rule Lconst)
done
lemma gfp_Lconst_eq_LList_corec:
"gfp (\<lambda>N. CONS M N) = LList_corec M (\<lambda>x. Some(x, x))"
apply (rule equals_LList_corec)
apply simp
apply (rule Lconst_fun_mono [THEN gfp_unfold])
done
subsubsection {* @{text Lmap} and @{text lmap} *}
definition
"Lmap f M = LList_corec M (List_case None (\<lambda>x M'. Some (f x, M')))"
definition
"lmap f l = llist_corec l
(\<lambda>z.
case z of LNil \<Rightarrow> None
| LCons y z \<Rightarrow> Some (f y, z))"
lemma Lmap_NIL [simp]: "Lmap f NIL = NIL"
and Lmap_CONS [simp]: "Lmap f (CONS M N) = CONS (f M) (Lmap f N)"
by (simp_all add: Lmap_def LList_corec)
lemma Lmap_type:
assumes M: "M \<in> LList A"
and f: "\<And>x. x \<in> A \<Longrightarrow> f x \<in> B"
shows "Lmap f M \<in> LList B"
proof -
from M have "Lmap f M \<in> {Lmap f N | N. N \<in> LList A}" by blast
then show ?thesis
proof coinduct
case (LList L)
then obtain N where L: "L = Lmap f N" and N: "N \<in> LList A" by blast
from N show ?case
proof cases
case NIL
with L have ?NIL by simp
then show ?thesis ..
next
case (CONS K a)
with f L have ?CONS by auto
then show ?thesis ..
qed
qed
qed
lemma Lmap_compose:
assumes M: "M \<in> LList A"
shows "Lmap (f o g) M = Lmap f (Lmap g M)" (is "?lhs M = ?rhs M")
proof -
have "(?lhs M, ?rhs M) \<in> {(?lhs N, ?rhs N) | N. N \<in> LList A}"
using M by blast
then show ?thesis
proof (coinduct taking: "range (\<lambda>N. N)" rule: LList_equalityI)
case (EqLList L M)
then obtain N where LM: "L = ?lhs N" "M = ?rhs N" and N: "N \<in> LList A" by blast
from N show ?case
proof cases
case NIL
with LM have ?EqNIL by simp
then show ?thesis ..
next
case CONS
with LM have ?EqCONS by auto
then show ?thesis ..
qed
qed
qed
lemma Lmap_ident:
assumes M: "M \<in> LList A"
shows "Lmap (\<lambda>x. x) M = M" (is "?lmap M = _")
proof -
have "(?lmap M, M) \<in> {(?lmap N, N) | N. N \<in> LList A}" using M by blast
then show ?thesis
proof (coinduct taking: "range (\<lambda>N. N)" rule: LList_equalityI)
case (EqLList L M)
then obtain N where LM: "L = ?lmap N" "M = N" and N: "N \<in> LList A" by blast
from N show ?case
proof cases
case NIL
with LM have ?EqNIL by simp
then show ?thesis ..
next
case CONS
with LM have ?EqCONS by auto
then show ?thesis ..
qed
qed
qed
lemma lmap_LNil [simp, nitpick_simp]: "lmap f LNil = LNil"
and lmap_LCons [simp, nitpick_simp]:
"lmap f (LCons M N) = LCons (f M) (lmap f N)"
by (simp_all add: lmap_def llist_corec)
lemma lmap_compose [simp]: "lmap (f o g) l = lmap f (lmap g l)"
by (coinduct l rule: llist_fun_equalityI) auto
lemma lmap_ident [simp]: "lmap (\<lambda>x. x) l = l"
by (coinduct l rule: llist_fun_equalityI) auto
subsubsection {* @{text Lappend} *}
definition
"Lappend M N = LList_corec (M, N)
(split (List_case
(List_case None (\<lambda>N1 N2. Some (N1, (NIL, N2))))
(\<lambda>M1 M2 N. Some (M1, (M2, N)))))"
definition
"lappend l n = llist_corec (l, n)
(split (llist_case
(llist_case None (\<lambda>n1 n2. Some (n1, (LNil, n2))))
(\<lambda>l1 l2 n. Some (l1, (l2, n)))))"
lemma Lappend_NIL_NIL [simp]:
"Lappend NIL NIL = NIL"
and Lappend_NIL_CONS [simp]:
"Lappend NIL (CONS N N') = CONS N (Lappend NIL N')"
and Lappend_CONS [simp]:
"Lappend (CONS M M') N = CONS M (Lappend M' N)"
by (simp_all add: Lappend_def LList_corec)
lemma Lappend_NIL [simp]: "M \<in> LList A \<Longrightarrow> Lappend NIL M = M"
by (erule LList_fun_equalityI) auto
lemma Lappend_NIL2: "M \<in> LList A \<Longrightarrow> Lappend M NIL = M"
by (erule LList_fun_equalityI) auto
lemma Lappend_type:
assumes M: "M \<in> LList A" and N: "N \<in> LList A"
shows "Lappend M N \<in> LList A"
proof -
have "Lappend M N \<in> {Lappend u v | u v. u \<in> LList A \<and> v \<in> LList A}"
using M N by blast
then show ?thesis
proof coinduct
case (LList L)
then obtain M N where L: "L = Lappend M N"
and M: "M \<in> LList A" and N: "N \<in> LList A"
by blast
from M show ?case
proof cases
case NIL
from N show ?thesis
proof cases
case NIL
with L and `M = NIL` have ?NIL by simp
then show ?thesis ..
next
case CONS
with L and `M = NIL` have ?CONS by simp
then show ?thesis ..
qed
next
case CONS
with L N have ?CONS by auto
then show ?thesis ..
qed
qed
qed
lemma lappend_LNil_LNil [simp, nitpick_simp]: "lappend LNil LNil = LNil"
and lappend_LNil_LCons [simp, nitpick_simp]: "lappend LNil (LCons l l') = LCons l (lappend LNil l')"
and lappend_LCons [simp, nitpick_simp]: "lappend (LCons l l') m = LCons l (lappend l' m)"
by (simp_all add: lappend_def llist_corec)
lemma lappend_LNil1 [simp]: "lappend LNil l = l"
by (coinduct l rule: llist_fun_equalityI) auto
lemma lappend_LNil2 [simp]: "lappend l LNil = l"
by (coinduct l rule: llist_fun_equalityI) auto
lemma lappend_assoc: "lappend (lappend l1 l2) l3 = lappend l1 (lappend l2 l3)"
by (coinduct l1 rule: llist_fun_equalityI) auto
lemma lmap_lappend_distrib: "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)"
by (coinduct l rule: llist_fun_equalityI) auto
subsection{* iterates *}
text {* @{text llist_fun_equalityI} cannot be used here! *}
definition
iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
"iterates f a = llist_corec a (\<lambda>x. Some (x, f x))"
lemma iterates [nitpick_simp]: "iterates f x = LCons x (iterates f (f x))"
apply (unfold iterates_def)
apply (subst llist_corec)
apply simp
done
lemma lmap_iterates: "lmap f (iterates f x) = iterates f (f x)"
proof -
have "(lmap f (iterates f x), iterates f (f x)) \<in>
{(lmap f (iterates f u), iterates f (f u)) | u. True}" by blast
then show ?thesis
proof (coinduct rule: llist_equalityI)
case (Eqllist q)
then obtain x where q: "q = (lmap f (iterates f x), iterates f (f x))"
by blast
also have "iterates f (f x) = LCons (f x) (iterates f (f (f x)))"
by (subst iterates) rule
also have "iterates f x = LCons x (iterates f (f x))"
by (subst iterates) rule
finally have ?EqLCons by auto
then show ?case ..
qed
qed
lemma iterates_lmap: "iterates f x = LCons x (lmap f (iterates f x))"
by (subst lmap_iterates) (rule iterates)
subsection{* A rather complex proof about iterates -- cf.\ Andy Pitts *}
lemma funpow_lmap:
fixes f :: "'a \<Rightarrow> 'a"
shows "(lmap f ^^ n) (LCons b l) = LCons ((f ^^ n) b) ((lmap f ^^ n) l)"
by (induct n) simp_all
lemma iterates_equality:
assumes h: "\<And>x. h x = LCons x (lmap f (h x))"
shows "h = iterates f"
proof
fix x
have "(h x, iterates f x) \<in>
{((lmap f ^^ n) (h u), (lmap f ^^ n) (iterates f u)) | u n. True}"
proof -
have "(h x, iterates f x) = ((lmap f ^^ 0) (h x), (lmap f ^^ 0) (iterates f x))"
by simp
then show ?thesis by blast
qed
then show "h x = iterates f x"
proof (coinduct rule: llist_equalityI)
case (Eqllist q)
then obtain u n where "q = ((lmap f ^^ n) (h u), (lmap f ^^ n) (iterates f u))"
(is "_ = (?q1, ?q2)")
by auto
also have "?q1 = LCons ((f ^^ n) u) ((lmap f ^^ Suc n) (h u))"
proof -
have "?q1 = (lmap f ^^ n) (LCons u (lmap f (h u)))"
by (subst h) rule
also have "\<dots> = LCons ((f ^^ n) u) ((lmap f ^^ n) (lmap f (h u)))"
by (rule funpow_lmap)
also have "(lmap f ^^ n) (lmap f (h u)) = (lmap f ^^ Suc n) (h u)"
by (simp add: funpow_swap1)
finally show ?thesis .
qed
also have "?q2 = LCons ((f ^^ n) u) ((lmap f ^^ Suc n) (iterates f u))"
proof -
have "?q2 = (lmap f ^^ n) (LCons u (iterates f (f u)))"
by (subst iterates) rule
also have "\<dots> = LCons ((f ^^ n) u) ((lmap f ^^ n) (iterates f (f u)))"
by (rule funpow_lmap)
also have "(lmap f ^^ n) (iterates f (f u)) = (lmap f ^^ Suc n) (iterates f u)"
by (simp add: lmap_iterates funpow_swap1)
finally show ?thesis .
qed
finally have ?EqLCons by (auto simp del: funpow.simps)
then show ?case ..
qed
qed
lemma lappend_iterates: "lappend (iterates f x) l = iterates f x"
proof -
have "(lappend (iterates f x) l, iterates f x) \<in>
{(lappend (iterates f u) l, iterates f u) | u. True}" by blast
then show ?thesis
proof (coinduct rule: llist_equalityI)
case (Eqllist q)
then obtain x where "q = (lappend (iterates f x) l, iterates f x)" by blast
also have "iterates f x = LCons x (iterates f (f x))" by (rule iterates)
finally have ?EqLCons by auto
then show ?case ..
qed
qed
setup {*
Nitpick.register_codatatype @{typ "'a llist"} @{const_name llist_case}
(map dest_Const [@{term LNil}, @{term LCons}])
*}
end