# HG changeset patch
# User blanchet
# Date 1253706428 -7200
# Node ID dd84779cd191438e8de7ad40bc25ef0d201105cb
# Parent  e54f47f9e28b2d166da8609a0b714c7101441d3e
Added "nitpick_const_simp" tags to lazy list theories.
(Will be useful once Nitpick is integrated in Isabelle.)

diff -r e54f47f9e28b -r dd84779cd191 src/HOL/Induct/LList.thy
--- a/src/HOL/Induct/LList.thy	Wed Sep 23 11:33:52 2009 +0200
+++ b/src/HOL/Induct/LList.thy	Wed Sep 23 13:47:08 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 e54f47f9e28b -r dd84779cd191 src/HOL/Library/Coinductive_List.thy
--- 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