src/HOL/Library/Coinductive_List.thy

 
 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)"

   finally show ?thesis .
 qed
 
 definition
   "LNil = Abs_llist NIL"
+definition
   "LCons x xs = Abs_llist (CONS (Datatype.Leaf x) (Rep_llist xs))"
 
 lemma LCons_not_LNil [iff]: "LCons x xs \<noteq> LNil"
   apply (simp add: LNil_def LCons_def)
   apply (subst Abs_llist_inject)

 
 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))"
 

 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)))))"
 

 subsection{* iterates *}
 
 text {* @{text llist_fun_equalityI} cannot be used here! *}
 
 definition
-  iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist"
+  iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
   "iterates f a = llist_corec a (\<lambda>x. Some (x, f x))"
 
 lemma iterates: "iterates f x = LCons x (iterates f (f x))"
   apply (unfold iterates_def)
   apply (subst llist_corec)