--- a/src/HOL/Library/Coinductive_List.thy Wed Sep 23 11:33:52 2009 +0200
+++ b/src/HOL/Library/Coinductive_List.thy Wed Sep 23 13:47:08 2009 +0200
@@ -260,7 +260,7 @@
qed
qed
-lemma llist_corec [code]:
+lemma llist_corec [code, nitpick_const_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")
@@ -656,8 +656,9 @@
qed
qed
-lemma lmap_LNil [simp]: "lmap f LNil = LNil"
- and lmap_LCons [simp]: "lmap f (LCons M N) = LCons (f M) (lmap f N)"
+lemma lmap_LNil [simp, nitpick_const_simp]: "lmap f LNil = LNil"
+ and lmap_LCons [simp, nitpick_const_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)"
@@ -728,9 +729,9 @@
qed
qed
-lemma lappend_LNil_LNil [simp]: "lappend LNil LNil = LNil"
- and lappend_LNil_LCons [simp]: "lappend LNil (LCons l l') = LCons l (lappend LNil l')"
- and lappend_LCons [simp]: "lappend (LCons l l') m = LCons l (lappend l' m)"
+lemma lappend_LNil_LNil [simp, nitpick_const_simp]: "lappend LNil LNil = LNil"
+ and lappend_LNil_LCons [simp, nitpick_const_simp]: "lappend LNil (LCons l l') = LCons l (lappend LNil l')"
+ and lappend_LCons [simp, nitpick_const_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"
@@ -754,7 +755,7 @@
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))"
+lemma iterates [nitpick_const_simp]: "iterates f x = LCons x (iterates f (f x))"
apply (unfold iterates_def)
apply (subst llist_corec)
apply simp