Added "nitpick_const_simp" tags to lazy list theories.
authorblanchet
Wed Sep 23 13:47:08 2009 +0200 (2009-09-23)
changeset 32655dd84779cd191
parent 32647 e54f47f9e28b
child 32656 3bd9296b16ac
Added "nitpick_const_simp" tags to lazy list theories.
(Will be useful once Nitpick is integrated in Isabelle.)
src/HOL/Induct/LList.thy
src/HOL/Library/Coinductive_List.thy
     1.1 --- a/src/HOL/Induct/LList.thy	Wed Sep 23 11:33:52 2009 +0200
     1.2 +++ b/src/HOL/Induct/LList.thy	Wed Sep 23 13:47:08 2009 +0200
     1.3 @@ -665,7 +665,7 @@
     1.4  apply (subst LList_corec, force)
     1.5  done
     1.6  
     1.7 -lemma llist_corec: 
     1.8 +lemma llist_corec [nitpick_const_simp]: 
     1.9      "llist_corec a f =   
    1.10       (case f a of None => LNil | Some(z,w) => LCons z (llist_corec w f))"
    1.11  apply (unfold llist_corec_def LNil_def LCons_def)
    1.12 @@ -774,10 +774,11 @@
    1.13  
    1.14  subsection{* The functional @{text lmap} *}
    1.15  
    1.16 -lemma lmap_LNil [simp]: "lmap f LNil = LNil"
    1.17 +lemma lmap_LNil [simp, nitpick_const_simp]: "lmap f LNil = LNil"
    1.18  by (rule lmap_def [THEN def_llist_corec, THEN trans], simp)
    1.19  
    1.20 -lemma lmap_LCons [simp]: "lmap f (LCons M N) = LCons (f M) (lmap f N)"
    1.21 +lemma lmap_LCons [simp, nitpick_const_simp]:
    1.22 +"lmap f (LCons M N) = LCons (f M) (lmap f N)"
    1.23  by (rule lmap_def [THEN def_llist_corec, THEN trans], simp)
    1.24  
    1.25  
    1.26 @@ -792,7 +793,7 @@
    1.27  
    1.28  subsection{* iterates -- @{text llist_fun_equalityI} cannot be used! *}
    1.29  
    1.30 -lemma iterates: "iterates f x = LCons x (iterates f (f x))"
    1.31 +lemma iterates [nitpick_const_simp]: "iterates f x = LCons x (iterates f (f x))"
    1.32  by (rule iterates_def [THEN def_llist_corec, THEN trans], simp)
    1.33  
    1.34  lemma lmap_iterates [simp]: "lmap f (iterates f x) = iterates f (f x)"
    1.35 @@ -847,18 +848,18 @@
    1.36  
    1.37  subsection{* @{text lappend} -- its two arguments cause some complications! *}
    1.38  
    1.39 -lemma lappend_LNil_LNil [simp]: "lappend LNil LNil = LNil"
    1.40 +lemma lappend_LNil_LNil [simp, nitpick_const_simp]: "lappend LNil LNil = LNil"
    1.41  apply (simp add: lappend_def)
    1.42  apply (rule llist_corec [THEN trans], simp)
    1.43  done
    1.44  
    1.45 -lemma lappend_LNil_LCons [simp]: 
    1.46 +lemma lappend_LNil_LCons [simp, nitpick_const_simp]: 
    1.47      "lappend LNil (LCons l l') = LCons l (lappend LNil l')"
    1.48  apply (simp add: lappend_def)
    1.49  apply (rule llist_corec [THEN trans], simp)
    1.50  done
    1.51  
    1.52 -lemma lappend_LCons [simp]: 
    1.53 +lemma lappend_LCons [simp, nitpick_const_simp]: 
    1.54      "lappend (LCons l l') N = LCons l (lappend l' N)"
    1.55  apply (simp add: lappend_def)
    1.56  apply (rule llist_corec [THEN trans], simp)
     2.1 --- a/src/HOL/Library/Coinductive_List.thy	Wed Sep 23 11:33:52 2009 +0200
     2.2 +++ b/src/HOL/Library/Coinductive_List.thy	Wed Sep 23 13:47:08 2009 +0200
     2.3 @@ -260,7 +260,7 @@
     2.4    qed
     2.5  qed
     2.6  
     2.7 -lemma llist_corec [code]:
     2.8 +lemma llist_corec [code, nitpick_const_simp]:
     2.9    "llist_corec a f =
    2.10      (case f a of None \<Rightarrow> LNil | Some (z, w) \<Rightarrow> LCons z (llist_corec w f))"
    2.11  proof (cases "f a")
    2.12 @@ -656,8 +656,9 @@
    2.13    qed
    2.14  qed
    2.15  
    2.16 -lemma lmap_LNil [simp]: "lmap f LNil = LNil"
    2.17 -  and lmap_LCons [simp]: "lmap f (LCons M N) = LCons (f M) (lmap f N)"
    2.18 +lemma lmap_LNil [simp, nitpick_const_simp]: "lmap f LNil = LNil"
    2.19 +  and lmap_LCons [simp, nitpick_const_simp]:
    2.20 +  "lmap f (LCons M N) = LCons (f M) (lmap f N)"
    2.21    by (simp_all add: lmap_def llist_corec)
    2.22  
    2.23  lemma lmap_compose [simp]: "lmap (f o g) l = lmap f (lmap g l)"
    2.24 @@ -728,9 +729,9 @@
    2.25    qed
    2.26  qed
    2.27  
    2.28 -lemma lappend_LNil_LNil [simp]: "lappend LNil LNil = LNil"
    2.29 -  and lappend_LNil_LCons [simp]: "lappend LNil (LCons l l') = LCons l (lappend LNil l')"
    2.30 -  and lappend_LCons [simp]: "lappend (LCons l l') m = LCons l (lappend l' m)"
    2.31 +lemma lappend_LNil_LNil [simp, nitpick_const_simp]: "lappend LNil LNil = LNil"
    2.32 +  and lappend_LNil_LCons [simp, nitpick_const_simp]: "lappend LNil (LCons l l') = LCons l (lappend LNil l')"
    2.33 +  and lappend_LCons [simp, nitpick_const_simp]: "lappend (LCons l l') m = LCons l (lappend l' m)"
    2.34    by (simp_all add: lappend_def llist_corec)
    2.35  
    2.36  lemma lappend_LNil1 [simp]: "lappend LNil l = l"
    2.37 @@ -754,7 +755,7 @@
    2.38    iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
    2.39    "iterates f a = llist_corec a (\<lambda>x. Some (x, f x))"
    2.40  
    2.41 -lemma iterates: "iterates f x = LCons x (iterates f (f x))"
    2.42 +lemma iterates [nitpick_const_simp]: "iterates f x = LCons x (iterates f (f x))"
    2.43    apply (unfold iterates_def)
    2.44    apply (subst llist_corec)
    2.45    apply simp