src/HOL/Library/Coinductive_List.thy
changeset 32655 dd84779cd191
parent 30971 7fbebf75b3ef
child 32960 69916a850301
     1.1 --- a/src/HOL/Library/Coinductive_List.thy	Wed Sep 23 11:33:52 2009 +0200
     1.2 +++ b/src/HOL/Library/Coinductive_List.thy	Wed Sep 23 13:47:08 2009 +0200
     1.3 @@ -260,7 +260,7 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 -lemma llist_corec [code]:
     1.8 +lemma llist_corec [code, nitpick_const_simp]:
     1.9    "llist_corec a f =
    1.10      (case f a of None \<Rightarrow> LNil | Some (z, w) \<Rightarrow> LCons z (llist_corec w f))"
    1.11  proof (cases "f a")
    1.12 @@ -656,8 +656,9 @@
    1.13    qed
    1.14  qed
    1.15  
    1.16 -lemma lmap_LNil [simp]: "lmap f LNil = LNil"
    1.17 -  and lmap_LCons [simp]: "lmap f (LCons M N) = LCons (f M) (lmap f N)"
    1.18 +lemma lmap_LNil [simp, nitpick_const_simp]: "lmap f LNil = LNil"
    1.19 +  and lmap_LCons [simp, nitpick_const_simp]:
    1.20 +  "lmap f (LCons M N) = LCons (f M) (lmap f N)"
    1.21    by (simp_all add: lmap_def llist_corec)
    1.22  
    1.23  lemma lmap_compose [simp]: "lmap (f o g) l = lmap f (lmap g l)"
    1.24 @@ -728,9 +729,9 @@
    1.25    qed
    1.26  qed
    1.27  
    1.28 -lemma lappend_LNil_LNil [simp]: "lappend LNil LNil = LNil"
    1.29 -  and lappend_LNil_LCons [simp]: "lappend LNil (LCons l l') = LCons l (lappend LNil l')"
    1.30 -  and lappend_LCons [simp]: "lappend (LCons l l') m = LCons l (lappend l' m)"
    1.31 +lemma lappend_LNil_LNil [simp, nitpick_const_simp]: "lappend LNil LNil = LNil"
    1.32 +  and lappend_LNil_LCons [simp, nitpick_const_simp]: "lappend LNil (LCons l l') = LCons l (lappend LNil l')"
    1.33 +  and lappend_LCons [simp, nitpick_const_simp]: "lappend (LCons l l') m = LCons l (lappend l' m)"
    1.34    by (simp_all add: lappend_def llist_corec)
    1.35  
    1.36  lemma lappend_LNil1 [simp]: "lappend LNil l = l"
    1.37 @@ -754,7 +755,7 @@
    1.38    iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
    1.39    "iterates f a = llist_corec a (\<lambda>x. Some (x, f x))"
    1.40  
    1.41 -lemma iterates: "iterates f x = LCons x (iterates f (f x))"
    1.42 +lemma iterates [nitpick_const_simp]: "iterates f x = LCons x (iterates f (f x))"
    1.43    apply (unfold iterates_def)
    1.44    apply (subst llist_corec)
    1.45    apply simp