# HG changeset patch
# User blanchet
# Date 1253706496 -7200
# Node ID 3bd9296b16acd57103b694d1c8736aa7e167493b
# Parent  dd84779cd191438e8de7ad40bc25ef0d201105cb# Parent  5f91274074304e24cfa6c89223078084875b6080
merged

diff -r 5f9127407430 -r 3bd9296b16ac src/HOL/Induct/LList.thy
--- a/src/HOL/Induct/LList.thy	Wed Sep 23 13:48:35 2009 +0200
+++ b/src/HOL/Induct/LList.thy	Wed Sep 23 13:48:16 2009 +0200
@@ -665,7 +665,7 @@
 apply (subst LList_corec, force)
 done
 
-lemma llist_corec: 
+lemma llist_corec [nitpick_const_simp]: 
     "llist_corec a f =   
      (case f a of None => LNil | Some(z,w) => LCons z (llist_corec w f))"
 apply (unfold llist_corec_def LNil_def LCons_def)
@@ -774,10 +774,11 @@
 
 subsection{* The functional @{text lmap} *}
 
-lemma lmap_LNil [simp]: "lmap f LNil = LNil"
+lemma lmap_LNil [simp, nitpick_const_simp]: "lmap f LNil = LNil"
 by (rule lmap_def [THEN def_llist_corec, THEN trans], simp)
 
-lemma lmap_LCons [simp]: "lmap f (LCons M N) = LCons (f M) (lmap f N)"
+lemma lmap_LCons [simp, nitpick_const_simp]:
+"lmap f (LCons M N) = LCons (f M) (lmap f N)"
 by (rule lmap_def [THEN def_llist_corec, THEN trans], simp)
 
 
@@ -792,7 +793,7 @@
 
 subsection{* iterates -- @{text llist_fun_equalityI} cannot be used! *}
 
-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))"
 by (rule iterates_def [THEN def_llist_corec, THEN trans], simp)
 
 lemma lmap_iterates [simp]: "lmap f (iterates f x) = iterates f (f x)"
@@ -847,18 +848,18 @@
 
 subsection{* @{text lappend} -- its two arguments cause some complications! *}
 
-lemma lappend_LNil_LNil [simp]: "lappend LNil LNil = LNil"
+lemma lappend_LNil_LNil [simp, nitpick_const_simp]: "lappend LNil LNil = LNil"
 apply (simp add: lappend_def)
 apply (rule llist_corec [THEN trans], simp)
 done
 
-lemma lappend_LNil_LCons [simp]: 
+lemma lappend_LNil_LCons [simp, nitpick_const_simp]: 
     "lappend LNil (LCons l l') = LCons l (lappend LNil l')"
 apply (simp add: lappend_def)
 apply (rule llist_corec [THEN trans], simp)
 done
 
-lemma lappend_LCons [simp]: 
+lemma lappend_LCons [simp, nitpick_const_simp]: 
     "lappend (LCons l l') N = LCons l (lappend l' N)"
 apply (simp add: lappend_def)
 apply (rule llist_corec [THEN trans], simp)
diff -r 5f9127407430 -r 3bd9296b16ac src/HOL/Library/Coinductive_List.thy
--- a/src/HOL/Library/Coinductive_List.thy	Wed Sep 23 13:48:35 2009 +0200
+++ b/src/HOL/Library/Coinductive_List.thy	Wed Sep 23 13:48:16 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