src/HOL/Library/Coinductive_List.thy
changeset 33056 791a4655cae3
parent 32960 69916a850301
child 33197 de6285ebcc05
--- a/src/HOL/Library/Coinductive_List.thy	Wed Oct 21 16:57:57 2009 +0200
+++ b/src/HOL/Library/Coinductive_List.thy	Wed Oct 21 17:34:35 2009 +0200
@@ -260,7 +260,7 @@
   qed
 qed
 
-lemma llist_corec [code, nitpick_const_simp]:
+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")
@@ -656,8 +656,8 @@
   qed
 qed
 
-lemma lmap_LNil [simp, nitpick_const_simp]: "lmap f LNil = LNil"
-  and lmap_LCons [simp, nitpick_const_simp]:
+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)
 
@@ -729,9 +729,9 @@
   qed
 qed
 
-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)"
+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"
@@ -755,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 [nitpick_const_simp]: "iterates f x = LCons x (iterates f (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